feat: respect user provided borrow annotations

[hargoniX]

This PR enables support for respecting user provided borrow annotations. This allows user to mark arguments of their definitions or local functions with (x : @&Ty) and have the borrow inference try its best to preserve this annotation, thus potentially reducing RC pressure. Note that in some cases this might not be possible. For example, the compiler prioritizes preserving tail calls over preserving borrow annotations. A precise reasoning of why the compiler chose to make its inference decisions can be obtained with trace.Compiler.inferBorrow.

The implementation consists of two parts:

1. A propagator in ToLCNF. This is required because the elaborator does not place the borrow annotations in the function binders themselves but just in type annotations of let binders/global declarations while LCNF expects them in the lambda variable binders themselves. Thus ToLCNF now implements a (very weak but strong enough for this purpose) propagator of the borrow annotations of a type annotation into the variable binders of the term affected by the annotations
2. A weakening of the InferBorrow heuristic. It now has a set of "forced" and "non-forced" reasons to mark a variable as owned instead of borrowed. If a variable is user annotated as borrowed, it will only be marked as owned if the reason is a forced one, e.g. preservation of tail calls.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for d72df3e against 68ea28c are in! @hargoniX

• 🟥 build//instructions: +2.1G (+0.02%)

Small changes (2🟥)

• 🟥 build/module/Lean.Compiler.LCNF.InferBorrow//instructions: +395.0M (+6.04%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Compiler.LCNF.ToLCNF//instructions: +395.3M (+2.09%) (reduced significance based on *//lines)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 68ea28c24f9ce74272a8f6aa88ad5bbc70f4034f --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-06 17:27:51)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-16 11:05:40)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 091726034110408555f0bca58cfebbf39b524147 --onto 6714601ee4a123fef0f6ff3e44f01086ba78dfce. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-18 10:09:57)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5e1b6ed663d03dccf8beda8352e0822b603dfdd9 --onto 87180a09c49c91577e54284703c73c5ca76be126. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-20 10:15:35)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 68ea28c24f9ce74272a8f6aa88ad5bbc70f4034f --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-06 17:27:53)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-16 11:05:42)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 091726034110408555f0bca58cfebbf39b524147 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-18 10:09:59)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5e1b6ed663d03dccf8beda8352e0822b603dfdd9 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-20 10:15:38)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for d939de5 against 0917260 are in. Significant changes detected! @hargoniX

• 🟥 build exited with code 2

Large changes (5✅)

• ✅ elab/big_do//instructions: -604.3M (-2.46%)
• ✅ elab/grind_bitvec2//instructions: -3.6G (-1.77%)
• ✅ elab/grind_list2//instructions: -1.3G (-2.31%)
• ✅ elab/simp_local//instructions: -1.5G (-3.41%)
• ✅ size/compile/.out//bytes: -176MiB (-9.19%)

Medium changes (17✅)

• ✅ elab/big_match_nat_split//instructions: -120.2M (-1.02%)
• ✅ elab/big_omega//instructions: -180.2M (-0.75%)
• ✅ elab/big_omega_MT//instructions: -186.4M (-0.78%)
• ✅ elab/big_struct_dep1//instructions: -121.6M (-1.97%)
• ✅ elab/bv_decide_rewriter//instructions: -161.1M (-1.51%)
• ✅ elab/cbv_arm_ldst//instructions: -683.4M (-0.89%)
• ✅ elab/cbv_divisors//instructions: -680.6M (-1.23%)
• ✅ elab/cbv_leroy//instructions: -810.3M (-1.64%)
• ✅ elab/iterators//instructions: -46.8M (-1.61%)
• ✅ elab/riscv-ast//instructions: -1.1G (-1.12%)
• ✅ elab/simp_bubblesort_256//instructions: -302.5M (-2.42%)
• ✅ interpreted/iterators//instructions: -47.4M (-0.13%)
• ✅ lake/inundation/config elab//instructions: -33.4M (-1.29%)
• ✅ misc/import Init.Data.BitVec.Lemmas//instructions: -1.5G (-1.18%)
• ✅ misc/import Init.Data.List.Sublist//instructions: -142.8M (-1.30%)
• ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -2.2G (-0.83%)
• ✅ misc/import Std.Data.Internal.List.Associative//instructions: -1.1G (-1.40%)

Small changes (20✅, 2🟥)

Too many entries to display here. View the full report on radar instead.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 162987d against 0917260 are in. Significant changes detected! @hargoniX

• ✅ build//instructions: -153.9G (-1.23%)

Large changes (9✅)

• ✅ elab/big_do//instructions: -603.7M (-2.46%)
• ✅ elab/grind_bitvec2//instructions: -3.5G (-1.75%)
• ✅ elab/grind_list2//instructions: -1.3G (-2.34%)
• ✅ elab/simp_local//instructions: -1.5G (-3.40%)
• ✅ size/all/.c//lines: -181.1k (-1.64%)
• ✅ size/all/.ir//bytes: -8MiB (-2.45%)
• ✅ size/compile/.out//bytes: -176MiB (-9.19%)
• ✅ size/install//bytes: -25MiB (-1.01%)
• ✅ size/libleanshared.so//bytes: -7MiB (-5.11%)

Medium changes (30✅)

Too many entries to display here. View the full report on radar instead.

Small changes (1169✅, 3🟥)

Too many entries to display here. View the full report on radar instead.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 22476d4 against 0917260 are in. Significant changes detected! @hargoniX

• 🟥 build exited with code 2
• 🟥 other exited with code 2

No significant changes detected.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 74b71dc against 0917260 are in. Significant changes detected! @hargoniX

• ✅ build//instructions: -169.6G (-1.35%)

Large changes (9✅)

• ✅ elab/big_do//instructions: -629.9M (-2.57%)
• ✅ elab/grind_bitvec2//instructions: -4.1G (-2.03%)
• ✅ elab/grind_list2//instructions: -1.4G (-2.63%)
• ✅ elab/simp_local//instructions: -1.6G (-3.62%)
• ✅ size/all/.c//lines: -228.1k (-2.06%)
• ✅ size/all/.ir//bytes: -9MiB (-2.75%)
• ✅ size/compile/.out//bytes: -184MiB (-9.64%)
• ✅ size/install//bytes: -26MiB (-1.06%)
• ✅ size/libleanshared.so//bytes: -8MiB (-5.50%)

Medium changes (37✅)

Too many entries to display here. View the full report on radar instead.

Small changes (1229✅, 2🟥)

Too many entries to display here. View the full report on radar instead.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 3b22c54 against 5e1b6ed are in. Significant changes detected! @hargoniX

• ✅ build//instructions: -11.7G (-0.10%)

Medium changes (1✅)

• ✅ elab/simp_local//instructions: -230.6M (-0.51%)

Small changes (21✅, 3🟥)

Too many entries to display here. View the full report on radar instead.