debug simp max recursion depth reached

Stream: mathlib4

[Winston Yin]

How can I look under the hood and debug a maximum recursion depth has been reached error when using simp? My wme is:

import Mathlib.Data.FunLike.Basic

variable {M N P F : Type _} [Mul M] [Mul N]

structure MulHom (M : Type _) (N : Type _) [Mul M] [Mul N] where
  toFun : M → N
  map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y

infixr:25 " →ₙ* " => MulHom

class MulHomClass (F : Type _) (M N : outParam <| Type _)
  [outParam <| Mul M] [outParam <| Mul N] extends FunLike F M fun _ => N where
  map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y

instance MulHom.mulHomClass : MulHomClass (M →ₙ* N) M N where
  coe := MulHom.toFun
  coe_injective' f g h := by cases f; cases g; congr
  map_mul := MulHom.map_mul'

@[simp]
theorem map_mul [MulHomClass F M N] (f : F) (x y : M) : f (x * y) = f x * f y :=
  MulHomClass.map_mul f x y

def MulHom.comp [Mul M] [Mul N] [Mul P] (hnp : N →ₙ* P) (hmn : M →ₙ* N) : M →ₙ* P where
  toFun := hnp ∘ hmn
  map_mul' x y := by simp
-- works: by simp only [Function.comp_apply, map_mul]

[Mario Carneiro]

set_option trace.Meta.Tactic.simp.rewrite true has some profitable things to say on this example:

[Meta.Tactic.simp.rewrite] @FunLike.coe_eq_coe_fn:1000, FunLike.coe ==> fun f => FunLike.coe f
[Meta.Tactic.simp.rewrite] @FunLike.coe_eq_coe_fn:1000, FunLike.coe ==> fun f => FunLike.coe f
[Meta.Tactic.simp.rewrite] @FunLike.coe_eq_coe_fn:1000, FunLike.coe ==> fun f => FunLike.coe f
[Meta.Tactic.simp.rewrite] @FunLike.coe_eq_coe_fn:1000, FunLike.coe ==> fun f => FunLike.coe f

[Mario Carneiro]

coe_eq_coe_fn is a bad simp lemma because it uses FunLike.coe on the RHS again (instead of using coe like in lean 3)