Canonical structures

[patrick-nicodemus]

Today I was formalizing an equivalence of categories today between two categories C and D. Both of the categories had concretely defined hom-types with their own names C_Hom and D_Hom, similarly to how the category of Groups has an associated type GroupHomomorphism defined; but one can also speak about them using the typeclass notation, Hom x y, where the instance is inferred. The theorems to be proved involved a mix of the two notations.

I started running into some quite painful errors where unification was unable to solve simple things like refine (alpha $@ _) because $@ expects its first argument to be an element of something which is of the form Hom x y by definition, but instead alpha was a 2-cell of the "concrete" type C_Hom2 f g, and unification was unable to solve for the missing IsGraph structure such that C_Hom2 x y would have been the projection. Now after unification fails, typeclass search is launched, and it tries to instantiate the typeclass instances in a consistent way. But since the category D was defined more recently than C, it guesses isgraph_D is01cat_D etc. for all the typeclass holes, so unification fails again because it infers the wrong category. So, I had to add lots of annotations.

I know that canonical structures can be used to solve for the record that a projection 'comes from', so I added:

Instance is2Graph_C : Is2Graph C := (...)

Definition isgraph_C_hom (a b : C)
  : IsGraph (C_hom a b)
  := isgraph_hom a b.

Canonical isgraph_C_hom.

Lo and behold, this worked like a charm, and suddenly I was able to remove all my annotations. I was pretty thrilled about this.

I originally had some fears that canonical structures and typeclasses would play together in unexpected and complex ways, leading to dynamics that are difficult to debug. I am no longer as worried about this, because canonical structures is part of unification whereas typeclasses is fairly separate from unification.

I hope this hint is helpful for others having unification woes!

[jdchristensen]

Looks promising! I haven't played with this, but I think @Alizter has.

[jdchristensen]

BTW, another alternative is to first define the graph structure, and then to define the special name Hom_C to be the wild-category graph structure. However, this has two downsides at the moment. One mild one is that any use of wild categories requires an extra universe variable. This isn't too big of an issue, and in the future we hope that this will go away by using a successor universe. The other issue is that it typically forces the types involved to be in the same universe, while the statements you are working on would naturally let the universes be separate. And while this seems like it reduces the number of universe variables, it often later increases the number, because when you want to apply the result to two types in independent universes, you need a third universe variable to serve at the upper bound.

[Alizter]

Do you have a small reproducible example where making isgraph_C_hom a canonical structure fixes a unification problem? I'm potentially interested in such a thing, I did some experimentation in #1641. My main worry is that it might break or cause performance issues, so it would be good to understand the situation in detail.