Make go-to-definition on a typeclass projection application go to the instance(s)

[rish987]

Closes #1722, pending #1903.

[rish987]

Hmm the CI test failures are puzzling me (it looks like they're still not getting the instance locations for some reason), because everything passes locally when I do:

$ ./test_single.sh {goTo,goto2}.lean

[Kha]

The interactive tests are not designed for referencing core files in their output. Either you'll need to change the existing tests not to reference core instances, or we implement something in the vein of #1722 (comment) that would prevent these tests from showing instances.

[leodemoura]

@rish987 Today we were discussing this PR in the dev meeting. Could you please clarify the semantics you are implementing?

[rish987]

Sure, I was trying to follow what Sebastian described here, basically, on go-to-definition or go-to-type if we get an Info node that represents an application of a typeclass projection, rather than going to the syntax or elaborator, we extract all of the relevant instances and present that in a list. I've also included the elaborator in this list because you were originally only able to get to that through go-to-definition (the syntax is still accessible as before through go-to-declaration).

I think I may need some help with the tests though (I blindly copied over expected outputs that I just noticed include URIs on my local filesystem 😰 so of course it won't work). Perhaps we need some additional filtering to preserve existing behavior (and some new tests as well to specifically test the new functionality), I was discussing this with @Kha yesterday and it sounded like he had an idea regarding that?

[Kha]

Right, the fundamental issue is that when looking at the typeclass method call Expr, we don't know if this info node was responsible for the TC synthesis, and thus whether original/canonical syntax was responsible for it. What I proposed to Rish is to simply whitelist syntax that we know does this, e.g. i.stx.isOfKind identKind || i.stx.isOfKind ``Parser.Term.app and probably others as well. A different, probably more general heuristic would be to check if no nested info node contains the same Expr (making use of the tree structure of the info tree, heh).

[rish987]

Okay this should finally be ready! I've merged in #1903 so it depends on that PR being merged first.

[rish987]

Whoops, didn't mean to close it!

[Kha]

Looks great all in all!

[Kha]

Let's move this to InfoUtils and use it in hoverableInfoAt? and locationLinksOfInfo etc. The deriving TypeName should probably be left here though.

[rish987]

Done, let me know what you think of the refactor.

[Vtec234]

Hi, sorry to only comment on this now but InfoWithCtx is only really intended for use as a way of bundling data together in the RPC protocol so that interactive expressions and go-to-def in the infoview work. As Gabriel put it, it's a kind of "type popup + go-to-def thunk". Unless you need to do something with RPC here, it would be better not to move it and to add another type with whatever semantics you need instead.

[Kha]

Duplicating it wouldn't be hard, but since the type is opaque in the RPC protocol I'm not really seeing the motivation. It's a sensible bundle of data to have in the server in general, and the name fits as well. Even if we don't necessarily need children in the widgets.

[Vtec234]

The type seems like a better fit for Elab.InfoTree, if anything, because it was already hacky as far as the RPC interface is concerned — the outputs of delaboration are Elab.Infos but they should really be a much more restricted Delab.Info without variants like .ofCompletion. But okay, since InfoWithCtx is opaque we can always keep it around for uses such as in this PR but replace it with something else in the RPC interface. Btw @rish987 you probably want to also make the output of hoverableInfoAt? and termGoalAt? be InfoWithCtx, document what the children field is, and change the docstring to note that it's used for more than just RPC.

[rish987]

Done, thanks for the suggestions.