Tracing simp that timeouts

Stream: mathlib4

[Yury G. Kudryashov]

I have a simp that timeouts with "maximum recursion depth has been reached". How do I debug/trace which lemmas does it apply? @Mario Carneiro @Gabriel Ebner ?

[Yury G. Kudryashov]

I tried some random set_option trace.Compiler.simp.* true, didn't work.

[Yury G. Kudryashov]

I'm talking about !4#2270

[Yury G. Kudryashov]

Probably, I introduced a simp cycle somewhere (why we don't see it elsewhere?)

[Reid Barton]

I think you want one or both of these instead

set_option trace.Meta.Tactic.simp true
set_option trace.Meta.Tactic.simp.rewrite true

[Yury G. Kudryashov]

Thanks! I found a cycle. Not sure if I have time to break it now.

[Yury G. Kudryashov]

The cycle is between MulHom.coe_mk and MulHom.toFun_eq_coe. It appears when it is applied to a MulHom which is reducibly equal to MulHom.mk _ _.

[Yury G. Kudryashov]

(in this case, it is MulEquiv.toMulHom _)

[Yury G. Kudryashov]

Why does MulHom.coe_mk simplify (e.toMulHom : _ → _) to e.toMulHom.toFun, not to e.toEquiv.toFun?

[Yury G. Kudryashov]

MulEquiv.toMulHom is defined as

@[reducible] def MulEquiv.toMulHom.{u_1, u_2} : {M : Type u_1} →
  {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → M →ₙ* N :=
fun M N [Mul M] [Mul N] self =>
  { toFun := self.toEquiv.toFun,
    map_mul' :=
      (_ : ∀ (x y : M), Equiv.toFun self.toEquiv (x * y) = Equiv.toFun self.toEquiv x * Equiv.toFun self.toEquiv y) }

[Yury G. Kudryashov]

And MulHom.coe_mk:

@[to_additive (attr := simp)]
theorem MulHom.coe_mk [Mul M] [Mul N] (f : M → N) (hmul) : (MulHom.mk f hmul : M → N) = f := rfl
#align mul_hom.coe_mk MulHom.coe_mk
#align add_hom.coe_mk AddHom.coe_mk

[Yury G. Kudryashov]

@Reid Barton @Mario Carneiro @Gabriel Ebner :up: