The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 20 Jul 2011 12:59:17 +0200,
Paolo Herms 
<paolo.herms AT cea.fr>
 a écrit :

> Hello,
> reference manual section 17.4 [1] claims that Identity Coercions
> could be "used to go around the uniform inheritance condition". It
> doesn't give an example and I don't understand how. Here's what I
> tried:
> 
> Parameter C : Type -> Type.
> Parameter D : Type -> Type -> Type.
> Parameter f : forall A B, C A -> D A B.
> 
> Fail Coercion f: C>->D. (* obviously *)
> 
> (* now I try what the section says, *)
> Definition C' (A B: Type) := C A.
> Identity Coercion idC'C: C'>->C.

I guess the problem is that you define a coercion from C' to C;
and you would like to have one from C to C';
so that you can branch it to follow this diagram: C>->C'>->D.

But I guess, that such a coercion is not possible.

I don't know if you are interested in this:

Parameter C : Type -> Type.
Parameter D : Type -> Type -> Type.
Parameter f : forall A, C A -> forall B, D A B.

Coercion f: C>-> Funclass.

Variable X: C nat.
Check (X nat: D nat nat).
Check (X: forall B, D nat B). 

> 
> (* but none of this works *)
> Fail Coercion f: C>->D.
> Fail Coercion f: C'>->D.
> 
> (* it is true that I can cast [f] to the desired type *) 
> Check f : forall A B, C' A B -> D A B.
> (* and like this I can manually define a coercion from [C'] to [D]
>    (even if I don't want to do it this way, because it introduces
> another identifier I'll have to unfold within proofs) *)
> Coercion f':= f : forall A B, C' A B -> D A B.
> 
> (* but the coercions don't chain *)
> Parameters X Y : Type.
> Parameter c : C X.
> Check c : C' X Y.
> Fail Check c : D X Y.
> (* this works but I wouldn't call this "implicit" *)
> Check (c : C' X Y) : D X Y.
> 
> Am I missing something or did I misunderstand the manual?
> Any ideas?
> Thanks in advance,

I never use coercions, so that I cannot tell for your last point.