From 9e913a29dec112d065ba51fdc8e7c748fe93cd6b Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 16 Jun 2025 16:13:07 -0700
Subject: [PATCH] chore: remove redundant headBeta call (#8824)

---
 src/Lean/Compiler/IR/ToIR.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index fc5b6cc451..d67fdcb2e7 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -110,7 +110,8 @@ def lowerType (e : Lean.Expr) : M IRType := do
       else
         return .object
   | .app f _ =>
-    if let .const name _ := f.headBeta then
+    -- All mono types are in headBeta form.
+    if let .const name _ := f then
       if let some scalarType ← lowerEnumToScalarType name then
         return scalarType
       else