From 691afbfdc87be1cfa32388793cfe446fe1f8d28e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 31 Oct 2022 07:49:49 -0700
Subject: [PATCH] fix: `ToLCNF` `visitNoConfusion`

---
 src/Lean/Compiler/LCNF/ToLCNF.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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}`"