From b91e22af2bb39b8c859106f275f2c8fca919145e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 22 May 2021 19:07:09 -0700
Subject: [PATCH] fix: fixes #241

---
 src/Lean/Elab/Do.lean             | 16 ++++++
 tests/compiler/rbmap_library.lean |  2 +-
 tests/lean/241.lean               | 86 +++++++++++++++++++++++++++++++
 tests/lean/241.lean.expected.out  | 13 +++++
 tests/lean/run/doNotation2.lean   |  4 +-
 5 files changed, 118 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/241.lean
 create mode 100644 tests/lean/241.lean.expected.out

diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 54349a16f1..cd50c5ad16 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -1150,6 +1150,14 @@ def checkReassignable (xs : Array Name) : M Unit := do
     unless ctx.mutableVars.contains x do
       throwInvalidReassignment x
 
+def checkNotShadowingMutable (xs : Array Name) : M Unit := do
+  let throwInvalidShadowing (x : Name) : M Unit :=
+    throwError "mutable variable '{x.simpMacroScopes}' cannot be shadowed"
+  let ctx ← read
+  for x in xs do
+    if ctx.mutableVars.contains x then
+      throwInvalidShadowing x
+
 @[inline] def withFor {α} (x : M α) : M α :=
   withReader (fun ctx => { ctx with insideFor := true }) x
 
@@ -1265,6 +1273,7 @@ mutual
     let decl    := doLetArrow[2]
     if decl.getKind == `Lean.Parser.Term.doIdDecl then
       let y := decl[0].getId
+      checkNotShadowingMutable #[y]
       let doElem := decl[3]
       let k ← withNewMutableVars #[y] (isMutableLet doLetArrow) (doSeqToCode doElems)
       match isDoExpr? doElem with
@@ -1396,6 +1405,7 @@ mutual
         doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
     else withRef doFor do
       let x         := doForDecls[0][0]
+      withRef x <| checkNotShadowingMutable (← getPatternVarsEx x)
       let xs        := doForDecls[0][2]
       let forElems  := getDoSeqElems doFor[3]
       let forInBodyCodeBlock ← withFor (doSeqToCode forElems)
@@ -1432,6 +1442,7 @@ mutual
     let alts ←  matchAlts.mapM fun matchAlt => do
       let patterns := matchAlt[1]
       let vars ← getPatternsVarsEx patterns.getSepArgs
+      withRef patterns <| checkNotShadowingMutable vars
       let rhs  := matchAlt[3]
       let rhs ← doSeqToCode (getDoSeqElems rhs)
       pure { ref := matchAlt, vars := vars, patterns := patterns, rhs := rhs : Alt CodeBlock }
@@ -1454,6 +1465,8 @@ mutual
     let catches ← doTry[2].getArgs.mapM fun catchStx => do
       if catchStx.getKind == `Lean.Parser.Term.doCatch then
         let x       := catchStx[1]
+        if x.isIdent then
+          withRef x <| checkNotShadowingMutable #[x.getId]
         let optType := catchStx[2]
         let c ← doSeqToCode (getDoSeqElems catchStx[4])
         pure { x := x, optType := optType, codeBlock := c : Catch }
@@ -1518,12 +1531,15 @@ mutual
           let k := doElem.getKind
           if k == `Lean.Parser.Term.doLet then
             let vars ← getDoLetVars doElem
+            checkNotShadowingMutable vars
             mkVarDeclCore vars doElem <$> withNewMutableVars vars (isMutableLet doElem) (doSeqToCode doElems)
           else if k == `Lean.Parser.Term.doHave then
             let var := getDoHaveVar doElem
+            checkNotShadowingMutable #[var]
             mkVarDeclCore #[var] doElem <$> (doSeqToCode doElems)
           else if k == `Lean.Parser.Term.doLetRec then
             let vars ← getDoLetRecVars doElem
+            checkNotShadowingMutable vars
             mkVarDeclCore vars doElem <$> (doSeqToCode doElems)
           else if k == `Lean.Parser.Term.doReassign then
             let vars ← getDoReassignVars doElem
diff --git a/tests/compiler/rbmap_library.lean b/tests/compiler/rbmap_library.lean
index cba7ac5c54..a35c09b01a 100644
--- a/tests/compiler/rbmap_library.lean
+++ b/tests/compiler/rbmap_library.lean
@@ -63,7 +63,7 @@ do IO.setRandSeed seed
        m := m.erase k
      i := i + 1
    check (sz m == a.size / 2)
-   let i := 0
+   i := 0
    for (k, v) in a do
      if i % 2 == 1 then
        check (m.find? k == some v)
