fix: make rw [foo] look in the local context for foo before it lo…

…oks in the environment (#2738)

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

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