From 49cff79712af7d9ecdda2bc7a786ca0ae00cf5c6 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 26 Sep 2025 15:26:10 +0200 Subject: [PATCH] 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. --- src/Lean/Environment.lean | 6 ++++++ src/Lean/Modifiers.lean | 21 ++++++++++++------- src/Lean/ResolveName.lean | 6 ++---- tests/lean/ctor_layout.lean | 3 --- tests/lean/ctor_layout.lean.expected.out | 8 ------- tests/pkg/module/Module.lean | 1 + tests/pkg/module/Module/Basic.lean | 9 ++++++++ tests/pkg/module/Module/ImportedAll.lean | 16 ++++++++++++++ .../module/Module/ImportedAllImportedAll.lean | 12 +++++++++++ 9 files changed, 60 insertions(+), 22 deletions(-) create mode 100644 tests/pkg/module/Module/ImportedAllImportedAll.lean diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index a7f5c15e73..0138a2e7db 100644 --- a/src/Lean/Environment.lean +++ b/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 diff --git a/src/Lean/Modifiers.lean b/src/Lean/Modifiers.lean index 02ec85190b..7980d83efe 100644 --- a/src/Lean/Modifiers.lean +++ b/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 diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index dd87103f53..6c3f7d15c1 100644 --- a/src/Lean/ResolveName.lean +++ b/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 diff --git a/tests/lean/ctor_layout.lean b/tests/lean/ctor_layout.lean index 12ea8d71a8..192aff7b91 100644 --- a/tests/lean/ctor_layout.lean +++ b/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 () diff --git a/tests/lean/ctor_layout.lean.expected.out b/tests/lean/ctor_layout.lean.expected.out index 373447dd9e..8a9ee7dd6c 100644 --- a/tests/lean/ctor_layout.lean.expected.out +++ b/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 ◾ diff --git a/tests/pkg/module/Module.lean b/tests/pkg/module/Module.lean index f907f80fce..04bca43cf7 100644 --- a/tests/pkg/module/Module.lean +++ b/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 diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 34355c3b1c..015074340d 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/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` -/ diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean index a2b1b22e25..0972a63b62 100644 --- a/tests/pkg/module/Module/ImportedAll.lean +++ b/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) diff --git a/tests/pkg/module/Module/ImportedAllImportedAll.lean b/tests/pkg/module/Module/ImportedAllImportedAll.lean new file mode 100644 index 0000000000..f9bfe47786 --- /dev/null +++ b/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)