diff --git a/src/Lean/Compiler/IR/Format.lean b/src/Lean/Compiler/IR/Format.lean
index ba84eb5904..9588ca6bcf 100644
--- a/src/Lean/Compiler/IR/Format.lean
+++ b/src/Lean/Compiler/IR/Format.lean
@@ -76,7 +76,7 @@ private partial def formatIRType : IRType → Format
     let _ : ToFormat IRType := ⟨formatIRType⟩
     "union " ++ Format.bracket "{" (Format.joinSep  tys.toList ", ") "}"
 
-instance : ToFormat IRType := ⟨formatIRType⟩
+instance : ToFormat IRType := ⟨private_decl% formatIRType⟩
 instance : ToString IRType := ⟨toString ∘ format⟩
 
 private def formatParam : Param → Format
diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean
index 6e0299985a..7accd18a20 100644
--- a/src/Lean/Compiler/LCNF/Basic.lean
+++ b/src/Lean/Compiler/LCNF/Basic.lean
@@ -715,7 +715,7 @@ partial def Code.collectUsed (code : Code) (s : FVarIdHashSet := {}) : FVarIdHas
   | .jmp fvarId args => collectArgs args <| s.insert fvarId
 end
 
-abbrev collectUsedAtExpr (s : FVarIdHashSet) (e : Expr) : FVarIdHashSet :=
+@[inline] def collectUsedAtExpr (s : FVarIdHashSet) (e : Expr) : FVarIdHashSet :=
   collectType e s
 
 /--
diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index 9a89bbdd4d..46c84485b3 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -203,7 +203,7 @@ private partial def beq' : Json → Json → Bool
   | _,      _      => false
 
 instance : BEq Json where
-  beq := beq'
+  beq := private beq'
 
 private partial def hash' : Json → UInt64
   | null   => 11
@@ -216,7 +216,7 @@ private partial def hash' : Json → UInt64
     mixHash 29 <| kvPairs.foldl (init := 7) fun r k v => mixHash r <| mixHash (hash k) (hash' v)
 
 instance : Hashable Json where
-  hash := hash'
+  hash := private hash'
 
 def mkObj (o : List (String × Json)) : Json :=
   obj <| Std.TreeMap.Raw.ofList o
diff --git a/src/Lean/Data/Trie.lean b/src/Lean/Data/Trie.lean
index 9118d4dbc5..7680c07f14 100644
--- a/src/Lean/Data/Trie.lean
+++ b/src/Lean/Data/Trie.lean
@@ -199,8 +199,8 @@ private partial def toStringAux {α : Type} : Trie α → List Format
       [ format (repr c), (Format.group $ Format.nest 4 $ flip Format.joinSep Format.line $ toStringAux t) ]
     ) cs.toList ts.toList
 
-instance {α : Type} : ToString (Trie α) :=
-  ⟨fun t => (flip Format.joinSep Format.line $ toStringAux t).pretty⟩
+instance {α : Type} : ToString (Trie α) where
+  toString t := private (flip Format.joinSep Format.line $ toStringAux t).pretty
 
 end Trie
 
diff --git a/src/Lean/Data/Xml/Basic.lean b/src/Lean/Data/Xml/Basic.lean
index 21b254e915..71d8d13e3e 100644
--- a/src/Lean/Data/Xml/Basic.lean
+++ b/src/Lean/Data/Xml/Basic.lean
@@ -41,5 +41,5 @@ private partial def cToString : Content → String
 | Content.Character c => c
 
 end
-instance : ToString Element := ⟨eToString⟩
-instance : ToString Content := ⟨cToString⟩
+instance : ToString Element := ⟨private_decl% eToString⟩
+instance : ToString Content := ⟨private_decl% cToString⟩
diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean
index 43e10702f5..89b96e952d 100644
--- a/src/Lean/Elab/MutualInductive.lean
+++ b/src/Lean/Elab/MutualInductive.lean
@@ -558,7 +558,7 @@ This is likely a mistake. The correct solution would be `Type (max u 1)` rather
 but by this point it is impossible to rectify. So, for `u ≤ ?r + 1` we record the pair of `u` and `1`
 so that we can inform the user what they should have probably used instead.
 -/
