The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 08/17/2017 11:35 PM, Pierre-Marie Pédrot wrote:
> Also, while I'm thinking about this, could you report this on the bug
> tracker with self-contained reproducible examples? Primitive projections
> ought to work out-of-the-box for canonical structures and the like.
See below for an example. It roughly follows the Ssreflect approach, and 
works just fine without primitive projections. However, with primitive 
projections is breaks.


Set Primitive Projections.

Structure semigroup := SemiGroup {
  sg_car :> Type;
  sg_op : sg_car -> sg_car -> sg_car;
}.

Structure monoid := Monoid {
  monoid_car :> Type;
  monoid_op : monoid_car -> monoid_car -> monoid_car;
  monoid_unit : monoid_car;
}.

Coercion monoid_sg (X : monoid) : semigroup :=
  SemiGroup (monoid_car X) (monoid_op X).
Canonical Structure monoid_sg.
(*
Projection value has no head constant: monoid_car _UNBOUND_REL_1 in 
canonical
instance monoid_sg of sg_car, ignoring it.
*)

Parameter X : monoid.
Parameter x y : X.

Fail Check (sg_op _ x y).
(*
Error: The term "x" has type "monoid_car X" while it is expected to have 
type "sg_car ?s".
*)

> (Notwithstanding the fact that the Coq bugzilla is currently down.)
I will create an actual bug when the bug tracker is alive again.