exact? suggests an extra id

[ldct]

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

exact? suggests term with id

Context

Steps to Reproduce

1. In this proof, hover over exact? to see what it suggests: example (a : Nat) (ha : a ≠ 0) : (0 < a ∨ a < 0) := by exact?

Expected behavior:

It suggests exact Nat.lt_or_gt_of_ne (Ne.symm ha)

Actual behavior:

It suggests exact Nat.lt_or_gt_of_ne (id (Ne.symm ha)) (note the extra id)

Versions

Lean 4.16.0-nightly-2025-01-19
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Thanks for the report. It seems that it's not pretty, but also not harmful, right?

(I wonder if the id comes from a type annotation added by the meta code, and omitting the type argument here means that in some case the roof term doesn't re-elaborate. Maybe an “expected Type hint” should use a variant of id that takes the type as an explicit argument. Or the delaborator could be clever about when to use @id.)