From b8fa6f17eecc28eb533de3071fffc869f1208f6e Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 18 Aug 2025 15:18:26 -0700
Subject: [PATCH] fix: make lcAny-producing arrow types lower to `tobj` rather
 than `obj` (#9972)

This PR fixes an issue when running Mathlib's `FintypeCat` as code,
where an erased type former is passed to a polymorphic function. We were
lowering the arrow type to`object`, which conflicts with the runtime
representation of an erased value as a tagged scalar.
---
 src/Lean/Compiler/IR/ToIRType.lean               | 16 +++++++++++++++-
 tests/compiler/typeFormerPolymorphism.lean       |  8 ++++++++
 .../typeFormerPolymorphism.lean.expected.out     |  1 +
 tests/lean/computedFieldsCode.lean.expected.out  |  8 ++++----
 4 files changed, 28 insertions(+), 5 deletions(-)
 create mode 100755 tests/compiler/typeFormerPolymorphism.lean
 create mode 100644 tests/compiler/typeFormerPolymorphism.lean.expected.out

diff --git a/src/Lean/Compiler/IR/ToIRType.lean b/src/Lean/Compiler/IR/ToIRType.lean
index d6ba927e1f..3cf47d993c 100644
--- a/src/Lean/Compiler/IR/ToIRType.lean
+++ b/src/Lean/Compiler/IR/ToIRType.lean
@@ -79,6 +79,12 @@ where fillCache : CoreM IRType := do
       else
         return .tobject
 
+private def isAnyProducingType (type : Lean.Expr) : Bool :=
+  match type with
+  | .const ``lcAny _ => true
+  | .forallE _ _ b _ => isAnyProducingType b
+  | _ => false
+
 def toIRType (type : Lean.Expr) : CoreM IRType := do
   match type with
   | .const name _ => nameToIRType name
@@ -86,7 +92,15 @@ 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 .object
+  | .forallE _ _ b _ =>
+    -- Type formers are erased, but can be used polymorphically as
+    -- an arrow type producing `lcAny`. The runtime representation of
+    -- erased values is a tagged scalar, so this means that any such
+    -- polymorphic type must be represented as `.tobject`.
+    if isAnyProducingType b then
+      return .tobject
+    else
+      return .object
   | .mdata _ b => toIRType b
   | _ => unreachable!
 
diff --git a/tests/compiler/typeFormerPolymorphism.lean b/tests/compiler/typeFormerPolymorphism.lean
new file mode 100755
index 0000000000..bceeb8b7b2
--- /dev/null
+++ b/tests/compiler/typeFormerPolymorphism.lean
@@ -0,0 +1,8 @@
+@[noinline]
+def foo (α : Type 0) (β : Type 1) (f : α → β) (a : α) : α × β × (α → β) × (α → β) :=
+  ⟨a, f a, f, f⟩
+
+def alwaysNat (_ : Nat) : Type 0 := Nat
+
+def main : IO Unit :=
+  IO.println f!"{foo Nat (Type 0) alwaysNat 42 |>.1}"
diff --git a/tests/compiler/typeFormerPolymorphism.lean.expected.out b/tests/compiler/typeFormerPolymorphism.lean.expected.out
new file mode 100644
index 0000000000..d81cc0710e
--- /dev/null
+++ b/tests/compiler/typeFormerPolymorphism.lean.expected.out
@@ -0,0 +1 @@
+42
diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out
index 75aa658759..7e4a5a9e2d 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 : obj) (x_3 : obj) (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 : tobj) (x_3 : tobj) (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 : obj) (x_4 : obj) (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 : tobj) (x_4 : tobj) (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 : obj) (x_3 : obj) (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 : tobj) (x_3 : tobj) (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 : obj) (x_4 : obj) (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;