From 655a39ceb8c7123dc14a064e0d4e4ae292a3b436 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 27 Aug 2025 15:43:56 +0200
Subject: [PATCH] chore: improve error message on trying to access an
 identifier imported privately from the public scope (#10153)

---
 src/Lean/Exception.lean                      | 13 +++++++++----
 tests/lean/bootstrapSorry.lean.expected.out  |  2 +-
 tests/pkg/module/Module/Basic.lean           |  4 ++--
 tests/pkg/module/Module/ImportedAll.lean     |  2 +-
 tests/pkg/module/Module/PrivateImported.lean |  4 ++--
 5 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index 682bb35dc5..2695f614d4 100644
--- a/src/Lean/Exception.lean
+++ b/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
 
 /--
diff --git a/tests/lean/bootstrapSorry.lean.expected.out b/tests/lean/bootstrapSorry.lean.expected.out
index d725b815cb..66f7f39dac 100644
--- a/tests/lean/bootstrapSorry.lean.expected.out
+++ b/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`.
diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean
index fd92f2a22b..b184e01761 100644
--- a/tests/pkg/module/Module/Basic.lean
+++ b/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
diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean
index ce2d845d65..f2ef22a419 100644
--- a/tests/pkg/module/Module/ImportedAll.lean
+++ b/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
diff --git a/tests/pkg/module/Module/PrivateImported.lean b/tests/pkg/module/Module/PrivateImported.lean
index 38beb160f1..a82ad0eb56 100644
--- a/tests/pkg/module/Module/PrivateImported.lean
+++ b/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