From dbcf5b9d9deef43de378c2ac7fb32f9cace95142 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Tue, 1 Jul 2025 13:00:34 -0700
Subject: [PATCH] fix: call lowerEnumToScalarType? with ConstructorVal.induct
 (#9134)

This PR changes ToIR to call `lowerEnumToScalarType?` with
`ConstructorVal.induct` rather than the name of the constructor itself.
This was an oversight in some refactoring of code in the new compiler
before landing it. It should not affect runtime of compiled code (due to
the extra tagging/untagging being optimized by LLVM), but it does make
IR for the interpreter slightly more efficient.
---
 src/Lean/Compiler/IR/ToIR.lean                  |  2 +-
 tests/lean/4240.lean.expected.out               | 10 ++++------
 tests/lean/computedFieldsCode.lean.expected.out | 10 ++++------
 3 files changed, 9 insertions(+), 13 deletions(-)

diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index 27c6093123..e0d06e672a 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -208,7 +208,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
             return code
           else
             mkExpr (.fap name irArgs)
-        else if let some scalarType ← lowerEnumToScalarType? ctorVal.name then
+        else if let some scalarType ← lowerEnumToScalarType? ctorVal.induct then
           assert! args.isEmpty
           let var ← bindVar decl.fvarId
           return .vdecl var scalarType (.lit (.num ctorVal.cidx)) (← lowerCode k)
diff --git a/tests/lean/4240.lean.expected.out b/tests/lean/4240.lean.expected.out
index 4693783eb0..83a83e685f 100644
--- a/tests/lean/4240.lean.expected.out
+++ b/tests/lean/4240.lean.expected.out
@@ -2,13 +2,11 @@
     def MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 (x_1 : @& obj) : u8 :=
       case x_1 : obj of
       MyOption.none →
-        let x_2 : obj := ctor_0[Bool.false];
-        let x_3 : u8 := unbox x_2;
-        ret x_3
+        let x_2 : u8 := 0;
+        ret x_2
       MyOption.some →
-        let x_4 : obj := ctor_1[Bool.true];
-        let x_5 : u8 := unbox x_4;
-        ret x_5
+        let x_3 : u8 := 1;
+        ret x_3
     def isSomeWithInstanceNat (x_1 : @& obj) : u8 :=
       let x_2 : usize := 0;
       let x_3 : obj := Array.uget ◾ x_1 x_2 ◾;
diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out
index 9bf7a277c6..6452a084e6 100644
--- a/tests/lean/computedFieldsCode.lean.expected.out
+++ b/tests/lean/computedFieldsCode.lean.expected.out
@@ -175,13 +175,11 @@
     def g (x_1 : @& obj) : u8 :=
       case x_1 : obj of
       Exp.a3._impl →
-        let x_2 : obj := ctor_1[Bool.true];
-        let x_3 : u8 := unbox x_2;
-        ret x_3
+        let x_2 : u8 := 1;
+        ret x_2
       default →
-        let x_4 : obj := ctor_0[Bool.false];
-        let x_5 : u8 := unbox x_4;
-        ret x_5
+        let x_3 : u8 := 0;
+        ret x_3
     def g._boxed (x_1 : obj) : obj :=
       let x_2 : u8 := g x_1;
       dec x_1;