fix: allow exact? to suggest local private declarations (part 2) (#11759)

This PR contains changes that were meant to be part of #11736, but I
accidentally merged without pushing my final local changes.

src/Lean/Meta/LazyDiscrTree.lean

@@ -802,17 +802,27 @@ structure Cache where
 
 def Cache.empty (ngen : NameGenerator) : Cache := { ngen := ngen, core := {}, «meta» := {} }
 
-/-- Check if a private name belongs to the given module -/
-private def isPrivateNameOf (declName : Name) (mainModule : Name) : Bool :=
-  if let some pfx := privatePrefix? declName then
-    pfx == Name.mkNum (privateHeader ++ mainModule) 0
+/--
+Check if a private declaration is accessible from the current environment.
+- Local private declarations (defined in current module) are always accessible.
+- Imported private declarations are accessible only in the module system with `import all`.
+-/
+private def isAccessiblePrivateName (env : Environment) (declName : Name) : Bool :=
+  if !isPrivateName declName then
+    false -- Not private; the isInternalDetail check should still apply
   else
-    false
+    match env.getModuleIdxFor? declName with
+    | some modIdx =>
+      -- Imported private: accessible only in module system with `import all`
+      env.header.isModule && env.header.modules[modIdx]?.any (·.importAll)
+    | none =>
+      -- Local private: always accessible
+      true
 
 def blacklistInsertion (env : Environment) (declName : Name) : Bool :=
   !allowCompletion env declName
   || declName == ``sorryAx
-  || (declName.isInternalDetail && !isPrivateNameOf declName env.header.mainModule)
+  || (declName.isInternalDetail && !isAccessiblePrivateName env declName)
   || (declName matches .str _ "inj")
   || (declName matches .str _ "noConfusionType")
 

tests/lean/run/exact_private.lean

@@ -3,10 +3,17 @@ module
 /-!
 # Tests for `exact?` with private declarations
 
-This tests that `exact?` can suggest private theorems defined locally in the same module.
+This tests that `exact?` can suggest private theorems.
+
+## Accessibility rules for private declarations in `exact?`:
+- Local private declarations (defined in current file/module): always suggested
+- Imported private declarations:
+  - In module system with `import all`: suggested
+  - In module system without `import all`: not suggested
+  - Outside module system: not suggested
 -/
 
--- Test that exact? suggests private declarations
+-- Test that exact? suggests local private declarations
 axiom P : Prop
 private axiom p : P