From d69a8eff3fa153c081485bdd093fa58e2792a696 Mon Sep 17 00:00:00 2001
From: JovanGerb <56355248+JovanGerb@users.noreply.github.com>
Date: Thu, 15 May 2025 12:33:10 +0100
Subject: [PATCH] fix: deduplicate elaboration of constant argument to `rw`
 (#8232)

This PR fixes elaboration of constants in the `rewrite` tactic.
previously, `rw [eq_self]` would elaborate `eq_self` twice, and add it
to the infotree twice. This would lead to the "Expected type" being
delaborated with an unknown universe metavariable.

I added a test to show this error during delaboration of the "Expected
type".

This was reported on Zulip as a panic message during delaboration:
[#mathlib4 > Crash in &#96;sup&#96;/&#96;inf&#96; /
&#96;max&#96;/&#96;min&#96;
delaborators](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Crash.20in.20.60sup.60.2F.60inf.60.20.2F.20.60max.60.2F.60min.60.20delaborators/with/515946714)
---
 src/Lean/Elab/Tactic/Rewrite.lean             |  4 ++--
 tests/lean/interactive/rwElabConst.lean       | 21 +++++++++++++++++++
 .../interactive/rwElabConst.lean.expected.out |  5 +++++
 3 files changed, 28 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/interactive/rwElabConst.lean
 create mode 100644 tests/lean/interactive/rwElabConst.lean.expected.out

diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
index 9f52fe3546..ecb83fefef 100644
--- a/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -51,7 +51,7 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
         let term := rule[1]
         let processId (id : Syntax) : TacticM Unit := do
           -- See if we can interpret `id` as a hypothesis first.
-          if (← optional <| getFVarId id).isSome then
+          if (← withMainContext <| Term.isLocalIdent? id).isSome then
             x symm term
           else
             -- Try to get equation theorems for `id`.
@@ -62,8 +62,8 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
             let rec go : List Name →  TacticM Unit
               | [] => throwError "failed to rewrite using equation theorems for '{declName}'.{hint}"
               | eqThm::eqThms => (x symm (mkCIdentFrom id eqThm)) <|> go eqThms
-            go eqThms.toList
             discard <| Term.addTermInfo id (← mkConstWithFreshMVarLevels declName) (lctx? := ← getLCtx)
+            go eqThms.toList
         match term with
         | `($id:ident)  => processId id
         | `(@$id:ident) => processId id
diff --git a/tests/lean/interactive/rwElabConst.lean b/tests/lean/interactive/rwElabConst.lean
new file mode 100644
index 0000000000..beec4acb25
--- /dev/null
+++ b/tests/lean/interactive/rwElabConst.lean
@@ -0,0 +1,21 @@
+import Lean
+
+/-!
+Previously, `rw [my_lemma]` would elaborate `my_lemma` twice, both times generating new universe metavariables.
+This caused the "Expected type" to contain a universe metavariable that wasn't in the metavariable context.
+
+This test verifies that the generated universe level is in the metavariable context.
+-/
+
+open Lean PrettyPrinter Delaborator SubExpr
+/-- No-op delaborator that checks that the universe level is in the metavariable context -/
+@[delab app.Eq]
+def checkUniv : Delab := do
+  let .const _ [.mvar u] := (← getExpr).getAppFn | failure
+  _ ← u.getLevel -- if `u` isn't in the metavariable context, this throws an error during elaboration
+  failure
+
+example : True := by
+  try rw [eq_self]
+          --^ $/lean/plainTermGoal
+  trivial
diff --git a/tests/lean/interactive/rwElabConst.lean.expected.out b/tests/lean/interactive/rwElabConst.lean.expected.out
new file mode 100644
index 0000000000..b49a64f1da
--- /dev/null
+++ b/tests/lean/interactive/rwElabConst.lean.expected.out
@@ -0,0 +1,5 @@
+{"textDocument": {"uri": "file:///rwElabConst.lean"},
+ "position": {"line": 18, "character": 12}}
+{"range":
+ {"start": {"line": 18, "character": 10}, "end": {"line": 18, "character": 17}},
+ "goal": "⊢ ∀ {α : Sort ?u} (a : α), (a = a) = True"}