diff --git a/src/Lean/Compiler/LCNF/MonoTypes.lean b/src/Lean/Compiler/LCNF/MonoTypes.lean index 924ab80cccb7..ce366b187d23 100644 --- a/src/Lean/Compiler/LCNF/MonoTypes.lean +++ b/src/Lean/Compiler/LCNF/MonoTypes.lean @@ -74,8 +74,6 @@ partial def toMonoType (type : Expr) : CoreM Expr := do let type := type.headBeta if type.isErased then return erasedExpr - else if type.isErased then - return erasedExpr else if isTypeFormerType type then return erasedExpr else match type with