The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

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.

(* 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,
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / INRIA ProVal Project
Paris, France

[1] http://coq.inria.fr/refman/Reference-Manual023.html#toc123