From fb1dc9112b2f6b66d54aaf39ac030dae7153c822 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 23 Mar 2026 22:39:17 +0100
Subject: [PATCH] perf: forward and backward borrow propagation is non-forced
 (#13066)

This PR changes the behavior of forward and backward projection
propagation in the context of user defined borrows. The reason to have
them be "forced" override (i.e. override user annotations as well) was
that a user annotated borrowed value can potentially flow into a
reset-reuse transitively through a projection and must thus have
accurate reference count. The reasons that this is no longer necessary
are:
1. Forward never had to be forced anyways, it can only affect the `z` in
`let z := oproj x i` which can't be annotated by a user
2. Backward is no longer necessary as the forward propagator for user
annotations prevents the reset-reuse insertion from working with values
that have user defined borrow annotations entirely.
---
 src/Lean/Compiler/LCNF/InferBorrow.lean   | 12 +++++++++---
 tests/elab/lcnf_borrow_expected_type.lean |  4 ----
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/InferBorrow.lean b/src/Lean/Compiler/LCNF/InferBorrow.lean
index a95055d2da..73c65a466a 100644
--- a/src/Lean/Compiler/LCNF/InferBorrow.lean
+++ b/src/Lean/Compiler/LCNF/InferBorrow.lean
@@ -243,13 +243,19 @@ def OwnReason.isForced (reason : OwnReason) : Bool :=
   -- All of these reasons propagate through ABI decisions and can thus safely be ignored as they
   -- will be accounted for by the reference counting pass.
   | .constructorArg .. | .functionCallArg .. | .fvarCall .. | .partialApplication ..
-  | .jpArgPropagation .. => false
+  | .jpArgPropagation ..
+  -- forward propagation can never affect a user-annotated parameter
+  | .forwardProjectionProp ..
+  -- backward propagation on a user-annotated parameter is only necessary if the projected value
+  -- directly flows into a reset-reuse. However, the borrow annotation propagator ensures this
+  -- situation never arises
+  | .backwardProjectionProp .. => false
   -- Results of functions and constructors are naturally owned.
   | .constructorResult .. | .functionCallResult ..
   -- We cannot pass borrowed values to reset or have borrow annotations destroy tail calls for
   -- correctness reasons.
-  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation .. | .ownedAnnotation
-  | .forwardProjectionProp .. | .backwardProjectionProp .. => true
+  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation ..
+  | .ownedAnnotation => true
 
 /--
 Infer the borrowing annotations in a SCC through dataflow analysis.
diff --git a/tests/elab/lcnf_borrow_expected_type.lean b/tests/elab/lcnf_borrow_expected_type.lean
index 5b5edb9ef9..fef9a3d711 100644
--- a/tests/elab/lcnf_borrow_expected_type.lean
+++ b/tests/elab/lcnf_borrow_expected_type.lean
@@ -139,8 +139,6 @@ structure Quad where
 /-- Only traverses → parameter stays borrowed. -/
 @[noinline] def measuree (xs : List Nat) : Nat := xs.length
 
-/-
-
 /--
 trace: [Compiler.explicitRc] size: 22
     def cascadeDemo @&t : tobj :=
@@ -257,5 +255,3 @@ def preserveTailCall (x : @&Prod Nat Nat) (a : Nat) : Nat :=
   match a with
   | 0 => x.fst
   | a + 1 => preserveTailCall (mkNewProd x a) a
-
--/