The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Hi everyone,

I would like to understand what identity coercions are for.  The
reference manual says they are used to go around the "uniform
inheritance condition".  That suggests to me that they might be usable
to solve a problem like the following.

> Parameters (A : nat -> Type) (B : Type) (f : A 0 -> B).

Suppose I would like to declare f as a coercion.  Writing

> Coercion f : A 0 >-> B.

is not even syntactically valid.  I can try

> Definition A' := A 0.
> Coercion f : A' >-> B.

But that fails with 'Cannot recognize A' as a source class of f.'  Now I can 
try

> Definition f' : A' -> B := f.
> Coercion f' : A' >-> B.

Which at least is accepted.  Now I can say

> Parameter y : A'.
> Check y : B.

which succeeds, but

> Parameter x : A 0.
> Check x : B.

fails with 'The term "x" has type "A 0" while it is expected to have
type "B"'.  Is this something that identity coercions are supposed to
help with?  I've tried writing

> Identity Coercion IdA'A : A' >-> A.

but that doesn't seem to affect the behavior of any of the above commands.

The reference manual includes only one example of identity coercions,
which is essentially the following:

> Parameters (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set).
> Parameter T : E true -> nat.
> Parameter g : forall (n:nat) (b:bool), D n b -> E b.
> Coercion g : D >-> E.
> Definition D' (b:bool) := D 1 b.
> Identity Coercion IdD'D : D' >-> D.
> Parameter d' : D' true.
> Check (T d').

However, in this case *removing* the "Identity Coercion" command
doesn't seem to change the behavior!  So this example doesn't really
help me see what the identity coercion is for.

Thanks for your help,
Mike