-def accLevel (u : Level) (r : Level) (rOffset : Nat) : ExceptT MessageData (StateT AccLevelState Id) Unit := do
+private def accLevel (u : Level) (r : Level) (rOffset : Nat) : ExceptT MessageData (StateT AccLevelState Id) Unit := do
   go u rOffset
 where
   go (u : Level) (rOffset : Nat) : ExceptT MessageData (StateT AccLevelState Id) Unit := do
@@ -579,7 +579,7 @@ where
 /--
 Auxiliary function for `updateResultingUniverse`. Applies `accLevel` to the given constructor parameter.
 -/
-def accLevelAtCtor (ctorParam : Expr) (r : Level) (rOffset : Nat) : StateT AccLevelState TermElabM Unit := do
+private def accLevelAtCtor (ctorParam : Expr) (r : Level) (rOffset : Nat) : StateT AccLevelState TermElabM Unit := do
   let type ← inferType ctorParam
   let u ← instantiateLevelMVars (← getLevel type)
   match (← modifyGet fun s => accLevel u r rOffset |>.run |>.run s) with
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index b6b3a1de95..3c2a86ae6f 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -502,7 +502,7 @@ private instance : ToMessageData ExpandedFieldVal where
 private instance : ToMessageData ExpandedField where
   toMessageData field := m!"field '{field.name}' is {field.val}"
 
-abbrev ExpandedFields := NameMap ExpandedField
+private abbrev ExpandedFields := NameMap ExpandedField
 
 /--
 Normalizes and expands the field views.
diff --git a/src/Lean/Elab/Tactic/Config.lean b/src/Lean/Elab/Tactic/Config.lean
index b21f222642..2ed5d6200d 100644
--- a/src/Lean/Elab/Tactic/Config.lean
+++ b/src/Lean/Elab/Tactic/Config.lean
@@ -17,12 +17,12 @@ public section
 namespace Lean.Elab.Tactic
 open Meta Parser.Tactic Command
 
-private structure ConfigItemView where
+structure ConfigItemView where
   ref : Syntax
   option : Ident
   value : Term
   /-- Whether this was using `+`/`-`, to be able to give a better error message on type mismatch. -/
-  (bool : Bool := false)
+  bool : Bool := false
 
 /-- Interprets the `config` as an array of option/value pairs. -/
 def mkConfigItemViews (c : TSyntaxArray ``configItem) : Array ConfigItemView :=
diff --git a/src/Lean/LoadDynlib.lean b/src/Lean/LoadDynlib.lean
index 66f88b447f..93e88dbf6c 100644
--- a/src/Lean/LoadDynlib.lean
+++ b/src/Lean/LoadDynlib.lean
@@ -14,8 +14,8 @@ namespace Lean
 
 private opaque DynlibImpl : NonemptyType.{0}
 /-- A dynamic library handle. -/
-@[expose] def Dynlib := DynlibImpl.type
-instance : Nonempty Dynlib := DynlibImpl.property
+def Dynlib := DynlibImpl.type
+instance : Nonempty Dynlib := by exact DynlibImpl.property
 
 private opaque Dynlib.SymbolImpl (dynlib : Dynlib) : NonemptyType.{0}
 /-- A reference to a symbol within a dynamic library. -/
diff --git a/src/Lean/Meta/ReduceEval.lean b/src/Lean/Meta/ReduceEval.lean
index a52d3bda02..bc74d73d46 100644
--- a/src/Lean/Meta/ReduceEval.lean
+++ b/src/Lean/Meta/ReduceEval.lean
@@ -61,6 +61,6 @@ private partial def evalName (e : Expr) : MetaM Name := do
     throwFailedToEval e
 
 instance : ReduceEval Name where
