Hovering over underscore (`_`) shows type, but not term

Aaron1011 commented 4 days ago

Prerequisites

Please put an X between the brackets as you perform the following steps:

[X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
[X] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

Under certain circumstances, hovering over an _ term only shows the type (e.g. Nat) in the hover window. Normally, it shows both the inferred term and the inferred type (e.g. Nat.zero: Nat).

Context

I ran into this when inspecting an exact h _ expression in a more complicated theorem: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Show.20inferred.20value.20for.20.60_.60.20with.20vscode-lean4/near/470644209

Steps to Reproduce

Paste the following code into the Lean web editor:

theorem bad_lsp (h: ∀ m : Nat, Nat.zero = m) : Nat.zero = (Nat.zero + Nat.zero) := by show_term exact h _

Hover over the _, and note that the editor just shows:
```
Nat
A placeholder term, to be synthesized by unification.
```
Hovering over show_term shows Try this: exact h (Nat.zero + Nat.zero)
Replace (Nat.zero + Nat.zero) with (Nat.zero) in the editor
Hover over the _ again, and note that the editor now shows:
```
Nat.zero : Nat
A placeholder term, to be synthesized by unification.
```
Hovering over show_term shows Try this: exact h Nat.zero

Expected behavior: The hover output should always contain the term (Nat.zero + Nat.zero) suggested by show_term

Actual behavior: The hover output only displays the type (Nat)

Versions

"4.12.0-nightly-2024-09-16"

Additional Information

Impact

kmill commented 2 days ago

I think it would be a great improvement if hovering over _ would show the solved-for term!

If I'm reading the code correctly, the relevant popup logic is in Lean.Elab.Info.fmtHover?.fmtTermAndModule?, which only shows terms that are constants or otherwise "atomic". This explains the observed behavior, since Nat.zero is a constant (so appears in the hover) and Nat.zero + Nat.zero is not "atomic". If this issue is accepted, an implementation could be to show the term in the event ti.elaborator is Lean.Elab.Term.elabHole. I think this should happen before the .const exception, since we want to know the actual solved-for term, not the signature of the constant (without solved-for universe levels).

thorimur commented 13 hours ago

By the way, I'd love if this functionality were implemented as a special case of setting a flag in TermInfo which could be accessed by e.g. passing an optional argument to addTermInfo. This would enable metaprogrammers to add more explicit term hovers to custom notations/elaborators; see, for example, this discussion on zulip.

leanprover / lean4