fix: compilation of projections on non trivial structures (#11340)

This PR fixes a miscompilation when encountering projections of non
trivial structure types.

Closes: #11322

src/Lean/Compiler/LCNF/StructProjCases.lean

@@ -19,9 +19,10 @@ def findStructCtorInfo? (typeName : Name) : CoreM (Option ConstructorVal) := do
   let some (.ctorInfo ctorInfo) := (← getEnv).find? ctorName | return none
   return ctorInfo
 
-def mkFieldParamsForCtorType (ctorType : Expr) (numParams : Nat) (numFields : Nat)
-    : CompilerM (Array Param) := do
-  let mut type := ctorType
+def mkFieldParamsForCtorType (ctorType : Expr) (numParams : Nat) (numFields : Nat) :
+    CompilerM (Array Param) := do
+  let mut type ← Meta.MetaM.run' <| toLCNFType ctorType
+  type ← toMonoType type
   for _ in *...numParams do
     match type with
     | .forallE _ _ body _ =>
@@ -31,7 +32,7 @@ def mkFieldParamsForCtorType (ctorType : Expr) (numParams : Nat) (numFields : Na
   for _ in *...numFields do
     match type with
     | .forallE name fieldType body _ =>
-      let param ← mkParam name (← toMonoType fieldType) false
+      let param ← mkParam name fieldType false
       fields := fields.push param
       type := body
     | _ => unreachable!

tests/lean/run/11322.lean

@@ -0,0 +1,18 @@
+/-!
+This is a regression test for https://github.com/leanprover/lean4/issues/11322
+-/
+
+abbrev Prop1 (U : Type) := U -> Prop
+
+structure Object where
+    type : Type
+    isAllowedProp1 : Prop1 type -> Prop
+
+abbrev Object.prop1 (U : Object) := Subtype U.isAllowedProp1
+
+structure Hom (A B : Object) where
+    mapType : A.type -> B.type
+    mapProp1 : A.prop1 -> B.prop1
+    mapProp1_valid (p : A.prop1) (x : A.type) : (mapProp1 p).val (mapType x) = p.val x
+
+def Hom.mapType' {U V : Object} (h : Hom U V) : U.type -> V.type := h.mapType