diff --git a/tests/lean/241.lean b/tests/lean/241.lean
new file mode 100644
index 0000000000..195ca3db00
--- /dev/null
+++ b/tests/lean/241.lean
@@ -0,0 +1,86 @@
+def ex1 : IO Unit := do
+  let mut xs : Array Nat := #[]
+  let xs := xs -- Error
+  xs := xs.push 0
+  IO.println xs
+
+def ex2 : IO Unit := do
+  let mut xs : Array Nat := #[]
+  let (xs, _) := (xs, 4) -- Error
+  xs := xs.push 0
+  IO.println xs
+
+def ex3 : IO Unit := do
+  let mut xs : Array Nat := #[]
+  match (1, 2) with
+  | (xs, ys) => -- Error
+    xs := xs.push 0
+    IO.println xs
+
+def ex4 : IO Unit := do
+  let mut xs : Array Nat := #[]
+  let (xs, _) ← pure (xs, 4) -- Error
+  xs := xs.push 0
+  IO.println xs
+
+def ex5 : IO Unit := do
+  let mut xs : Array Nat := #[]
+  let xs ← pure xs -- Error
+  xs := xs.push 0
+  IO.println xs
+
+def ex6 : IO Unit := do
+  let mut xs : Array Nat := #[]
+  if let some xs ← pure (some 4) then -- Error
+    IO.println xs
+  else
+    pure ()
+
+def ex7 : IO Unit := do
+  let mut xs : Array Nat := #[]
+  if let some xs := some 4 then -- Error
+    IO.println xs
+  else
+    pure ()
+
+def ex8 : IO Unit := do
+  let mut xs : Array Nat := #[]
+  if let some xs ← pure (some 4) then -- Error
+    IO.println xs
+  else
+    pure ()
+
+def ex9 : IO Unit := do
+  let mut xs : Array Nat := #[]
+  try
+    IO.println xs
+  catch
+    | IO.Error.userError xs => -- Error
+      pure ()
+    | _ =>
+      pure ()
+
+def ex10 : IO Unit := do
+  let mut xs : Array Nat := #[]
+  try
+    IO.println xs
+  catch xs => -- Error
+    pure ()
+
+def ex11 : IO Unit := do
+  let mut xs : Array (Nat × Nat) := #[(1,2)]
+  for (xs, y) in xs do -- Error
+    xs := xs.push (0, 0)
+    IO.println xs
+
+def ex12 : IO Unit := do
+  let mut xs : Array Nat := #[1,2,3]
+  for xs in xs do -- Error
+    xs := xs.push 0
+    IO.println xs
+
+def ex13 : IO Unit := do
+  let mut xs : Array Nat := #[1,2,3]
+  for a in [:10], xs in [1,2,3] do -- Error
+    xs := xs.push 0
+    IO.println xs
diff --git a/tests/lean/241.lean.expected.out b/tests/lean/241.lean.expected.out
new file mode 100644
index 0000000000..98ae306cab
--- /dev/null
+++ b/tests/lean/241.lean.expected.out
@@ -0,0 +1,13 @@
+241.lean:3:2-3:14: error: mutable variable 'xs' cannot be shadowed
+241.lean:9:2-9:24: error: mutable variable 'xs' cannot be shadowed
+241.lean:16:4-16:12: error: mutable variable 'xs' cannot be shadowed
+241.lean:22:2-22:28: error: mutable variable 'xs' cannot be shadowed
+241.lean:28:2-28:18: error: mutable variable 'xs' cannot be shadowed
+241.lean:34:9-34:16: error: mutable variable 'xs' cannot be shadowed
+241.lean:41:9-41:16: error: mutable variable 'xs' cannot be shadowed
+241.lean:48:9-48:16: error: mutable variable 'xs' cannot be shadowed
+241.lean:58:6-58:27: error: mutable variable 'xs' cannot be shadowed
+241.lean:67:8-67:10: error: mutable variable 'xs' cannot be shadowed
+241.lean:72:6-72:13: error: mutable variable 'xs' cannot be shadowed
+241.lean:78:6-78:8: error: mutable variable 'xs' cannot be shadowed
+241.lean:84:2-86:17: error: mutable variable 'xs' cannot be shadowed
diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean
index d3843b889a..50ff6af1ec 100644
--- a/tests/lean/run/doNotation2.lean
+++ b/tests/lean/run/doNotation2.lean
@@ -34,8 +34,8 @@ def h (x : Nat) (y : Nat) : Nat := do
 let mut x := x
 let mut y := y
 if x > 0 then
-  let y := x + 1 -- this is a new `y` that shadows the one above
-  x := y
+  let y' := x + 1
+  x := y'
 else
   y := y + 1
 return x + y