SimpNF time-out involving subobjects and HasPulbacks

Stream: mathlib4

[Michael Rothgang]

The following example (minimisation due to Eric Wieser) fails on master.

import Mathlib

universe u v
variable {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {A : C}

set_option trace.Meta.synthInstance true in
#synth OrderBot (CategoryTheory.Subobject A)

The error message is

failed to synthesize
  OrderBot (CategoryTheory.Subobject A)
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

This came up in #23371. I don't understand what's happening here. Any ideas are appreciated.

[Aaron Liu]

It seems to be going through the algebraic hierarchy..

[Aaron Liu]

docs#CanonicallyOrderedAdd.toOrderBot introduces the algebraic hierarchy

[Kevin Buzzard]

I am confused. Do you expect this to succeed?

[Matthew Ballard]

docs#CategoryTheory.Subobject.orderBot is what should be found?

[Kevin Buzzard]

failed to synthesize
  CategoryTheory.Limits.HasInitial C

[Aaron Liu]

The problem seems to be the algebraic hierarchy being very slow to fail with 170 typeclasses, which gets traversed 4 times here (for CategoryTheory.Subobject A, for PEmpty.{1}, for ∀ (J : Type ?u), and for ∀ (J : Type))

[Michael Rothgang]

I would expect #23371 to pass CI - but the simpNF linter times out; the time-out can be reduced to the above.

[Eric Wieser]

To be clear, this is expected to fail, but it should do so without timing out

[Eric Wieser]

Rationale: synthesis failures cause simp to ignore the lemma that requested them. Synthesis timeouts cause simp to crash, because the alternative would be a nondeterministic simp.

[Floris van Doorn]

Aaron Liu said:

docs#CanonicallyOrderedAdd.toOrderBot introduces the algebraic hierarchy

What is the default type-class inference synthesis ordering of lemma arguments? I hope that if we synthesize the last argument (CanonicallyOrderedAdd) first, then it doesn't have to traverse (much of) the algebraic hierarchy?
Maybe this will also be fixed by #20676?

[Kevin Buzzard]

Eric Wieser said:

To be clear, this is expected to fail, but it should do so without timing out

(so set_option synthInstance.maxHeartbeats 40000 is a fix)

[Eric Wieser]

(I don't think we can set that for the simpNF linter)

[Jovan Gerbscheid]

Looking at the trace led me to two problematic type classes:
docs#UnivLE

abbrev UnivLE : Prop := ∀ α : Type u, Small.{v} α

docs#CategoryTheory.Limits.HasProducts

abbrev HasProducts :=
  ∀ J : Type w, HasLimitsOfShape (Discrete J) C

I think they should not be abbrev. Lean has special support for ∀ binders in type classes, essentially introducing the variable. In this case, it ends up searching the algebraic hierarchy not only for CategoryTheory.Subobject A, but also for ∀ α : Type u and for ∀ J : Type w. I would suggest to define these type classes as structures, and hopefully not too many instances need to be modified to fix any breakages.

There's also HasCoProducts, Has(Co)Limits, HasPushouts and HasPullbacks that are abbrevs for foralls.

[Eric Wieser]

I don't buy that argument that this is an issue, docs#DecidablePred is defined in this way (and therefore there is surely native support for this)

[Eric Wieser]

Unless of course there is some universe complication

[Matthew Ballard]

I was testing this out on docs#Quiver.IsThin #23600

[Jovan Gerbscheid]

Eric Wieser said:

I don't buy that argument that this is an issue, docs#DecidablePred is defined in this way (and therefore there is surely native support for this)

In DecidablePred

abbrev DecidablePred {α : Sort u} (r : α → Prop) :=
  (a : α) → Decidable (r a)

As long as r is a reasonable term, Decidable (r a) will be a reasonable type class goal. However, I don't think ∀ α : Type u, Small.{v} α is much of a reasonable goal.

In fact, the following searches the entire hierarchy:

import Mathlib

universe u v
open CategoryTheory Limits

set_option trace.Meta.synthInstance true
#synth UnivLE.{u,v}

[Kevin Buzzard]

Wow!

    [] 420 more entries... ▼
      [] ✅️ apply littleWedderburn to (α : Type (max u v)) → Field α ▼
...

[Eric Wieser]

Agreed that that makes docs#UnivLE very suspect

[Eric Wieser]

Is HasProducts problematic in the same way though?

[Jovan Gerbscheid]

Maybe not, it could be a matter of reordering the arguments in some instances.

[Aaron Liu]

Eric Wieser said:

Agreed that that makes UnivLE very suspect

Does this make docs#Countable suspect too?

[Eric Wieser]

No, because it's a structure

[Jovan Gerbscheid]

Countable.toSmall in combination with UnivLE creates the nasty goal ∀ α : Type u, Countable α.

Countable itself is in some sense suspect, because there are simply a LOT of things that are countable :sweat_smile: (Similar to Nonempty)

[Eric Wieser]

I'll make a PR for univLE (edit: #23611)

[Jovan Gerbscheid]

A few weeks ago in #22968 I reordered some instances to avoid "leaking" a type class search from category theory into the algebraic hierarchy. But it seems there are a few more bad ones:

docs#CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProducts
docs#CategoryTheory.Limits.instHasLimitsOfShapeOfCountableCategoryOfHasCountableLimits
docs#CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits

[Jovan Gerbscheid]

From the above mentioned, it's actually only Has(Co)Products that is problematic, not the other Limit classes. The particular problem at hand can be solved by adjusting the 3 instances I wrote here. However, I think it would be a more principled solution to make these into structures.

[Jovan Gerbscheid]

All right, I've made a PR for these (#23612). It turns out to be the exact same change as #22968, but for limits/products instead of colimits/coproducts :face_palm:

Edit: yay, it gives a speedup:

build   -97.179⬝10⁹     (-0.05%)

[Michael Rothgang]

This thread is the mathlib community at its best: I'm posting about a place where I'm stuck, and when I get up the next morning, several people have diagnosed (parts of) the failure and two PRs spawned by this were merged. Thanks a lot!
I'm incredibly grateful to be part of this community.

[Eric Wieser]

It looks like the titular issue is now fixed