Should head function syntax be hoverable?

[Vtec234]

trafficstars

Continuing discussion from here and #1157.

There is currently an inconsistency between whether the head symbol in a function application is hoverable/selectable in source code and in the infoview. I think of this as fundamentally an inconsistency between how we elaborate and delaborate Elab.Info nodes, although it could also be fixed at later stages (e.g. in the LSP request handlers).

Consider the context

/-- Fooifies the args. -/
constant foo : ℕ → ℕ → ℕ
/-- A bar. -/
constant bar : ℕ

Then in the editor we have the following LSP hovers

#check foo bar bar = id bar
/-     ------------0-------
       ---1-------   --2---
       -3- -4- -4-   5- -4-
0 => Prop
1 => Nat
2 => Nat
3 => foo : Nat → Nat → Nat | Fooify args.
4 => bar : Nat | A bar.
5 => id.{1} : {α : Type} → α → α
-/

Note that

• Since the smallest one is always selected, to see e.g. the full application 1, you have to hover over the space. It seemed reasonable to me since space is actually the function application operator, however @gebner pointed out to me that this is not very discoverable.
• The head function syntaxes are selectable, e.g. in 3, and we can see the docstrings for them. However this is not true of notation applications, i.e. = is not selectable.

Whereas in the infoview we have

/- foo bar bar = id bar
   ------------0-------
   ---1-------   --2---
       -3- -3-      -3-
0 => @Eq.eq Nat (foo bar bar) (id bar) : Prop
1 => foo bar bar : Nat
2 => @id Nat bar : Nat
3 => bar : Nat | A bar.
-/

And here

• We cannot select the head function, only the total application. This makes it easier to point at things since the span is wider.
• Since we only show the docstring for constants, the doc for foo is not shown at 1.
• The notation symbol = is similarly not selectable.

Now, should we make those entirely consistent? My intuition would be 'yes', although the infoview has extra capabilities — the contents of hover popups are themselves interactive — that might imply we should display less there unless the user requests it.

If we do make them consistent, which one to go for? In past discussions I preferred the editor variant (with hover-over-space), but I think I am in the minority on this. If we select the full-application variant, we should also show the docstring for the head constant on Expr.app nodes.

This also has some implications for upcoming widget APIs. The selectable regions from the delaborator correspond to SubexprInfo nodes which widget tactics will be given in their execution context and will use to decide e.g. where to zoom in with conv. For this they might need a custom delaborator mode which tags any subexpression including partial applications like foo bar.

For completeness, in Lean 3 the editor hovers are

example : foo bar bar = id bar := sorry
/-        -0- -1- -1- 2 3- -1-
0 => foo : ℕ → ℕ → ℕ | Fooify args.
1 => bar : ℕ | A bar.
2 => eq : Π {α : Type}, α → α → Prop
3 => id : id : Π {α : Type}, α → α
-/

and the infoview shows

/- expected type:
   ⊢ foo bar bar = id bar
     ------------0-------
     -----1-----   --2---
         -3- -3-      -3-
0 => @eq ℕ (foo bar bar) (id bar) : Prop
1 => foo bar bar : ℕ
2 => @id ℕ bar : ℕ
3 => bar : ℕ
-/

[gebner]

There is another syntax now which is hard to hover: a[i]. There are two one-character ranges that show the full term.