-  reduceEval := evalName
+  reduceEval := private evalName
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean
index 0768fed795..039882089e 100644
--- a/src/Lean/Meta/Tactic/Grind/Canon.lean
+++ b/src/Lean/Meta/Tactic/Grind/Canon.lean
@@ -132,7 +132,7 @@ private inductive ShouldCanonResult where
     visit
   deriving Inhabited
 
-instance : Repr ShouldCanonResult where
+private instance : Repr ShouldCanonResult where
   reprPrec r _ := private match r with
     | .canonType => "canonType"
     | .canonInst => "canonInst"
@@ -142,7 +142,7 @@ instance : Repr ShouldCanonResult where
 /--
 See comments at `ShouldCanonResult`.
 -/
-def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM ShouldCanonResult := do
+private def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM ShouldCanonResult := do
   if h : i < pinfos.size then
     let pinfo := pinfos[i]
     if pinfo.isInstImplicit then
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index 958ea2a1df..960569e5a4 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -581,12 +581,12 @@ private structure Context where
   /-- Only symbols with priority `>= minPrio` are considered in patterns. -/
   minPrio  : Nat
 
-abbrev M := ReaderT Context StateRefT State MetaM
+private abbrev M := ReaderT Context StateRefT State MetaM
 
 /-- Helper declaration for finding bootstrapping issues. See `isCandidateSymbol`. -/
 private abbrev badForPatterns := [``Eq, ``HEq, ``Iff, ``And, ``Or, ``Not]
 
-def isCandidateSymbol (declName : Name) (root : Bool) : M Bool := do
+private def isCandidateSymbol (declName : Name) (root : Bool) : M Bool := do
   let ctx ← read
   let prio := ctx.symPrios.getPrio declName
   -- Priority 0 are never considered, they are treated as forbidden
@@ -741,7 +741,7 @@ def main (patterns : List Expr) (symPrios : SymbolPriorities) (minPrio : Nat) :
   let (patterns, s) ← patterns.mapM (go (inSupport := false) (root := true)) { symPrios, minPrio } |>.run {}
   return (patterns, s.symbols.toList, s.bvarsFound)
 
-def normalizePattern (e : Expr) : M Expr := do
+private def normalizePattern (e : Expr) : M Expr := do
   go e (inSupport := false) (root := true)
 
 end NormalizePattern
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index bfa03a192f..f03224002f 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -104,6 +104,10 @@ private def containsDeclOrReserved (env : Environment) (declName : Name) : Bool
   env.containsOnBranch declName || isReservedName env declName || env.contains declName
 
 private partial def resolvePrivateName (env : Environment) (declName : Name) : Option Name := do
+  -- No point in checking private names when exporting. This is an optimization but also necessary
+  -- for correct visibility checking while we still carry some private names (e.g. kernel-generated
+  -- from `inductive`) in the public env.
+  guard !env.isExporting
   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
diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean
index 47c9d22923..c9705c0294 100644
--- a/src/Lean/Server/Rpc/RequestHandling.lean
+++ b/src/Lean/Server/Rpc/RequestHandling.lean
@@ -23,7 +23,7 @@ private structure RpcProcedure where
 /- We store the builtin RPC handlers in a Ref and users' handlers in an extension. This ensures
 that users don't need to import core Lean modules to make builtin handlers work, but also that
 they *can* easily create custom handlers and use them in the same file. -/
-builtin_initialize builtinRpcProcedures : IO.Ref (PHashMap Name RpcProcedure) ←
+private builtin_initialize builtinRpcProcedures : IO.Ref (PHashMap Name RpcProcedure) ←
   IO.mkRef {}
 builtin_initialize userRpcProcedures : MapDeclarationExtension Name ←
   mkMapDeclarationExtension
