From c0079fd9ddbf065fe51af7a009ab46d5fbbd3234 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 14 Jul 2025 12:58:01 -0700
Subject: [PATCH] perf: allow boxed scalars passed to scalar params to be
 borrowed (#9360)

---
 src/Lean/Compiler/IR/Borrow.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean
index 5315bfc548..f1f089fb46 100644
--- a/src/Lean/Compiler/IR/Borrow.lean
+++ b/src/Lean/Compiler/IR/Borrow.lean
@@ -196,7 +196,7 @@ def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit :=
   xs.size.forM fun i _ => do
     let x := xs[i]
     let p := ps[i]!
-    unless p.borrow do ownArg x
+    unless p.borrow || p.ty.isScalar do ownArg x
 
 /-- For each xs[i], if xs[i] is owned, then mark ps[i] as owned.
    We use this action to preserve tail calls. That is, if we have