From 5cd5885da4a46ba6f55da77e98c8f95c2af51470 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Fri, 18 Jul 2025 13:10:52 -0700
Subject: [PATCH] fix: make IRType.erased a tobject when boxing it (#9431)

This PR changes `IRType.boxed` to map `erased` to `tobject` rather than
`object`, since `erased` has a representation of a boxed scalar 0 when
we are forced to represent it at runtime. This case does not occur at
all in the Lean codebase.
---
 src/Lean/Compiler/IR/Basic.lean                 | 2 +-
 tests/lean/computedFieldsCode.lean.expected.out | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean
index 3afdb08f6f..85d8ef0305 100644
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@@ -113,7 +113,7 @@ def isErased : IRType → Bool
   | _ => false
 
 def boxed : IRType → IRType
-  | object | erased | float | float32 => object
+  | object | float | float32 => object
   | tagged | uint8 | uint16 => tagged
   | _ => tobject
 
diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out
index 33f1f1799e..7e4a5a9e2d 100644
--- a/tests/lean/computedFieldsCode.lean.expected.out
+++ b/tests/lean/computedFieldsCode.lean.expected.out
@@ -93,7 +93,7 @@
       dec x_5;
       dec x_4;
       ret x_9
-    def Exp.casesOn._override._boxed (x_1 : obj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) (x_9 : tobj) : tobj :=
+    def Exp.casesOn._override._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) (x_9 : tobj) : tobj :=
       let x_10 : tobj := Exp.casesOn._override x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9;
       dec x_9;
       dec x_8;