- rule args = (TyConApp tycon tys, substTyWith tvs_eta tys rhs_eta, rest)
- where
- tys = take co_con_arity args
- rest = drop co_con_arity args
-
- -- 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