fix: inaccessible private messages in the module system (#9518)

This PR ensures previous "is marked as private" messages are still
triggered under the module system

src/Init/Dynamic.lean

@@ -37,7 +37,7 @@ class TypeName (α : Type) where unsafe mk ::
 class TypeName (α : Type u) where private mk' ::
   private data : (TypeNameData α).type
 
-instance : Nonempty (TypeName α) := (TypeNameData α).property.elim (⟨⟨·⟩⟩)
+instance : Nonempty (TypeName α) := by exact (TypeNameData α).property.elim (⟨⟨·⟩⟩)
 
 /--
 Creates a `TypeName` instance.

src/Lean/Elab/App.lean

@@ -1581,7 +1581,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 isPrivateNameFromImportedModule (← getEnv) info.projFn then
+      if isInaccessiblePrivateName (← getEnv) info.projFn then
         throwError "Field `{fieldName}` from structure `{structName}` is private"
       let projFn ← mkConst info.projFn
       let projFn ← addProjTermInfo lval.getRef projFn

src/Lean/Elab/BuiltinNotation.lean

@@ -50,7 +50,7 @@ open Meta
         (fun ival _ => do
           match ival.ctors with
           | [ctor] =>
-            if isPrivateNameFromImportedModule (← getEnv) ctor then
+            if isInaccessiblePrivateName (← getEnv) 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/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 isPrivateNameFromImportedModule env ctorVal.name then
+  if isInaccessiblePrivateName env 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/Modifiers.lean

@@ -22,12 +22,10 @@ def mkPrivateName (env : Environment) (n : Name) : Name :=
   -- is private to *this* module.
   mkPrivateNameCore env.mainModule <| privateToUserName n
 
-def isPrivateNameFromImportedModule (env : Environment) (n : Name) : Bool :=
+def isInaccessiblePrivateName (env : Environment) (n : Name) : Bool :=
   if env.header.isModule then
     -- Allow access through `import all`.
-    -- TODO: this should not be relevant as soon as we make sure we never export any kind of private
-    -- constant.
-    !env.contains n && (env.setExporting false).contains n
+    env.isExporting && isPrivateName n
   else match privateToUserName? n with
     | some userName => mkPrivateName env userName != n
     | _ => false

src/Std/Sat/AIG/Basic.lean

@@ -31,7 +31,7 @@ node which consists of a `Nat` describing the input node and a `Bool` saying whe
 on the input.
 -/
 structure Fanin where
-  private of ::
+  ofRaw ::
     val : Nat
   deriving Hashable, Repr, DecidableEq, Inhabited
 

src/Std/Time/Zoned/ZonedDateTime.lean

@@ -45,7 +45,7 @@ structure ZonedDateTime where
   timezone : TimeZone
 
 instance : Inhabited ZonedDateTime where
-  default := ⟨Thunk.mk Inhabited.default, Inhabited.default, Inhabited.default, Inhabited.default⟩
+  default := private ⟨Thunk.mk Inhabited.default, Inhabited.default, Inhabited.default, Inhabited.default⟩
 
 namespace ZonedDateTime
 open DateTime

tests/pkg/module/Module/Basic.lean

@@ -211,3 +211,26 @@ info: theorem f_exp_wfrec.eq_unfold : f_exp_wfrec = fun x x_1 =>
   | n.succ, acc => f_exp_wfrec n (acc + 1)
 -/
 #guard_msgs in #print sig f_exp_wfrec.eq_unfold
+
+/-! Private fields should force private ctors. -/
+
+public structure StructWithPrivateField where
+  private x : Nat
+
+/--
+info: structure StructWithPrivateField : Type
+number of parameters: 0
+fields:
+  private StructWithPrivateField.x : Nat
+constructor:
+  private StructWithPrivateField.mk (x : Nat) : StructWithPrivateField
+-/
+#guard_msgs in
+#print StructWithPrivateField
+
+#check { x := 1 : StructWithPrivateField }
+
+/-- error: invalid {...} notation, constructor for 'StructWithPrivateField' is marked as private -/
+#guard_msgs in
+#with_exporting
+#check { x := 1 : StructWithPrivateField }