From e9df183e872779dd12b7ef0861e72e08be70acca Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 11 Aug 2025 22:27:35 -0700
Subject: [PATCH] perf: avoid ref count increments for borrowed array accesses
 (#9866)

---
 src/Lean/Compiler/IR/RC.lean | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean
index 3743b4a751..6a8d3959c6 100644
--- a/src/Lean/Compiler/IR/RC.lean
+++ b/src/Lean/Compiler/IR/RC.lean
@@ -70,6 +70,12 @@ private partial def visitFnBody (b : FnBody) : M Unit := do
     match e with
     | .proj _ parent =>
       addDerivedValue parent x
+    | .fap ``Array.getInternal args =>
+      if let .var parent := args[1]! then
+        addDerivedValue parent x
+    | .fap ``Array.get!Internal args =>
+      if let .var parent := args[2]! then
+        addDerivedValue parent x
     | .reset _ x =>
       removeFromParent x
     | _ => pure ()
@@ -351,7 +357,13 @@ private def processVDecl (ctx : Context) (z : VarId) (t : IRType) (v : Expr) (b
     | .fap f ys =>
       let ps := (getDecl ctx f).params
       let b  := addDecAfterFullApp ctx ys ps b bLiveVars
-      let b  := .vdecl z t v b
+      let v  :=
+        if f == ``Array.getInternal && bLiveVars.borrows.contains z then
+          .fap ``Array.getInternalBorrowed ys
+        else if f == ``Array.get!Internal && bLiveVars.borrows.contains z then
+          .fap ``Array.get!InternalBorrowed ys
+        else v
+      let b := .vdecl z t v b
       addIncBefore ctx ys ps b bLiveVars
     | .ap x ys =>
       let ysx := ys.push (.var x) -- TODO: avoid temporary array allocation