perf: make high arity closures pass their arguments linearly if possible

[hargoniX]

This PR introduces new fast paths to high arity closure applications. Previously, they would always maintain ownership of their arguments as they pass them to their underlying function pointer, causing non-linearities. This PR introduces the same fast paths as with the other low arity closures for passing the arguments linearly if the closure is passed linearly.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 3d45db0 against 624fffa are in. There are significant results. @hargoniX

• 🟥 build//instructions: +14.2G (+0.13%)

Large changes (3🟥)

• 🟥 compiled/parser//instructions: +331.6M (+0.93%)
• 🟥 compiled/select//maxrss: +6MiB (+10.47%)
• 🟥 size/all/.cpp//lines: +261.0 (+0.91%)

Medium changes (5🟥)

• 🟥 compiled/rbmap//instructions: +8.0M (+0.10%)
• 🟥 compiled/rbmap_checkpoint2//instructions: +8.0M (+0.09%)
• 🟥 compiled/rbmap_fbip//instructions: +8.0M (+0.11%)
• 🟥 elab/lift_lets_spine//instructions: +130.0M (+1.93%)
• 🟥 interpreted/identifier_completion//maxrss: +18MiB (+2.47%)

Small changes (3✅, 33🟥)

• 🟥 build/module/Init.Control.Lawful.MonadAttach//instructions: +2.9M (+0.58%)
• 🟥 build/module/Init.Control.Lawful.MonadLift//instructions: +2.9M (+0.58%)
• 🟥 build/module/Init.Data.Array//instructions: +2.9M (+0.54%)
• 🟥 build/module/Init.Data.Dyadic//instructions: +2.9M (+0.56%)
• 🟥 build/module/Init.Data.Fin.MinMax//instructions: +2.9M (+0.50%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Fin.Package//instructions: +3.0M (+0.38%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Float.Model.Unpacked//instructions: +2.9M (+0.54%)
• 🟥 build/module/Init.Data.Int.DivMod//instructions: +2.8M (+0.59%)
• 🟥 build/module/Init.Data.Int.Package//instructions: +2.8M (+0.44%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Iterators.Combinators//instructions: +2.9M (+0.58%)
• 🟥 build/module/Init.Data.Iterators.Consumers//instructions: +2.9M (+0.57%)
• 🟥 build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic//instructions: +2.9M (+0.56%)
• 🟥 build/module/Init.Data.Iterators.Lemmas.Producers//instructions: +2.9M (+0.57%)
• 🟥 build/module/Init.Data.Iterators.Producers//instructions: +2.9M (+0.57%)
• 🟥 build/module/Init.Data.List.Sort//instructions: +2.8M (+0.58%)
• 🟥 build/module/Init.Data.Nat.Internal//instructions: +2.8M (+0.65%)
• 🟥 build/module/Init.Data.Nat.Package//instructions: +2.9M (+0.55%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Nat.Sqrt//instructions: +2.8M (+0.67%)
• 🟥 build/module/Init.Data.Sum//instructions: +2.8M (+0.58%)
• 🟥 build/module/Init.Data.UInt//instructions: +2.9M (+0.55%)
• and 16 more

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 282dbad against 624fffa are in. There are significant results. @hargoniX

• ✅ build//instructions: -24.3G (-0.22%)

Large changes (1✅, 1🟥)

• ✅ compiled/parser//instructions: -279.9M (-0.78%)
• 🟥 compiled/select//maxrss: +24MiB (+44.58%)

Medium changes (6✅)

• ✅ compiled/rbmap//instructions: -6.0M (-0.08%)
• ✅ compiled/rbmap_checkpoint2//instructions: -6.0M (-0.07%)
• ✅ compiled/rbmap_fbip//instructions: -6.0M (-0.09%)
• ✅ elab/lift_lets_binders//maxrss: -23MiB (-1.29%)
• ✅ elab/lift_lets_spine//instructions: -130.6M (-1.94%)
• ✅ size/all/.cpp//lines: -139.0 (-0.48%)

Small changes (39✅)

• ✅ build/module/Init.Control.Lawful.MonadAttach//instructions: -3.0M (-0.61%)
• ✅ build/module/Init.Control.Lawful.MonadLift//instructions: -3.0M (-0.61%)
• ✅ build/module/Init.Data.Array//instructions: -3.1M (-0.57%)
• ✅ build/module/Init.Data.Dyadic//instructions: -3.0M (-0.59%)
• ✅ build/module/Init.Data.Fin.MinMax//instructions: -3.3M (-0.57%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Fin.Package//instructions: -3.7M (-0.47%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Float.Model.Unpacked//instructions: -3.1M (-0.57%)
• ✅ build/module/Init.Data.FloatArray//instructions: -3.1M (-0.57%)
• ✅ build/module/Init.Data.Int.DivMod//instructions: -3.0M (-0.61%)
• ✅ build/module/Init.Data.Int.Package//instructions: -3.4M (-0.54%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Iterators.Combinators//instructions: -3.0M (-0.60%)
• ✅ build/module/Init.Data.Iterators.Consumers//instructions: -3.0M (-0.60%)
• ✅ build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic//instructions: -3.0M (-0.59%)
• ✅ build/module/Init.Data.Iterators.Lemmas.Producers//instructions: -3.0M (-0.60%)
• ✅ build/module/Init.Data.Iterators.Producers//instructions: -3.0M (-0.60%)
• ✅ build/module/Init.Data.List.Sort//instructions: -3.0M (-0.61%)
• ✅ build/module/Init.Data.List.SplitOn//instructions: -3.0M (-0.62%)
• ✅ build/module/Init.Data.Nat.Internal//instructions: -2.9M (-0.68%)
• ✅ build/module/Init.Data.Nat.Package//instructions: -3.1M (-0.60%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Nat.Sqrt//instructions: -2.9M (-0.70%)
• and 19 more