From 61edf19334d5bfa470b779cc9252309ea27f0bd2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Sep 2022 17:28:02 -0700 Subject: [PATCH] fix: allow LCNF discriminant to have `any` type --- src/Lean/Compiler/LCNF/Check.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Check.lean b/src/Lean/Compiler/LCNF/Check.lean index 7777737fea..cc388bb543 100644 --- a/src/Lean/Compiler/LCNF/Check.lean +++ b/src/Lean/Compiler/LCNF/Check.lean @@ -150,9 +150,10 @@ partial def checkCases (c : Cases) : CheckM Expr := do let mut hasDefault := false checkFVar c.discr let discrType ← inferFVarType c.discr - let .const declName _ := discrType.headBeta.getAppFn | throwError "unexpected LCNF discriminant type {discrType}" - unless c.typeName == declName do - throwError "invalid LCNF `{c.typeName}.casesOn`, discriminant has type{indentExpr discrType}" + unless discrType.isAnyType do + let .const declName _ := discrType.headBeta.getAppFn | throwError "unexpected LCNF discriminant type {discrType}" + unless c.typeName == declName do + throwError "invalid LCNF `{c.typeName}.casesOn`, discriminant has type{indentExpr discrType}" for alt in c.alts do let type ← match alt with