I am having trouble with canonical structure inference and I don't understand why I have this error.

I will link my code (see later down the thread for a slightly more minimized version)

https://github.com/patrick-nicodemus/HoTT/blob/bundled-wildcat/theories/WildCat/Core.v

(The linked file is the only file modified from the HoTT library, I think that individual file should work independently if the coq-HoTT package is installed from Opam)

I have something like the following (where things are wrapped in modules for namespacing). I have been trying to follow the packed classes discipline.

```
Record 01Cat : Type := Pack
{ sort : Type;
is_graph : IsGraph sort;
is01cat : Is01Cat sort
}.
Record 1Cat : Type := Pack {
sort : Type;
isGraph : IsGraph sort;
is2Graph : Is2Graph sort;
is01Cat : Is01Cat sort;
is1Cat : Is1Cat sort
}.
Canonical ZeroOneCatOfOneCat (A : 1Cat) : ZeroOneCat.type :=
ZeroOneCat.Pack (OneCat.sort A) _ _ .
Definition cat_postcomp {A : 01Cat}
(a : A) {b c : A} (g : b $-> c)
: (a $-> b) -> (a $-> c)
:= cat_comp g.
(...)
Definition cat_postwhisker {A : 1Cat} {a b c : A}
{f g : a $-> b} (h : b $-> c) (p : f $== g)
: h $o f $== h $o g
:= fmap (cat_postcomp a h) p.
```

So the last definition is what I want to focus on, the function `cat_postcomp`

expects a `01Cat`

, not a `1Cat`

, so there's some canonical structures magic happening here. This works as intended, it is able to infer that, because `a : 1Cat.sort A`

that the first (implicit) argument should be some `01Cat`

, say `B`

, such that `1Cat.sort A = 01Cat.sort B`

. And then it uses the `Canonical ZeroOneCatOfOneCat`

hint to solve for `B`

, setting `B = ZeroOneCatOfOneCat A`

.

But adding the wrong Canonical hints breaks this inference. I wanted to add the hint:

```
Canonical Build_OneCat (A : Type) {Hk : Is1Cat A} :=
OneCat.Pack A _ _ _ Hk.
```

so if it can find a typeclass for Is1Cat A sitting around it will automatically construct the record. But if I add this hint it breaks the definition of cat_postwhisker. (It's commented out in the github link) I've been trying to debug this:

```
The term "a" has type "1Cat.sort A"
while it is expected to have type "01Cat.sort ?A0".
```

The documentation page suggests the following warning:

```
If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered.
```

I am wondering if somehow this extra hint is leading it to construct the wrong canonical structure, something that isn't unifiable with A

I should note that this works -

```
:= fmap (@cat_postcomp (ZeroOneCatOfOneCat _) a _ _ h) p.
```

so for some reason the `ZeroOneCatOfOneCat`

isn't being applied

(deleted)

Is fmap a typeclass method? Don't know if it's the problem here but typeclasses and canonical structures have "fun" interactions (unification in TC search doesn't always handle CSes correctly)

That is a helpful hint.

```
Definition toy_example {A : 1Cat} {a b c : A} {h : b $-> c}
:= cat_postcomp a h.
```

This smaller example does not mention `fmap`

, and has the same problem with the Canonical hint above (`Build_OneCat`

).

But I am using typeclasses heavily.

All of the `Is1Cat`

, `Is01Cat`

, `IsGraph`

, etc. are all typeclasses.

Here is a self contained version of the problem.

```
(* -*- mode: coq; mode: visual-line -*- *)
From HoTT Require Import Basics.
Class IsGraph (A : Type) :=
{
Hom : A -> A -> Type
}.
Module Graph.
Structure type :=
Pack { sort :> Type;
is_graph : IsGraph sort }.
End Graph.
Notation "a $-> b" := (@Hom _ (Graph.is_graph _) a b).
Coercion Graph.sort : Graph.type >-> Sortclass.
Canonical Build_Graph (A : Type) `(H : IsGraph A) : Graph.type
:= Graph.Pack A H.
Definition graph_hfiber {B : Type} {C : Graph.type}
(F : B -> C) (c : C)
:= {b : B & F b $-> c}.
Class Is01Cat (A : Type) `{IsGraph A} :=
{
Id : forall (a : A), a $-> a;
cat_comp' :
forall (a b c : A), (b $-> c) -> (a $-> b) -> (a $-> c);
}.
Module ZeroOneCat.
Structure type :=
Pack
{
sort : Type;
is_graph : IsGraph sort;
is01cat : Is01Cat sort
}.
Module Exports.
Definition cat_comp `(A : type) :=
@cat_comp' (sort A) (is_graph A) (is01cat A).
Arguments cat_comp {A a b c}.
Notation "g $o f" := (cat_comp g f).
Coercion sort : type >-> Sortclass.
Notation "01Cat" := type.
End Exports.
End ZeroOneCat.
Export ZeroOneCat.Exports.
Canonical Build_ZeroOneCat (A : Type) {H : IsGraph A}
{H0 : Is01Cat A} := ZeroOneCat.Pack A H H0.
Definition cat_postcomp {A : 01Cat}
(a : A) {b c : A} (g : b $-> c)
: (a $-> b) -> (a $-> c)
:= cat_comp g.
```

If I delete the last canonical declaration of `Build_ZeroOneCat`

, then the definition of cat_postcomp succeeds; but with the declaration it fails.

Last updated: Jun 18 2024 at 22:01 UTC