- -- if the rhs_ty is a type application and it has a tail equal to a tail
- -- of the tvs, then we eta-contract the type of the coercion
- rhs_args = let (ty, ty_args) = splitAppTys rhs_ty in ty_args
-
- n_eta_tys = count_eta (reverse rhs_args) (reverse tvs)
-
- count_eta ((TyVarTy tv):rest_ty) (tv':rest_tv)
- | tv == tv' && (not $ any (elemVarSet tv . tyVarsOfType) rest_ty)
- -- if the last types are the same, and not free anywhere else
- -- then eta contract
- = 1 + (count_eta rest_ty rest_tv)
- | otherwise -- don't
- = 0
- count_eta _ _ = 0
-
-
- eqVar (TyVarTy tv) tv' = tv == tv'
- eqVar _ _ = False
-
- co_con_arity = (tyConArity tycon) - n_eta_tys
-
- tvs_eta = (reverse (drop n_eta_tys (reverse tvs)))
-
- rhs_eta
- | (ty, ty_args) <- splitAppTys rhs_ty
- = mkAppTys ty (reverse (drop n_eta_tys (reverse ty_args)))
-