fix: ToLCNF visitNoConfusion

2022-10-31 07:49:49 -07:00 · 2022-10-31 07:49:49 -07:00 · 691afbfdc8
commit 691afbfdc8
parent 67e2735f07
1 changed files with 2 additions and 1 deletions
--- 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}`"