fix: privacy checks and import all (#10550)

This PR ensures private declarations are accessible from the private
scope iff they are local or imported through an `import all` chain,
including for anonymous notation and structure instance notation.

Author: Kha

src/Lean/Environment.lean

@@ -182,6 +182,12 @@ structure EnvironmentHeader where
   `ModuleIdx` for the same module.
   -/
   modules      : Array EffectiveImport := #[]
+  /--
+  Subset of `modules` for which `importAll` is `true`. This is assumed to be a much smaller set so
+  we precompute it instead of iterating over all of `modules` multiple times. However, note that
+  in a non-`module` file, this is identical to `modules`.
+  -/
+  importAllModules : Array EffectiveImport := modules.filter (·.importAll)
   /-- Module data for all imported modules. -/
   moduleData   : Array ModuleData := #[]
   deriving Nonempty

src/Lean/Modifiers.lean

@@ -26,12 +26,19 @@ def mkPrivateName (env : Environment) (n : Name) : Name :=
   -- is private to *this* module.
   mkPrivateNameCore env.mainModule <| privateToUserName n
 
-def isInaccessiblePrivateName (env : Environment) (n : Name) : Bool :=
-  if env.header.isModule then
-    -- Allow access through `import all`.
-    env.isExporting && isPrivateName n
-  else match privateToUserName? n with
-    | some userName => mkPrivateName env userName != n
-    | _ => false
+def isInaccessiblePrivateName (env : Environment) (n : Name) : Bool := Id.run do
+  if !isPrivateName n then
+    return false
+  -- All private names are inaccessible from the public scope
+  if env.isExporting then
+    return true
+  -- In the private scope, ...
+  match env.getModuleIdxFor? n with
+  | some modIdx =>
+    -- ... allow access through `import all`
+    !env.header.isModule || !env.header.modules[modIdx]?.any (·.importAll)
+  | none =>
+    -- ... allow all accesses in the current module
+    false
 
 end Lean

src/Lean/ResolveName.lean

@@ -111,11 +111,9 @@ private partial def resolvePrivateName (env : Environment) (declName : Name) : O
   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.
+  -- them one 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
+  env.header.importAllModules.findSome? fun i => do
     let n := mkPrivateNameCore i.module declName
     guard <| containsDeclOrReserved env n
     return n

tests/lean/ctor_layout.lean

@@ -7,9 +7,6 @@ def test : CoreM Unit := do
    let ctorLayout ← getCtorLayout ``Lean.IR.Expr.reuse;
    ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
    IO.println "---";
-   let ctorLayout ← getCtorLayout ``Lean.EnvironmentHeader.mk;
-   ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
-   IO.println "---";
    let ctorLayout ← getCtorLayout ``Subtype.mk;
    ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
    pure ()

tests/lean/ctor_layout.lean.expected.out

@@ -3,13 +3,5 @@ obj@1:obj
 scalar#1@0:u8
 obj@2:obj
 ---
-scalar#4@0:u32
-obj@0:tobj
-scalar#1@4:u8
-obj@1:obj
-obj@2:obj
-obj@3:obj
-obj@4:obj
----
 obj@0:tobj
 ◾

tests/pkg/module/Module.lean

@@ -5,6 +5,7 @@ import Module.ImportedAll
 import Module.ImportedPrivateImported
 import Module.PrivateImported
 import Module.ImportedAllPrivateImported
+import Module.ImportedAllImportedAll
 import Module.NonModule
 import Module.MetaImported
 

tests/pkg/module/Module/Basic.lean

@@ -312,6 +312,15 @@ constructor:
 #with_exporting
 #check { x := 1 : StructWithPrivateField }
 
+#check (⟨1⟩ : StructWithPrivateField)
+
+/--
+error: Invalid `⟨...⟩` notation: Constructor for `StructWithPrivateField` is marked as private
+-/
+#guard_msgs in
+#with_exporting
+#check (⟨1⟩ : StructWithPrivateField)
+
 #check StructWithPrivateField.x
 
 /-- error: Unknown constant `StructWithPrivateField.x` -/

tests/pkg/module/Module/ImportedAll.lean

@@ -144,3 +144,19 @@ Note: A private declaration `priv✝` (from `Module.Basic`) exists but would nee
 -/
 #guard_msgs in
 @[expose] public def pub' := priv
+
+#check { x := 1 : StructWithPrivateField }
+
+/-- error: invalid {...} notation, constructor for `StructWithPrivateField` is marked as private -/
+#guard_msgs in
+#with_exporting
+#check { x := 1 : StructWithPrivateField }
+
+#check (⟨1⟩ : StructWithPrivateField)
+
+/--
+error: Invalid `⟨...⟩` notation: Constructor for `StructWithPrivateField` is marked as private
+-/
+#guard_msgs in
+#with_exporting
+#check (⟨1⟩ : StructWithPrivateField)

tests/pkg/module/Module/ImportedAllImportedAll.lean

@@ -0,0 +1,12 @@
+module
+
+prelude
+import all Module.ImportedAll
+
+/-! `import all` should chain with nested `import all`s. -/
+
+#check priv
+
+#check { x := 1 : StructWithPrivateField }
+
+#check (⟨1⟩ : StructWithPrivateField)