diff --git a/src/Lean/Compiler/LCNF/Types.lean b/src/Lean/Compiler/LCNF/Types.lean
index 5c381690b5..50f0880b90 100644
--- a/src/Lean/Compiler/LCNF/Types.lean
+++ b/src/Lean/Compiler/LCNF/Types.lean
@@ -487,7 +487,8 @@ def Lean.Expr.isDefiniteRef : Expr → Bool
 The boxed version of types.
 -/
 def Lean.Expr.boxed : Expr → Expr
-  | ImpureType.object | ImpureType.float | ImpureType.float32 => ImpureType.object
+  | ImpureType.object | ImpureType.float | ImpureType.float32 | ImpureType.uint64 =>
+    ImpureType.object
   | ImpureType.void | ImpureType.tagged | ImpureType.uint8 | ImpureType.uint16 => ImpureType.tagged
   | _ => ImpureType.tobject
 
diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out
index 54d3d38ce2..ccdea68d89 100644
--- a/tests/lean/computedFieldsCode.lean.expected.out
+++ b/tests/lean/computedFieldsCode.lean.expected.out
@@ -240,10 +240,10 @@
       default →
         let x_4 : u64 := 42;
         ret x_4
-    def Exp.hash._override._boxed (x_1 : tobj) : tobj :=
+    def Exp.hash._override._boxed (x_1 : tobj) : obj :=
       let x_2 : u64 := Exp.hash._override x_1;
       dec x_1;
-      let x_3 : tobj := box x_2;
+      let x_3 : obj := box x_2;
       ret x_3
 [Compiler.IR] [result]
     def Exp.app._override (x_1 : tobj) (x_2 : tobj) : tobj :=
diff --git a/tests/lean/externBoxing.lean.expected.out b/tests/lean/externBoxing.lean.expected.out
index 53a9c93aba..3f69094ecb 100644
--- a/tests/lean/externBoxing.lean.expected.out
+++ b/tests/lean/externBoxing.lean.expected.out
@@ -1,8 +1,8 @@
 [Compiler.IR] [result]
     extern _private.lean.externBoxing.0.Foo.bar (x_1 : obj) (x_2 : u64) : u64
-    def _private.lean.externBoxing.0.Foo.bar._boxed (x_1 : obj) (x_2 : tobj) : tobj :=
+    def _private.lean.externBoxing.0.Foo.bar._boxed (x_1 : obj) (x_2 : obj) : obj :=
       let x_3 : u64 := unbox x_2;
       dec x_2;
       let x_4 : u64 := _private.lean.externBoxing.0.Foo.bar x_1 x_3;
-      let x_5 : tobj := box x_4;
+      let x_5 : obj := box x_4;
       ret x_5
diff --git a/tests/lean/run/10443.lean b/tests/lean/run/10443.lean
index 700150c1c5..6f255cdf53 100644
--- a/tests/lean/run/10443.lean
+++ b/tests/lean/run/10443.lean
@@ -12,11 +12,11 @@ trace: [Compiler.IR] [result]
       let x_2 : u64 := 9223372036854775808;
       let x_3 : u64 := UInt64.add x_2 x_1;
       ret x_3
-    def mwe._boxed (x_1 : tobj) : tobj :=
+    def mwe._boxed (x_1 : obj) : obj :=
       let x_2 : u64 := unbox x_1;
       dec x_1;
       let x_3 : u64 := mwe x_2;
-      let x_4 : tobj := box x_3;
+      let x_4 : obj := box x_3;
       ret x_4
 -/
 #guard_msgs in
diff --git a/tests/lean/run/4278.lean b/tests/lean/run/4278.lean
index fc91c897c2..1d71741fe1 100644
--- a/tests/lean/run/4278.lean
+++ b/tests/lean/run/4278.lean
@@ -11,9 +11,9 @@ trace: [Compiler.IR] [result]
       let x_2 : u64 := sproj[0, 0] x_1;
       dec x_1;
       ret x_2
-    def get_unboxed._boxed (x_1 : obj) : tobj :=
+    def get_unboxed._boxed (x_1 : obj) : obj :=
       let x_2 : u64 := get_unboxed x_1;
-      let x_3 : tobj := box x_2;
+      let x_3 : obj := box x_2;
       ret x_3
 -/
 #guard_msgs in
diff --git a/tests/lean/sint_basic.lean.expected.out b/tests/lean/sint_basic.lean.expected.out
index 18863fb23c..f6fc83f01f 100644
--- a/tests/lean/sint_basic.lean.expected.out
+++ b/tests/lean/sint_basic.lean.expected.out
@@ -322,11 +322,11 @@ true
 [Compiler.IR] [result]
     def _private.lean.sint_basic.0.myId64 (x_1 : u64) : u64 :=
       ret x_1
-    def _private.lean.sint_basic.0.myId64._boxed (x_1 : tobj) : tobj :=
+    def _private.lean.sint_basic.0.myId64._boxed (x_1 : obj) : obj :=
       let x_2 : u64 := unbox x_1;
       dec x_1;
       let x_3 : u64 := _private.lean.sint_basic.0.myId64 x_2;
-      let x_4 : tobj := box x_3;
+      let x_4 : obj := box x_3;
       ret x_4
 ISize : Type
 20