The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Here's my solution.  The key is what I call the "convoy pattern" here:
   http://adam.chlipala.net/cpdt/

The type of [cast] is not refined inside a case analysis on a subterm 
that appears in [cast]'s type.  Instead, you need to explicitly abstract 
over [cast], so that its type can be rewritten properly by dependent 
[match].

Section test.
 Variable I : Type.
 Variable T : I -> Type.
 Variable i1 i2 : I.
 Variable dT : T i2 -> Type.
 Variable F : forall t : T i2, dT t.
 Variable convertible : I -> I -> bool.
 Variable cast : T i1 -> convertible i1 i2 = true -> T i2.

 Definition dT' (t : T i1) :=
   (if convertible i1 i2 as b return (convertible i1 i2 = b -> Type)
     then (fun p : convertible i1 i2 = true => dT (cast t p))
     else (fun p : convertible i1 i2 = false => unit)) (refl_equal _).

 Definition F' (t : T i1) : dT' t :=
   (if convertible i1 i2 as b' return forall cast : T i1 -> b' = true 
-> T i2,
     ((if b' as b return (b' = b -> Type)
       then (fun p : b' = true => dT (cast t p))
       else (fun p : b' = false => unit)) (refl_equal _))
     then fun cast => F (cast t (refl_equal _))
     else fun _ => tt) cast.
End test.