perf: type class experiment

[leodemoura]

This PR is just an experiment for testing a modification in the type class resolution procedure. It tries to postpone some isDefEq tests at tryResolve. It addresses problematic cases such as trying to synthesize

AddRightCancel (Kernel α Ω)

using candidate

IsRightCancelAdd.toGrindAddRightCancel

[leodemoura]

!bench

[leanprover-radar]

Benchmark results for 6679791 against 1422c82 are in. There are significant results. @leodemoura

• ✅ build//instructions: -47.5G (-0.42%)

Large changes (2✅, 2🟥)

• ✅ elab/cbv_decide//instructions: -2.0G (-4.63%)
• ✅ elab/grind_list2//instructions: -1.3G (-2.85%)
• 🟥 vcgen/AddSubCancelSimp/700/kernel//wall-clock: +26ms (+23.21%)
• 🟥 vcgen/AddSubCancelSimp/700/vcgen//wall-clock: +150ms (+15.59%)

Medium changes (7✅, 6🟥)

• ✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -2.3G (-1.21%)
• ✅ build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: -1.6G (-2.38%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.TreeMap.Raw.Lemmas//instructions: -1.0G (-2.59%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: +2.7G (+4.66%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul//instructions: +1.3G (+6.40%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: +4.7G (+5.09%) (reduced significance based on absolute threshold)
• ✅ elab/big_do//instructions: -59.0M (-0.31%)
• 🟥 elab/big_omega//instructions: +226.1M (+1.06%)
• 🟥 elab/big_omega_MT//instructions: +232.2M (+1.08%)
• ✅ elab/grind_bitvec2//instructions: -2.4G (-1.61%)
• ✅ misc/import Std.Data.Internal.List.Associative//instructions: -1.0G (-1.49%)
• 🟥 vcgen/AddSubCancelSimp/400/vcgen//wall-clock: +80ms (+14.98%)
• ✅ vcgen/MatchIota/1500/vcgen//wall-clock: -19ms (-9.36%)

Small changes (511✅, 71🟥)

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

[leodemoura]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@94e88be against leanprover-community/mathlib4-nightly-testing@de3a9cf are in. There are significant results. @leodemoura

• 🟥 main exited with code 1

No significant changes detected.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-07-07 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-07-08 03:06:01)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-14318 build failed against this PR. (2026-07-08 03:26:34) View Log
• 💥 Mathlib branch lean-pr-testing-14318 build failed against this PR. (2026-07-08 14:56:54) View Log

[leodemoura]

!bench

[leodemoura]

!bench mathlib

[leanprover-radar]

Benchmark results for 9f1bdd8 against 1422c82 are in. There are significant results. @leodemoura

• ✅ build//instructions: -86.4G (-0.77%)

Large changes (1✅)

• ✅ elab/cbv_decide//instructions: -2.0G (-4.59%)

Medium changes (11✅)

• ✅ build//instructions: -86.4G (-0.77%)
• ✅ build/module/Init.Data.BitVec.Lemmas//instructions: -1.0G (-0.83%)
• ✅ build/module/Lean.Elab.Do.Legacy//instructions: -1.2G (-2.38%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.PrettyPrinter.Delaborator.Builtins//instructions: -1.1G (-2.81%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -2.0G (-1.06%)
• ✅ build/module/Std.Data.Internal.List.Associative//instructions: -1.1G (-1.39%)
• ✅ build/profile/typeclass inference//wall-clock: -11s (-7.21%)
• ✅ elab/grind_bitvec2//instructions: -1.5G (-1.05%)
• ✅ elab/grind_list2//instructions: -688.6M (-1.54%)
• ✅ misc/import Init.Data.BitVec.Lemmas//instructions: -950.7M (-0.83%)
• ✅ misc/import Std.Data.Internal.List.Associative//instructions: -1.1G (-1.61%)

and 1 hidden

Small changes (710✅, 3🟥)

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

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@94e88be against leanprover-community/mathlib4-nightly-testing@de3a9cf are in. (These commits have already been benchmarked in a previous command.) There are significant results. @leodemoura

• 🟥 main exited with code 1

No significant changes detected.

[leodemoura]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@e2f5e42 against leanprover-community/mathlib4-nightly-testing@de3a9cf are in. There are significant results. @leodemoura

• 🟥 main exited with code 1

No significant changes detected.

[leodemoura]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@e2f5e42 against leanprover-community/mathlib4-nightly-testing@de3a9cf are in. (These commits have already been benchmarked in a previous command.) There are significant results. @leodemoura

• 🟥 main exited with code 1

No significant changes detected.

[leodemoura]

!bench

[leanprover-radar]

Benchmark results for f0d26ed against 1422c82 are in. There are significant results. @leodemoura

• ✅ build//instructions: -85.3G (-0.76%)

Large changes (1✅)

• ✅ elab/cbv_decide//instructions: -2.0G (-4.57%)

Medium changes (10✅)

• ✅ build//instructions: -85.3G (-0.76%)
• ✅ build/module/Init.Data.BitVec.Lemmas//instructions: -1.0G (-0.83%)
• ✅ build/module/Lean.Elab.Do.Legacy//instructions: -1.1G (-2.36%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.PrettyPrinter.Delaborator.Builtins//instructions: -1.1G (-2.81%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -2.0G (-1.06%)
• ✅ build/module/Std.Data.Internal.List.Associative//instructions: -1.1G (-1.35%)
• ✅ elab/grind_bitvec2//instructions: -1.4G (-0.93%)
• ✅ elab/grind_list2//instructions: -629.2M (-1.41%)
• ✅ misc/import Init.Data.BitVec.Lemmas//instructions: -1.0G (-0.89%)
• ✅ misc/import Std.Data.Internal.List.Associative//instructions: -1.1G (-1.64%)

and 1 hidden

Small changes (703✅, 5🟥)

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

[leodemoura]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@e058bab against leanprover-community/mathlib4-nightly-testing@de3a9cf are in. There are significant results. @leodemoura

• ✅ build//instructions: -5.2T (-3.21%)

Large changes (2✅)

• ✅ build//instructions: -5.2T (-3.21%)
• ✅ build/module/Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas//instructions: -19.7G (-16.52%)

and 1 hidden

Medium changes (230✅, 2🟥)

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

Small changes (1039✅, 2🟥)

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