diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index f65f814384..867145b8c0 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -629,7 +629,8 @@ where
             let major := mkAppN major args[arity+1:]
             visit major
         else
-          mkUnreachable (← inferType e)
+          let type ← toLCNFType (← liftMetaM <| Meta.inferType e)
+          mkUnreachable type
       | _, _ =>
         throwError "code generator failed, unsupported occurrence of `{declName}`"