fix: don't treat types with erased constructor types as having trivial structure (#8634)

This PR makes `hasTrivialStructure?` return false for types whose
constructors have types that are erased, e.g. if they construct a
`Prop`.

Author: zwarich

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -46,6 +46,8 @@ def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo)
   let .inductInfo info ← getConstInfo declName | return none
   if info.isUnsafe || info.isRec then return none
   let [ctorName] := info.ctors | return none
+  let ctorType ← getOtherDeclBaseType ctorName []
+  if ctorType.isErased then return none
   let mask ← getRelevantCtorFields ctorName
   let mut result := none
   for h : i in [:mask.size] do

tests/lean/run/projWithIrrelevantFields.lean

@@ -0,0 +1,19 @@
+structure S (α : Type) where
+  a : Nat
+  b : Nat
+  nothing : Nonempty α
+
+def f {α : Type} (s : S α) : Nat := s.a
+
+def g {α : Type} (s : S α) : Nat :=
+  match s with
+  | .mk _ b _ => b
+
+structure T (α : Type) where
+  b : Nat
+  nothing : Nonempty α
+
+def h {α : Type} (s : S α) : T α :=
+  match s with
+  | .mk _ b nothing => { b, nothing }
+