Reversible coercions (+ canonical structures and typeclasses)

[Alizter]

Coq has a new feature in the upcoming 8.16 release (around summer). Something called reversible coercions. Here is an example of something that we have wanted for a long time:

Set Primitive Projections.

Class IsPointed (A : Type) := point : A.

Record pType : Type := {
  pointed_type : Type ;
  ispointed_pointed_type : IsPointed pointed_type ;
}.
#[reversible]
Coercion pointed_type : pType >-> Sortclass.
Canonical Build_pType' (A : Type) (a : IsPointed A) := Build_pType A a.

Axiom A : Type.
#[export]
Instance a : IsPointed A. Proof. Admitted.

(* Type command is Check without evars (typeclass search etc.) *)
Type (A : pType).

OK, so here is what happens:

• you give A : Type where ?x : pType is expected
• no coercion Sortclass >-> pType but (according to Print Graph) we have [pointed_type] : pType ↣ Sortclass (reversible)
• so reversible coercions look for ?x : pType such that pointed_type ?x = A
• and canonical structure mechanism infers ?x = Build_pType' A _
• finally, typeclass resolution fills the last _ with a

This is something we have wanted to do for a while, and has a lot of potential for us. The key feature here isn't reversible coercions on it's own but the interaction of reversible coercions, typeclasses and canonical structures all together.

When HoTT updates to 8.16 (I'm guessing around September) we should definitely start using this. This will allow us to:

• Use groups in lemmas about abelian groups (as long as there is a proof of abelianess somewhere)
• Use lemmas about pType for any Type and an instance of IsPointed
• Use unbundled equivalences in lemmas about bundled equivalences
• We could set issig lemmas as a reversible coercions allowing the issig step to always be implicit.
• Bundle up many things in the WildCat library knowing that Coq will know how to turn a type into a category
• etc.

Upstream reversible coercions hasn't quite been merged yet, but will be merged soon, check out the PR here: https://github.com/coq/coq/pull/15693

Please suggest any ideas that you would like to try once this feature is available. I think it has great potential to make the HoTT library much easier to use. :-)

[mikeshulman]

Sounds exciting!

[jarlg]

Indeed! Does this solve #1530?

[Alizter]

I suspect it would make sense now to define Pi as a group directly now, so in a sense yes. Given how we currently do WildCat things, if I do, for a group G and abelian group A, Hom G A then that will be Hom in Grp whilst Hom A G will be hom in AbGrp. Of course, these are the exact same thing, but the wildcat instances will be different. The design of some wildcat stuff might have to change to make this clearer perhaps.

In fact, we could try something even more extreme, which is to not define Pi as a group at all, but rather as a type directly. If we make "Group := { A : Type ; IsGroup A; }" a canonical structure, and the first projection a coercion, then Coq will know how to elaborate any type into a Group as long as there is an IsGroup instance somewhere. This will have to be done carefully however, since we need to make sure the structure we are elaborating is unique in some sense. Or else headaches will ensue.

[Alizter]

I have another example where this might be very useful. Currently we have some tension in the library between TruncType and IsTrunc (with the latter mostly winning). I believe this feature would allow us to say foo (X : hProp) and then pass a Type X into foo rather than having to bundle it up. That is something we thought canonical structures would do before, but I suppose now this would be the missing piece.

This has applications not only to truncations but reflective subuniverses too.