perf: handle match_same_ctor.het similar to matchers in compiler

[hargoniX]

This PR optimizes the handling of match_same_ctor.het to make it emit nice match trees as opposed to unoptimized CPS style code.

match_same_ctor.het is essentially a specialized kind of matcher where we know that two objects are built from the same constructor and we wish to call a continuation on their data. This means for every constructor that contains data het takes one closure as an argument. Then after matching on one of the objects every closure but the one relevant for the match is released in every match arm, causing quadratic code generation. This PR ensures that the het declarations get inlined and then further processed by ordinary matcher and casesOn compilation, thereby removing all of the continuations from the compiled code.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 1140ac1 against e2b500b are in! @hargoniX

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

Small changes (92🟥)

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

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for a513f68 against e2b500b are in. There are no significant changes. @Garmelon @hargoniX

• 🟥 build//instructions: +1.3G (+0.01%)

Small changes (2✅, 2🟥)

• 🟥 build/module/Lean.Compiler.LCNF.Main//instructions: +37.8M (+0.80%)
• 🟥 build/module/Lean.Compiler.LCNF.ToDecl//instructions: +106.3M (+2.71%) (reduced significance based on *//lines)
• ✅ compiled/binarytrees.st//task-clock: -167ms (-5.73%)
• ✅ compiled/binarytrees.st//wall-clock: -167ms (-5.71%)

[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 e2b500b204cacbb3149f42feda880c8bdfcab7db --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-09 15:28:48)

[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 e2b500b204cacbb3149f42feda880c8bdfcab7db --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-09 15:28:50)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for a513f68 against e2b500b are in. There are no significant changes. @hargoniX

• 🟥 build//instructions: +1.3G (+0.01%)

Small changes (2✅, 2🟥)

• 🟥 build/module/Lean.Compiler.LCNF.Main//instructions: +37.8M (+0.80%)
• 🟥 build/module/Lean.Compiler.LCNF.ToDecl//instructions: +106.3M (+2.71%) (reduced significance based on *//lines)
• ✅ compiled/binarytrees.st//task-clock: -167ms (-5.73%)
• ✅ compiled/binarytrees.st//wall-clock: -167ms (-5.71%)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 1bca92e against e2b500b are in. Significant changes detected! @hargoniX

• ✅ build//instructions: -30.3G (-0.24%)

Large changes (1✅)

• ✅ elab/big_do//instructions: -153.7M (-0.62%)

Medium changes (2✅)

• ✅ elab/big_beq//instructions: -197.9M (-1.96%)
• ✅ elab/big_beq_rec//instructions: -290.6M (-1.52%)

Small changes (346✅, 2🟥)

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