From d0e097cd1d7100b2d2baae79e55e5e782b930ce8 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Sun, 6 Jul 2025 06:24:24 -0700 Subject: [PATCH] chore: remove IRType.{isStruct,isUnion} (#9219) These are used by the checker for `.ctor`, but I don't think that that unboxed types will reuse `.ctor`, whose implementation details are intimately connected to our runtime representation of objects. --- src/Lean/Compiler/IR/Basic.lean | 8 -------- src/Lean/Compiler/IR/Checker.lean | 2 +- 2 files changed, 1 insertion(+), 9 deletions(-) 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 =>