From 50f2154cbb8caaaba07e933f02a3348d40df620a Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Sun, 29 Oct 2023 23:08:02 -0400
Subject: [PATCH] fix: make `rw [foo]` look in the local context for `foo`
 before it looks in the environment (#2738)

---
 src/Lean/Elab/Tactic/Rewrite.lean             | 20 +++++++++++-------
 tests/lean/rwPrioritizesLCtxOverEnv.lean      | 21 +++++++++++++++++++
 ...rwPrioritizesLCtxOverEnv.lean.expected.out |  0
 3 files changed, 33 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/rwPrioritizesLCtxOverEnv.lean
 create mode 100644 tests/lean/rwPrioritizesLCtxOverEnv.lean.expected.out

diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
index 55f56d835e..0a0f1f5819 100644
--- a/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -45,14 +45,18 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
         let symm := !rule[0].isNone
         let term := rule[1]
         let processId (id : Syntax) : TacticM Unit := do
-          -- Try to get equation theorems for `id` first
-          let declName ← try resolveGlobalConstNoOverload id catch _ => return (← x symm term)
-          let some eqThms ← getEqnsFor? declName (nonRec := true) | x symm term
-          let rec go : List Name →  TacticM Unit
-            | [] => throwError "failed to rewrite using equation theorems for '{declName}'"
-            | eqThm::eqThms => (x symm (mkIdentFrom id eqThm)) <|> go eqThms
-          go eqThms.toList
-          discard <| Term.addTermInfo id (← mkConstWithFreshMVarLevels declName) (lctx? := ← getLCtx)
+          -- See if we can interpret `id` as a hypothesis first.
+          if (← optional <| getFVarId id).isSome then
+            x symm term
+          else
+            -- Try to get equation theorems for `id`.
+            let declName ← try resolveGlobalConstNoOverload id catch _ => return (← x symm term)
+            let some eqThms ← getEqnsFor? declName (nonRec := true) | x symm term
+            let rec go : List Name →  TacticM Unit
+              | [] => throwError "failed to rewrite using equation theorems for '{declName}'"
+              | eqThm::eqThms => (x symm (mkIdentFrom id eqThm)) <|> go eqThms
+            go eqThms.toList
+            discard <| Term.addTermInfo id (← mkConstWithFreshMVarLevels declName) (lctx? := ← getLCtx)
         match term with
         | `($id:ident)  => processId id
         | `(@$id:ident) => processId id
diff --git a/tests/lean/rwPrioritizesLCtxOverEnv.lean b/tests/lean/rwPrioritizesLCtxOverEnv.lean
new file mode 100644
index 0000000000..a6672c267a
--- /dev/null
+++ b/tests/lean/rwPrioritizesLCtxOverEnv.lean
@@ -0,0 +1,21 @@
+/-! # Ensure `rw` prioritizes the local context over the environment
+
+This test ensures that `rw [foo]` looks for `foo` in the local context before it looks for a
+constant named `foo` in the environment. See issue #2729.
+-/
+
+-- Introduce `foo` to the environment.
+/-- A constant whose name should conflict with that of a local declaration. -/
+def foo : List Nat := [0]
+
+/-! ## Ensure that `foo` from the LCtx is used instead of the constant `foo` -/
+
+example (A B : Prop) (foo : A ↔ B) (b : B) : A := by
+  rw [foo] -- should be interpreted as `foo : A ↔ B`, not `foo : List Nat`, and succeed
+  assumption
+
+/-! ## Ensure that we can access the constant `foo` by writing `rw [_root_.foo]` -/
+
+set_option linter.unusedVariables false in
+example (A B : Prop) (foo : A ↔ B) : _root_.foo = [0] := by
+  rw [_root_.foo] -- should be interpreted as `foo : List Nat`, not `foo : A ↔ B`, and succeed
diff --git a/tests/lean/rwPrioritizesLCtxOverEnv.lean.expected.out b/tests/lean/rwPrioritizesLCtxOverEnv.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2