Bug in widgets: type of `i` in `∃ i, ...` is wrong

[jcommelin]

Description

In the widget view, if you hover over the i in ∃ i, ... it doesn't show the type of i, but the type of the lambda that goes into the existential. Hover in the source code window works as expected.

Steps to Reproduce

Consider

example {α : Type} (h : ∃i : α, i = i) : True :=
by
  trivial

and put your cursor between by and trivial.

Now hover over the i that follows ∃, both in the source code window and in the infoview.

Expected behavior:

If you hover over the corresponding i in the source window, you get i : α in the popup

Actual behavior:

Now hover over the i that follows ∃, in the info view. I would expect the type i : α to show up. But instead the type of the lambda that is part of the ∃ is shown.

Reproduces how often:

100%

Versions

Lean (version 4.0.0-nightly-2022-09-11, commit 1749210a4b39, Release) Linux (NixOS unstable)

[leodemoura]

[EdAyers]

Also true for all other kinds of binder. I think the problem is in withBindingBodyUnusedName in src/lean/prettyprinter/delaborator/basic.lean.

We are annotating the i with the subexpr position of the parent expression. Unfortunately with the way that delaborator works it might not be super-easy to fix this; since there is no subexpr position that would produce the i : α output. Using the binding domain position gives α : Type which is a little confusing.

One way to fix this is to modify SubExpr.Pos to also include a new coordinate value that says we want to report the newly made bound variable.