+-- deep applies a TyConApp coercion as a substitution to a reflexive coercion
+-- deepCast t [a1,...,an] co corresponds to deep(t, [a1,...,an], co) from
+-- FC paper
+deepCast :: Type -> [TyVar] -> Coercion -> Coercion
+deepCast ty tyVars co
+ = ASSERT( let {(lty, rty) = coercionKind co;
+ Just (tc1, lArgs) = splitTyConApp_maybe lty;
+ Just (tc2, rArgs) = splitTyConApp_maybe rty}
+ in
+ tc1 == tc2 && length lArgs == length rArgs &&
+ length lArgs == length tyVars )
+ substTyWith tyVars coArgs ty
+ where
+ -- coArgs = [right (left (left co)), right (left co), right co]
+ coArgs = decomposeCo (length tyVars) co
+