Stream: Coq users

Topic: Canonical structures frustration

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 03:17):

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

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 03:18):

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)

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 03:19):

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.

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 03:19):

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.

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 03:21):

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

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 03:22):

I should note that this works -

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

so for some reason the ZeroOneCatOfOneCat isn't being applied

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 03:31):

(deleted)

view this post on Zulip Paolo Giarrusso (Dec 05 2022 at 05:06):

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)

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 06:48):

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).

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 06:48):

But I am using typeclasses heavily.

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 06:49):

All of the Is1Cat, Is01Cat, IsGraph, etc. are all typeclasses.

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 07:57):

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.

view this post on Zulip Patrick Nicodemus (Dec 05 2022 at 07:57):

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: Oct 13 2024 at 01:02 UTC