typeclass inference problems for `has_colimits`

Stream: general

[Scott Morrison]

Hi @Reid Barton, I am getting lots of strange errors that claim to be about typeclass inference for has_colimits. A typical example is:

failed to synthesize type class instance for
C : Type u,
𝒞 : category C,
_inst_1 : has_colimits C,
F G H : PresheafedSpace C,
α : F ⟶ G,
β : G ⟶ H,
x : ↥(F.X)
⊢ Π {J : Type v} {𝒥 : small_category J} (F : J ⥤ C), has_colimit F

[Scott Morrison]

(The goal is just the definition of has_colimits C.)

[Scott Morrison]

Do you have any idea what going on here?

[Scott Morrison]

The current place it is cropping up, very mysteriously is here, and for now blocking me working on stalks.

[Scott Morrison]

Is it some strange bug in Lean dealing with [class] attributes on function types?

[Scott Morrison]

Or maybe I'm doing something dumb.

[Reid Barton]

Yeah I've seen errors like this before. It seems that the @[class] def has_colimits := a Pi-type doesn't actually totally work, even though it seems to mostly work. It takes some slightly complicated setup for it to stop working and I never got to the bottom of it.
I think we just need to change each of the classes to be a structure

[Reid Barton]

with instances that specialize has_colimits -> has_colimits_of_shape -> has_colimit

[Reid Barton]

and you won't be able to go back the other way from Pi J, has_colimits_of_shape J to has_colimits automatically, but that probably doesn't really matter in practice

[Scott Morrison]

ok. I will try this out at some point.