chore: update stage0

src/Lean/Elab/BuiltinTerm.lean

@@ -374,7 +374,7 @@ private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
     if (← getEnv).isExporting then
       let name ← mkAuxDeclName `_private
       withoutExporting do
-        let e ← elabTerm e expectedType?
+        let e ← elabTermAndSynthesize e expectedType?
         -- Inline as changing visibility should not affect run time.
         -- Eventually we would like to be more conscious about inlining of instance fields,
         -- irrespective of `private` use.

src/Lean/Elab/Deriving/FromToJson.lean

@@ -166,9 +166,9 @@ def mkToJsonAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
   if ctx.usePartial then
     let letDecls ← mkLocalInstanceLetDecls ctx ``ToJson header.argNames
     body ← mkLet letDecls body
-    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Json := $body:term)
+    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Json := $body:term)
   else
-    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Json := $body:term)
+    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Json := $body:term)
 
 def mkFromJsonBody (ctx : Context) (e : Expr) : TermElabM Term := do
   let indName := e.getAppFn.constName!
@@ -188,9 +188,9 @@ def mkFromJsonAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
   if ctx.usePartial || indval.isRec then
     let letDecls ← mkLocalInstanceLetDecls ctx ``FromJson header.argNames
     body ← mkLet letDecls body
-    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Except String $(← mkInductiveApp ctx.typeInfos[i]! header.argNames) := $body:term)
+    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Except String $(← mkInductiveApp ctx.typeInfos[i]! header.argNames) := $body:term)
   else
-    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Except String $(← mkInductiveApp ctx.typeInfos[i]! header.argNames) := $body:term)
+    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Except String $(← mkInductiveApp ctx.typeInfos[i]! header.argNames) := $body:term)
 
 
 def mkToJsonMutualBlock (ctx : Context) : TermElabM Command := do

src/Lean/Elab/Deriving/Repr.lean

@@ -97,9 +97,9 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
     body ← mkLet letDecls body
   let binders    := header.binders
   if ctx.usePartial then
-    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
+    `(@[no_expose] partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
   else
-    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
+    `(@[no_expose] def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Format := $body:term)
 
 def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]

src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean

@@ -151,7 +151,7 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
 
     -- Adjust the body of each function to take the other functions as a
     -- (packed) parameter
-    let Fs ← preDefs.mapIdxM fun funIdx preDef => do
+    let Fs ← withoutExporting do preDefs.mapIdxM fun funIdx preDef => do
       let body ← fixedParamPerms.perms[funIdx]!.instantiateLambda preDef.value fixedArgs
       withLocalDeclD (← mkFreshUserName `f) packedType fun f => do
         let body' ← withoutModifyingEnv do
@@ -163,7 +163,7 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
     -- Construct and solve monotonicity goals for each function separately
     -- This way we preserve the user's parameter names as much as possible
     -- and can (later) use the user-specified per-function tactic
-    let hmonos ← preDefs.mapIdxM fun i preDef => do
+    let hmonos ← withoutExporting do preDefs.mapIdxM fun i preDef => do
       let type := types[i]!
       let F := Fs[i]!
       let inst ← toPartialOrder insts'[i]! type

src/Lean/Elab/Structure.lean

