fix: pretty printing of constants should consider accessibility of names

src/Lean/Elab/PreDefinition/Main.lean

@@ -336,7 +336,7 @@ def addPreDefinitions (docCtx : LocalContext × LocalInstances) (preDefs : Array
                   (structuralRecursion docCtx preDefs termMeasures?s)
                   (wfRecursion docCtx preDefs termMeasures?s))
                 (fun msg =>
-                  let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
+                  let preDefMsgs := preDefs.toList.map (MessageData.ofConstName <| ·.declName)
                   m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
           catch ex =>
             logException ex

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -100,17 +100,31 @@ Rather, it is called through the `app` delaborator.
 -/
 def delabConst : Delab := do
   let Expr.const c₀ ls ← getExpr | unreachable!
-  let unresolveName (n : Name) : DelabM Name := do
-    unresolveNameGlobalAvoidingLocals n (fullNames := ← getPPOption getPPFullNames)
-  let mut c := c₀
-  if isPrivateName c₀ then
-    unless (← getPPOption getPPPrivateNames) do
-      c ← unresolveName c
-      if let some n := privateToUserName? c then
-        -- The private name could not be made non-private, so make the result inaccessible
-        c ← withFreshMacroScope <| MonadQuotation.addMacroScope n
-  else
-    c ← unresolveName c
+  let env ← getEnv
+  let c ←
+    if ← pure (isPrivateName c₀) <&&> getPPOption getPPPrivateNames then
+      pure c₀
+    else if let some c ← unresolveNameGlobalAvoidingLocals? c₀ (fullNames := ← getPPOption getPPFullNames) then
+      pure c
+    else if !env.contains c₀ then
+      -- The compiler pretty prints constants that are not defined in the environment.
+      -- Use such names as-is, without additional macro scopes.
+      -- We still remove the private prefix if the name would be accessible to the current module.
+      if isPrivateName c₀ && mkPrivateName env (privateToUserName c₀.eraseMacroScopes) == c₀.eraseMacroScopes then
+        pure <| Name.modifyBase c₀ privateToUserName
+      else
+        pure c₀
+    else
+      -- The identifier cannot be referred to. To indicate this, we add a delaboration-specific macro scope.
+      -- If the name is private, we also erase the private prefix and add it as an additional macro scope, ensuring
+      -- no collisions between names with different private prefixes.
+      let c := if let some (.num priv 0) := privatePrefix? c₀.eraseMacroScopes then
+          -- The private prefix before `0` is of the form `_private.modulename`, which works as a macro scope context
+          Lean.addMacroScope priv (Name.modifyBase c₀ privateToUserName) reservedMacroScope
+        else
+          c₀
+      pure <| Lean.addMacroScope `_delabConst c reservedMacroScope
+
   let stx ←
     if !ls.isEmpty && (← getPPOption getPPUniverses) then
       let mvars ← getPPOption getPPMVarsLevels

src/Lean/ResolveName.lean

@@ -622,7 +622,7 @@ def resolveLocalName [MonadLCtx m] (n : Name) : m (Option (Expr × List String))
   loop view.name [] (globalDeclFound := false)
 
 /--
-Finds a name that unambiguously resolves to the given name `n₀`.
+Finds an efficient name that unambiguously resolves to the given name `n₀`, if possible.
 Considers suffixes of `n₀` and suffixes of aliases of `n₀` when "unresolving".
 Aliases are considered first.
 
@@ -639,61 +639,63 @@ If `n₀` is an accessible name, then the result will be an accessible name.
 
 The name `n₀` may be private.
 -/
-def unresolveNameGlobal (n₀ : Name) (fullNames := false) (allowHorizAliases := false)
-    (filter : Name → m Bool := fun _ => pure true) : m Name := do
-  if n₀.hasMacroScopes then return n₀
-  -- `n₁` is the name without any private prefix, and `qn₁?` is a valid fully-qualified name.
-  let (n₁, qn₁?) := if let some n := privateToUserName? n₀ then
-    if n₀ == mkPrivateName (← getEnv) n then
-      -- The private name is for the current module. `ResolveName.resolveExact` allows `_root_` for such names.
-      (n, some (rootNamespace ++ n))
-    else
-      (n, none)
-  else
-    (n₀, some (rootNamespace ++ n₀))
+def unresolveNameGlobal? (n₀ : Name)
+    (fullNames := false) (allowHorizAliases := false)
+    (filter : Name → m Bool := fun _ => pure true) :
+    m (Option Name) := OptionT.run do
+  let view := extractMacroScopes n₀
+  -- `n₁` is the name without any private prefix or macro scopes
+  let n₁ := privateToUserName view.name
   if fullNames then
-    if let [(potentialMatch, _)] ← resolveGlobalName n₁ (enableLog := false) then
-      if (← pure (potentialMatch == n₀) <&&> filter n₁) then
-        return n₁
-    if let some qn₁ := qn₁? then
-      -- We assume that the fully-qualified name resolves.
-      return qn₁
-    else
-      -- This is the imported private name case. Return the original private name.
-      return n₀
-  -- `initialNames` is an array of names to try taking suffixes of.
-  -- First are all the names that have `n₀` as an alias.
-  -- If horizontal aliases are not allowed, then any aliases that aren't from a parent namespace are filtered out.
-  let mut initialNames := (getRevAliases (← getEnv) n₀).toArray
+    -- Prefer `n₀` without `_root_`, but add it if necessary.
+    -- (Note: `ResolveName.resolveExact` allows `_root_` for private names accessible to the current module.)
+    return ← tryResolve view n₁ <|> tryResolve view (rootNamespace ++ n₁)
+  -- Now we consider aliases and the (potential) fully qualified name.
+  -- If horizontal aliases are not allowed, then any aliases that aren't from a parent namespace of `n₁` are skipped.
+  -- We try all suffixes for each option, taking the first that resolves to `n₀`, if any.
+  let mut aliases := (getRevAliases (← getEnv) n₀).toArray
   unless allowHorizAliases do
-    initialNames := initialNames.filter fun n => n.getPrefix.isPrefixOf n₁.getPrefix
-  -- After aliases is the fully-qualified name.
-  if let some qn₁ := qn₁? then
-    initialNames := initialNames.push qn₁
-  for initialName in initialNames do
-    if let some n ← unresolveNameCore initialName then
-      return n
-  -- Both non-private names and current-module private names should be handled already,
-  -- but as a backup we return the original name.
-  -- Imported private names will often get to this point.
-  return n₀
+    aliases := aliases.filter fun n => n.getPrefix.isPrefixOf n₁.getPrefix
+  aliases.firstM (unresolveNameCore none) -- do not apply macro scopes on `n₀` to aliases
+    <|> unresolveNameCore view (rootNamespace ++ n₁)
 where
-  unresolveNameCore (n : Name) : m (Option Name) := do
-    if n.hasMacroScopes then return none
+  /-- Adds any macro scopes to `n`, then returns it if it resolves to `n₀` and isn't filtered out. -/
+  tryResolve (view? : Option MacroScopesView) (n : Name) : OptionT m Name := do
+    let n' := if let some view := view? then { view with name := n }.review else n
+    let [(potentialMatch, _)] ← resolveGlobalName (enableLog := false) n' | failure
+    guard <| potentialMatch == n₀
+    guard <| ← filter n'
+    return n'
+  unresolveNameCore (view? : Option MacroScopesView) (n : Name) : OptionT m Name := do
+    guard <| !n.hasMacroScopes
     let n := privateToUserName n
     let mut revComponents := n.componentsRev
     let mut candidate := Name.anonymous
     for cmpt in revComponents do
       candidate := Name.appendCore cmpt candidate
-      if let [(potentialMatch, _)] ← resolveGlobalName (enableLog := false) candidate then
-        if potentialMatch == n₀ then
-          if (← filter candidate) then
-            return some candidate
-    return none
-
-/-- Like `Lean.unresolveNameGlobal`, but also ensures that the unresolved name does not conflict
-with the names of any local declarations. -/
-def unresolveNameGlobalAvoidingLocals [MonadLCtx m] (n₀ : Name) (fullNames := false) : m Name :=
-  unresolveNameGlobal n₀ (fullNames := fullNames) (filter := fun n => Option.isNone <$> resolveLocalName n)
+      try
+        return ← tryResolve view? candidate
+      catch _ : Unit => pure ()
+    failure
+
+/--
+Finds an efficient name that unambiguously resolves to the given name `n₀`, if possible.
+If not, it returns `n₀`. (See `unresolveNameGlobal?`, which returns `none` instead.)
+-/
+def unresolveNameGlobal (n₀ : Name) (fullNames := false) (allowHorizAliases := false)
+    (filter : Name → m Bool := fun _ => pure true) : m Name := do
+  let n? ← unresolveNameGlobal? n₀ (fullNames := fullNames) (allowHorizAliases := allowHorizAliases) (filter := filter)
+  return n?.getD n₀
+
+/-- Like `Lean.unresolveNameGlobal?`, but also ensures that the unresolved name does not conflict
+with the names of any local declarations. Returns `none` if the name cannot be referred to.
+For example, the name may be private and not accessible to the current module, or it may have macro scopes.-/
+def unresolveNameGlobalAvoidingLocals? [MonadLCtx m] (n₀ : Name) (fullNames := false) : m (Option Name) :=
+  unresolveNameGlobal? n₀ (fullNames := fullNames) (filter := fun n => Option.isNone <$> resolveLocalName n)
+
+/-- Like `Lean.unresolveNameGlobalAvoidingLocals?`, but returns `n₀` unchanged if the name cannot be referred to. -/
+def unresolveNameGlobalAvoidingLocals [MonadLCtx m] (n₀ : Name) (fullNames := false) : m Name := do
+  let n? ← unresolveNameGlobalAvoidingLocals? n₀ (fullNames := fullNames)
+  return n?.getD n₀
 
 end Lean

tests/lean/run/10771.lean

@@ -0,0 +1,53 @@
+module
+import all Init.Prelude
+
+/-!
+# Pretty printing imported private names
+https://github.com/leanprover/lean4/issues/10771
+https://github.com/leanprover/lean4/issues/10772
+https://github.com/leanprover/lean4/issues/10773
+-/
+
+/-!
+This used to print `Lean.eraseMacroScopesAux✝ = Lean.eraseMacroScopesAux✝¹`.
+-/
+/-- info: Lean.eraseMacroScopesAux = Lean.eraseMacroScopesAux : Prop -/
+#guard_msgs in
+#check Lean.eraseMacroScopesAux = Lean.eraseMacroScopesAux
+
+/-!
+The first used to print `Lean.eraseMacroScopesAux✝`
+-/
+section
+open Lean Name
+/-- info: eraseMacroScopesAux : Name → Name -/
+#guard_msgs in #check (eraseMacroScopesAux)
+/-- info: eraseMacroScopes : Name → Name -/
+#guard_msgs in #check (eraseMacroScopes)
+end
+
+/-!
+This used to suggest `simp only [_private.Init.Prelude.0.Lean.eraseMacroScopesAux]`.
+-/
+/--
+info: Try this:
+  [apply] simp only [Lean.eraseMacroScopesAux]
+-/
+#guard_msgs in
+example : Lean.eraseMacroScopesAux .anonymous = .anonymous := by
+  simp? [Lean.eraseMacroScopesAux]
+
+/-!
+Fixing these issues involved rewriting how name unresolution handled macro scopes.
+Here's a test that hygienic names can be unresolved too.
+-/
+macro "mk_struct" n:ident : command => `(
+  structure S where
+  def $n : S := {})
+namespace NS
+mk_struct T
+/-- info: T : S✝ -/
+#guard_msgs in #check (T)
+end NS
+/-- info: NS.T : NS.S✝ -/
+#guard_msgs in #check (NS.T)

tests/lean/run/986.lean

@@ -5,16 +5,16 @@ attribute [simp] Array.insertionSort.swapLoop
 
 /--
 info: Array.insertionSort.swapLoop.eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (xs : Array α) (h : 0 < xs.size) :
-  Array.insertionSort.swapLoop✝ lt xs 0 h = xs
+  Array.insertionSort.swapLoop lt xs 0 h = xs
 -/
 #guard_msgs in
 #check Array.insertionSort.swapLoop.eq_1
 
 /--
 info: Array.insertionSort.swapLoop.eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (xs : Array α) (j' : Nat)
   (h : j'.succ < xs.size) :
-  Array.insertionSort.swapLoop✝ lt xs j'.succ h =
-    if lt xs[j'.succ] xs[j'] = true then Array.insertionSort.swapLoop✝¹ lt (xs.swap j'.succ j' h ⋯) j' ⋯ else xs
+  Array.insertionSort.swapLoop lt xs j'.succ h =
+    if lt xs[j'.succ] xs[j'] = true then Array.insertionSort.swapLoop lt (xs.swap j'.succ j' h ⋯) j' ⋯ else xs
 -/
 #guard_msgs in
 #check Array.insertionSort.swapLoop.eq_2

tests/lean/run/bv_enums.lean

@@ -21,17 +21,17 @@ inductive State where
   | so
   | sp
 
-/-- info: _root_.Ex1.State.enumToBitVec : State → BitVec 4 -/
+/-- info: Ex1.State.enumToBitVec✝ : State → BitVec 4 -/
 #guard_msgs in
 #check State.enumToBitVec
 
 /--
-info: _root_.Ex1.State.eq_iff_enumToBitVec_eq (x y : State) : x = y ↔ x.enumToBitVec = y.enumToBitVec
+info: Ex1.State.eq_iff_enumToBitVec_eq✝ (x y : State) : x = y ↔ x.enumToBitVec = y.enumToBitVec
 -/
 #guard_msgs in
 #check State.eq_iff_enumToBitVec_eq
 
-/-- info: _root_.Ex1.State.enumToBitVec_le (x : State) : x.enumToBitVec ≤ 15#4 -/
+/-- info: Ex1.State.enumToBitVec_le✝ (x : State) : x.enumToBitVec ≤ 15#4 -/
 #guard_msgs in
 #check State.enumToBitVec_le
 

tests/lean/run/do_for_loop_levenstein_compiler_test.lean

@@ -32,7 +32,7 @@ trace: [Compiler.saveMono] size: 13
         | Bool.false =>
           let _x.4 := 1;
           let _x.5 := USize.add i _x.4;
-          let _x.6 := Array.anyMUnsafe.any._at_.Array.contains._at_.deletions.spec_0.spec_0.2 a as _x.5 stop;
+          let _x.6 := _private.Init.Data.Array.Basic.0.Array.anyMUnsafe.any._at_.Array.contains._at_.deletions.spec_0.spec_0 a as _x.5 stop;
           return _x.6
         | Bool.true =>
           return _x.3
@@ -54,7 +54,7 @@ trace: [Compiler.saveMono] size: 13
         | Bool.true =>
           let _x.4 := 0;
           let _x.5 := USize.ofNat _x.2;
-          let _x.6 := Array.anyMUnsafe.any._at_.Array.contains._at_.deletions.spec_0.spec_0.2 a as _x.4 _x.5;
+          let _x.6 := _private.Init.Data.Array.Basic.0.Array.anyMUnsafe.any._at_.Array.contains._at_.deletions.spec_0.spec_0 a as _x.4 _x.5;
           return _x.6
 [Compiler.saveMono] size: 19
     def Array.forInNew'Unsafe.loop._at_.deletions.spec_2 as sz i s : Array String :=

tests/lean/run/emptyLcnf.lean

@@ -29,7 +29,7 @@ trace: [Compiler.saveMono] size: 5
       let _x.7 := Array.mkEmpty ◾ _x.6;
       let _x.8 := Array.push ◾ _x.7 _x.5;
       let _x.9 := PUnit.unit;
-      let _f.10 := _eval._lam_0.2 _x.8 _x.9;
+      let _f.10 := _eval._lam_0 _x.8 _x.9;
       let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
       return _x.11
 -/

tests/lean/run/erased.lean

@@ -49,8 +49,7 @@ trace: [Compiler.saveMono] size: 5
       let _f.11 : Lean.Elab.Term.Context →
         lcAny →
           Lean.Meta.Context →
-            lcAny →
-              Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._lam_0.2 _x.9 _x.10;
+            lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._lam_0 _x.9 _x.10;
       let _x.12 : EST.Out Lean.Exception lcAny PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 a.3;
       return _x.12
 -/

tests/lean/run/inlineApp.lean

@@ -31,7 +31,7 @@ trace: [Compiler.saveMono] size: 1
       let _x.6 := 1;
       let _x.7 := Array.mkEmpty ◾ _x.6;
       let _x.8 := Array.push ◾ _x.7 _x.5;
-      let _f.9 := _eval._lam_0.2 _x.8;
+      let _f.9 := _eval._lam_0 _x.8;
       let _x.10 := Lean.Elab.Command.liftTermElabM._redArg _f.9 a.1 a.2 a.3;
       return _x.10
 -/

tests/lean/run/wfUnfold.lean

@@ -42,7 +42,7 @@ j : Fin as.size
 ⊢ (if i < ↑j then
         let j' := ⟨↑j - 1, ⋯⟩;
         let as_1 := as.swap ↑j' ↑j ⋯ ⋯;
-        Array.insertIdx.loop✝ i as_1 ⟨↑j', ⋯⟩
+        insertIdx.loop i as_1 ⟨↑j', ⋯⟩
       else as).size =
     as.size
 -/

tests/pkg/module/Module/ImportedAll.lean

@@ -140,7 +140,7 @@ public def pub := priv
 /--
 error: Unknown identifier `priv`
 
-Note: A private declaration `priv✝` (from `Module.Basic`) exists but would need to be public to access here.
+Note: A private declaration `priv` (from `Module.Basic`) exists but would need to be public to access here.
 -/
 #guard_msgs in
 @[expose] public def pub' := priv