The Coq mailing list

[Anders Lundstedt <anders AT anderslundstedt.se>]

Here is another example, which I think is closely related to my
problem (1). http://pastebin.com/CWwWvPRu

  Parameter A : nat -> Type.
  SubClass A0 := A 0.
  SubClass A1 := A 1.
  Parameter A0toA1 :> A0 -> A1.
  Print Graph.
  (* we now have coercions A0,A1 >-> A and A0  >-> A1 *)

  Parameter (a0 : A 0) (a1 : A 1).
  Parameter (a0' : A0) (a1' : A1).
  Parameter f : A 1 -> Type.
  Parameter f' : A1 -> Type.

  (* term of type A0 when term of type A1 expected: *)
  Check (f' a0'). (* OK *)

  (* possible to avoid casts below, e.g. get "f a0'" to typecheck? *)

  (* term of type A0 when type of A 1 expected: *)
  Check (f (a0' : A1)).

  (* term of type A 0 when term of type A1 expected: *)
  Check (f' (a0 : A0)).

  (* term of type A 0 when term of type A 1 expected: *)
  Check (f ((a0 : A0) : A1)). (* note: double cast needed! *)