The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Daniel,

  The reason is Opaque was not respected (or rather understood as really Opaque) by the elaboration/unification, only by the kernel, this will change in the next version (maybe using a Rigid flag instead).

Cheers,

-- Matthieu

Le samedi 18 janvier 2014, Daniel Schepler a écrit :

On a related note, I've tried something like this in the past, and was surprised that it didn't work the way I wanted it to:

Class Plus (A:Type) :=

plus : A -> A -> A.

Instance nat_plus : Plus nat := Peano.plus.

Definition nat_copy : Type := nat.

Hint Opaque nat_copy : typeclass_instances.

Instance nat_copy_plus : Plus nat_copy := Peano.plus.

Definition zero1 : nat := 0.

Definition zero2 : nat_copy := 0.

(* Want the Hint Opaque to cause this to fail but it works. *)

Check (plus zero1 zero2).

(What I actually wanted to use it for was to declare an opposite category as OpCat C := C and force it to use the opposite Hom, id, comp instead of the ones from the original category when objects were declared of type OpCat C.)

-- 

Daniel Schepler

On Fri, Jan 17, 2014 at 11:06 AM, <drg AT illinois.edu> wrote:

One way to implement the notion of group G (for example) would be as a record,
the first element of which is the type X of the elements of the group.  The
multiplication operation could be defined with something like

   Definition op {G:Group} (g:pr1 G) (h:pr1 G) := ... .

where pr1 is projection on the first component.  If pr1 is defined as a
coercion,
then it can be written more suggestively as

   Definition op {G:Group} (g:G) (h:G) := ... .

If G' is another group sharing X with G, but not the other data, and g : G and
g' : G', then " op g g' " will be well-typed, which is mathematically
surprising
and might lead the user astray.

Assuming this issue has already been encountered in the past, I wonder what
the best solution is.  I'm tempted to say that an element g of G should be
defined
to be a pair (G,x) with x:X, and the coercion would then be the one that sends
G
to the type of such pairs.  This would be mathematically pleasing, as elements
of groups would know to which group they belong, just as elements of a type
"know" to which type they belong.

The actual situation where this arose was with two objects of a category and
the type of isomorphisms between them.

-- 
-- Matthieu