X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FCoercion.lhs;h=25d04ecd249eab0ed571018ceffb19e4ca5c0904;hb=80c89b80c355b2aaebcd53330e6c6170c3f05aca;hp=52e4f420e60849224a502fe41daf3768c9f1de49;hpb=f80c996a1357445dac8471b149ee9a5c74b299c6;p=ghc-hetmet.git diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 52e4f42..25d04ec 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -36,12 +36,15 @@ module Coercion ( import TypeRep import Type ( Type, Kind, PredType, substTyWith, mkAppTy, mkForAllTy, mkFunTy, splitAppTy_maybe, splitForAllTy_maybe, coreView, - kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys + kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys, + 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, @@ -59,6 +62,8 @@ import Outputable ------------------------------ decomposeCo :: Arity -> Coercion -> [Coercion] -- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c] +-- So this breaks a coercion with kind T A B C :=: T D E F into +-- a list of coercions of kinds A :=: D, B :=: E and E :=: F decomposeCo n co = go n co [] where @@ -105,7 +110,6 @@ type CoercionKind = Kind -- A CoercionKind is always of form (ty1 :=: ty2) coercionKind :: Coercion -> (Type, Type) -- c :: (t1 :=: t2) -- Then (coercionKind c) = (t1,t2) - coercionKind (TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a) | otherwise = let t = (TyVarTy a) in (t, t) coercionKind (AppTy ty1 ty2) @@ -114,6 +118,7 @@ coercionKind (AppTy ty1 ty2) (mkAppTy t1 s1, mkAppTy t2 s2) coercionKind (TyConApp tc args) | Just (ar, rule) <- isCoercionTyCon_maybe tc + -- CoercionTyCons carry their kinding rule, so we use it here = if length args >= ar then splitCoercionKind (rule args) else pprPanic ("arity/arguments mismatch in coercionKind:") @@ -162,19 +167,42 @@ mkAppsCoercion co1 tys = foldl mkAppTy co1 tys mkForAllCoercion tv co = ASSERT ( isTyVar tv ) mkForAllTy tv co mkFunCoercion co1 co2 = mkFunTy co1 co2 + +-- This smart constructor creates a sym'ed version its argument, +-- but tries to push the sym's down to the leaves. If we come to +-- sym tv or sym tycon then we can drop the sym because tv and tycon +-- are reflexive coercions mkSymCoercion co | Just co2 <- splitSymCoercion_maybe co = co2 - | Just (co1, co2) <- splitAppCoercion_maybe co - -- should make this case better - = mkAppCoercion (mkSymCoercion co1) (mkSymCoercion co2) + -- sym (sym co) --> co + | Just (co1, arg_tys) <- splitTyConApp_maybe co + , not (isCoercionTyCon co1) = mkTyConApp co1 (map mkSymCoercion arg_tys) + -- we can drop the sym for a TyCon + -- sym (ty [t1, ..., tn]) --> ty [sym t1, ..., sym tn] + | (co1, arg_tys) <- splitAppTys co + , isTyVarTy co1 = mkAppTys (maybe_drop co1) (map mkSymCoercion arg_tys) + -- sym (tv [t1, ..., tn]) --> tv [sym t1, ..., sym tn] + -- if tv type variable + -- sym (cv [t1, ..., tn]) --> (sym cv) [sym t1, ..., sym tn] + -- if cv is a coercion variable + -- fall through if head is a CoercionTyCon | Just (co1, co2) <- splitTransCoercion_maybe co + -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2) = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1) | Just (co, ty) <- splitInstCoercion_maybe co + -- sym (co @ ty) --> (sym co) @ ty = mkInstCoercion (mkSymCoercion co) ty | Just co <- splitLeftCoercion_maybe co + -- sym (left co) --> left (sym co) = mkLeftCoercion (mkSymCoercion co) | Just co <- splitRightCoercion_maybe co + -- sym (right co) --> right (sym co) = mkRightCoercion (mkSymCoercion co) + where + maybe_drop (TyVarTy tv) + | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv] + | otherwise = TyVarTy tv + maybe_drop other = other mkSymCoercion (ForAllTy tv ty) = ForAllTy tv (mkSymCoercion ty) -- for atomic types and constructors, we can just ignore sym since these -- are reflexive coercions @@ -182,7 +210,6 @@ mkSymCoercion (TyVarTy tv) | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv] | otherwise = TyVarTy tv mkSymCoercion co = mkCoercion symCoercionTyCon [co] - -- this should not happen but does -- Smart constructors for left and right mkLeftCoercion co @@ -252,20 +279,51 @@ 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 +-- 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 = mkCoercion unsafeCoercionTyCon [ty1, ty2] --- make the coercion associated with a newtype +-- See note [Newtype coercions] in TyCon 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 (substTyWith tvs args rhs_ty) (TyConApp tycon args) + 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... @@ -286,7 +344,7 @@ mkKindingFun f args = symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon :: TyCon -- Each coercion TyCon is built with the special CoercionTyCon record and --- carries its won kinding rule. Such CoercionTyCons must be fully applied +-- carries its own kinding rule. Such CoercionTyCons must be fully applied -- by any TyConApp in which they are applied, however they may also be over -- applied (see example above) and the kinding function must deal with this. symCoercionTyCon = @@ -299,7 +357,9 @@ symCoercionTyCon = transCoercionTyCon = mkCoercionTyCon transCoercionTyConName 2 (mkKindingFun composeCoercionKindsOf) where - composeCoercionKindsOf (co1:co2:rest) = (a1, r2, rest) + composeCoercionKindsOf (co1:co2:rest) = + WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug") + (a1, r2, rest) where (a1, r1) = coercionKind co1 (a2, r2) = coercionKind co2 @@ -361,7 +421,7 @@ unsafeCoercionTyConName = mkCoConName FSLIT("CoUnsafe") unsafeCoercionTyConKey u -- this is here to avoid module loops splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion) --- Sometimes we want to look through a recursive newtype, and that's what happens here +-- Sometimes we want to look through a newtype and get its associated coercion -- It only strips *one layer* off, so the caller will usually call itself recursively -- Only applied to types of kind *, hence the newtype is always saturated splitNewTypeRepCo_maybe ty @@ -376,6 +436,5 @@ splitNewTypeRepCo_maybe (TyConApp tc tys) Just (substTyWith tvs tys rep_ty, mkTyConApp co_con tys) where co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo tc) - splitNewTypeRepCo_maybe other = Nothing \end{code}