The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

On 18.08.2017 10:29, Robbert Krebbers wrote:
> 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.

There is at least one other longstanding issue around primitive
projection, making it impossible for us to use them in many cases
currently:  Many cases of intros break in Iris when we switch things to
primitive projections.
https://coq.inria.fr/bugs/show_bug.cgi?id=5245

This bug persists in Coq 8.7.  I also verified that Robbert's example
still fails in 8.7.  (Did you report the bug yet, Robbert?)

Kind regards,
Ralf


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