feat: allow access to private names through import all (#8828)

This PR extends the experimental module system to support resolving
private names imported (transitively) through `import all`.

src/Lean/Modifiers.lean

@@ -20,7 +20,7 @@ def isProtected (env : Environment) (n : Name) : Bool :=
 def mkPrivateName (env : Environment) (n : Name) : Name :=
   -- If name is already private, remove previous suffix first. We need to ensure the resulting name
   -- is private to *this* module.
-  Name.mkNum (privateHeader ++ env.mainModule) 0 ++ privateToUserName n
+  mkPrivateNameCore env.mainModule <| privateToUserName n
 
 def isPrivateNameFromImportedModule (env : Environment) (n : Name) : Bool :=
   match privateToUserName? n with

src/Lean/ResolveName.lean

@@ -99,6 +99,19 @@ private def containsDeclOrReserved (env : Environment) (declName : Name) : Bool
   -- avoid blocking from `Environment.contains` if possible
   env.containsOnBranch declName || isReservedName env declName || env.contains declName
 
+private partial def resolvePrivateName (env : Environment) (declName : Name) : Option Name := do
+  if containsDeclOrReserved env (mkPrivateName env declName) then
+    return mkPrivateName env declName
+  -- Under the module system, we assume there are at most a few `import all`s and we can just test
+  -- them on by one.
+  guard <| env.header.isModule
+  -- As `all` is not transitive, we only have to check the direct imports.
+  env.header.imports.findSome? fun i => do
+    guard i.importAll
+    let n := mkPrivateNameCore i.module declName
+    guard <| containsDeclOrReserved env n
+    return n
+
 /-- Check whether `ns ++ id` is a valid namespace name and/or there are aliases names `ns ++ id`. -/
 private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : List Name :=
   let resolvedId    := ns ++ id
@@ -107,9 +120,7 @@ private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : L
   if (containsDeclOrReserved env resolvedId && (!id.isAtomic || !isProtected env resolvedId)) then
     resolvedId :: resolvedIds
   else
-    -- Check whether environment contains the private version. That is, `_private.<module_name>.ns.id`.
-    let resolvedIdPrv := mkPrivateName env resolvedId
-    if containsDeclOrReserved env resolvedIdPrv then resolvedIdPrv :: resolvedIds
+    if let some resolvedIdPrv := resolvePrivateName env resolvedId then resolvedIdPrv :: resolvedIds
     else resolvedIds
 
 /-- Check surrounding namespaces -/
@@ -129,9 +140,7 @@ private def resolveExact (env : Environment) (id : Name) : Option Name :=
     else
       -- We also allow `_root_` when accessing private declarations.
       -- If we change our minds, we should just replace `resolvedId` with `id`
-      let resolvedIdPrv := mkPrivateName env resolvedId
-      if containsDeclOrReserved env resolvedIdPrv then some resolvedIdPrv
-      else none
+      resolvePrivateName env resolvedId
 
 /-- Check `OpenDecl`s -/
 private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl → List Name → List Name
@@ -178,8 +187,7 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
         | some newId => [(newId, projs)]
         | none =>
           let resolvedIds := if containsDeclOrReserved env id then [id] else []
-          let idPrv       := mkPrivateName env id
-          let resolvedIds := if containsDeclOrReserved env idPrv then [idPrv] ++ resolvedIds else resolvedIds
+          let resolvedIds := if let some idPrv := resolvePrivateName env id then [idPrv] ++ resolvedIds else resolvedIds
           let resolvedIds := resolveOpenDecls env id openDecls resolvedIds
           let resolvedIds := getAliases env id (skipProtected := id.isAtomic) ++ resolvedIds
           match resolvedIds with

tests/pkg/module/Module/ImportedAll.lean

@@ -35,19 +35,7 @@ example : P f := by dsimp only [trfl]; exact hP1
 #guard_msgs in
 example : P f := by dsimp only [trfl']; exact hP1
 
-/--
-error: unknown identifier 'trflprivate'
----
-error: dsimp made no progress
--/
-#guard_msgs in
 example : P f := by dsimp only [trflprivate]; exact hP1
-/--
-error: unknown identifier 'trflprivate''
----
-error: dsimp made no progress
--/
-#guard_msgs in
 example : P f := by dsimp only [trflprivate']; exact hP1
 
 
@@ -136,3 +124,11 @@ info: theorem f_exp_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat
       ∀ (a a_1 : Nat), motive a a_1 (f_exp_wfrec a a_1)
 -/
 #guard_msgs(pass trace, all) in #print sig f_exp_wfrec.induct_unfolding
+
+/-! `import all` should allow access to private defs, privately. -/
+
+def pub := priv
+
+/-- error: unknown identifier 'priv' -/
+#guard_msgs in
+@[expose] def pub' := priv