unknown metavariable error in `rw [] at *`

[JovanGerb]

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

The "Expected type" information for e in rw [e] at * doesn't have acess to the right metavariable context if the rewrite failed in the targed expression. In the following code, put your cursor on the _:

example (h : 1 + 2 = 3) : True := by
  rw [Nat.add_comm _] at *

Then the infoview says:

Error updating: Error fetching goals: Rpc error: InternalError: unknown metavariable '?_uniq.187'.`

This is caused by the following chain of events:

1. Nat.add_comm _ is elaborated to try rewriting in the goal, and this adds "Expected type" information to the info tree. However, the rewrite fails, so the metavariable context is reverted.
2. Nat.add_comm _ is elaborated again to try rewriting at h, and this also adds "Expected type" information to the info tree. This succeeds, so the metavariable context is not reverted.
3. This metavariable context is stored in the info tree. This happens in the call to withTacticInfoContext inside of withRWRulesSeq

When putting the cursor on _, you would see the "Expected type" information from step 1, pretty printed with the metavariable context that was stored in step 3. Hence, we get an unknown metavariable error and the infoview crashes.

Context

This issue was reported by Bhavik Mehta, where it was Mathlib's max/min delaborator that failed. In this case is was an unknown universe metavariable, so there was a panic error instead of a usual error.

#mathlib4 > Crash in `sup`/`inf` / `max`/`min` delaborators @ 💬

Steps to Reproduce

In this code, put your cursor on the _

example (h : 1 + 2 = 3) : True := by
  rw [Nat.add_comm _] at *

Expected behavior:

You see the expected type (which is Nat)

Actual behavior:

The tactic state and the "Expected type" are not visible, but instead there is an error Error updating: Error fetching goals: Rpc error: InternalError: unknown metavariable '?_uniq.187'. Try again.

Lean 4.26.0-nightly-2025-10-22

Additional Information

There are two ways in which this problem could be solved:

1. Make sure that we add the metavariable context to the info tree before reverting the metavariable context
2. When we revert the metavariable context after a failed rewrite, also revert the changes to the info tree. This has the advantage that we only get hover information for cases where rewriting succeeded. However, if no case succeeded, then we don't have any hover information anymore, so it would need to be added again.

Impact

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