diff --git a/src/Lean/Compiler/LCNF/StructProjCases.lean b/src/Lean/Compiler/LCNF/StructProjCases.lean index 495e8de1f8..8dec4e8269 100644 --- a/src/Lean/Compiler/LCNF/StructProjCases.lean +++ b/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! diff --git a/tests/lean/run/11322.lean b/tests/lean/run/11322.lean new file mode 100644 index 0000000000..cd53d508c8 --- /dev/null +++ b/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