From d4e11f754a9997e498b055e346d5ca1427e2e29c Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Fri, 11 Jul 2025 09:46:48 -0700
Subject: [PATCH] chore: clean up loop over ctor fields (#9313)

---
 src/Lean/Compiler/IR/ToIR.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index 5a484c0d70..413f165844 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -178,9 +178,11 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
       let irArgs := irArgs.extract (start := ctorVal.numParams)
       let objArgs : Array Arg ← do
         let mut result : Array Arg := #[]
-        for i in *...fields.size do
-          if fields[i]! matches .object .. then
+        for h : i in *...fields.size do
+          match fields[i] with
+          | .object .. =>
             result := result.push irArgs[i]!
+          | .usize .. | .scalar .. | .irrelevant => pure ()
         pure result
       let objVar ← bindVar decl.fvarId
       let rec lowerNonObjectFields (_ : Unit) : M FnBody :=