Codebase Server: /getDefinition of a data constructor results in mission definition

[hojberg]

When requesting data constructors they come back as a missingDefinition.

Here's base.Map.Map:

{ 
  "termDefinitions": {},
  "typeDefinitions": {}, 
  "missingDefinitions": [ 
"#7di5ureqgi60ue42886240kbovfhko0fg85rp2thpkl8af699upsl0os1btk27te1cjdmuerad5oi9bdd04me6mjh2m25djbj236fbo#d0" 
  ] 
}

I think we might want to return the type even though it's a term?

Credit goes to @rlmark for reporting this issue, that i'd been sitting on.

[hojberg]

Would love to get folks thoughts on the right approach. I also added this to the M2 release ticket.

[pchiusano]

I'd probably just return the type declaration that the constructor is a part of in this case. This is what we do elsewhere.

Another possibility which I like less is to keep the behavior as is and force the front end to convert constructors to their corresponding type reference when requesting a definition.

@runarorama WDYT?

Regardless, it would also be nice if the front-end highlighted (perhaps temporarily, with a fading highlight?) the relevant constructor when opening or scrolling to the definition.

[runarorama]

It would be nice if the frontend could just request the type. All the necessary information is there to do something cool like highlight the relevant constructor. E.g. if the constructor requested is #abc#d0 then the first Constructor element of the syntax text returned by getDefinition for #abc is the thing to be highlighted.

[pchiusano]

@runarorama I don't disagree with what you said that it could be handled nicely on the front end.

However, if the back-end isn't prepared to do anything sensible with a constructor passed to getDefinition, then the input type for that endpoint should be changed to be a Reference rather than a Referent. I think this would be a fine choice. Having it advertise that it can be passed a Referent but then it never gives any results for those inputs is weird though. :)

So I'd either a) change the input type of that endpoint or b) return the decl that the constructor belongs to when a constructor is passed to getDefinition.

[pchiusano]

Just discussed with @runarorama and @hojberg. @hojberg is going to handle this on the front-end - Simon feel free to create an issue to track that in the codebase-ui repo.

@runarorama clarified for me - the getDefinition endpoint already takes just a plain ol' string as input. So there's not really anything it can do differently if passed a string that happens to correspond to a constructor. Basically, the front end just shouldn't do that going forward.

[hojberg]

Tracked here: unisonweb/codebase-ui#60