@@ -200,12 +200,15 @@ The structure constructor syntax is
 leading_parser try (declModifiers >> ident >> " :: ")
 ```
 -/
-private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : TermElabM CtorView := do
+private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name)
+    (forcePrivate : Bool) : TermElabM CtorView := do
   let useDefault := do
+    let visibility := if forcePrivate then .private else .regular
     let declName := structDeclName ++ defaultCtorName
+    let declName ← applyVisibility visibility declName
     let ref := structStx[1].mkSynthetic
     addDeclarationRangesFromSyntax declName ref
-    pure { ref, declId := ref, modifiers := default, declName }
+    pure { ref, declId := ref, modifiers := { (default : Modifiers) with visibility }, declName }
   if structStx[4].isNone then
     useDefault
   else
@@ -215,12 +218,14 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
     else
       let ctor := optCtor[0]
       withRef ctor do
-      let ctorModifiers ← elabModifiers ctor[0]
+      let mut ctorModifiers ← elabModifiers ctor[0]
       checkValidCtorModifier ctorModifiers
       if ctorModifiers.isPrivate && structModifiers.isPrivate then
         throwError "invalid 'private' constructor in a 'private' structure"
       if ctorModifiers.isProtected && structModifiers.isPrivate then
         throwError "invalid 'protected' constructor in a 'private' structure"
+      if !ctorModifiers.isPrivate && forcePrivate then
+        throwError "invalid constructor visibility, must be private in presence of private fields"
       let name := ctor[1].getId
       let declName := structDeclName ++ name
       let declName ← applyVisibility ctorModifiers.visibility declName
@@ -377,8 +382,10 @@ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM Str
       pure type?
   let parents ← expandParents exts
   let derivingClasses ← getOptDerivingClasses stx[5]
-  let ctor ← expandCtor stx modifiers declName
   let fields ← expandFields stx modifiers declName
+  -- Private fields imply a private constructor; in the module system only for back-compat
+  let ctor ← expandCtor (forcePrivate := (← getEnv).header.isModule && fields.any (·.modifiers.isPrivate))
+    stx modifiers declName
   fields.forM fun field => do
     if field.declName == ctor.declName then
       throwErrorAt field.ref "invalid field name '{field.name}', it is equal to structure constructor name"
@@ -939,14 +946,15 @@ private def elabFieldTypeValue (structParams : Array Expr) (view : StructFieldVi
       match view.default? with
       | none => return (none, paramInfoOverrides, none)
       | some (.optParam valStx) =>
-        Term.synthesizeSyntheticMVarsNoPostponing
-        let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true))
-        let value ← Term.withoutAutoBoundImplicit <| Term.elabTerm valStx none
-        let value ← runStructElabM (init := state) <| solveParentMVars value
-        registerFailedToInferFieldType view.name (← inferType value) view.nameId
-        registerFailedToInferDefaultValue view.name value valStx
-        let value ← mkLambdaFVars params value
-        return (none, paramInfoOverrides, StructFieldDefault.optParam value)
+        withoutExporting (when := view.modifiers.isPrivate) do
+          Term.synthesizeSyntheticMVarsNoPostponing
+          let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true))
+          let value ← Term.withoutAutoBoundImplicit <| Term.elabTerm valStx none
+          let value ← runStructElabM (init := state) <| solveParentMVars value
+          registerFailedToInferFieldType view.name (← inferType value) view.nameId
+          registerFailedToInferDefaultValue view.name value valStx
+          let value ← mkLambdaFVars params value
+          return (none, paramInfoOverrides, StructFieldDefault.optParam value)
       | some (.autoParam tacticStx) =>
         throwErrorAt tacticStx "invalid field declaration, type must be provided when auto-param tactic is used"
     | some typeStx =>
@@ -960,13 +968,14 @@ private def elabFieldTypeValue (structParams : Array Expr) (view : StructFieldVi
         let type ← mkForallFVars params type
         return (type, paramInfoOverrides, none)
       | some (.optParam valStx) =>
-        let value ← Term.withoutAutoBoundImplicit <| Term.elabTermEnsuringType valStx type
-        let value ← runStructElabM (init := state) <| solveParentMVars value
-        registerFailedToInferDefaultValue view.name value valStx
-        Term.synthesizeSyntheticMVarsNoPostponing
-        let type  ← mkForallFVars params type
-        let value ← mkLambdaFVars params value
-        return (type, paramInfoOverrides, StructFieldDefault.optParam value)
+        withoutExporting (when := view.modifiers.isPrivate) do
+          let value ← Term.withoutAutoBoundImplicit <| Term.elabTermEnsuringType valStx type
+          let value ← runStructElabM (init := state) <| solveParentMVars value
+          registerFailedToInferDefaultValue view.name value valStx
+          Term.synthesizeSyntheticMVarsNoPostponing
+          let type  ← mkForallFVars params type
+          let value ← mkLambdaFVars params value
+          return (type, paramInfoOverrides, StructFieldDefault.optParam value)
       | some (.autoParam tacticStx) =>
         let name := mkAutoParamFnOfProjFn view.declName
         discard <| Term.declareTacticSyntax tacticStx name
@@ -1288,7 +1297,8 @@ private def addDefaults (levelParams : List Name) (params : Array Expr) (replace
           (← mkDefinitionValInferrringUnsafe declName levelParams type value ReducibilityHints.abbrev)
     for fieldInfo in fieldInfos do
       if let some (.optParam value) := fieldInfo.default? then
-        addDefault (mkDefaultFnOfProjFn fieldInfo.declName) value
+        withoutExporting (when := isPrivateName fieldInfo.declName) do
+          addDefault (mkDefaultFnOfProjFn fieldInfo.declName) value
       else if let some (.optParam value) := fieldInfo.resolvedDefault? then
         addDefault (mkInheritedDefaultFnOfProjFn fieldInfo.declName) value
 

src/Lean/Environment.lean

@@ -2532,9 +2532,13 @@ def withExporting [Monad m] [MonadEnv m] [MonadFinally m] [MonadOptions m] (x :
   finally
     modifyEnv (·.setExporting old)
 
-/-- Sets `Environment.isExporting` to false while executing `x`. -/
-def withoutExporting [Monad m] [MonadEnv m] [MonadFinally m] [MonadOptions m] (x : m α) : m α :=
-  withExporting (isExporting := false) x
+/-- If `when` is true, sets `Environment.isExporting` to false while executing `x`. -/
+def withoutExporting [Monad m] [MonadEnv m] [MonadFinally m] [MonadOptions m] (x : m α)
+    (when : Bool := true) : m α :=
+  if when then
+    withExporting (isExporting := false) x
+  else
+    x
 
 /-- Constructs a DefinitionVal, inferring the `unsafe` field -/
 def mkDefinitionValInferrringUnsafe [Monad m] [MonadEnv m] (name : Name) (levelParams : List Name)

src/Lean/Meta/SizeOf.lean

@@ -481,10 +481,10 @@ register_builtin_option genSizeOfSpec : Bool := {
 }
 
 def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
-  withExporting (isExporting := !isPrivateName typeName) do
+  let indInfo ← withoutExporting <| getConstInfoInduct typeName
+  withExporting (isExporting := !isPrivateName typeName && !indInfo.ctors.any isPrivateName) do
   if (← getEnv).contains ``SizeOf && genSizeOf.get (← getOptions) && !(← isInductivePredicate typeName) then
     withTraceNode `Meta.sizeOf (fun _ => return m!"{typeName}") do
