- cast_co (tv,ty) (Type co) = Type $ mkSymCoercion (substTyVar theta tv)
- `mkTransCoercion` co
- `mkTransCoercion` (substTy theta ty)
- new_co_args = zipWith cast_co dc_eq_spec co_args
+ cast_co_spec (tv, ty) co
+ = cast_co_theta (mkEqPred (mkTyVarTy tv, ty)) co
+ cast_co_theta eqPred (Type co)
+ | (ty1, ty2) <- getEqPredTys eqPred
+ = Type $ mkSymCoercion (substTy theta ty1)
+ `mkTransCoercion` co
+ `mkTransCoercion` (substTy theta ty2)
+ new_co_args = zipWith cast_co_spec dc_eq_spec co_args_spec ++
+ zipWith cast_co_theta dc_eq_theta co_args_theta