The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

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