@@ -33,7 +33,7 @@ private unsafe def evalRpcProcedureUnsafe (env : Environment) (opts : Options) (
   env.evalConstCheck RpcProcedure opts ``RpcProcedure procName
 
 @[implemented_by evalRpcProcedureUnsafe]
-opaque evalRpcProcedure (env : Environment) (opts : Options) (procName : Name) :
+private opaque evalRpcProcedure (env : Environment) (opts : Options) (procName : Name) :
     Except String RpcProcedure
 
 open RequestM in
@@ -71,7 +71,7 @@ def handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json) := do
 builtin_initialize
   registerLspRequestHandler "$/lean/rpc/call" Lsp.RpcCallParams Json handleRpcCall
 
-def wrapRpcProcedure (method : Name) paramType respType
+private def wrapRpcProcedure (method : Name) paramType respType
     [RpcEncodable paramType] [RpcEncodable respType]
     (handler : paramType → RequestM (RequestTask respType)) : RpcProcedure where
   wrapper seshId j := do
diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean
index 01bef37500..db3118e369 100644
--- a/src/Lean/Structure.lean
+++ b/src/Lean/Structure.lean
@@ -84,7 +84,7 @@ private structure StructureState where
   map : PersistentHashMap Name StructureInfo := {}
   deriving Inhabited
 
