From 357b52928f905bfb85a3496e411cf12fa20e730c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 19 Jun 2024 07:52:45 +0200
Subject: [PATCH] fix: global definition shadowing a local one when using
 dot-notation (#4497)

closes #3079
---
 src/Lean/Elab/Term.lean  | 21 +++++++++++++----
 tests/lean/run/3079.lean | 49 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 66 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/3079.lean

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 81dfec93a9..69c23f1ee0 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1398,7 +1398,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
   ```
   def foo.aux := 1
   def foo : Nat → Nat
-    | n => foo.aux -- should not be interpreted as `(foo).bar`
+    | n => foo.aux -- should not be interpreted as `(foo).aux`
   ```
   See test `aStructPerfIssue.lean` for another example.
   We skip auxiliary declarations when `projs` is not empty and `globalDeclFound` is true.
@@ -1415,16 +1415,29 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
   -/
   let rec loop (n : Name) (projs : List String) (globalDeclFound : Bool) := do
     let givenNameView := { view with name := n }
-    let mut globalDeclFound := globalDeclFound
+    let mut globalDeclFoundNext := globalDeclFound
     unless globalDeclFound do
       let r ← resolveGlobalName givenNameView.review
       let r := r.filter fun (_, fieldList) => fieldList.isEmpty
       unless r.isEmpty do
-        globalDeclFound := true
+        globalDeclFoundNext := true
+    /-
+    Note that we use `globalDeclFound` instead of `globalDeclFoundNext` in the following test.
+    Reason: a local should shadow a global with the same name.
+    Consider the following example. See issue #3079
+    ```
+    def foo : Nat := 1
+
+    def bar : Nat :=
+      foo.add 1 -- should be 11
+    where
+      foo := 10
+    ```
+    -/
     match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && not projs.isEmpty) with
     | some decl => return some (decl.toExpr, projs)
     | none => match n with
-      | .str pre s => loop pre (s::projs) globalDeclFound
+      | .str pre s => loop pre (s::projs) globalDeclFoundNext
       | _ => return none
   loop view.name [] (globalDeclFound := false)
 
diff --git a/tests/lean/run/3079.lean b/tests/lean/run/3079.lean
new file mode 100644
index 0000000000..5f4484799a
--- /dev/null
+++ b/tests/lean/run/3079.lean
@@ -0,0 +1,49 @@
+def foo : Nat := 1
+
+def bar : Nat :=
+  let rec foo := 10
+  foo.add 1
+
+def baz : Nat :=
+  .add foo 1
+where
+  foo := 10
+
+def bar2 : Nat :=
+  foo.add 1
+where
+  foo := 10
+
+/--
+info: 11
+-/
+#guard_msgs in
+#eval bar -- 11
+/--
+info: 11
+-/
+#guard_msgs in
+#eval baz -- 11
+/--
+info: 11
+-/
+#guard_msgs in
+#eval bar2
+
+def bla.aux := 1
+def bla : Nat → Nat
+ | n => n + bla.aux -- should not be interpreted as `(bla).aux`
+
+/--
+info: 4
+-/
+#guard_msgs in
+#eval bla 3
+
+def boo : Nat :=
+  let n := 0
+  n.succ + (m |>.succ) + m.succ
+where
+  m := 1
+
+example : boo = 5 := rfl