+
+ -- then we cast the existential coercion arguments
+ orig_tvs = dc_tyvars ++ dc_ex_tyvars
+ gammas = decomposeCo arity co
+ new_tys = gammas ++ (map (\ (Type t) -> t) ex_args)
+ theta = substTyWith orig_tvs new_tys
+ cast_ty tv (Type ty)
+ | isCoVar tv
+ , (ty1, ty2) <- splitCoercionKind (tyVarKind tv)
+ = Type $ mkTransCoercion (mkSymCoercion (theta ty1))
+ (mkTransCoercion ty (theta ty2))
+ | otherwise
+ = Type ty
+ new_ex_args = zipWith cast_ty dc_ex_tyvars ex_args
+