Difficulty with `id_phant`

[jonsterling]

I am trying to define categories using HB and ran into a little issue that I wasn't sure how to deal with; am sorry if opening a ticket is not the right place for me to ask for help, please let me know if there is another place where I should ask. Here is what I tried to do:

From Coq Require Import Utf8.
From HB Require Import structures.

HB.mixin Record IsGraph (obj : Type) :=
  {hom : obj → obj → Type}.

HB.structure Definition Graph := {𝒞 of IsGraph 𝒞}.

Infix "~>" := hom (at level 10).

HB.mixin Record IsPrecategory 𝒞 of IsGraph 𝒞 :=
  {idn : ∀ x : 𝒞, x ~> x;
   seq : ∀ x y z : 𝒞, x ~> y → y ~> z → x ~> z}.

HB.structure Definition Precategory := {𝒞 of IsPrecategory 𝒞 & IsGraph 𝒞}.

(* TODO *)
HB.mixin Record IsCategory 𝒞 of IsPrecategory 𝒞 := {}.

The last clause throws the following error:

Error:
elpi: parameter illtyped: In environment
𝒞 : Type 
The term "id_phant" has type "phantom Type 𝒞 → phantom Type 𝒞"
while it is expected to have type
 "unify Type Type 𝒞 ?t (Some (is_not_canonically_a, Graph.type))".

[gares]

There is a Zulip stream you can use for questions.

I would consider this a bug, anyway. You can work around it by using

HB.mixin Record IsCategory 𝒞 of IsPrecategory 𝒞 & isGraph 𝒞 := {}.

or

HB.mixin Record IsCategory 𝒞 of Precategory 𝒞 := {}.

which mean the same.

Let's see what @CohenCyril things about this error

[CohenCyril]

We did not close mixins deps transitively, we should do it or warn (or add an attribute). Thanks for reporting

[gares]

FTR with #252 the error is even worse (elpi fails), we should fix both problem before the next release

[jonsterling]

Hi all, thanks very much for looking into this! I have some other questions but I don't want to spam your tickets until I know if they are bugs. Which zulip stream do you prefer I use? I am logged into the Coq zulip.

[CohenCyril]

Hi @jonsterling here is the appropriate stream Hierarchy-Builder stream