slow typeclass synthesis: takes 16000 heartbeats to fail on NonUnitalNonAssocSemiring (elementalStarAlgebra ℂ x)

[semorrison]

import Mathlib

/--
error: failed to synthesize
  NonUnitalNonAssocSemiring ↥(elementalStarAlgebra ℂ x)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (16000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
-/
#guard_msgs in
set_option synthInstance.maxHeartbeats 16000 in
variable {A : Type} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A]
  [CstarRing A] [StarModule ℂ A] (x : A) in
#synth NonUnitalNonAssocSemiring (elementalStarAlgebra ℂ x)

-- This gets slightly worse on `nightly-testing` after https://github.com/leanprover/lean4/pull/3807,
-- and causes the simpNF failure on `elementalStarAlgebra.characterSpaceToSpectrum_coe`

[mattrobball]

Also fixed by leanprover/lean4#4085