IDE command to print docs for the type at point

[ohad]

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

Summary

The IDE protocol currently supports a DocsFor command for presenting the documentation for some name.
When that name is a hole, what the user wants is the documentation for the type of hole, rather than the non-existing documentation for the hole.

Motivation

data MyFancyType : Type where
  C1 : List String -> MyFancyType
  C2 : (Bool,Type) -> MyFancyType
  C3 : Either MyFancyType Nat -> MyFancyType

Foo : MyFancyType
--    ^1
Foo = ?whatToChoose
--     ^2

If the user places their cursor at the character pointed at by caret 1 (on MyFancyType) and issues a DocsFor command (e.g., idris-docs-at-point (C-c C-d d) in emacs's idris-mode), we get a lot of useful information:

data Main.MyFancyType : Type
  Totality: total
  Visibility: private
  Constructors:
    C1 : List String -> MyFancyType
    C2 : (Bool, Type) -> MyFancyType
    C3 : Either MyFancyType Nat -> MyFancyType

[back]

But if we're pointing at the hole whatToChoose (caret 2), then asking for the docs gives us nothing:

[back]

What we really want at this point is the docs for the type of whatToChoose, which will give us the earlier output, which will help us choose the right constructor.

In this example, we can work around by navigating to Foo's type declaration and asking for the docs, but if we're working on a hole nested inside another term, we can't do it so easily. What we need to do in that case is ask idris for the type of the name under the cursor (idris-type-at-point (C-c C-t), switch to the info buffer so that the cursor now points at the type, and then ask the IDE protocol for the docs.

The proposal

Add a DocsForTypeOf command to the IDE protocol that returns the docs for the type of the name given.

Examples

In the example above, placing the cursor at caret 2 and issuing a DocsForTypeOf (say, idris-docs-for-type-at-point (C-c C-d t)) would display:

Documentation for type of whatToChoose : MyFancyType:
data Main.MyFancyType : Type
  Totality: total
  Visibility: private
  Constructors:
    C1 : List String -> MyFancyType
    C2 : (Bool, Type) -> MyFancyType
    C3 : Either MyFancyType Nat -> MyFancyType

[back]

Technical implementation

1. Adding a new command to Protocol.IDE.Command
2. Adding serialisation/deserialisation code for it.
3. Bumping up the IDE protocol minor version number.
4. Implementing the functionality, hopefully by composing the functionality for TypeOf and DocsFor.
5. Implementing the corresponding command in the idris-mode.
   Relevant developers there might be @ohad or @gallais , or post about it here or in the #interactive-editing channel on the Discord server.

The implementation may be relatively high-level, and can be a good opportunity to get acquainted with the various moving parts of the IDE protocol without (hopefully) getting bogged down with too many low level details.

Alternatives considered

Can be worked around by composing two IDE commands manually. It breaks the flow of development because dev needs to encode the command as a sequence of two commands, switch buffers etc.

Conclusion

An optional change to improve type-driven development with complex datatypes and make the interaction with the type-checker more expressive and smoother.