fix: sanitizeNames

A macro scoped name cannot shadow a name without macro scopes.

src/Lean/LocalContext.lean

@@ -411,26 +411,22 @@ def getSanitizeNames (o : Options) : Bool:= o.get `pp.sanitizeNames sanitizeName
 def sanitizeNames (lctx : LocalContext) (options : Options) : LocalContext :=
 if !getSanitizeNames options then lctx else
 let unicode   := Format.getUnicode options;
-let (lctx, _) := lctx.decls.size.foldRev
-  (fun i (acc : LocalContext × NameMap Nat) =>
-    let (lctx, usedName2Idx) := acc;
+let (lctx, _, _) := lctx.decls.size.foldRev
+  (fun i (acc : LocalContext × NameSet × NameMap Nat) =>
+    let (lctx, usedNames, usedName2Idx) := acc;
     match lctx.decls.get! i with
     | none      => acc
     | some decl =>
-      let mkFreshUserName (userName : Name) (idx : Nat) : LocalContext × NameMap Nat :=
-        let (userNameNew, usedName2Idx) := mkFreshInaccessibleUserName unicode usedName2Idx userName idx;
-        let lctx := lctx.setUserName decl.fvarId userNameNew;
-        (lctx, usedName2Idx);
       let userName := decl.userName;
-      if userName.hasMacroScopes then
+      if userName.hasMacroScopes || usedNames.contains userName then
         let userName := userName.eraseMacroScopes;
         let idx      := (usedName2Idx.find? userName).getD 1;
-        mkFreshUserName userName idx
+        let (userNameNew, usedName2Idx) := mkFreshInaccessibleUserName unicode usedName2Idx userName idx;
+        let lctx := lctx.setUserName decl.fvarId userNameNew;
+        (lctx, usedNames, usedName2Idx)
       else
-        match usedName2Idx.find? userName with
-        | none => (lctx, usedName2Idx.insert userName 1)
-        | some idx => mkFreshUserName userName idx)
-  (lctx, {});
+        (lctx, usedNames.insert userName, usedName2Idx))
+  (lctx, {}, {});
 lctx
 
 end LocalContext

tests/lean/shadow.lean

@@ -8,9 +8,13 @@ theorem ex2 {α} (x : α) (h : x = x) (x : α) : x = x :=
 h -- this error is confusing because we have disabled `pp.sanitizeNames`
 
 set_option pp.sanitizeNames true in
-def foo {α} [Inhabited α] (inst inst : α) : {β δ : Type} → α → β → δ → α × β × δ :=
+def foo1 {α} [Inhabited α] (inst inst : α) : {β δ : Type} → α → β → δ → α × β × δ :=
 _
 
 set_option pp.sanitizeNames false in
-def foo {α} [Inhabited α] (inst inst : α) : {β δ : Type} → α → β → δ → α × β × δ :=
+def foo2 {α} [Inhabited α] (inst inst : α) : {β δ : Type} → α → β → δ → α × β × δ :=
+_
+
+set_option pp.sanitizeNames true in
+def foo3 {α β} (inst : α) (b : β) (inst : α) [Inhabited α] : {β δ : Type} → α → β → δ → α × β × δ :=
 _

tests/lean/shadow.lean.expected.out

@@ -37,3 +37,13 @@ inst.19 : Inhabited α
 inst inst : α
 β.44 δ.45 : Type
 ⊢ α → β.44 → δ.45 → α×β.44×δ.45
+shadow.lean:20:0: error: don't know how to synthesize placeholder
+context:
+α : Type u_1
+β : Sort u_2
+inst✝² : α
+b : β
+inst : α
+inst✝¹ : Inhabited α
+β✝¹ δ✝¹ : Type
+⊢ α → β✝¹ → δ✝¹ → α×β✝¹×δ✝¹