The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  I think I understand what you are trying to achieve, and why it doesn't 
work.
Canonical declarations work by giving hints to the unification engine: the 
declaration
    Canonical Structure nat_setoid := {|sCarrier = nat; sEqual = eq_nat; 
sEqualsEquiv = eq_nat_equiv|}.
adds (amongst others) the rule nat <- sCarrier (nat_setoid), which the lets 
it solve unification problems of the form
   sCarrier ?33 =~= nat
with ?33 := nat_setoid. To form this rule Coq need to peek inside the 
definition of nat_setoid, find an explicit record construction, pull out the 
expressions for the fields with named projectors (here, sCarrier) that are 
either constant or the application of a constant (plus a handful of special 
cases).
  Each such field yields a rule that matches problems of the form projector _ 
... _ =~= constant _ ... _. The matching is SYNTACTIC, so Coq never tries to 
evaluate the field value, since this would nearly always destroy head 
constants. However, Coq will try to reduce the Canonical structure in order 
to expose an explicit record constructor, but using HEAD call-by-name 
reduction ONLY.
    In your case this means that the sCarrier field vaulue msCarrier 
multi_struct_nat is never reduced to nat, hence Coq does not register the 
hint you intended. The solution is to write msCarrier more carefully, and 
ensure that you only construct the fields you intend. You can do this here by 
using match rather than projectors to get at the MultiStruct fields:
   Definition msCarrier m := let 'Build_MultiStruct T e EQ_e := m in 
Build_Setoid T e EQ_e.
This way, head evaluation has to reduce the let in order to expose 
Build_Setoid. You can use type inference and unification to extract fields; 
this is somewhat more flexible in dealing with intricate dependent types and 
multiple inheritance. The idiom for doing that is described at the end of the 
new chapter on canonical structures in the 8.5beta manual.
   Cheers,
Georges

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Enrico Tassi
Sent: 28 January 2015 09:38
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Grouping several canonical structures in one record - 
strange effect of Canonical Structure command

On Mon, Jan 26, 2015 at 03:27:07PM +0000, Soegtrop, Michael wrote:
> Structure Setoid : Type :=
> {
>   sCarrier      :> Set;
>   sEqual        : relation sCarrier;
>   sEqualIsEquiv : equivalence sCarrier sEqual }.
> 
> Record MultiStruct : Type :=
> {
> msCarrier      : Set;
>   msEqual        : relation msCarrier;
>   msEqualIsEquiv : equivalence msCarrier msEqual;
>   msSetoid       := Build_Setoid msCarrier msEqual msEqualIsEquiv
> }.
> 
> Axiom eq_nat_equiv : equivalence nat eq_nat.
> Definition multistruct_nat := Build_MultiStruct nat eq_nat eq_nat_equiv.
> 
> Canonical Structure nat_setoid := msSetoid multistruct_nat.
> 
> msCarrier <- sCarrier ( nat_setoid )

This print is misleading because it only prints the head constant of the 
value on the left.  The hint you are adding is:

  ?Y   ===   multi_struct_nat
  ?X   ===   nat_setoid
 -----------------------------------
  sCarrier ?X   ===   msCarrier ?Y

To test it:

Fail Check (refl_equal _ : sCarrier _ = nat).
Check (refl_equal _ : sCarrier _ = msCarrier _).

Also "Print msSetoid" tells you why this is the case:

 msSetoid = fun m : MultiStruct =>
   Build_Setoid (msCarrier m) (msEqual m) (msEqualIsEquiv m)

This way you see eactly the values of the fields of the record instance you 
are declaring as canonical.  Its sCarrier component is (msCarrier m) for the 
m you passed to it, here multi_struct_nat.

Not sure what you are trying to achieve, but the hint you declare does not 
make much sense to me.

Hope it helps,
--
Enrico Tassi