Ensure shadowed variables are inaccessible in quotations

Qq/Macro.lean

@@ -300,9 +300,29 @@ def unquoteLevelLCtx (addDefEqs := true) : UnquoteM Unit := do
 
 def unquoteLCtx : UnquoteM Unit := do
   unquoteLevelLCtx
+  let mut latestIdForName : PersistentHashMap Name FVarId := {}
   for ldecl in (← getLCtx) do
     let fv := ldecl.toExpr
     let ty := ldecl.type
+    let userName := addDollar ldecl.userName
+
+    /-
+      Ensure that names which (in the original context) are shadowed by the currently considered
+      variable are also inaccessible in the quotation context, even if the variable is not added
+      to the new context
+    -/
+    if let some id := latestIdForName.find? userName then
+      -- Shadowed names are made inaccessible by making them hygienic
+      let hygienicName ← MonadQuotation.addMacroScope userName
+      modify fun s => { s with
+          unquoted := s.unquoted.modifyLocalDecl id fun shadowed =>
+            if shadowed.userName == userName then
+              shadowed.setUserName hygienicName
+            else
+              shadowed
+        }
+    latestIdForName := latestIdForName.insert userName ldecl.fvarId
+
     let whnfTy ← withReducible <| whnf ty
     if whnfTy.isAppOfArity ``QuotedLevelDefEq 2 || whnfTy.isAppOfArity ``Level 0 then
       pure () -- see above
@@ -311,7 +331,7 @@ def unquoteLCtx : UnquoteM Unit := do
       let newTy ← unquoteExpr qTy
       modify fun s => { s with
         unquoted := s.unquoted.addDecl $
-          LocalDecl.cdecl ldecl.index ldecl.fvarId (addDollar ldecl.userName) newTy ldecl.binderInfo ldecl.kind
+          LocalDecl.cdecl ldecl.index ldecl.fvarId userName newTy ldecl.binderInfo ldecl.kind
         exprBackSubst := s.exprBackSubst.insert fv (.quoted fv)
         exprSubst := s.exprSubst.insert fv fv
       }
@@ -323,7 +343,7 @@ def unquoteLCtx : UnquoteM Unit := do
       let eqTy := mkApp3 (.const ``Eq [tyLevel]) ty lhs rhs
       let unquoted := (← get).unquoted
       let unquoted := unquoted.addDecl <|
-        .cdecl ldecl.index ldecl.fvarId (addDollar ldecl.userName) eqTy ldecl.binderInfo ldecl.kind
+        .cdecl ldecl.index ldecl.fvarId userName eqTy ldecl.binderInfo ldecl.kind
       let unquoted := (← withUnquotedLCtx do makeDefEq lhs rhs).getD unquoted
       modify fun s => { s with
         unquoted
@@ -334,7 +354,7 @@ def unquoteLCtx : UnquoteM Unit := do
       let .succ u ← getLevel ty | pure ()
       let LOption.some inst ← trySynthInstance (mkApp (.const ``ToExpr [u]) ty) | pure ()
       modify fun s => { s with
-        unquoted := s.unquoted.addDecl (ldecl.setUserName (addDollar ldecl.userName))
+        unquoted := s.unquoted.addDecl (ldecl.setUserName userName)
         exprBackSubst := s.exprBackSubst.insert fv (.quoted (mkApp3 (.const ``toExpr [u]) ty inst fv))
         exprSubst := s.exprSubst.insert fv fv
       }

examples/shadowing.lean

@@ -0,0 +1,31 @@
+import Qq
+open Qq
+
+-- TODO; use Std's `guard_msgs` instead
+open Lean.Elab in
+/-- `success_if_error% f with "msg"` expects `f` to emit the provided error -/
+elab "success_if_error% " f:term " with " msg:str : term <= expected_type => do
+  let initMsgs ← modifyGetThe Lean.Core.State fun st => (st.messages, { st with messages := {} })
+  let fe ← Term.elabTerm f expected_type
+  let msgs := (← getThe Lean.Core.State).messages.msgs.filter (·.severity == .error)
+  modifyThe Lean.Core.State fun st => { st with messages := initMsgs }
+  match msgs.toList with
+  | m :: _ =>
+    let ex_msg ← m.data.toString
+    if ex_msg ≠ msg.getString then
+      Lean.logErrorAt msg m!"got\n{ex_msg}\nexpected\n{msg}"
+  | [] =>
+    Lean.logErrorAt f "Elaborated with no error"
+  return fe
+
+/-
+  This fails, the second definition of `n`, which is not of type `Nat`, shadows the first,
+  `Nat`-typed, definition of `n`.
+  Even if the second definition is not available inside the quotation (`Nat → Nat` does not implement `ToExpr`)
+  we don't want `$n` to refer to the shadowed definition, that would be confusing
+-/
+example : Q(Nat) :=
+  let n : Nat := 1
+  let n : Nat := 2
+  let n : Nat → Nat := fun _ => n
+  success_if_error% q($n) with "unknown identifier '«$n»'"