perf: do not inhibit caching of default-level match reduction

[Kha]

Resolves #2564.

Note that this does not resolve the same issue at reducible level, e.g. during simp. This would require adding a new cache (@leodemoura like I thought we would already need here but it turned out to be much more simple). But this should warrant separate motivation. In most non-trivial match cases like in #2564, it seems we do match on non-reducible functions.

[Kha]

(Speedup is ~100x for the specific example but as the old behavior is exponential, that's just one data point)

[leanprover-community-mathlib4-bot]

• ✅ Mathlib branch lean-pr-testing-2612 has successfully built against this PR. (2023-10-02 11:21:54) View Log
• ❌ Mathlib branch lean-pr-testing-2612 built against this PR, but testing failed. (2023-10-04 19:06:21) View Log
• ✅ Mathlib branch lean-pr-testing-2612 has successfully built against this PR. (2023-10-04 23:52:11) View Log

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 62f5ae7.
There were significant changes against commit 06e0577:

  Benchmark          Metric          Change
  ==================================================
- lake build clean   branch-misses     1.5% (13.7 σ)
- stdlib             type checking     1.1% (10.1 σ)
- stdlib             wall-clock        1.2% (10.6 σ)

[Kha]

Unclear if statistically significant?
!bench

[Kha]

mathlib4 comparison with master: http://speed.lean-fro.org/mathlib4/compare/e7b27246-a3e6-496a-b552-ff4b45c7236e/to/6cc64386-e156-4029-9d32-5f95588c85c1?hash1=f1a26d74c6f24f344bb4656785c9c24958df74da. No significant change overall, which makes sense given the relative lack of match in mathlib, but some significant improvements in a few specific files.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 62f5ae7.
There were significant changes against commit 06e0577:

  Benchmark          Metric          Change
  ==================================================
- lake build clean   branch-misses     1.5% (13.7 σ)
- stdlib             type checking     1.1% (10.1 σ)
- stdlib             wall-clock        1.2% (10.6 σ)

[collares]

This PR also fixes a timeout in the following example:

def dedup {α} [DecidableEq α] : List α → List α :=
List.foldr (fun x IH => if IH.all (· ≠ x) then x :: IH else IH) []

example : dedup (List.replicate 11 0) = [0] := rfl