Internal error due to lazy definition realization and backtracking

Consider

@[reducible] def g (x : α) := x

-- def foo := @g.eq_def

example (P : Nat → Prop) : P (id (g 42)) := by
  simp only [g.eq_def]

and hover over the g.eq_def in the last line. You’ll get

mathlib-demo.lean:6:16
Error updating: Error fetching goals: Rpc error: InternalError: unknown constant 'g.eq_def'. Try again.
Messages (2)
mathlib-demo.lean:6:2

invalid `simp` theorem, equation is equivalent to
  x = x

mathlib-demo.lean:6:2

simp made no progress

All Messages (2)

What happens (I believe) is that simp tries to elaborate g.eq_def which generates the equational theorem. But it doesn’t like it (it’s x=x due to g being reducible), some state gets backtracked, and that includes the side-effect of materializing the lazy definition. So when trying to hover it, it’s not there.

Realizing the .eq_def before (e.g. commenting out the def above) makes it work.

It’s unclear if somehow simp is at fault for reverting changes to the environment too much (possibly a regression due to my #4177/#4359, didn’t check yet), or if some other component (language server) needs to try to realize constants here.

Versions

4.11.0-rc2 and 4.12.0-nightly-2024-08-19

Impact

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

Start by reproducing the supplied example in Lean 4.11.0-rc2 or the 2024-08-19 nightly, then inspect the simp elaboration and language-server hover path around lazy realization and backtracking. Done means hovering over g.eq_def no longer reports an unknown constant after the failed simp attempt.