Lean 4.22.0 performance regression with kernel type checking

Stream: general

[RexWang]

Hi. I found a Lean proof that completes in seconds on Lean versions < 4.22.0, but takes about 84s on Lean versions ≥ 4.22.0.

Here's the minimal code to reproduce the issue:

import Mathlib

-- set_option debug.skipKernelTC true

def a := Finset.image (fun n ↦ n * n) (Finset.Icc 1 1000)

theorem weird_code : {1} ∪ a = a := by
  unfold a
  simp [Finset.union_sdiff_self_eq_union]

#print axioms weird_code

Also, a note from @Thomas Zhu: Adding the debug option debug.skipKernelTC would allow one to skip the kernel check, making the proof complete immediately. However, this option can result in false positives and should be avoided in practice.

Does anyone have ideas about what might be happening behind the scenes that causes this performance regression?