[REBASED] fix: codegen should not inspect private ctor of public type

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

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