- arity = tyConArity tc
- val_args = drop arity args
- to_arg_tys = dataConInstArgTys dc tc_arg_tys
- mk_coerce ty arg = mkCoerce ty arg
- new_val_args = zipWith mk_coerce to_arg_tys val_args
+ -- here we do the PushC reduction rule as described in the FC paper
+ arity = tyConArity tc
+ n_ex_tvs = length dc_ex_tyvars
+
+ (univ_args, rest) = splitAt arity args
+ (ex_args, val_args) = splitAt n_ex_tvs rest
+
+ arg_tys = dataConRepArgTys dc
+ dc_tyvars = dataConUnivTyVars dc
+ dc_ex_tyvars = dataConExTyVars dc
+
+ deep arg_ty = deepCast arg_ty dc_tyvars co
+
+ -- first we appropriately cast the value arguments
+ arg_cos = map deep arg_tys
+ new_val_args = zipWith mkCoerce (map deep arg_tys) val_args
+
+ -- 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
+