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

Prerequisites

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

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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

1. 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 _

2. 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)
3. Replace (Nat.zero + Nat.zero) with (Nat.zero) in the editor
4. 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

Start in the Lean web editor with the minimal bad_lsp reproduction and compare hover results for _ before and after replacing (Nat.zero + Nat.zero) with Nat.zero. Investigate the hover information produced around show_term; done means the hover output includes the inferred term as well as its type in both cases.