Go-to-definition on typeclass method should go to instance

[Kha]

trafficstars

...while go-to-declaration should go to the typeclass as it does right now. I hope that's not too controversial (and may even have been suggested before)? Note that you can still move from the instance to the class by using go-to-definition on the method name again.

[gebner]

:+1: for the go-to-instance feature, this is often requested.

while go-to-declaration should go to the typeclass as it does right now

Actually, I think it goes to the notation. And go-to-definition goes to the macro expander. At least for a + b.

Generally speaking, there are multiple items we want to go-to (for a + b):

• Syntax definition.
• Macro expander (or elaborator).
• HAdd.hAdd.
• Instance(s?). (For example it could be helpful to show three instances for (1, 2.0) + (2, 1.0).)

Another question is what counts as a "typeclass method". (Should it work on a ≥ b?)

[rish987]

I'm looking into this. In the a + b example, it looks like + corresponds to the Info.ofTermInfo node corresponding to @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) a b. Would the correct approach be to make the + correspond to a node for instAddNat? This would fix the go-to-definition problem, but I'm not yet familiar enough with InfoTree generation to know whether this would be idiomatic. It would also break hover, replacing the documentation for HAdd.hAdd with the (non-existent) documentation for instAddNat.

Would a fundamental fix here be to make + correspond to an info node for @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat), and reduce this to end up with Nat.add? Is there a way for InfoTree generation to correspond different atoms of user syntax to different parts of the elaborated term?

[Kha]

I don't think we need to change the info tree for this. From the existing Expr for + you noted, we can tell if it is a class projection application via getProjectionFnInfo?. Then we can get the corresponding class via getProjectionStructureName? and search for a parameter of that type in the projection's signature, which should give us the index of the instance argument (@instHAdd.{0} Nat instAddNat in this case). The remaining question is what to report from that instance argument. If we want to report multiple instances, like Gabriel suggested, we could simply collect all Expr.consts in the argument and report them if they satisfy isInstance. So in this example we would report both instHAdd and instAddNat, which seems like the ideal "exhaustive" solution. And possibly all the other items Gabriel mentioned, which sounds like a good idea to me when we're already presenting a list.

[rish987]

Thanks for the pointer. Since this will be very much immediately useful, I'll put something like this together right away.

But I wanted to ask more about the expected behavior here in the long term. If you go-to-definition on + in 1 + 2 isn't it most likely you want to instantly end up at Nat.add? And for the more general case, there could be multiple fields of the class, so just listing all of the isInstance constants that TC produced would ignore the information that is available of what particular projection you've done.

So in the case of a projection of a struct-like class couldn't we normalize the field of the instance corresponding to the projection before searching for candidate constants for go-to-definition? And we could bundle everything else (TC instances, syntax, etc.) under go-to-declaration/go-to-type. This would remove two levels of indirection in the common case (first for the user to sift through the go-to-definition list and select the base instance, and second for them to find and go-to-definition on the correct field in the instance).

[Kha]

I just remembered a basic issue we discussed in the frontend meeting: how do we decide whether a macro fundamentally stands for a typeclass method invocation or simply, accidentally ends with one? We already had a question about this for the existing hover/completion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Term.20Macro.20Docstrings.

The good thing is that we now have canonical synthetic info to differentiate between these two cases. So we could limit this "Expr sniffing" in the server to e.g. cases of a syntactical application after expansion where the application head is original/canonical. And then add a heuristic for notation to mark the function head (if any) canonical.

But really when opening this issue I wasn't thinking about notations at all, so doing this only for nodes with original info would already be a good start.