diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index 26c100d2be..c643c6ba9a 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -100,14 +100,6 @@ def isIrrelevant : IRType → Bool | irrelevant => true | _ => false -def isStruct : IRType → Bool - | struct _ _ => true - | _ => false - -def isUnion : IRType → Bool - | union _ _ => true - | _ => false - end IRType /-- Arguments to applications, constructors, etc. diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean index 7966dcb6af..3a2346c680 100644 --- a/src/Lean/Compiler/IR/Checker.lean +++ b/src/Lean/Compiler/IR/Checker.lean @@ -133,7 +133,7 @@ def checkExpr (ty : IRType) (e : Expr) : M Unit := do throw s!"constructor '{c.name}' has too many fields" if c.ssize + c.usize * usizeSize > maxCtorScalarsSize then throw s!"constructor '{c.name}' has too many scalar fields" - if !ty.isStruct && !ty.isUnion && c.isRef then + if c.isRef then checkObjType ty checkArgs ys | .reset _ x =>