-builtin_initialize structureExt : PersistentEnvExtension StructureInfo StructureInfo (Unit × StructureState) ← registerPersistentEnvExtension {
+private builtin_initialize structureExt : PersistentEnvExtension StructureInfo StructureInfo (Unit × StructureState) ← registerPersistentEnvExtension {
   mkInitial       := pure ((), {})
   addImportedFn   := fun _ => pure ((), {})
   addEntryFn      := fun (_, s) e => ((), { s with map := s.map.insert e.structName e })
diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean
index 0e1960be64..738b3a8ffa 100644
--- a/src/Lean/Widget/TaggedText.lean
+++ b/src/Lean/Widget/TaggedText.lean
@@ -78,12 +78,12 @@ private structure TaggedState where
   column   : Nat                                 := 0
   deriving Inhabited
 
-instance : Std.Format.MonadPrettyFormat (StateM TaggedState) where
-  pushOutput s       := private modify fun ⟨out, ts, col⟩ => ⟨out.appendText s, ts, col + s.length⟩
-  pushNewline indent := private modify fun ⟨out, ts, _⟩ => ⟨out.appendText ("\n".pushn ' ' indent), ts, indent⟩
-  currColumn         := private return (←get).column
-  startTag n         := private modify fun ⟨out, ts, col⟩ => ⟨TaggedText.text "", (n, col, out) :: ts, col⟩
-  endTags n          := private modify fun ⟨out, ts, col⟩ =>
+private instance : Std.Format.MonadPrettyFormat (StateM TaggedState) where
+  pushOutput s       := modify fun ⟨out, ts, col⟩ => ⟨out.appendText s, ts, col + s.length⟩
+  pushNewline indent := modify fun ⟨out, ts, _⟩ => ⟨out.appendText ("\n".pushn ' ' indent), ts, indent⟩
+  currColumn         := return (←get).column
+  startTag n         := modify fun ⟨out, ts, col⟩ => ⟨TaggedText.text "", (n, col, out) :: ts, col⟩
+  endTags n          := modify fun ⟨out, ts, col⟩ =>
     let (ended, left) := (ts.take n, ts.drop n)
     let out' := ended.foldl (init := out) fun acc (n, col', top) => top.appendTag (n, col') acc
     ⟨out', left, col⟩
diff --git a/src/Std/Internal/UV/TCP.lean b/src/Std/Internal/UV/TCP.lean
index 3f4ed27239..7e7dae5e07 100644
--- a/src/Std/Internal/UV/TCP.lean
+++ b/src/Std/Internal/UV/TCP.lean
@@ -11,7 +11,7 @@ public import Init.System.Promise
 public import Init.Data.SInt
 public import Std.Net
 
-@[expose] public section
+public section
 
 namespace Std
 namespace Internal
diff --git a/src/Std/Internal/UV/Timer.lean b/src/Std/Internal/UV/Timer.lean
index dc1e5f7603..852e37cece 100644
--- a/src/Std/Internal/UV/Timer.lean
+++ b/src/Std/Internal/UV/Timer.lean
@@ -9,7 +9,7 @@ prelude
 public import Init.System.IO
 public import Init.System.Promise
 
-@[expose] public section
+public section
 
 namespace Std
 namespace Internal
@@ -30,7 +30,7 @@ of all functions on `Timer`s.
 -/
 def Timer : Type := TimerImpl.type
 
-instance : Nonempty Timer := TimerImpl.property
+instance : Nonempty Timer := by exact TimerImpl.property
 
 namespace Timer
 
diff --git a/src/Std/Internal/UV/UDP.lean b/src/Std/Internal/UV/UDP.lean
index e3f79bfa56..163a679899 100644
--- a/src/Std/Internal/UV/UDP.lean
+++ b/src/Std/Internal/UV/UDP.lean
@@ -10,7 +10,7 @@ public import Init.System.IO
 public import Init.System.Promise
 public import Std.Net
 
-@[expose] public section
+public section
 
 namespace Std
 namespace Internal
@@ -26,7 +26,7 @@ Represents a UDP socket.
 -/
 def Socket : Type := SocketImpl.type
 
-instance : Nonempty Socket := SocketImpl.property
+instance : Nonempty Socket := by exact SocketImpl.property
 
 namespace Socket
 
diff --git a/src/Std/Sync/Channel.lean b/src/Std/Sync/Channel.lean
index abb3d655cf..a5e66bc5ab 100644
--- a/src/Std/Sync/Channel.lean
+++ b/src/Std/Sync/Channel.lean
@@ -800,7 +800,7 @@ private partial def forIn [Monad m] [MonadLiftT BaseIO m]
 
 /-- `for msg in ch.sync do ...` receives all messages in the channel until it is closed. -/
 instance [MonadLiftT BaseIO m] : ForIn m (Sync α) α where
-  forIn ch b f := ch.forIn f b
+  forIn ch b f := private ch.forIn f b
 
 end Sync
 
@@ -927,7 +927,7 @@ private partial def forIn [Inhabited α] [Monad m] [MonadLiftT BaseIO m]
 
 /-- `for msg in ch.sync do ...` receives all messages in the channel until it is closed. -/
 instance [Inhabited α] [MonadLiftT BaseIO m] : ForIn m (Sync α) α where
-  forIn ch b f := ch.forIn f b
+  forIn ch b f := private ch.forIn f b
 
 end Sync
 
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..b3911deb05 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Dear CI, please update stage 0
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean
index dd113f27c7..e10351a21e 100644
--- a/tests/pkg/module/Module/Basic.lean
+++ b/tests/pkg/module/Module/Basic.lean
@@ -260,6 +260,43 @@ constructor:
 #with_exporting
 #check { x := 1 : StructWithPrivateField }
 
+#check StructWithPrivateField.x
+
+/-- error: Unknown constant `StructWithPrivateField.x` -/
+#guard_msgs in
+#with_exporting
+#check StructWithPrivateField.x
+
+/-! Private constructors should be compatible with public fields. -/
+
+public structure StructWithPrivateCtor where private mk ::
+  x : Nat
+
+/--
+info: structure StructWithPrivateCtor : Type
+number of parameters: 0
+fields:
+  StructWithPrivateCtor.x : Nat
+constructor:
+  private StructWithPrivateCtor.mk (x : Nat) : StructWithPrivateCtor
+-/
+#guard_msgs in
+#print StructWithPrivateCtor
+
+/-- error: invalid {...} notation, constructor for 'StructWithPrivateCtor' is marked as private -/
+#guard_msgs in
+#with_exporting
+#check { x := 1 : StructWithPrivateCtor }
+
+#with_exporting
+#check StructWithPrivateCtor.x
+
+#check StructWithPrivateCtor.mk
+
+/-- error: Unknown constant `StructWithPrivateCtor.mk` -/
+#guard_msgs in
+#with_exporting
+#check StructWithPrivateCtor.mk
 
 /-! Private duplicate in public section should not panic. -/