slow typeclass synthesis: takes 15000 heartbeats to fail in SMul ℚᵐᵒᵖ α

[kim-em]

import Mathlib

open Matrix in
/--
error: failed to synthesize
  SMul ℚᵐᵒᵖ α
(deterministic) timeout at 'typeclass', maximum number of heartbeats (15000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
-/
#guard_msgs in
set_option synthInstance.maxHeartbeats 15000 in
example [AddCommGroup α] [StarAddMonoid α] [Module ℚ α] (c : ℚ)
    (M : Matrix m n α) : (c • M)ᴴ = c • Mᴴ := by simp

This then gets slightly worse after leanprover/lean4#3807, and thereafter causes the simpNF linter to fail on Matrix.conjTranspose_rat_smul.

[mattrobball]

This appears fixed by leanprover/lean4#4085

[jcommelin]

I confirm that this now works

import Mathlib

variable {α m n : Type*}

open Matrix in
set_option synthInstance.maxHeartbeats 9000 in
example [AddCommGroup α] [StarAddMonoid α] [Module ℚ α] (c : ℚ)
    (M : Matrix m n α) : (c • M)ᴴ = c • Mᴴ := by simp