-      let indInfo ← getConstInfoInduct typeName
       unless indInfo.isUnsafe do
         let (fns, recMap) ← mkSizeOfFns typeName
         for indTypeName in indInfo.all, fn in fns do

src/Lean/Meta/Tactic/AuxLemma.lean

@@ -10,8 +10,15 @@ import Lean.DefEqAttrib
 
 namespace Lean.Meta
 
+structure AuxLemmaKey where
+  type : Expr
+  -- When an aux lemma is created in a private context and thus has a private name, we must not
+  -- reuse it in an exported context.
+  isPrivate : Bool
+deriving BEq, Hashable
+
 structure AuxLemmas where
-  lemmas : PHashMap Expr (Name × List Name) := {}
+  lemmas : PHashMap AuxLemmaKey (Name × List Name) := {}
   deriving Inhabited
 
 builtin_initialize auxLemmasExt : EnvExtension AuxLemmas ←
@@ -32,6 +39,7 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : O
     (cache := true) (inferRfl := false) : MetaM Name := do
   let env ← getEnv
   let s := auxLemmasExt.getState env
+  let key := { type, isPrivate := !env.isExporting }
   let mkNewAuxLemma := do
     let auxName ← mkAuxDeclName (kind := kind?.getD `_proof)
     let decl :=
@@ -51,12 +59,17 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : O
     addDecl decl
     if inferRfl then
       inferDefEqAttr auxName
-    modifyEnv fun env => auxLemmasExt.modifyState env fun ⟨lemmas⟩ => ⟨lemmas.insert type (auxName, levelParams)⟩
+    modifyEnv fun env => auxLemmasExt.modifyState env fun ⟨lemmas⟩ => ⟨lemmas.insert key (auxName, levelParams)⟩
     return auxName
   if cache then
-    if let some (name, levelParams') := s.lemmas.find? type then
+    if let some (name, levelParams') := s.lemmas.find? key then
       if levelParams == levelParams' then
         return name
+    -- private contexts may reuse public matchers
+    if key.isPrivate then
+      if let some (name, levelParams') := s.lemmas.find? { key with isPrivate := false } then
+        if levelParams == levelParams' then
+          return name
   mkNewAuxLemma
 
 end Lean.Meta

src/Lean/Meta/Transform.lean

@@ -187,6 +187,9 @@ def zetaDeltaFVars (e : Expr) (fvars : Array FVarId) : MetaM Expr :=
 def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do
   withoutModifyingEnv do
     let env ← getEnv
+    -- There might have been nested proof abstractions, which yield private helper theoresms, so
+    -- make sure we can find them. They will later be re-abstracted again.
+    let biggerEnv := biggerEnv.setExporting false
     setEnv biggerEnv -- `e` has declarations from `biggerEnv` that are not in `env`
     let pre (e : Expr) : CoreM TransformStep := do
       let .const declName us := e | return .continue