diff --git a/src/Lean/Compiler/LCNF/InferType.lean b/src/Lean/Compiler/LCNF/InferType.lean
index 5bfe15a2fb..9d6da755de 100644
--- a/src/Lean/Compiler/LCNF/InferType.lean
+++ b/src/Lean/Compiler/LCNF/InferType.lean
@@ -102,8 +102,11 @@ mutual
         for _ in [:idx] do
           match ctorType with
           | .forallE _ _ body _ =>
-            assert! !body.hasLooseBVars
-            ctorType := body
+            if body.hasLooseBVars then
+              -- This can happen when one of the fields is a type or type former.
+              ctorType := body.instantiate1 anyTypeExpr
+            else
+              ctorType := body
           | _ =>
             if ctorType.isAnyType then return anyTypeExpr
             failed ()
diff --git a/tests/lean/run/lcnfInferProjTypeBug.lean b/tests/lean/run/lcnfInferProjTypeBug.lean
new file mode 100644
index 0000000000..e680089cc1
--- /dev/null
+++ b/tests/lean/run/lcnfInferProjTypeBug.lean
@@ -0,0 +1,4 @@
+import Lean
+
+set_option trace.Compiler.result true
+#eval Lean.Compiler.compile #[``Lean.Meta.mapMetaM]