From 6f5532f069e62f0f6b3fc72ff7c89764397d8b36 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 21 Jul 2025 18:16:45 -0700
Subject: [PATCH] perf: make function types object rather than tobject (#9461)

---
 src/Lean/Compiler/IR/ToIRType.lean              | 2 +-
 tests/lean/computedFieldsCode.lean.expected.out | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Compiler/IR/ToIRType.lean b/src/Lean/Compiler/IR/ToIRType.lean
index 4c1849e106..8b5f5df97e 100644
--- a/src/Lean/Compiler/IR/ToIRType.lean
+++ b/src/Lean/Compiler/IR/ToIRType.lean
@@ -82,7 +82,7 @@ def toIRType (type : Lean.Expr) : CoreM IRType := do
     -- All mono types are in headBeta form.
     let .const name _ := type.getAppFn | unreachable!
     nameToIRType name
-  | .forallE .. => return .tobject
+  | .forallE .. => return .object
   | .mdata _ b => toIRType b
   | _ => unreachable!
 
diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out
index 7e4a5a9e2d..75aa658759 100644
--- a/tests/lean/computedFieldsCode.lean.expected.out
+++ b/tests/lean/computedFieldsCode.lean.expected.out
@@ -1,5 +1,5 @@
 [Compiler.IR] [result]
-    def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
+    def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : obj) (x_3 : obj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
       case x_1 : tobj of
       Exp.var._impl →
         dec x_3;
@@ -42,7 +42,7 @@
         dec x_2;
         inc x_8;
         ret x_8
-    def Exp.casesOn._override (x_1 : ◾) (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 (x_1 : ◾) (x_2 : tobj) (x_3 : obj) (x_4 : obj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) (x_9 : @& tobj) : tobj :=
       case x_2 : tobj of
       Exp.var._impl →
         dec x_4;
@@ -85,7 +85,7 @@
         dec x_3;
         inc x_9;
         ret x_9
-    def Exp.casesOn._override._redArg._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) : tobj :=
+    def Exp.casesOn._override._redArg._boxed (x_1 : tobj) (x_2 : obj) (x_3 : obj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) : tobj :=
       let x_9 : tobj := Exp.casesOn._override._redArg x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8;
       dec x_8;
       dec x_7;
@@ -93,7 +93,7 @@
       dec x_5;
       dec x_4;
       ret x_9
-    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 :=
+    def Exp.casesOn._override._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : obj) (x_4 : obj) (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;