From d23e66f015e6889bfbb03d7cd4174b9fc8f65cdf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 18 Jul 2026 10:31:33 +0000 Subject: [PATCH] fix: restore ambient exporting scope in `mkAuxDefinition` This PR fixes a regression from #14437 where the auxiliary definitions wrapping `private` references in exposed bodies (`private_decl%`) had their bodies exported, producing dangling references to private constants that broke importing modules (caught by Mathlib CI). `mkAuxDefinition` again adds the declaration under the ambient exporting scope; the `exposeBody` parameter introduced by #14437 is removed. `wrapInstance` instead wraps its `mkAuxDefinition` calls in `withoutExporting (when := !exposeAux)`: the aux names are minted under the ambient exporting scope beforehand, so the aux defs keep their public names and exported signatures while their bodies stay unexported, as required by the `inferInstanceAs` wrapper fix. Co-Authored-By: Claude Fable 5 --- src/Lean/Meta/Closure.lean | 5 ++--- src/Lean/Meta/WrapInstance.lean | 8 ++++---- tests/elab/privateDeclExpose.lean | 22 ++++++++++++++++++++++ 3 files changed, 28 insertions(+), 7 deletions(-) create mode 100644 tests/elab/privateDeclExpose.lean diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index d79b11305a72..d5c6d4bf86de 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -432,14 +432,13 @@ end Closure returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on, and `t_j`s are free and meta variables `type` and `value` depend on. -/ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false) - (compile : Bool := true) (logCompileErrors : Bool := true) (exposeBody : Bool := true) : - MetaM Expr := do + (compile : Bool := true) (logCompileErrors : Bool := true) : MetaM Expr := do let result ← Closure.mkValueTypeClosure type value zetaDelta let env ← getEnv let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1) let decl := Declaration.defnDecl (← mkDefinitionValInferringUnsafe name result.levelParams.toList result.type result.value hints) - withExporting (isExporting := exposeBody) <| addDecl decl + addDecl decl if compile then compileDecl decl (logErrors := logCompileErrors) return mkAppN (mkConst name result.levelArgs.toList) result.exprArgs diff --git a/src/Lean/Meta/WrapInstance.lean b/src/Lean/Meta/WrapInstance.lean index cf7c8fcdc0d0..f0bc556a2d9c 100644 --- a/src/Lean/Meta/WrapInstance.lean +++ b/src/Lean/Meta/WrapInstance.lean @@ -183,8 +183,8 @@ where go (inst expectedType : Expr) (isEta : Bool) : MetaM (Option Expr) := do if backward.inferInstanceAs.wrap.instances.get (← getOptions) then let name ← mkAuxDeclName - let wrapped ← mkAuxDefinition name expectedType inst (compile := false) - (exposeBody := exposeAux) + let wrapped ← withoutExporting (when := !exposeAux) <| + mkAuxDefinition name expectedType inst (compile := false) setReducibilityStatus name <| if (← withImplicit <| isDefEq expectedType instType) then .implicitReducible @@ -279,8 +279,8 @@ where go (inst expectedType : Expr) (isEta : Bool) : MetaM (Option Expr) := do mvarId.assign arg else let name ← mkAuxDeclName - mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false) - (exposeBody := exposeAux)) + mvarId.assign (← withoutExporting (when := !exposeAux) <| + mkAuxDefinition name argExpectedType arg (compile := false)) setReducibilityStatus name <| if (← withImplicit <| isDefEq argExpectedType argType) then .implicitReducible diff --git a/tests/elab/privateDeclExpose.lean b/tests/elab/privateDeclExpose.lean new file mode 100644 index 000000000000..94ed5a19f298 --- /dev/null +++ b/tests/elab/privateDeclExpose.lean @@ -0,0 +1,22 @@ +module + +/-! Term `private` should create unexposed bodies regardless of context. -/ + +def privVal : Nat := 5 + +@[expose] public def pubVal : Nat := private_decl% privVal + +/-- +info: @[expose] def pubVal : Nat := +pubVal._private_1 +-/ +#guard_msgs in +#print pubVal + +-- The aux def must not be `@[expose]`: its body references the private `privVal`. +/-- +info: def pubVal._private_1 : Nat := +privVal +-/ +#guard_msgs in +#print pubVal._private_1