(deterministic) timeout at 'typeclass' for InvolutiveStar

Stream: mathlib4

[Utensil Song]

An almost minimal #mwe :

import Mathlib.GroupTheory.GroupAction.ConjAct
import Mathlib.Algebra.Star.Unitary
import Mathlib.LinearAlgebra.CliffordAlgebra.Star
import Mathlib.Tactic

variable {R : Type*} [CommRing R]

variable {M : Type*} [AddCommGroup M] [Module R M]

variable {Q : QuadraticForm R M}

section Pin

open CliffordAlgebra MulAction

open scoped Pointwise

def lipschitz (Q : QuadraticForm R M) :=
  Subgroup.closure (Units.val ⁻¹' Set.range (ι Q) : Set (CliffordAlgebra Q)ˣ)

def pinGroup (Q : QuadraticForm R M) : Submonoid (CliffordAlgebra Q) :=
  (lipschitz Q).toSubmonoid.map (Units.coeHom <| CliffordAlgebra Q) ⊓ unitary _

namespace pinGroup

theorem star_mem {x : CliffordAlgebra Q} (hx : x ∈ pinGroup Q) : star x ∈ pinGroup Q := sorry

instance : Star (pinGroup Q) :=
  ⟨fun x => ⟨star x, star_mem x.prop⟩⟩

@[simp, norm_cast]
theorem coe_star {x : pinGroup Q} : ↑(star x) = (star x : CliffordAlgebra Q) :=
  rfl

-- on live.lean-lang.org need to uncomment the following to trigger
-- set_option synthInstance.maxHeartbeats 20000 in
instance : InvolutiveStar (pinGroup Q) :=
  ⟨fun _ => by
    /-
    failed to synthesize

    (deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
    -/
    ext; simp only [coe_star, star_star]
  ⟩

end pinGroup

end Pin

(background: I'm trying to port mathlib#16040 to Lean 4)

[Utensil Song]

I wonder if I should simply increase the maxHeartbeats or something is wrong here.

An interesting observation is that if I remove import Mathlib.Tactic, it also no longer times out.

[Utensil Song]

I don't know how to read these outputs of set_option trace.Meta.synthInstance true

With import Mathlib.Tactic:
image.png
Without import Mathlib.Tactic:
image.png

[Eric Wieser]

Replacing the simp only with simp_rw [coe_star, star_star] makes it fine

[Eric Wieser]

The problem is that lean first tries to find InvolutiveStar ↥(pinGroup Q) which obviously doesn't exist (yet) because you're in the middle of defining it, but it's taking too long to conclude that it doesn't exist

[Utensil Song]

It's intriguing why Lean tries to find InvolutiveStar ↥(pinGroup Q) only if import Mathlib.Tactic (not import Mathlib.Tactic.Common).

[Eric Wieser]

I would assumes it tries it anyway, but the extra imports make the search take too long

[Kevin Buzzard]

This is a recent regression -- I tried the code with a one week old version of mathlib and it works fine, but it fails on current master. Currently bisecting: let me know if I've misunderstood the issue here.

[Kevin Buzzard]

The commit which pushes it over the edge is ee87d34d605d52b7ea8073b70a858769c5f3db3d, the commit which introduces CommMagma. Perhaps this isn't surprising, this did cause some typeclass slowdowns. That commit also had to increase synthInstance.maxHeartbeats at some other point: changing the default from 20000 to 22000 in the code above gets it compiling again so the commit just pushed it over the edge.

[Jireh Loreaux]

@Kevin Buzzard can you count the heartbeats prior to the CommMagma change? I'm curious how big the jump was.

[Kevin Buzzard]

post CommMagma: 21839, pre it's 21751.

[Kevin Buzzard]

So it's really epsilon, which is good news. I guess that a few of those heartbeats are doing some admin, and the synthInstance.maxHeartbeats is not counting all of them (so something is going from just under 20000 to just over 20000 and then there's a bit of noise on top)

[Jireh Loreaux]

great, thanks for the recon!

[Kevin Buzzard]

I owed Utensil one ;-)

[Utensil Song]

I'm confused by the fact that I wake up this morning to find out that it no longer time out, but I haven't updated Mathlib at all (still at 9df2cbf62c359b33807151422ca975894413d876 when I reported this), or changed any code at all. The heartbeat is now 16500.

Dec  2 22:26 lakefile.olean
Dec  2 22:26 .lake
Dec  2 22:25 lean-toolchain
Dec  2 22:25 lake-manifest.json

[Utensil Song]

I've updated Mathlib to c6ea155e725345888c36b7c1629e8c922d88e7e8 and it also no longer time out by default and the heartbeat is now 20038. Anyway this issue is solved and the puzzle is volatile in nature so no need for further investigation. Thanks!

[Anne Baanen]

This timeout seems to be triggered a lot by #8386. Ideally we'd avoid looking for a Star instance entirely but it does indicate this part of the hierarchy should be optimized.

[Matthew Ballard]

This is fixed with lean4#2478. Profiler goes from ~550ms to ~200ms for typeclass inference of InvolutiveStar. Synthesizing the instance needs about 9500 heartbeats.