perf: tagged values can be interpreted as borrowed

[hargoniX]

This PR informs the RC optimizer that tagged values can also be considered as "borrowed" in the sense that we do not need to consider them as owned values for the borrow analysis (they do of course not have an allocation they actually borrow from).

Implementation note: For the derived borrows analysis we instead just disregard parents that are tagged. Note that we cannot match on types in passes before boxing as the IR might still be type incorrect at that point.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 958d50d against c71a0ea are in. Significant changes detected! @hargoniX

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

Large changes (1✅)

• ✅ compiled/phashmap//instructions: -254.1M (-2.60%)

Medium changes (2✅, 1🟥)

• ✅ compiled/parser//instructions: -34.9M (-0.09%)
• 🟥 elab/big_match_nat//instructions: +134.8M (+2.55%)
• ✅ elab/cbv_arm_ldst//instructions: -1.2G (-1.51%)

Small changes (10✅, 8🟥)

• ✅ build/module/Init.Data.Array.Lex.Lemmas//instructions: -44.8M (-0.39%)
• 🟥 build/module/Lean.Compiler.LCNF.ExplicitRC//instructions: +153.7M (+1.78%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Compiler.LCNF.PropagateBorrow//instructions: +27.6M (+0.89%)
• 🟥 build/module/Lean.Elab.Tactic.Grind.Config//instructions: +32.1M (+0.44%)
• 🟥 build/module/Lean.Server.FileWorker.SemanticHighlighting//instructions: +41.0M (+0.46%)
• 🟥 build/module/Lean.Util.Recognizers//instructions: +44.8M (+2.19%)
• ✅ build/module/Std.Data.DHashMap.Internal.RawLemmas//instructions: -986.9M (-0.37%)
• ✅ build/module/Std.Data.DHashMap.RawLemmas//instructions: -534.4M (-0.36%)
• ✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -441.1M (-0.21%)
• ✅ build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: -111.7M (-0.15%)
• ✅ build/module/Std.Data.Internal.List.Associative//instructions: -246.3M (-0.28%)
• ✅ elab/big_do//instructions: -19.6M (-0.08%)
• 🟥 elab/big_match_nat_split//instructions: +66.7M (+0.57%)
• ✅ elab/big_omega//instructions: -64.4M (-0.27%)
• ✅ elab/big_omega_MT//instructions: -70.1M (-0.29%)
• 🟥 elab/bv_decide_realworld//wall-clock: +55ms (+4.86%)
• 🟥 elab/riscv-ast//instructions: +733.3M (+0.71%)
• ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -1.0G (-0.39%)

[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 c71a0ea9a51a90bfad5f1c53192e3736742617f4 --onto 4786e082dca22873d14d2a5b9b7c8843380c6e78. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-27 11:36:30)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 79ac2d93b054fab824534be6c92a2f086a892165 --onto 4786e082dca22873d14d2a5b9b7c8843380c6e78. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-27 16:34:14)

[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 c71a0ea9a51a90bfad5f1c53192e3736742617f4 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-27 11:36:31)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 79ac2d93b054fab824534be6c92a2f086a892165 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-27 16:34:16)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for e486d31 against e06fc0b are in. Significant changes detected! @hargoniX

• 🟥 build//instructions: +293.6M (+0.00%)

Large changes (2✅)

• ✅ compiled/phashmap//instructions: -254.6M (-2.60%)
• ✅ mvcgen/sym/MatchIota/50/kernel//wall-clock: -1ms (-5.56%)

Medium changes (2✅)

• ✅ compiled/parser//instructions: -34.5M (-0.09%)
• ✅ elab/cbv_arm_ldst//instructions: -1.1G (-1.50%)

Small changes (8✅, 7🟥)

• ✅ build/module/Init.Data.Array.Lex.Lemmas//instructions: -41.5M (-0.36%)
• 🟥 build/module/Lake.Load.Toml//instructions: +53.3M (+0.36%)
• 🟥 build/module/Lean.Compiler.LCNF.ExplicitRC//instructions: +535.2M (+6.20%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Compiler.LCNF.InferBorrow//instructions: +34.1M (+0.48%)
• 🟥 build/module/Lean.Compiler.LCNF.PropagateBorrow//instructions: +30.9M (+0.99%)
• 🟥 build/module/Lean.Elab.BuiltinTerm//instructions: +38.0M (+0.34%)
• 🟥 build/module/Lean.Meta.Match.Match//instructions: +44.4M (+0.25%)
• ✅ build/module/Std.Data.DHashMap.Internal.RawLemmas//instructions: -1.1G (-0.42%)
• ✅ build/module/Std.Data.DHashMap.RawLemmas//instructions: -486.1M (-0.33%)
• ✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -417.4M (-0.19%)
• ✅ build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: -117.2M (-0.15%)
• 🟥 build/profile/compilation (LCNF impure)//wall-clock: +1s (+5.06%)
• ✅ elab/big_omega//instructions: -69.0M (-0.29%)
• ✅ elab/big_omega_MT//instructions: -72.7M (-0.30%)
• ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -957.2M (-0.37%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 9ba9497 against e06fc0b 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 ab77b10 against e06fc0b 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 88fb9b1 against 79ac2d9 are in. Significant changes detected! @hargoniX

• ✅ build//instructions: -1.7G (-0.01%)

Large changes (1✅)

• ✅ compiled/phashmap//instructions: -254.2M (-2.60%)

Medium changes (2✅)

• ✅ compiled/parser//instructions: -33.9M (-0.09%)
• ✅ elab/cbv_arm_ldst//instructions: -1.1G (-1.47%)

Small changes (8✅, 3🟥)

• ✅ build/module/Init.Data.Array.Lex.Lemmas//instructions: -42.1M (-0.37%)
• ✅ build/module/Init.Data.Range.Polymorphic.Lemmas//instructions: -112.1M (-0.22%)
• 🟥 build/module/Lean.Compiler.LCNF.ExplicitRC//instructions: +91.6M (+1.06%)
• 🟥 build/module/Lean.Compiler.LCNF.PropagateBorrow//instructions: +32.8M (+1.05%)
• ✅ build/module/Std.Data.DHashMap.Internal.RawLemmas//instructions: -1.1G (-0.41%)
• ✅ build/module/Std.Data.DHashMap.RawLemmas//instructions: -489.0M (-0.33%)
• ✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -433.2M (-0.20%)
• 🟥 build/profile/compilation (LCNF impure)//wall-clock: +1s (+3.62%)
• ✅ elab/big_omega//instructions: -67.4M (-0.28%)
• ✅ elab/big_omega_MT//instructions: -69.2M (-0.29%)
• ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -1.0G (-0.40%)