chore: improve error message on trying to access an identifier imported privately from the public scope (#10153)

src/Lean/Exception.lean

@@ -125,10 +125,15 @@ def mkUnknownIdentifierMessage [Monad m] [MonadEnv m] [MonadError m] (msg : Mess
   if !declHint.isAnonymous && env.isExporting && (env.setExporting false).contains declHint then
     let c := .withContext {
       env := env.setExporting false, opts := {}, mctx := {}, lctx := {} } <| .ofConstName declHint
-    let mod := match env.getModuleIdxFor? declHint with
-      | none     => "this module"
-      | some idx => m!"`{env.header.moduleNames[idx]!}`"
-    msg := msg ++ .note m!"A private declaration `{c}` (from {mod}) exists but is not accessible in the current context."
+    msg := match env.getModuleIdxFor? declHint with
+      | none     =>
+        msg ++ .note m!"A private declaration `{c}` (from the current module) exists but would need to be public to access here."
+      | some idx =>
+        let mod := env.header.moduleNames[idx]!
+        if isPrivateName declHint then
+          msg ++ .note m!"A private declaration `{c}` (from `{mod}`) exists but would need to be public to access here."
+        else
+          msg ++ .note m!"A public declaration `{c}` exists but is imported privately; consider adding `public import {mod}`."
   return MessageData.tagged unknownIdentifierMessageTag msg
 
 /--

tests/lean/bootstrapSorry.lean.expected.out

@@ -1,3 +1,3 @@
 bootstrapSorry.lean:8:21-8:24: error(lean.unknownIdentifier): Unknown identifier `Nat`
 
-Note: A private declaration `Nat` (from `Init.Prelude`) exists but is not accessible in the current context.
+Note: A public declaration `Nat` exists but is imported privately; consider adding `public import Init.Prelude`.

tests/pkg/module/Module/Basic.lean

@@ -44,7 +44,7 @@ def fpriv := 1
 /--
 error: Unknown identifier `fpriv`
 
-Note: A private declaration `fpriv` (from this module) exists but is not accessible in the current context.
+Note: A private declaration `fpriv` (from the current module) exists but would need to be public to access here.
 -/
 #guard_msgs in
 public theorem tpriv : fpriv = 1 := rfl
@@ -144,7 +144,7 @@ def priv := 2
 /--
 error: Unknown identifier `priv`
 
-Note: A private declaration `priv` (from this module) exists but is not accessible in the current context.
+Note: A private declaration `priv` (from the current module) exists but would need to be public to access here.
 -/
 #guard_msgs in
 public abbrev h := priv

tests/pkg/module/Module/ImportedAll.lean

@@ -137,7 +137,7 @@ public def pub := priv
 /--
 error: Unknown identifier `priv`
 
-Note: A private declaration `priv✝` (from `Module.Basic`) exists but is not accessible in the current context.
+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

tests/pkg/module/Module/PrivateImported.lean

@@ -9,7 +9,7 @@ public def g := f
 /--
 error: Unknown identifier `f`
 
-Note: A private declaration `f` (from `Module.Basic`) exists but is not accessible in the current context.
+Note: A public declaration `f` exists but is imported privately; consider adding `public import Module.Basic`.
 -/
 #guard_msgs in
 public theorem t2 : f = 1 := sorry
@@ -17,7 +17,7 @@ public theorem t2 : f = 1 := sorry
 /--
 error: Unknown identifier `f`
 
-Note: A private declaration `f` (from `Module.Basic`) exists but is not accessible in the current context.
+Note: A public declaration `f` exists but is imported privately; consider adding `public import Module.Basic`.
 -/
 #guard_msgs in
 @[expose] public def h : True := f