feat: use sanitizeNames at ppGoal

src/Lean/LocalContext.lean

@@ -395,13 +395,6 @@ def isInaccessibleUserName : Name → Bool
 | Name.num p idx _ => isInaccessibleUserName p
 | _                => false
 
-private def sanitizeMacroScopes (unicode : Bool) (mainModule : Name) (userName : Name) : Name :=
-if !userName.hasMacroScopes then
-  userName
-else
-  let userName := if (extractMacroScopes userName).mainModule == mainModule then userName.simpMacroScopes else userName;
-  mkInaccessibleUserName unicode userName
-
 private partial def mkFreshInaccessibleUserName (unicode : Bool) (usedName2Idx : NameMap Nat) (userName : Name) : Nat → Name × NameMap Nat
 | idx =>
   let userNameNew := mkInaccessibleUserName unicode (mkNameNum userName idx);
@@ -410,21 +403,33 @@ private partial def mkFreshInaccessibleUserName (unicode : Bool) (usedName2Idx :
   else
    (userNameNew, usedName2Idx.insert userName (idx+1))
 
-def sanitizeNames (lctx : LocalContext) (options : Options) (mainModule : Name) : LocalContext :=
+def sanitizeNamesDefault := true
+@[init] def sanitizeNamesOption : IO Unit :=
+registerOption `pp.sanitizeNames { defValue := sanitizeNamesDefault, group := "pp", descr := "add suffix '_{<idx>}' to shadowed variables when pretty printing" }
+def getSanitizeNames (o : Options) : Bool:= o.get `pp.sanitizeNames sanitizeNamesDefault
+
+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;
     match lctx.decls.get! i with
     | none      => acc
-    | some decl => do
-      let userName := decl.userName.eraseMacroScopes;
-      match usedName2Idx.find? userName with
-      | none     => (lctx, usedName2Idx.insert userName 1)
-      | some idx =>
+    | 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))
+        (lctx, usedName2Idx);
+      let userName := decl.userName;
+      if userName.hasMacroScopes then
+        let userName := userName.eraseMacroScopes;
+        let idx      := (usedName2Idx.find? userName).getD 1;
+        mkFreshUserName userName idx
+      else
+        match usedName2Idx.find? userName with
+        | none => (lctx, usedName2Idx.insert userName 1)
+        | some idx => mkFreshUserName userName idx)
   (lctx, {});
 lctx
 

src/Lean/Message.lean

@@ -58,16 +58,8 @@ registerOption `syntaxMaxDepth { defValue := (2 : Nat), group := "", descr := "m
 def getSyntaxMaxDepth (opts : Options) : Nat :=
 opts.getNat `syntaxMaxDepth 2
 
-def sanitizeNamesDefault := true
-@[init] def sanitizeNamesOption : IO Unit :=
-registerOption `pp.sanitizeNames { defValue := sanitizeNamesDefault, group := "pp", descr := "add suffix '_{<idx>}' to shadowed variables when pretty printing" }
-def getSanitizeNames (o : Options) : Bool:= o.get `pp.sanitizeNames sanitizeNamesDefault
-
 private def sanitizeNames (ctx : MessageDataContext) : MessageDataContext :=
-if getSanitizeNames ctx.opts then
-  { ctx with lctx := ctx.lctx.sanitizeNames ctx.opts ctx.env.mainModule }
-else
-  ctx
+{ ctx with lctx := ctx.lctx.sanitizeNames ctx.opts }
 
 def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext :=
 { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts,

src/Lean/Util/PPGoal.lean

@@ -22,6 +22,7 @@ match mctx.findDecl? mvarId with
   let indent       := 2; -- Use option
   let showAuxDecls := getShowAuxDecls opts;
   let lctx         := mvarDecl.lctx;
+  let lctx         := lctx.sanitizeNames opts;
   let ppCtx        := { ppCtx with lctx := lctx };
   let pp (e : Expr) : IO Format := ppExpr ppCtx e;
   let instMVars (e : Expr) : Expr := (mctx.instantiateMVars e).1;
@@ -38,7 +39,7 @@ match mctx.findDecl? mvarId with
         typeFmt ← pp type;
         pure $ fmt ++ (Format.joinSep ids.reverse " " ++ " :" ++ Format.nest indent (Format.line ++ typeFmt)).group
       };
-  (varNames, type?, fmt) ← mvarDecl.lctx.foldlM
+  (varNames, type?, fmt) ← lctx.foldlM
     (fun (acc : List Name × Option Expr × Format) (localDecl : LocalDecl) =>
        if !showAuxDecls && localDecl.isAuxDecl then pure acc else
        let (varNames, prevType?, fmt) := acc;

tests/lean/shadow.lean

@@ -3,7 +3,14 @@ new_frontend
 theorem ex1 {α} (x : α) (h : x = x) (x : α) : x = x :=
 h
 
-set_option pp.sanitizeNames false
-
+set_option pp.sanitizeNames false in
 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} → α → β → δ → α × β × δ :=
+_
+
+set_option pp.sanitizeNames false in
+def foo {α} [Inhabited α] (inst inst : α) : {β δ : Type} → α → β → δ → α × β × δ :=
+_

tests/lean/shadow.lean.expected.out

@@ -6,7 +6,7 @@ but it is expected to have type
   x=x
 failed to synthesize instance
   CoeT (x✝¹=x✝¹) _ (x=x)
-shadow.lean:9:0: error: type mismatch
+shadow.lean:8:0: error: type mismatch
   h
 has type
   x=x
@@ -14,3 +14,26 @@ but it is expected to have type
   x=x
 failed to synthesize instance
   CoeT (x=x) _ (x=x)
+with resulting expansion
+   section set_option pp.sanitizeNames false theorem ex2 {α} (x : α) (h : x = x) (x : α) : x = x :=
+  h -- this error is confusing because we have disabled `pp.sanitizeNames`
+  
+   end 
+while expanding
+  set_option pp.sanitizeNames false in
+  theorem ex2 {α} (x : α) (h : x = x) (x : α) : x = x :=
+  h 
+shadow.lean:12:0: error: don't know how to synthesize placeholder
+context:
+α : Type u_1
+inst✝² : Inhabited α
+inst✝¹ inst : α
+β✝¹ δ✝¹ : Type
+⊢ α → β✝¹ → δ✝¹ → α×β✝¹×δ✝¹
+shadow.lean:16:0: error: don't know how to synthesize placeholder
+context:
+α : Type u_1
+inst.19 : Inhabited α
+inst inst : α
+β.44 δ.45 : Type
+⊢ α → β.44 → δ.45 → α×β.44×δ.45