slow typeclass synthesis: takes 19000 heartbeats to fail in AddHomClass (AbsoluteValue ℂ ℝ) ?m ?m

[semorrison]

import Mathlib

open Complex in
/--
error: failed to synthesize
  AddHomClass (AbsoluteValue ℂ ℝ) ?m ?m
(deterministic) timeout at 'typeclass', maximum number of heartbeats (19000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
-/
#guard_msgs in
set_option synthInstance.maxHeartbeats 19000 in
example (x : ℝ) : abs (cos x + sin x * I) = 1 := by simp

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

[mattrobball]

This one gets very fast with leanprover/lean4#4085