From 52ab0141cd0fbb9696981e09f67db587a76dfb78 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 30 Jun 2025 16:13:02 -0700
Subject: [PATCH] chore: share more code in toIRType (#9115)

---
 src/Lean/Compiler/IR/ToIRType.lean | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Compiler/IR/ToIRType.lean b/src/Lean/Compiler/IR/ToIRType.lean
index 5921c88369..686e52c36f 100644
--- a/src/Lean/Compiler/IR/ToIRType.lean
+++ b/src/Lean/Compiler/IR/ToIRType.lean
@@ -56,22 +56,21 @@ def toIRType (e : Lean.Expr) : CoreM IRType := do
     | ``Float => return .float
     | ``Float32 => return .float32
     | ``lcErased => return .irrelevant
-    | _ =>
-      if let some scalarType ← lowerEnumToScalarType? name then
-        return scalarType
-      else
-        return .object
+    | _ => nameToIRType name
   | .app f _ =>
     -- All mono types are in headBeta form.
     if let .const name _ := f then
-      if let some scalarType ← lowerEnumToScalarType? name then
-        return scalarType
-      else
-        return .object
+      nameToIRType name
     else
       return .object
   | .forallE .. => return .object
   | _ => panic! "invalid type"
+where
+  nameToIRType name := do
+    if let some scalarType ← lowerEnumToScalarType? name then
+      return scalarType
+    else
+      return .object
 
 inductive CtorFieldInfo where
   | irrelevant