chore: more module system fixes and refinements for finishing batteries port (#10819)

src/Lean/AddDecl.lean

@@ -96,13 +96,17 @@ def warnIfUsesSorry (decl : Declaration) : CoreM Unit := do
         -- This case should not happen, but it ensures a warning will get logged no matter what.
         logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
 
+builtin_initialize
+  registerTraceClass `addDecl
+
 /--
 Adds the given declaration to the environment's private scope, deriving a suitable presentation in
 the public scope if under the module system and if the declaration is not private. If `forceExpose`
 is true, exposes the declaration body, i.e. preserves the full representation in the public scope,
 independently of `Environment.isExporting` and even for theorems.
 -/
-def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit := do
+def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit :=
+  withTraceNode `addDecl (fun _ => return m!"adding declarations {decl.getNames}") do
   -- register namespaces for newly added constants; this used to be done by the kernel itself
   -- but that is incompatible with moving it to a separate task
   -- NOTE: we do not use `getTopLevelNames` here so that inductive types are registered as
@@ -115,26 +119,37 @@ def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit := do
   let (name, info, kind) ← match decl with
     | .thmDecl thm =>
       if !forceExpose && (← getEnv).header.isModule then
+        trace[addDecl] "exporting theorem {thm.name} as axiom"
         exportedInfo? := some <| .axiomInfo { thm with isUnsafe := false }
       pure (thm.name, .thmInfo thm, .thm)
     | .defnDecl defn | .mutualDefnDecl [defn] =>
       if !forceExpose && (← getEnv).header.isModule && !(← getEnv).isExporting then
+        trace[addDecl] "exporting definition {defn.name} as axiom"
         exportedInfo? := some <| .axiomInfo { defn with isUnsafe := defn.safety == .unsafe }
       pure (defn.name, .defnInfo defn, .defn)
     | .opaqueDecl op =>
       if !forceExpose && (← getEnv).header.isModule && !(← getEnv).isExporting then
+        trace[addDecl] "exporting opaque {op.name} as axiom"
         exportedInfo? := some <| .axiomInfo { op with }
       pure (op.name, .opaqueInfo op, .opaque)
     | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
-    | _ => return (← doAdd)
+    | _ =>
+      trace[addDecl] "no matching async adding rules, adding synchronously"
+      return (← doAdd)
 
-  if decl.getTopLevelNames.all isPrivateName && !(← ResolveName.backward.privateInPublic.getM) then
-    exportedInfo? := none
+  if decl.getTopLevelNames.all isPrivateName then
+    if (← ResolveName.backward.privateInPublic.getM) then
+      trace[addDecl] "private decl under `privateInPublic`, exporting as is"
+      exportedInfo? := some info
+    else
+      trace[addDecl] "not exporting private declaration at all"
+      exportedInfo? := none
   else
     -- preserve original constant kind in extension if different from exported one
     if exportedInfo?.isSome then
       modifyEnv (privateConstKindsExt.insert · name kind)
     else
+      trace[addDecl] "no matching exporting rules, exporting as is"
       exportedInfo? := some info
 
   -- no environment extension changes to report after kernel checking; ensures we do not

src/Lean/Attributes.lean

@@ -148,11 +148,14 @@ def throwAttrDeclNotOfExpectedType (attrName declName : Name) (givenType expecte
   throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` has type{indentExpr givenType}\n\
     but `[{attrName}]` can only be added to declarations of type{indentExpr expectedType}"
 
-def ensureAttrDeclIsPublic [MonadEnv m] (attrName declName : Name) (attrKind : AttributeKind) : m Unit := do
-  if (← getEnv).header.isModule && attrKind != .local && !((← getEnv).setExporting true).contains declName then
-    throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` must be public"
+def ensureAttrDeclIsPublic (attrName declName : Name) (attrKind : AttributeKind) : AttrM Unit := do
+  if (← getEnv).header.isModule && attrKind != .local then
+    withExporting do
+      checkPrivateInPublic declName
+      if !(← hasConst declName) then
+        throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` must be public"
 
-def ensureAttrDeclIsMeta [MonadEnv m] (attrName declName : Name) (attrKind : AttributeKind) : m Unit := do
+def ensureAttrDeclIsMeta (attrName declName : Name) (attrKind : AttributeKind) : AttrM Unit := do
   if (← getEnv).header.isModule && !isMeta (← getEnv) declName then
     throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` must be marked as `meta`"
   -- Make sure attributed decls can't refer to private meta imports, which is already checked for

src/Lean/Compiler/LCNF/Types.lean

@@ -195,6 +195,10 @@ where
   visitApp (f : Expr) (args : Array Expr) := do
     let fNew ← match f with
       | .const declName us =>
+        if (← getEnv).isExporting && isPrivateName declName then
+          -- This branch can happen under `backward.privateInPublic`; restore original behavior of
+          -- failing here, which is caught and ignored above by `observing`.
+          throwError "internal compiler error: private in public"
         let .inductInfo _ ← getConstInfo declName | return anyExpr
         pure <| .const declName us
       | .fvar .. => pure f

src/Lean/Elab/App.lean

@@ -1617,7 +1617,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
     | LValResolution.projFn baseStructName structName fieldName =>
       let f ← mkBaseProjections baseStructName structName f
       let some info := getFieldInfo? (← getEnv) baseStructName fieldName | unreachable!
-      if isInaccessiblePrivateName (← getEnv) info.projFn then
+      if (← isInaccessiblePrivateName info.projFn) then
         throwError "Field `{fieldName}` from structure `{structName}` is private"
       let projFn ← mkConst info.projFn
       let projFn ← addProjTermInfo lval.getRef projFn
@@ -1751,7 +1751,7 @@ where
       match resultTypeFn with
       | .const declName .. =>
         let env ← getEnv
-        if isInaccessiblePrivateName env declName then
+        if (← isInaccessiblePrivateName declName) then
           throwError "The private declaration `{.ofConstName declName}` is not accessible in the current context"
         -- Recall that the namespace for private declarations is non-private.
         let fullName := privateToUserName declName ++ id

src/Lean/Elab/BuiltinNotation.lean

@@ -56,7 +56,7 @@ open Meta
         (fun ival _ => do
           match ival.ctors with
           | [ctor] =>
-            if isInaccessiblePrivateName (← getEnv) ctor then
+            if (← isInaccessiblePrivateName ctor) then
               throwError "Invalid `⟨...⟩` notation: Constructor for `{ival.name}` is marked as private"
             let cinfo ← getConstInfoCtor ctor
             let numExplicitFields ← forallTelescopeReducing cinfo.type fun xs _ => do

src/Lean/Elab/BuiltinTerm.lean

@@ -164,7 +164,7 @@ private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do
     -- `by` switches from an exported to a private context, so we must disallow unassigned
     -- metavariables in the goal in this case as they could otherwise leak private data back into
     -- the exported context.
-    mkTacticMVar expectedType stx .term (delayOnMVars := (← getEnv).isExporting)
+    mkTacticMVar expectedType stx .term (delayOnMVars := (← getEnv).isExporting && !(← backward.proofsInPublic.getM))
   | none =>
     tryPostpone
     throwError ("invalid 'by' tactic, expected type has not been provided")

src/Lean/Elab/MutualDef.lean

@@ -1222,7 +1222,9 @@ where
     assert! view.kind.isTheorem
     let env ← getEnv
     let async ← env.addConstAsync declId.declName .thm
-      (exportedKind? := guard (!isPrivateName declId.declName) *> some .axiom)
+      (exportedKind? :=
+        guard (!isPrivateName declId.declName || (← ResolveName.backward.privateInPublic.getM)) *>
+        some .axiom)
     setEnv async.mainEnv
 
     -- TODO: parallelize header elaboration as well? Would have to refactor auto implicits catch,

src/Lean/Elab/PreDefinition/Basic.lean

@@ -135,7 +135,10 @@ private def shouldGenCodeFor (preDef : PreDefinition) : Bool :=
   !preDef.kind.isTheorem && !preDef.modifiers.isNoncomputable
 
 private def compileDecl (decl : Declaration) : TermElabM Unit := do
-  Lean.compileDecl (logErrors := !(← read).isNoncomputableSection) decl
+  Lean.compileDecl
+    -- `meta` should disregard `noncomputable section`
+    (logErrors := !(← read).isNoncomputableSection || decl.getTopLevelNames.any (isMeta (← getEnv)))
+    decl
 
 register_builtin_option diagnostics.threshold.proofSize : Nat := {
   defValue := 16384

src/Lean/Elab/StructInst.lean

@@ -1190,7 +1190,7 @@ private def elabStructInstView (s : StructInstView) (structName : Name) (structT
     TermElabM Expr := withRef s.ref do
   let env ← getEnv
   let ctorVal := getStructureCtor env structName
-  if isInaccessiblePrivateName env ctorVal.name then
+  if (← isInaccessiblePrivateName ctorVal.name) then
     throwError "invalid \{...} notation, constructor for `{.ofConstName structName}` is marked as private"
   let { ctorFn, ctorFnType, structType, levels, params } ← mkCtorHeader ctorVal structType?
   let (_, fields) ← expandFields structName s.fields (recover := (← read).errToSorry)

src/Lean/Elab/SyntheticMVars.lean

@@ -340,6 +340,13 @@ private def TacticMVarKind.maybeWithoutRecovery (kind : TacticMVarKind) (m : Tac
   else
     m
 
+register_builtin_option backward.proofsInPublic : Bool := {
+  defValue := false
+  descr    := "(module system) Do not abstract proofs used in the public scope into auxiliary \
+    theorems. Enabling this option may lead to failures or, when `backward.privateInPublic` and \
+    its `warn` sub-option are enabled, additional warnings from private accesses."
+}
+
 mutual
 
   /--
@@ -352,7 +359,7 @@ mutual
   partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (kind : TacticMVarKind) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
     let wasExporting := (← getEnv).isExporting
     -- exit exporting context if entering proof
-    let isNoLongerExporting ← pure wasExporting <&&> do
+    let isNoLongerExporting ← pure (wasExporting && !(← backward.proofsInPublic.getM)) <&&> do
       mvarId.withContext do
         isProp (← mvarId.getType)
     instantiateMVarDeclMVars mvarId

src/Lean/Elab/Tactic/Ext.lean

@@ -112,7 +112,7 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
     try
       Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do
         let type ← mkExtType structName flat
-        let pf ← withSynthesize do
+        let pf ← withoutExporting <| withSynthesize do
           let indVal ← getConstInfoInduct structName
           let params := Array.replicate indVal.numParams (← `(_))
           Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
@@ -149,7 +149,7 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
       let info ← getConstInfo extName
       Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do
         let type ← mkExtIffType extName
-        let pf ← withSynthesize do
+        let pf ← withoutExporting <| withSynthesize do
           Elab.Term.elabTermEnsuringType (expectedType? := type) <| ← `(by
             intros
             refine ⟨?_, ?_⟩

src/Lean/Meta/Check.lean

@@ -194,6 +194,24 @@ def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
     throwError "invalid {declKind} declaration, term{indentExpr v}\nhas type{indentExpr vType}\nbut is expected to have type{indentExpr t}"
   | _ => unreachable!
 
+/-- Adds note about definitions not unfolded because of the module system, if any. -/
+def mkUnfoldAxiomsNote (givenType expectedType : Expr) : MetaM MessageData := do
+  let env ← getEnv
+  if env.header.isModule then
+    let origDiag := (← get).diag
+    try
+      let _ ← observing <| withOptions (diagnostics.set · true)  <| isDefEq givenType expectedType
+      let blocked := (← get).diag.unfoldAxiomCounter.toList.filterMap fun (n, count) => do
+        let count := count - origDiag.unfoldAxiomCounter.findD n 0
+        guard <| count > 0 && getOriginalConstKind? env n matches some .defn
+        return m!"{.ofConstName n} ↦ {count}"
+      if !blocked.isEmpty then
+        return MessageData.note m!"The following definitions were not unfolded because \
+          their definition is not exposed:{indentD <| .joinSep blocked Format.line}"
+    finally
+      modify ({ · with diag := origDiag })
+  return .nil
+
 /--
 Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
 Adds the type’s types unless they are defeq.
@@ -226,19 +244,7 @@ def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr)
       let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
       let trailing := trailing?.map (m!"\n" ++ ·) |>.getD .nil
       pure m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}{trailing}")
-    let env ← getEnv
-    if env.header.isModule then
-      let origDiag := (← get).diag
-      let _ ← observing <| withOptions (diagnostics.set · true)  <| isDefEq givenType expectedType
-      let blocked := (← get).diag.unfoldAxiomCounter.toList.filterMap fun (n, count) => do
-        let count := count - origDiag.unfoldAxiomCounter.findD n 0
-        guard <| count > 0 && getOriginalConstKind? env n matches some .defn
-        return m!"{.ofConstName n} ↦ {count}"
-      if !blocked.isEmpty then
-        msg := msg ++ MessageData.note m!"The following definitions were not unfolded because \
-          their definition is not exposed:{indentD <| .joinSep blocked Format.line}"
-      modify ({ · with diag := origDiag })
-    return msg
+    return msg ++ (← mkUnfoldAxiomsNote givenType expectedType)
 
 def throwAppTypeMismatch (f a : Expr) : MetaM α := do
   -- Clarify that `a` is "last" only if it may be confused with some preceding argument; otherwise,

src/Lean/Meta/Tactic/Apply.lean

@@ -34,7 +34,7 @@ private def throwApplyError {α} (mvarId : MVarId)
     let (conclusionType, targetType) ← addPPExplicitToExposeDiff conclusionType targetType
     let conclusion := if conclusionType?.isNone then "type" else "conclusion"
     return m!"could not unify the {conclusion} of {term?.getD "the term"}{indentExpr conclusionType}\n\
-      with the goal{indentExpr targetType}{note}"
+      with the goal{indentExpr targetType}{note}{← mkUnfoldAxiomsNote conclusionType targetType}"
 
 def synthAppInstances (tacticName : Name) (mvarId : MVarId) (mvarsNew : Array Expr) (binderInfos : Array BinderInfo)
     (synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit := do

src/Lean/Meta/Tactic/FunInd.lean

@@ -283,7 +283,7 @@ improve the errors, for example by passing down a flag whether we expect the sam
 occurrences of `newIH`), or whether we are in “supple mode”, and catch it earlier if the rewriting
 fails.
 -/
-partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (e : Expr) : M Expr := do
+partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (e : Expr) : M Expr := withoutExporting do
   unless e.containsFVar oldIH do
     return e
   withTraceNode `Meta.FunInd (pure m!"{exceptEmoji ·} foldAndCollect ({mkFVar oldIH} → {mkFVar newIH})::{indentExpr e}") do

src/Lean/Modifiers.lean

@@ -25,19 +25,4 @@ def mkPrivateName (env : Environment) (n : Name) : Name :=
   -- is private to *this* module.
   mkPrivateNameCore env.mainModule <| privateToUserName n
 
-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/PrettyPrinter/Delaborator/FieldNotation.lean

@@ -45,22 +45,22 @@ private def projInfo (c : Name) : MetaM (Option (Name × Nat × Bool × Bool ×
 /--
 Checks that `e` is an application of a constant that equals `baseName`, taking into consideration private name mangling.
 -/
-private def isAppOfBaseName (env : Environment) (e : Expr) (baseName : Name) : Bool :=
+private def isAppOfBaseName (e : Expr) (baseName : Name) : MetaM Bool := do
   if let some c := e.cleanupAnnotations.getAppFn.constName? then
-    privateToUserName c == baseName && !isInaccessiblePrivateName env c
+    return privateToUserName c == baseName && !(← isInaccessiblePrivateName c)
   else
-    false
+    return false
 
 /--
 Like `Lean.Elab.Term.typeMatchesBaseName` but does not use `Function` for pi types.
 -/
 private partial def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
   withReducibleAndInstances do
-    if isAppOfBaseName (← getEnv) type baseName then
+    if (← isAppOfBaseName type baseName) then
       return true
     else
       let type ← whnfCore type
-      if isAppOfBaseName (← getEnv) type baseName then
+      if (← isAppOfBaseName type baseName) then
         return true
       else
         match ← unfoldDefinition? type with
@@ -94,7 +94,7 @@ private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name ×
         -- We require an exact match for the base name.
         -- While `Lean.Elab.Term.resolveLValLoop` is able to unfold the type and iterate, we do not attempt to exploit this feature.
         -- (To get it right, we would need to check that each relevant namespace does not contain a declaration named `field`.)
-        guard <| isAppOfBaseName (← getEnv) (← instantiateMVars <| ← inferType args[i]!) baseName
+        guard (← isAppOfBaseName (← instantiateMVars <| ← inferType args[i]!) baseName)
         return (field, i)
       else
         -- We only use the first explicit argument for field notation.
@@ -114,7 +114,7 @@ returns the field name to use and the argument index for the object of the field
 def fieldNotationCandidate? (f : Expr) (args : Array Expr) (useGeneralizedFieldNotation : Bool) : MetaM (Option (Name × Nat)) := do
   let env ← getEnv
   let .const c .. := f.consumeMData | return none
-  if isInaccessiblePrivateName (← getEnv) c then
+  if (← isInaccessiblePrivateName c) then
     return none
   if c.getPrefix.isAnonymous then return none
   -- If there is `pp_nodot` on this function, then don't use field notation for it.

src/Lean/ResolveName.lean

@@ -275,6 +275,23 @@ def checkPrivateInPublic (id : Name) : m Unit := do
       this is allowed only because the `backward.privateInPublic` option is enabled. \n\n\
       Disable `backward.privateInPublic.warn` to silence this warning."
 
+def isInaccessiblePrivateName [Monad m] [MonadEnv m] [MonadOptions m] (n : Name) : m Bool := do
+  if !isPrivateName n then
+    return false
+  let env ← getEnv
+  -- All private names are inaccessible from the public scope
+  if env.isExporting && !(← ResolveName.backward.privateInPublic.getM) then
+    return true
+  checkPrivateInPublic n
+  -- In the private scope, ...
+  match env.getModuleIdxFor? n with
+  | some modIdx =>
+    -- ... allow access through `import all`
+    return !env.header.isModule || !env.header.modules[modIdx]?.any (·.importAll)
+  | none =>
+    -- ... allow all accesses in the current module
+    return false
+
 /--
 Given a name `n`, return a list of possible interpretations.
 Each interpretation is a pair `(declName, fieldList)`, where `declName`

src/Std.lean

@@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
 module
+
 prelude
-import Std.Data
-import Std.Do
-import Std.Sat
-import Std.Sync
-import Std.Time
-import Std.Tactic
-import Std.Internal
-import Std.Net
+public import Std.Data
+public import Std.Do
+public import Std.Sat
+public import Std.Sync
+public import Std.Time
+public import Std.Tactic
+public import Std.Internal
+public import Std.Net

tests/pkg/module/Module/Basic.lean

@@ -496,3 +496,11 @@ Note: A private declaration `S.s` (from the current module) exists but would nee
 -/
 #guard_msgs in
 @[expose] public def useS (s : S) := s.s
+
+/- `meta` should trump `noncomputable`. -/
+
+noncomputable section
+/-- error: Invalid `meta` definition `m`, `S.s` not marked `meta` -/
+#guard_msgs in
+meta def m := S.s
+end

tests/pkg/module/Module/Imported.lean

@@ -27,6 +27,23 @@ Note: The following definitions were not unfolded because their definition is no
 #guard_msgs in
 example : f = 1 := rfl
 
+/--
+error: Tactic `apply` failed: could not unify the conclusion of `@rfl`
+  ?a = ?a
+with the goal
+  f = 1
+
+Note: The full type of `@rfl` is
+  ∀ {α : Sort ?u.115} {a : α}, a = a
+
+Note: The following definitions were not unfolded because their definition is not exposed:
+  f ↦ 1
+
+⊢ f = 1
+-/
+#guard_msgs in
+example : f = 1 := by apply rfl
+
 /-! Theorems should be exported without their bodies -/
 
 /--