IDE protocol: jump to fixity

[ohad]

• [X] I have read CONTRIBUTING.md.
• [X] I have checked that there is no existing PR/issue about my proposal.

Summary

Motivation

In Idris2 fixity declarations are separate from the function declaration and are more-or-less global. It's helpful for the programmer to be able to tell which fixity declaration is in effect.

The proposal

1. Add a mechanism for finding the fixity declaration in effect in a given point at a file.
2. Add an IDE command for returning the location of this declaration and its precedence value.
3. Support this command in various IDE clients to jump-to-fixity / display this information.
4. Make this functionality available from the REPL:

   > :fixity ^
   infixl 6 ^

   Examples

   TBC

Technical implementation

TBC

Alternatives considered

Agda doesn't support overloading.

The other functional languages in this area don't really have an IDE protocol.

If someone is familiar with other language protocols, that would be helpful.

Conclusion

Not a ground-breaking feature, but might be an easy entry / good-first-issue into the IDE protocol.

[gwerbin]

In response to a question on Discord, the reason this is desirable is that it makes it easy to edit the code.

Unlike :doc, which is useful for learning about a thing while using the thing, "jump to X" is useful for modifying things, or otherwise working and reasoning about the source code underlying that thing. In this case "X" could be a definition, a type declaration, or a fixity declaration.

[andrevidela]

@gwerbin That's definitely a valid use-case, but the issue needs a lot more details in order to be actionable:

• Are we talking about go-to fixity? Why is "go to definition" not enough? (fixities are not necessarily in the same file for example)
• Should we have a mechanism that lists all fixities in scope? What would be different from that and a list of functions in scope?
• Is this the opportunity to talk about conflicting fixity definitions and how to resolve them? We could generate nicer error messages than "ambiguous name"

There is definitely something to do here but we need to scope the problem a little bit better first. All those could be their own proposals in themselves!