diff --git a/src/Lean/Compiler/LCNF/Irrelevant.lean b/src/Lean/Compiler/LCNF/Irrelevant.lean
index 79baa4a0a4f4..f884142759dd 100644
--- a/src/Lean/Compiler/LCNF/Irrelevant.lean
+++ b/src/Lean/Compiler/LCNF/Irrelevant.lean
@@ -41,6 +41,8 @@ public structure TrivialStructureInfo where
 Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t.
 - It does not have builtin support in the runtime.
 - It has only one constructor.
+  - The constructor must be as visible as the type, otherwise the compiler may attempt to access
+    not-imported data.
 - This constructor has only one computationally relevant field.
 -/
 public def Irrelevant.hasTrivialStructure?
@@ -57,6 +59,7 @@ where fillCache : CoreM (Option TrivialStructureInfo) := do
   let .inductInfo info ← getConstInfo declName | return none
   if info.isUnsafe || info.isRec then return none
   let [ctorName] := info.ctors | return none
+  if isPrivateName ctorName && !isPrivateName declName then return none
   let ctorType ← getOtherDeclBaseType ctorName []
   if ctorType.isErased then return none
   let mask ← getRelevantCtorFields ctorName trivialType
diff --git a/src/Lean/Compiler/LCNF/ToImpureType.lean b/src/Lean/Compiler/LCNF/ToImpureType.lean
index d259110b7dce..684d34b90a14 100644
--- a/src/Lean/Compiler/LCNF/ToImpureType.lean
+++ b/src/Lean/Compiler/LCNF/ToImpureType.lean
@@ -72,6 +72,10 @@ where fillCache : CoreM Expr := do
       let numCtors := ctorNames.length
       let mut numScalarCtors := 0
       for ctorName in ctorNames do
+        if isPrivateName ctorName && !isPrivateName name then
+          -- If the constructor is private but the type is not, we cannot access the constructor's
+          -- fields and thus must assume it has a non-scalar layout.
+          return ImpureType.tobject
         let some (.ctorInfo ctorInfo) := env.find? ctorName | unreachable!
         let hasRelevantField ← Meta.MetaM.run' <|
                                Meta.forallTelescope ctorInfo.type fun params _ => do
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 45feac318313..efcf063d290f 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -80,7 +80,7 @@ endif
 
 Lake: Lean
 # lake is in its own subdirectory, so must adjust relative paths...
-	+"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export  PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean
+	+"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export  PKG=Lake $(LEANMAKE_OPTS) LEAN_OPTS+="--plugin ${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}" OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean
 
 LeanChecker: Lake
 	+"${LEAN_BIN}/leanmake" lib PKG=LeanChecker $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" TEMP_OUT="${LIB}/temp" OLEAN_OUT="$(OUTARC)"
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index e44444704908..60b1b4acd319 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Dear CI, please build stage2
+
 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 1af071c62311..835b564132ed 100644
--- a/tests/pkg/module/Module/Basic.lean
+++ b/tests/pkg/module/Module/Basic.lean
@@ -52,6 +52,10 @@ This is a current compiler limitation for `module`s that may be lifted in the fu
 #guard_msgs in
 public def Fun.mk (f : Nat → Nat) : Fun := f
 
+public structure Struct where
+  x : Nat
+deriving Inhabited
+
 #guard_msgs(drop warning) in
 /-- A theorem. -/
 public theorem t : f = 1 := testSorry
diff --git a/tests/pkg/module/Module/ImportedPrivateImported.lean b/tests/pkg/module/Module/ImportedPrivateImported.lean
index d907685ce65c..40c38c2f34bd 100644
--- a/tests/pkg/module/Module/ImportedPrivateImported.lean
+++ b/tests/pkg/module/Module/ImportedPrivateImported.lean
@@ -15,3 +15,6 @@ public import Module.PrivateImported
 
 /-! #12833: namespaces privately imported but publicly used must be re-exported. -/
 open Namespaced
+
+set_option trace.Compiler true
+def f : StructWithPrivImportedFieldType := default
diff --git a/tests/pkg/module/Module/PrivateImported.lean b/tests/pkg/module/Module/PrivateImported.lean
index a6f89267db01..04583da43943 100644
--- a/tests/pkg/module/Module/PrivateImported.lean
+++ b/tests/pkg/module/Module/PrivateImported.lean
@@ -41,3 +41,7 @@ fail with `Unknown constant` in this public theorem signature. -/
 public theorem hmulDefaultPrivacy (m : Nat) : ∀ n, m * n = m * n := by
   intro n
   rfl
+
+public structure StructWithPrivImportedFieldType where
+  private field : Struct
+deriving Inhabited