X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FCoercion.lhs;h=ca1b1a68154fc88a18206d3dcf7e260e8fd9987e;hp=fb91a0de67d9d14d63e8e9d637e903c04e37aaee;hb=b00b5bc04ff36a551552470060064f0b7d84ca30;hpb=a7a32655a398d0bad611314f0f73c0dcbf2588f4 diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index fb91a0d..ca1b1a6 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -37,14 +37,12 @@ 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, - tyVarsOfType, mkTyVarTys + coreEqType, splitAppTys, isTyVarTy, splitTyConApp_maybe ) -import TyCon ( TyCon, tyConArity, mkCoercionTyCon, isNewTyCon, - newTyConRhs, newTyConCo, +import TyCon ( TyCon, tyConArity, mkCoercionTyCon, isClosedNewTyCon, + newTyConRhs, newTyConCo_maybe, isCoercionTyCon, isCoercionTyCon_maybe ) import Var ( Var, TyVar, isTyVar, tyVarKind ) -import VarSet ( elemVarSet ) import Name ( BuiltInSyntax(..), Name, mkWiredInName, tcName ) import OccName ( mkOccNameFS ) import PrelNames ( symCoercionTyConKey, @@ -110,8 +108,8 @@ 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 ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a) + | otherwise = (ty, ty) coercionKind (AppTy ty1 ty2) = let (t1, t2) = coercionKind ty1 (s1, s2) = coercionKind ty2 in @@ -119,10 +117,11 @@ coercionKind (AppTy ty1 ty2) 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:") - (ppr ar $$ ppr tc <+> ppr args) + = ASSERT( length args >= ar ) -- Always saturated + let (ty1,ty2) = rule (take ar args) -- Apply the rule to the right number of args + (tys1, tys2) = coercionKinds (drop ar args) + in (mkAppTys ty1 tys1, mkAppTys ty2 tys2) + | otherwise = let (lArgs, rArgs) = coercionKinds args in (TyConApp tc lArgs, TyConApp tc rArgs) @@ -287,42 +286,14 @@ mkUnsafeCoercion ty1 ty2 -- 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 co_con_arity (mkKindingFun rule) +mkNewTypeCoercion :: Name -> TyCon -> ([TyVar], Type) -> TyCon +mkNewTypeCoercion name tycon (tvs, rhs_ty) + = mkCoercionTyCon name co_con_arity rule where - 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 + co_con_arity = length tvs - 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))) + rule args = ASSERT( co_con_arity == length args ) + (TyConApp tycon args, substTyWith tvs args rhs_ty) -- Coercion identifying a data/newtype representation type and its family -- instance. It has the form `Co tvs :: F ts :=: R tvs', where `Co' is the @@ -336,17 +307,12 @@ mkDataInstCoercion :: Name -- unique name for the coercion tycon -> TyCon -- representation tycon (`R') -> TyCon -- => coercion tycon (`Co') mkDataInstCoercion name tvs family instTys rep_tycon - = mkCoercionTyCon name coArity (mkKindingFun rule) + = mkCoercionTyCon name coArity rule where coArity = length tvs - - rule args = (substTyWith tvs tys $ -- with sigma = [tys/tvs], + rule args = (substTyWith tvs args $ -- with sigma = [tys/tvs], TyConApp family instTys, -- sigma (F ts) - TyConApp rep_tycon tys, -- :=: R tys - rest) -- surplus arguments - where - tys = take coArity args - rest = drop coArity args + TyConApp rep_tycon args) -- :=: R tys -------------------------------------- -- Coercion Type Constructors... @@ -357,14 +323,6 @@ mkDataInstCoercion name tvs family instTys rep_tycon -- sym d :: p2=q2 -- sym e :: p3=q3 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3) --- --- (mkKindingFun f) is given the args [c, sym d, sym e] -mkKindingFun :: ([Type] -> (Type, Type, [Type])) -> [Type] -> Kind -mkKindingFun f args = - let (ty1, ty2, rest) = f args in - let (argtys1, argtys2) = unzip (map coercionKind rest) in - mkCoKind (mkAppTys ty1 argtys1) (mkAppTys ty2 argtys2) - symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon :: TyCon -- Each coercion TyCon is built with the special CoercionTyCon record and @@ -372,33 +330,34 @@ symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, ins -- 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 = - mkCoercionTyCon symCoercionTyConName 1 (mkKindingFun flipCoercionKindOf) + mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf where - flipCoercionKindOf (co:rest) = (ty2, ty1, rest) + flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1) where (ty1, ty2) = coercionKind co transCoercionTyCon = - mkCoercionTyCon transCoercionTyConName 2 (mkKindingFun composeCoercionKindsOf) + mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf where - composeCoercionKindsOf (co1:co2:rest) = + composeCoercionKindsOf (co1:co2:rest) + = ASSERT( null rest ) WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug") - (a1, r2, rest) + (a1, r2) where (a1, r1) = coercionKind co1 (a2, r2) = coercionKind co2 leftCoercionTyCon = - mkCoercionTyCon leftCoercionTyConName 1 (mkKindingFun leftProjectCoercionKindOf) + mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf where - leftProjectCoercionKindOf (co:rest) = (ty1, ty2, rest) + leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2) where (ty1,ty2) = fst (splitCoercionKindOf co) rightCoercionTyCon = - mkCoercionTyCon rightCoercionTyConName 1 (mkKindingFun rightProjectCoercionKindOf) + mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf where - rightProjectCoercionKindOf (co:rest) = (ty1, ty2, rest) + rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2) where (ty1,ty2) = snd (splitCoercionKindOf co) @@ -414,25 +373,26 @@ splitCoercionKindOf co = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2)) instCoercionTyCon - = mkCoercionTyCon instCoercionTyConName 2 (mkKindingFun instCoercionKind) + = mkCoercionTyCon instCoercionTyConName 2 instCoercionKind where instantiateCo t s = let Just (tv, ty) = splitForAllTy_maybe t in substTyWith [tv] [s] ty - instCoercionKind (co1:ty:rest) = (instantiateCo t1 ty, instantiateCo t2 ty, rest) + instCoercionKind (co1:ty:rest) = ASSERT( null rest ) + (instantiateCo t1 ty, instantiateCo t2 ty) where (t1, t2) = coercionKind co1 unsafeCoercionTyCon - = mkCoercionTyCon unsafeCoercionTyConName 2 (mkKindingFun unsafeCoercionKind) + = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind where - unsafeCoercionKind (ty1:ty2:rest) = (ty1,ty2,rest) + unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2) -------------------------------------- -- ...and their names mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ) - key Nothing (ATyCon coCon) BuiltInSyntax + key (ATyCon coCon) BuiltInSyntax transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon symCoercionTyConName = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon @@ -451,7 +411,7 @@ splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion) splitNewTypeRepCo_maybe ty | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty' splitNewTypeRepCo_maybe (TyConApp tc tys) - | isNewTyCon tc + | isClosedNewTyCon tc = ASSERT( tys `lengthIs` tyConArity tc ) -- splitNewTypeRepCo_maybe only be applied -- to *types* (of kind *) case newTyConRhs tc of @@ -459,6 +419,6 @@ splitNewTypeRepCo_maybe (TyConApp tc tys) ASSERT( length tvs == length tys ) Just (substTyWith tvs tys rep_ty, mkTyConApp co_con tys) where - co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo tc) + co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo_maybe tc) splitNewTypeRepCo_maybe other = Nothing \end{code}