Slow elaboration of simple equation with overloaded operator

[nomeata]

In the context of Terry Tao’s equational_theories project, we are look at a few thousand equations defined like Equation374794 here:

universe u

class Magma (α : Type u) where
  /-- `a ∘ b` computes a binary operation of `a` and `b`. -/
  op : α → α → α

@[inherit_doc] infixl:65 " ∘ "   => Magma.op

-- 48ms
abbrev Equation374794 (G : Type u) [Magma G] := ∀ x y z : G, x = (((y ∘ y) ∘ y) ∘ x) ∘ ((y ∘ y) ∘ z)

-- 1ms
abbrev Equation374794_ (G : Type u) [inst: Magma G] := ∀ x y z : G, x = inst.op (inst.op (inst.op (inst.op y y)  y) x) (inst.op (inst.op y y) z)

Unfortunately, elaboration is surprisingly slow for these relative simple definitions, and I had to work around it by writing a custom elaborator that replaces ∘ with op.inst, so likely the issue is with type class inference.

Is there some low-hanging fruit we can pluck in lean here so that such definitions work just fine? Probably needs someone with good profiling skills to have a look.

Versions

4.12.0-nightly-2024-09-30

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Ok, had a closer look, and the reason this is slow because ∘ already exists as function composition, and it tries both in each instance, so probably something exponential is going on. Using a different symbol it elaborates in 3ms. Still slower than the explicit one, but at least bearable.