simp fails with "failed to synthesize Subsingleton"

Stream: mathlib4

[Eric Wieser]

In branch#eric-wieser/simp-typeclass-failure (this commit triggers the failure), I have a simp tactic that fails with:

failed to synthesize
  Subsingleton (A ⊗[R] CliffordAlgebra Q)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

What's going on here? Why is simp trying to synthesize this instance?

[Kevin Buzzard]

Could it be something to do with this?

[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
      ?a = ?a
    with
      ↑(TensorProduct.AlgebraTensorModule.map LinearMap.id
              (LinearMap.comp (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)))
                (AlgHom.toLinearMap CliffordAlgebra.reverseOp)))
          (↑(CliffordAlgebra.toBaseChange A Q) x) =
        ↑(TensorProduct.map LinearMap.id
              (LinearMap.comp (↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R)))
                (AlgHom.toLinearMap CliffordAlgebra.reverseOp)))
          (↑(CliffordAlgebra.toBaseChange A Q) x)

(trace obtained with trace.Meta.Tactic.simp)
Both terms have type A ⊗[R] CliffordAlgebra Q.

[Kevin Buzzard]

Perhaps a better answer is this: I have noticed in the past that if Lean doesn't have enough heartbeats then sometimes a calculation will just stop randomly in the middle when the error is reported, e.g. a line which used to work now magically fails because something tipped Lean over the edge. In this case I think the error message is worth ignoring. If you put set_option synthInstance.maxHeartbeats 80000 in before the theorem then the error goes away -- simp succeeds after all.

[Eric Wieser]

It would be great if simp could include the lemma name that pushed it over the edge in the error message

[Eric Wieser]

(I don't actually need a solution to this problem as dsimp already worked, but wanted to record the weirdness somewhere)

[Scott Morrison]

@Eric Wieser, could you open an issue for the suggestion that simp reports the name of the lemma it was trying at the moment the synthesis timeout occurred?

[Kevin Buzzard]

So in this case Eric wants the report to say "I was happily doing a bunch of typeclass stuff and the moment I ran out of heartbeats I happened to be applying Subsingleton.Elim, a totally irrelevant lemma which was going to fail quickly but which happened in the mean time to push a count from 19999 to 20000"?

[Yaël Dillies]

I would rather it give me which two or three lemmas it used the most in its invokation, as that would instantly tell me what the loop is.

[Kevin Buzzard]

Here there wasn't a loop, it just ran out of time and barfed what it happened to be doing the moment it did

[Eric Wieser]

Yes, I want to know the lemma that caused the issue so that I can replace simp with simp [-that_lemma]

[Scott Morrison]

But couldn't this be a timeout in typeclass inference for a simp lemma that wasn't going to be used anyway?

[Scott Morrison]

Writing -that_lemma means it will just fail on the next one.

[Eric Wieser]

The fact the lemma wasn't going to be used anyway is kind of the point; I want my simp call to work, and manually skipping the lemma (s) that times out achieves that

[Eric Wieser]

(the alternative of silencing the error internally would be much worse, as then the effect of simp would change depending on the remaining heartbeat budget)