From fadef64b512886b6fe01b87fd2cd07fd952ab662 Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Wed, 20 Sep 2006 18:19:59 +0000 Subject: [PATCH] Make newtype Coercion eta-contract if the tails of lhs and rhs match up Mon Sep 18 17:20:17 EDT 2006 Manuel M T Chakravarty * Make newtype Coercion eta-contract if the tails of lhs and rhs match up Sun Aug 6 20:57:10 EDT 2006 Manuel M T Chakravarty * Make newtype Coercion eta-contract if the tails of lhs and rhs match up Thu Aug 3 12:26:52 EDT 2006 kevind@bu.edu --- compiler/types/Coercion.lhs | 40 ++++++++++++++++++++++++++++++++++++---- compiler/types/TyCon.lhs | 18 +++++++++++++----- 2 files changed, 49 insertions(+), 9 deletions(-) diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 55a282d..25d04ec 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -37,12 +37,14 @@ import TypeRep import Type ( Type, Kind, PredType, substTyWith, mkAppTy, mkForAllTy, mkFunTy, splitAppTy_maybe, splitForAllTy_maybe, coreView, kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys, - coreEqType, splitAppTys, isTyVarTy, splitTyConApp_maybe + coreEqType, splitAppTys, isTyVarTy, splitTyConApp_maybe, + tyVarsOfType ) import TyCon ( TyCon, tyConArity, mkCoercionTyCon, isNewTyCon, newTyConRhs, newTyConCo, isCoercionTyCon, isCoercionTyCon_maybe ) import Var ( Var, TyVar, isTyVar, tyVarKind ) +import VarSet ( elemVarSet ) import Name ( BuiltInSyntax(..), Name, mkWiredInName, tcName ) import OccName ( mkOccNameFS ) import PrelNames ( symCoercionTyConKey, @@ -277,7 +279,7 @@ splitRightCoercion_maybe (TyConApp tc [co]) splitRightCoercion_maybe other = Nothing -- Unsafe coercion is not safe, it is used when we know we are dealing with --- bottom, which is the one case in which it is safe. It is also used to +-- bottom, which is one case in which it is safe. It is also used to -- implement the unsafeCoerce# primitive. mkUnsafeCoercion :: Type -> Type -> Coercion mkUnsafeCoercion ty1 ty2 @@ -288,10 +290,40 @@ mkUnsafeCoercion ty1 ty2 mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon mkNewTypeCoercion name tycon tvs rhs_ty = ASSERT (length tvs == tyConArity tycon) - mkCoercionTyCon name (tyConArity tycon) rule + mkCoercionTyCon name co_con_arity (mkKindingFun rule) where - rule args = mkCoKind (TyConApp tycon args) (substTyWith tvs args rhs_ty) + 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 + + 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))) + -------------------------------------- -- Coercion Type Constructors... diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index 785d085..83cd8f2 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -238,12 +238,20 @@ The NewTyCon field nt_co is a a TyCon (a coercion constructor in fact) which is used for coercing from the representation type of the newtype, to the newtype itself. For example, - newtype T a = MkT [a] + newtype T a = MkT (a -> a) -the NewTyCon for T will contain nt_co = CoT where CoT t : T t :=: [t]. -This TyCon is a CoercionTyCon, so it does not have a kind on its own; -it basically has its own typing rule for the fully-applied version. -If the newtype T has k type variables then CoT has arity k. +the NewTyCon for T will contain nt_co = CoT where CoT t : T t :=: t -> +t. This TyCon is a CoercionTyCon, so it does not have a kind on its +own; it basically has its own typing rule for the fully-applied +version. If the newtype T has k type variables then CoT has arity at +most k. In the case that the right hand side is a type application +ending with the same type variables as the left hand side, we +"eta-contract" the coercion. So if we had + + newtype S a = MkT [a] + +then we would generate the arity 0 coercion CoS : S :=: []. The +primary reason we do this is to make newtype deriving cleaner. In the paper we'd write axiom CoT : (forall t. T t) :=: (forall t. [t]) -- 1.7.10.4