X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FCoercion.lhs;h=faab46304421562cc7ab117447019d7bf650a5b7;hp=83a5af341cacc4c33acb5a8a390b2852b47ee2b8;hb=c80364f8e4681b34e974f5df36ecdacec7cd9cd8;hpb=bcadca676448e38427b910bad5d7063f948a99c8 diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 83a5af3..faab463 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -1,27 +1,36 @@ -T% +% % (c) The University of Glasgow 2006 % \begin{code} -{-# OPTIONS -fno-warn-incomplete-patterns #-} --- The above warning supression flag is a temporary kludge. --- While working on this module you are encouraged to remove it and fix --- any warnings in the module. See --- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings --- for details - --- | Module for type coercions, as used in System FC. See 'CoreSyn.Expr' for +-- | Module for (a) type kinds and (b) type coercions, +-- as used in System FC. See 'CoreSyn.Expr' for -- more on System FC and how coercions fit into it. -- -- Coercions are represented as types, and their kinds tell what types the --- coercion works on. The coercion kind constructor is a special TyCon that must always be saturated, like so: +-- coercion works on. The coercion kind constructor is a special TyCon that +-- must always be saturated, like so: -- --- > typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type] +-- > typeKind (symCoercion type) :: TyConApp CoTyCon{...} [type, type] module Coercion ( -- * Main data type - Coercion, - - mkCoKind, mkReflCoKind, coVarKind, + Coercion, Kind, + typeKind, + + -- ** Deconstructing Kinds + kindFunResult, kindAppResult, synTyConResKind, + splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe, + + -- ** Predicates on Kinds + isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, + isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, + isCoSuperKind, isSuperKind, isCoercionKind, + mkArrowKind, mkArrowKinds, + + isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind, + isSubKindCon, + + mkCoKind, mkCoPredTy, coVarKind, coVarKind_maybe, coercionKind, coercionKinds, isIdentityCoercion, -- ** Equality predicates @@ -30,24 +39,28 @@ module Coercion ( -- ** Coercion transformations mkCoercion, mkSymCoercion, mkTransCoercion, - mkLeftCoercion, mkRightCoercion, mkRightCoercions, + mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion, mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion, mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion, mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion, - splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo, + mkClassPPredCo, mkIParamPredCo, mkEqPredCo, + mkCoVarCoercion, mkCoPredCo, + unsafeCoercionTyCon, symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon, - -- ** Optimisation - optCoercion, + -- ** Decomposition + decompLR_maybe, decompCsel_maybe, decompInst_maybe, + splitCoPredTy_maybe, + splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo, -- ** Comparison - coreEqCoercion, + coreEqCoercion, coreEqCoercion2, -- * CoercionI CoercionI(..), @@ -55,8 +68,8 @@ module Coercion ( mkSymCoI, mkTransCoI, mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI, mkForAllTyCoI, - fromCoI, fromACo, - mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI + fromCoI, + mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, mkCoPredCoI ) where @@ -67,13 +80,156 @@ import Type import TyCon import Class import Var +import VarEnv +import VarSet import Name import PrelNames import Util import BasicTypes import Outputable import FastString +\end{code} + +%************************************************************************ +%* * + Functions over Kinds +%* * +%************************************************************************ +\begin{code} +-- | Essentially 'funResultTy' on kinds +kindFunResult :: Kind -> Kind +kindFunResult k = funResultTy k + +kindAppResult :: Kind -> [arg] -> Kind +kindAppResult k [] = k +kindAppResult k (_:as) = kindAppResult (kindFunResult k) as + +-- | Essentially 'splitFunTys' on kinds +splitKindFunTys :: Kind -> ([Kind],Kind) +splitKindFunTys k = splitFunTys k + +splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind) +splitKindFunTy_maybe = splitFunTy_maybe + +-- | Essentially 'splitFunTysN' on kinds +splitKindFunTysN :: Int -> Kind -> ([Kind],Kind) +splitKindFunTysN k = splitFunTysN k + +-- | Find the result 'Kind' of a type synonym, +-- after applying it to its 'arity' number of type variables +-- Actually this function works fine on data types too, +-- but they'd always return '*', so we never need to ask +synTyConResKind :: TyCon -> Kind +synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon) + +-- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's +isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool +isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon, + isUnliftedTypeKindCon, isSubArgTypeKindCon :: TyCon -> Bool + +isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey + +isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc +isOpenTypeKind _ = False + +isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey + +isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc +isUbxTupleKind _ = False + +isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey + +isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc +isArgTypeKind _ = False + +isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey + +isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc +isUnliftedTypeKind _ = False + +isSubOpenTypeKind :: Kind -> Bool +-- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow) +isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) ) + ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) ) + False +isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True +isSubOpenTypeKind other = ASSERT( isKind other ) False + -- This is a conservative answer + -- It matters in the call to isSubKind in + -- checkExpectedKind. + +isSubArgTypeKindCon kc + | isUnliftedTypeKindCon kc = True + | isLiftedTypeKindCon kc = True + | isArgTypeKindCon kc = True + | otherwise = False + +isSubArgTypeKind :: Kind -> Bool +-- ^ True of any sub-kind of ArgTypeKind +isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc +isSubArgTypeKind _ = False + +-- | Is this a super-kind (i.e. a type-of-kinds)? +isSuperKind :: Type -> Bool +isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc +isSuperKind _ = False + +-- | Is this a kind (i.e. a type-of-types)? +isKind :: Kind -> Bool +isKind k = isSuperKind (typeKind k) + +isSubKind :: Kind -> Kind -> Bool +-- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@ +isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2 +isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2) +isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2')) + = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2' +isSubKind _ _ = False + +eqKind :: Kind -> Kind -> Bool +eqKind = tcEqType + +isSubKindCon :: TyCon -> TyCon -> Bool +-- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@ +isSubKindCon kc1 kc2 + | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True + | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True + | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True + | isOpenTypeKindCon kc2 = True + -- we already know kc1 is not a fun, its a TyCon + | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True + | otherwise = False + +defaultKind :: Kind -> Kind +-- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more +-- information on what that means + +-- When we generalise, we make generic type variables whose kind is +-- simple (* or *->* etc). So generic type variables (other than +-- built-in constants like 'error') always have simple kinds. This is important; +-- consider +-- f x = True +-- We want f to get type +-- f :: forall (a::*). a -> Bool +-- Not +-- f :: forall (a::??). a -> Bool +-- because that would allow a call like (f 3#) as well as (f True), +--and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr. +defaultKind k + | isSubOpenTypeKind k = liftedTypeKind + | isSubArgTypeKind k = liftedTypeKind + | otherwise = k +\end{code} + +%************************************************************************ +%* * + Coercions +%* * +%************************************************************************ + + +\begin{code} -- | A 'Coercion' represents a 'Type' something should be coerced to. type Coercion = Type @@ -95,28 +251,51 @@ decomposeCo n co go n co cos = go (n-1) (mkLeftCoercion co) (mkRightCoercion co : cos) ------------------------------- ------------------------------------------------------- -- and some coercion kind stuff coVarKind :: CoVar -> (Type,Type) -- c :: t1 ~ t2 -coVarKind cv = splitCoVarKind (tyVarKind cv) +coVarKind cv = case coVarKind_maybe cv of + Just ts -> ts + Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv)) + +coVarKind_maybe :: CoVar -> Maybe (Type,Type) +coVarKind_maybe cv = splitCoKind_maybe (tyVarKind cv) -- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'. -- Panics if the argument is not a valid 'CoercionKind' -splitCoVarKind :: Kind -> (Type, Type) -splitCoVarKind co | Just co' <- kindView co = splitCoVarKind co' -splitCoVarKind (PredTy (EqPred ty1 ty2)) = (ty1, ty2) +splitCoKind_maybe :: Kind -> Maybe (Type, Type) +splitCoKind_maybe co | Just co' <- kindView co = splitCoKind_maybe co' +splitCoKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2) +splitCoKind_maybe _ = Nothing --- | Makes a 'CoercionKind' from two types: the types whose equality is proven by the relevant 'Coercion' +-- | Makes a 'CoercionKind' from two types: the types whose equality +-- is proven by the relevant 'Coercion' mkCoKind :: Type -> Type -> CoercionKind mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2) -- | (mkCoPredTy s t r) produces the type: (s~t) => r mkCoPredTy :: Type -> Type -> Type -> Type -mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r +mkCoPredTy s t r = ASSERT( not (co_var `elemVarSet` tyVarsOfType r) ) + ForAllTy co_var r + where + co_var = mkWildCoVar (mkCoKind s t) + +mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion +-- Creates a coercion between (s1~t1) => r1 and (s2~t2) => r2 +mkCoPredCo = mkCoPredTy + + +splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type) +splitCoPredTy_maybe ty + | Just (cv,r) <- splitForAllTy_maybe ty + , isCoVar cv + , Just (s,t) <- coVarKind_maybe cv + = Just (s,t,r) + | otherwise + = Nothing -- | Tests whether a type is just a type equality predicate isEqPredTy :: Type -> Bool @@ -133,83 +312,6 @@ getEqPredTys :: PredType -> (Type,Type) getEqPredTys (EqPred ty1 ty2) = (ty1, ty2) getEqPredTys other = pprPanic "getEqPredTys" (ppr other) --- | Create a reflexive 'CoercionKind' that asserts that a type can be coerced to itself -mkReflCoKind :: Type -> CoercionKind -mkReflCoKind ty = mkCoKind ty ty - --- | If it is the case that --- --- > c :: (t1 ~ t2) --- --- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@. -coercionKind :: Coercion -> (Type, Type) -coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a - | otherwise = (ty, ty) -coercionKind (AppTy ty1 ty2) - = let (t1, t2) = coercionKind ty1 - (s1, s2) = coercionKind ty2 in - (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 - = 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) -coercionKind (FunTy ty1 ty2) - = let (t1, t2) = coercionKind ty1 - (s1, s2) = coercionKind ty2 in - (mkFunTy t1 s1, mkFunTy t2 s2) - -coercionKind (ForAllTy tv ty) - | isCoVar tv --- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2 --- ---------------------------------------------- --- c1~c2 => c3 :: (s1~t1) => r1 ~ (s2~t2) => r2 --- or --- forall (_:c1~c2) - = let (c1,c2) = coVarKind tv - (s1,s2) = coercionKind c1 - (t1,t2) = coercionKind c2 - (r1,r2) = coercionKind ty - in - (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2) - - | otherwise --- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2 --- ---------------------------------------------- --- forall a:k. c :: forall a:k. t1 ~ forall a:k. t2 - = let (ty1, ty2) = coercionKind ty in - (ForAllTy tv ty1, ForAllTy tv ty2) - -coercionKind (PredTy (EqPred c1 c2)) - = pprTrace "coercionKind" (pprEqPred (c1,c2)) $ - let k1 = coercionKindPredTy c1 - k2 = coercionKindPredTy c2 in - (k1,k2) - -- These should not show up in coercions at all - -- becuase they are in the form of for-alls - where - coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2 - - - -coercionKind (PredTy (ClassP cl args)) - = let (lArgs, rArgs) = coercionKinds args in - (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs)) -coercionKind (PredTy (IParam name ty)) - = let (ty1, ty2) = coercionKind ty in - (PredTy (IParam name ty1), PredTy (IParam name ty2)) - --- | Apply 'coercionKind' to multiple 'Coercion's -coercionKinds :: [Coercion] -> ([Type], [Type]) -coercionKinds tys = unzip $ map coercionKind tys - -------------------------------------- isIdentityCoercion :: Coercion -> Bool isIdentityCoercion co = case coercionKind co of @@ -232,6 +334,9 @@ mkCoercion :: TyCon -> [Type] -> Coercion mkCoercion coCon args = ASSERT( tyConArity coCon == length args ) TyConApp coCon args +mkCoVarCoercion :: CoVar -> Coercion +mkCoVarCoercion cv = mkTyVarTy cv + -- | Apply a 'Coercion' to another 'Coercion', which is presumably a -- 'Coercion' constructor of some kind mkAppCoercion :: Coercion -> Coercion -> Coercion @@ -248,12 +353,12 @@ mkTyConCoercion con cos = mkTyConApp con cos -- | Make a function 'Coercion' between two other 'Coercion's mkFunCoercion :: Coercion -> Coercion -> Coercion -mkFunCoercion co1 co2 = mkFunTy co1 co2 +mkFunCoercion co1 co2 = mkFunTy co1 co2 -- NB: Handles correctly the forall for eqpreds! -- | Make a 'Coercion' which binds a variable within an inner 'Coercion' mkForAllCoercion :: Var -> Coercion -> Coercion -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar) -mkForAllCoercion tv co = ASSERT ( isTyVar tv ) mkForAllTy tv co +mkForAllCoercion tv co = ASSERT ( isTyCoVar tv ) mkForAllTy tv co ------------------------------- @@ -262,97 +367,25 @@ mkSymCoercion :: Coercion -> Coercion -- ^ Create a symmetric version of the given 'Coercion' that asserts equality -- between the same types but in the other "direction", so a kind of @t1 ~ t2@ -- becomes the kind @t2 ~ t1@. --- --- This function attempts to simplify the generated 'Coercion' by removing --- redundant applications of @sym@. This is done by pushing this new @sym@ --- down into the 'Coercion' and exploiting the fact that @sym (sym co) = co@. -mkSymCoercion co - | Just co' <- coreView co = mkSymCoercion co' - -mkSymCoercion (ForAllTy tv ty) = ForAllTy tv (mkSymCoercion ty) -mkSymCoercion (AppTy co1 co2) = AppTy (mkSymCoercion co1) (mkSymCoercion co2) -mkSymCoercion (FunTy co1 co2) = FunTy (mkSymCoercion co1) (mkSymCoercion co2) - -mkSymCoercion (TyConApp tc cos) - | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos) - -mkSymCoercion (TyConApp tc [co]) - | tc `hasKey` symCoercionTyConKey = co -- sym (sym co) --> co - | tc `hasKey` leftCoercionTyConKey = mkLeftCoercion (mkSymCoercion co) - | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co) - -mkSymCoercion (TyConApp tc [co1,co2]) - | tc `hasKey` transCoercionTyConKey - -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2) - -- Note reversal of arguments! - = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1) - - | tc `hasKey` instCoercionTyConKey - -- sym (co @ ty) --> (sym co) @ ty - -- Note: sym is not applied to 'ty' - = mkInstCoercion (mkSymCoercion co1) co2 - -mkSymCoercion (TyConApp tc cos) -- Other coercion tycons, such as those - = mkCoercion symCoercionTyCon [TyConApp tc cos] -- arising from newtypes - -mkSymCoercion (TyVarTy tv) - | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv] - | otherwise = TyVarTy tv -- Reflexive - -------------------------------- --- ToDo: we should be cleverer about transitivity +mkSymCoercion g = mkCoercion symCoercionTyCon [g] mkTransCoercion :: Coercion -> Coercion -> Coercion -- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's. --- --- This function attempts to simplify the generated 'Coercion' by exploiting the fact that --- @sym g `trans` g = id@. -mkTransCoercion g1 g2 -- sym g `trans` g = id - | (t1,_) <- coercionKind g1 - , (_,t2) <- coercionKind g2 - , t1 `coreEqType` t2 - = t1 - - | otherwise - = mkCoercion transCoercionTyCon [g1, g2] - - -------------------------------- --- Smart constructors for left and right +mkTransCoercion g1 g2 = mkCoercion transCoercionTyCon [g1, g2] mkLeftCoercion :: Coercion -> Coercion -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of -- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then: -- -- > mkLeftCoercion c :: f ~ g -mkLeftCoercion co - | Just (co', _) <- splitAppCoercion_maybe co = co' - | otherwise = mkCoercion leftCoercionTyCon [co] +mkLeftCoercion co = mkCoercion leftCoercionTyCon [co] mkRightCoercion :: Coercion -> Coercion -- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of -- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then: -- -- > mkLeftCoercion c :: x ~ y -mkRightCoercion co - | Just (_, co2) <- splitAppCoercion_maybe co = co2 - | otherwise = mkCoercion rightCoercionTyCon [co] - -mkRightCoercions :: Int -> Coercion -> [Coercion] --- ^ As 'mkRightCoercion', but finds the 'Coercion's available on the right side of @n@ --- nested application 'Coercion's, manufacturing new left or right cooercions as necessary --- if suffficiently many are not directly available. -mkRightCoercions n co - = go n co [] - where - go n co acc - | n > 0 - = case splitAppCoercion_maybe co of - Just (co1,co2) -> go (n-1) co1 (co2:acc) - Nothing -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc) - | otherwise - = acc - +mkRightCoercion co = mkCoercion rightCoercionTyCon [co] mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co] @@ -363,79 +396,27 @@ mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co] mkInstCoercion :: Coercion -> Type -> Coercion -- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs -- the resulting beta-reduction, otherwise it creates a suspended instantiation. -mkInstCoercion co ty - | Just (tv,co') <- splitForAllTy_maybe co - = substTyWith [tv] [ty] co' -- (forall a.co) @ ty --> co[ty/a] - | otherwise - = mkCoercion instCoercionTyCon [co, ty] +mkInstCoercion co ty = mkCoercion instCoercionTyCon [co, ty] mkInstsCoercion :: Coercion -> [Type] -> Coercion -- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right mkInstsCoercion co tys = foldl mkInstCoercion co tys -{- -splitSymCoercion_maybe :: Coercion -> Maybe Coercion -splitSymCoercion_maybe (TyConApp tc [co]) = - if tc `hasKey` symCoercionTyConKey - then Just co - else Nothing -splitSymCoercion_maybe co = Nothing --} - -splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion) --- ^ Splits a coercion application, being careful *not* to split @left c@ etc. --- This is because those are really syntactic constructs, not applications -splitAppCoercion_maybe co | Just co' <- coreView co = splitAppCoercion_maybe co' -splitAppCoercion_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2) -splitAppCoercion_maybe (AppTy ty1 ty2) = Just (ty1, ty2) -splitAppCoercion_maybe (TyConApp tc tys) - | not (isCoercionTyCon tc) - = case snocView tys of - Just (tys', ty') -> Just (TyConApp tc tys', ty') - Nothing -> Nothing -splitAppCoercion_maybe _ = Nothing - -{- -splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion) -splitTransCoercion_maybe (TyConApp tc [ty1, ty2]) - = if tc `hasKey` transCoercionTyConKey then - Just (ty1, ty2) - else - Nothing -splitTransCoercion_maybe other = Nothing - -splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type) -splitInstCoercion_maybe (TyConApp tc [ty1, ty2]) - = if tc `hasKey` instCoercionTyConKey then - Just (ty1, ty2) - else - Nothing -splitInstCoercion_maybe other = Nothing - -splitLeftCoercion_maybe :: Coercion -> Maybe Coercion -splitLeftCoercion_maybe (TyConApp tc [co]) - = if tc `hasKey` leftCoercionTyConKey then - Just co - else - Nothing -splitLeftCoercion_maybe other = Nothing - -splitRightCoercion_maybe :: Coercion -> Maybe Coercion -splitRightCoercion_maybe (TyConApp tc [co]) - = if tc `hasKey` rightCoercionTyConKey then - Just co - else - Nothing -splitRightCoercion_maybe other = Nothing --} - -- | Manufacture a coercion from this air. Needless to say, this is not usually safe, -- but it is used when we know we are dealing with bottom, which is one case in which -- it is safe. This is also used implement the @unsafeCoerce#@ primitive. +-- Optimise by pushing down through type constructors mkUnsafeCoercion :: Type -> Type -> Coercion -mkUnsafeCoercion ty1 ty2 - = mkCoercion unsafeCoercionTyCon [ty1, ty2] +mkUnsafeCoercion (TyConApp tc1 tys1) (TyConApp tc2 tys2) + | tc1 == tc2 + = TyConApp tc1 (zipWith mkUnsafeCoercion tys1 tys2) +mkUnsafeCoercion (FunTy a1 r1) (FunTy a2 r2) + = FunTy (mkUnsafeCoercion a1 a2) (mkUnsafeCoercion r1 r2) + +mkUnsafeCoercion ty1 ty2 + | ty1 `coreEqType` ty2 = ty1 + | otherwise = mkCoercion unsafeCoercionTyCon [ty1, ty2] -- See note [Newtype coercions] in TyCon @@ -445,12 +426,12 @@ mkUnsafeCoercion ty1 ty2 -- a subset of those 'TyVar's. mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon mkNewTypeCoercion name tycon tvs rhs_ty - = mkCoercionTyCon name co_con_arity rule + = mkCoercionTyCon name arity desc where - co_con_arity = length tvs - - rule args = ASSERT( co_con_arity == length args ) - (TyConApp tycon args, substTyWith tvs args rhs_ty) + arity = length tvs + desc = CoAxiom { co_ax_tvs = tvs + , co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs) + , co_ax_rhs = rhs_ty } -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type -- and its family instance. It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is @@ -462,13 +443,25 @@ mkFamInstCoercion :: Name -- ^ Unique name for the coercion tycon -> [Type] -- ^ Type instance (@ts@) -> TyCon -- ^ Representation tycon (@R@) -> TyCon -- ^ Coercion tycon (@Co@) -mkFamInstCoercion name tvs family instTys rep_tycon - = mkCoercionTyCon name coArity rule +mkFamInstCoercion name tvs family inst_tys rep_tycon + = mkCoercionTyCon name arity desc where - coArity = length tvs - rule args = (substTyWith tvs args $ -- with sigma = [tys/tvs], - TyConApp family instTys, -- sigma (F ts) - TyConApp rep_tycon args) -- ~ R tys + arity = length tvs + desc = CoAxiom { co_ax_tvs = tvs + , co_ax_lhs = mkTyConApp family inst_tys + , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) } + + +mkClassPPredCo :: Class -> [Coercion] -> Coercion +mkClassPPredCo cls = (PredTy . ClassP cls) + +mkIParamPredCo :: (IPName Name) -> Coercion -> Coercion +mkIParamPredCo ipn = (PredTy . IParam ipn) + +mkEqPredCo :: Coercion -> Coercion -> Coercion +mkEqPredCo co1 co2 = PredTy (EqPred co1 co2) + + \end{code} @@ -497,102 +490,15 @@ symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon, csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon -symCoercionTyCon = - mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf - where - flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1) - where - (ty1, ty2) = coercionKind co - -transCoercionTyCon = - mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf - where - composeCoercionKindsOf (co1:co2:rest) - = ASSERT( null rest ) - WARN( not (r1 `coreEqType` a2), - text "Strange! Type mismatch in trans coercion, probably a bug" - $$ - _err_stuff ) - (a1, r2) - where - (a1, r1) = coercionKind co1 - (a2, r2) = coercionKind co2 - - _err_stuff = vcat [ text "co1:" <+> ppr co1 - , text "co1 kind left:" <+> ppr a1 - , text "co1 kind right:" <+> ppr r1 - , text "co2:" <+> ppr co2 - , text "co2 kind left:" <+> ppr a2 - , text "co2 kind right:" <+> ppr r2 ] - ---------------------------------------------------- -leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 (fst . decompLR) -rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (snd . decompLR) - -decompLR :: [Type] -> ((Type,Type), (Type,Type)) --- Helper for left and right. Finds coercion kind of its input and --- returns the left and right projections of the coercion... --- --- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2)) -decompLR (co : rest) - | (ty1, ty2) <- coercionKind co - , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1 - , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2 - = ASSERT( null rest) - ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2)) -decompLR cos - = pprPanic "Coercion.decompLR" - (ppr cos $$ vcat (map (pprEqPred .coercionKind) cos)) - ---------------------------------------------------- -instCoercionTyCon - = mkCoercionTyCon instCoercionTyConName 2 instCoercionKind - where - instantiateCo t s = - let Just (tv, ty) = splitForAllTy_maybe t in - substTyWith [tv] [s] ty - - instCoercionKind (co1:ty:rest) = ASSERT( null rest ) - (instantiateCo t1 ty, instantiateCo t2 ty) - where (t1, t2) = coercionKind co1 - ---------------------------------------------------- -unsafeCoercionTyCon - = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind - where - unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2) - ---------------------------------------------------- --- The csel* family --- If co :: (s1~t1 => r1) ~ (s2~t2 => r2) --- Then csel1 co :: s1 ~ s2 --- csel2 co :: t1 ~ t2 --- cselR co :: r1 ~ r2 - -csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 (fstOf3 . decompCsel) -csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 (sndOf3 . decompCsel) -cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 (thirdOf3 . decompCsel) - -decompCsel :: [Coercion] -> ((Type,Type), (Type,Type), (Type,Type)) -decompCsel (co : rest) - | (ty1,ty2) <- coercionKind co - , Just (cv1, r1) <- splitForAllTy_maybe ty1 - , Just (cv2, r2) <- splitForAllTy_maybe ty2 - , (s1,t1) <- ASSERT( isCoVar cv1) coVarKind cv1 - , (s2,t2) <- ASSERT( isCoVar cv1) coVarKind cv2 - = ASSERT( null rest ) - ((s1,s2), (t1,t2), (r1,r2)) -decompCsel other = pprPanic "decompCsel" (ppr other) - -fstOf3 :: (a,b,c) -> a -sndOf3 :: (a,b,c) -> b -thirdOf3 :: (a,b,c) -> c -fstOf3 (a,_,_) = a -sndOf3 (_,b,_) = b -thirdOf3 (_,_,c) = c - --------------------------------------- --- Their Names +symCoercionTyCon = mkCoercionTyCon symCoercionTyConName 1 CoSym +transCoercionTyCon = mkCoercionTyCon transCoercionTyConName 2 CoTrans +leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 CoLeft +rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 CoRight +instCoercionTyCon = mkCoercionTyCon instCoercionTyConName 2 CoInst +csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 CoCsel1 +csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 CoCsel2 +cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 CoCselR +unsafeCoercionTyCon = mkCoercionTyCon unsafeCoercionTyConName 2 CoUnsafe transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName, @@ -613,6 +519,40 @@ mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ) key (ATyCon coCon) BuiltInSyntax \end{code} +\begin{code} +------------ +decompLR_maybe :: (Type,Type) -> Maybe ((Type,Type), (Type,Type)) +-- Helper for left and right. Finds coercion kind of its input and +-- returns the left and right projections of the coercion... +-- +-- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2)) +decompLR_maybe (ty1,ty2) + | Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1 + , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2 + = Just ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2)) +decompLR_maybe _ = Nothing + +------------ +decompInst_maybe :: (Type, Type) -> Maybe ((TyVar,TyVar), (Type,Type)) +decompInst_maybe (ty1, ty2) + | Just (tv1,r1) <- splitForAllTy_maybe ty1 + , Just (tv2,r2) <- splitForAllTy_maybe ty2 + = Just ((tv1,tv2), (r1,r2)) +decompInst_maybe _ = Nothing + +------------ +decompCsel_maybe :: (Type, Type) -> Maybe ((Type,Type), (Type,Type), (Type,Type)) +-- If co :: (s1~t1 => r1) ~ (s2~t2 => r2) +-- Then csel1 co :: s1 ~ s2 +-- csel2 co :: t1 ~ t2 +-- cselR co :: r1 ~ r2 +decompCsel_maybe (ty1, ty2) + | Just (s1, t1, r1) <- splitCoPredTy_maybe ty1 + , Just (s2, t2, r2) <- splitCoPredTy_maybe ty2 + = Just ((s1,s2), (t1,t2), (r1,r2)) +decompCsel_maybe _ = Nothing +\end{code} + %************************************************************************ %* * @@ -630,8 +570,8 @@ instNewTyCon_maybe tc tys = ASSERT( tys `lengthIs` tyConArity tc ) Just (substTyWith tvs tys ty, case mb_co_tc of - Nothing -> IdCo - Just co_tc -> ACo (mkTyConApp co_tc tys)) + Nothing -> IdCo (mkTyConApp tc tys) + Just co_tc -> ACo (mkTyConApp co_tc tys)) | otherwise = Nothing @@ -651,7 +591,7 @@ splitNewTypeRepCo_maybe (TyConApp tc tys) | Just (ty', coi) <- instNewTyCon_maybe tc tys = case coi of ACo co -> Just (ty', co) - IdCo -> panic "splitNewTypeRepCo_maybe" + IdCo _ -> panic "splitNewTypeRepCo_maybe" -- This case handled by coreView splitNewTypeRepCo_maybe _ = Nothing @@ -659,6 +599,9 @@ splitNewTypeRepCo_maybe _ -- | Determines syntactic equality of coercions coreEqCoercion :: Coercion -> Coercion -> Bool coreEqCoercion = coreEqType + +coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool +coreEqCoercion2 = coreEqType2 \end{code} @@ -679,192 +622,236 @@ coreEqCoercion = coreEqType -- 1. A proper 'Coercion' -- -- 2. The identity coercion -data CoercionI = IdCo | ACo Coercion +data CoercionI = IdCo Type | ACo Coercion + +liftCoI :: (Type -> Type) -> CoercionI -> CoercionI +liftCoI f (IdCo ty) = IdCo (f ty) +liftCoI f (ACo ty) = ACo (f ty) + +liftCoI2 :: (Type -> Type -> Type) -> CoercionI -> CoercionI -> CoercionI +liftCoI2 f (IdCo ty1) (IdCo ty2) = IdCo (f ty1 ty2) +liftCoI2 f coi1 coi2 = ACo (f (fromCoI coi1) (fromCoI coi2)) + +liftCoIs :: ([Type] -> Type) -> [CoercionI] -> CoercionI +liftCoIs f cois = go_id [] cois + where + go_id rev_tys [] = IdCo (f (reverse rev_tys)) + go_id rev_tys (IdCo ty : cois) = go_id (ty:rev_tys) cois + go_id rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois + + go_aco rev_tys [] = ACo (f (reverse rev_tys)) + go_aco rev_tys (IdCo ty : cois) = go_aco (ty:rev_tys) cois + go_aco rev_tys (ACo co : cois) = go_aco (co:rev_tys) cois instance Outputable CoercionI where - ppr IdCo = ptext (sLit "IdCo") + ppr (IdCo _) = ptext (sLit "IdCo") ppr (ACo co) = ppr co isIdentityCoI :: CoercionI -> Bool -isIdentityCoI IdCo = True -isIdentityCoI _ = False - --- | Tests whether all the given 'CoercionI's represent the identity coercion -allIdCoIs :: [CoercionI] -> Bool -allIdCoIs = all isIdentityCoI - --- | For each 'CoercionI' in the input list, return either the 'Coercion' it --- contains or the corresponding 'Type' from the other list -zipCoArgs :: [CoercionI] -> [Type] -> [Coercion] -zipCoArgs cois tys = zipWith fromCoI cois tys +isIdentityCoI (IdCo _) = True +isIdentityCoI (ACo _) = False -- | Return either the 'Coercion' contained within the 'CoercionI' or the given -- 'Type' if the 'CoercionI' is the identity 'Coercion' -fromCoI :: CoercionI -> Type -> Type -fromCoI IdCo ty = ty -- Identity coercion represented -fromCoI (ACo co) _ = co -- by the type itself +fromCoI :: CoercionI -> Type +fromCoI (IdCo ty) = ty -- Identity coercion represented +fromCoI (ACo co) = co -- by the type itself -- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion' mkSymCoI :: CoercionI -> CoercionI -mkSymCoI IdCo = IdCo -mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co] +mkSymCoI (IdCo ty) = IdCo ty +mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co] -- the smart constructor -- is too smart with tyvars -- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion' mkTransCoI :: CoercionI -> CoercionI -> CoercionI -mkTransCoI IdCo aco = aco -mkTransCoI aco IdCo = aco +mkTransCoI (IdCo _) aco = aco +mkTransCoI aco (IdCo _) = aco mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion' -mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI -mkTyConAppCoI tyCon tys cois - | allIdCoIs cois = IdCo - | otherwise = ACo (TyConApp tyCon (zipCoArgs cois tys)) +mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionI +mkTyConAppCoI tyCon cois = liftCoIs (mkTyConApp tyCon) cois -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion' -mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI -mkAppTyCoI _ IdCo _ IdCo = IdCo -mkAppTyCoI ty1 coi1 ty2 coi2 = - ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2) +mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI +mkAppTyCoI = liftCoI2 mkAppTy --- | Smart constructor for function-'Coercion's on 'CoercionI', see also 'mkFunCoercion' -mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI -mkFunTyCoI _ IdCo _ IdCo = IdCo -mkFunTyCoI ty1 coi1 ty2 coi2 = - ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2) +mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI +mkFunTyCoI = liftCoI2 mkFunTy -- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion' mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI -mkForAllTyCoI _ IdCo = IdCo -mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co - --- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion, --- panic -fromACo :: CoercionI -> Coercion -fromACo (ACo co) = co +mkForAllTyCoI tv = liftCoI (ForAllTy tv) -- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies: -- -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois)) -mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI -mkClassPPredCoI cls tys cois - | allIdCoIs cois = IdCo - | otherwise = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys) +mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI +mkClassPPredCoI cls = liftCoIs (PredTy . ClassP cls) -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI' mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI -mkIParamPredCoI _ IdCo = IdCo -mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co +mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn) -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI' -mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI -mkEqPredCoI _ IdCo _ IdCo = IdCo -mkEqPredCoI ty1 IdCo _ (ACo co2) = ACo $ PredTy $ EqPred ty1 co2 -mkEqPredCoI _ (ACo co1) ty2 coi2 = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2) +mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI +mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2)) + +mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI +mkCoPredCoI coi1 coi2 coi3 = mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3 + + \end{code} %************************************************************************ -%* * - Optimising coercions -%* * +%* * + The kind of a type, and of a coercion +%* * %************************************************************************ \begin{code} -optCoercion :: Coercion -> Coercion -optCoercion co - = ASSERT2( coercionKind co `eq` coercionKind result, - ppr co $$ ppr result $$ ppr (coercionKind co) $$ ppr (coercionKind result) ) - result +typeKind :: Type -> Kind +typeKind ty@(TyConApp tc tys) + | isCoercionTyCon tc = typeKind (fst (coercionKind ty)) + | otherwise = kindAppResult (tyConKind tc) tys + -- During coercion optimisation we *do* match a type + -- against a coercion (see OptCoercion.matchesAxiomLhs) + -- So the use of typeKind in Unify.match_kind must work on coercions too + -- Hence the isCoercionTyCon case above + +typeKind (PredTy pred) = predKind pred +typeKind (AppTy fun _) = kindFunResult (typeKind fun) +typeKind (ForAllTy _ ty) = typeKind ty +typeKind (TyVarTy tyvar) = tyVarKind tyvar +typeKind (FunTy _arg res) + -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*), + -- not unliftedTypKind (#) + -- The only things that can be after a function arrow are + -- (a) types (of kind openTypeKind or its sub-kinds) + -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *)) + | isTySuperKind k = k + | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind + where + k = typeKind res + +------------------ +predKind :: PredType -> Kind +predKind (EqPred {}) = coSuperKind -- A coercion kind! +predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are +predKind (IParam {}) = liftedTypeKind -- always represented by lifted types + +------------------ +-- | If it is the case that +-- +-- > c :: (t1 ~ t2) +-- +-- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, +-- then @coercionKind c = (t1, t2)@. +coercionKind :: Coercion -> (Type, Type) +coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a + | otherwise = (ty, ty) +coercionKind (AppTy ty1 ty2) + = let (s1, t1) = coercionKind ty1 + (s2, t2) = coercionKind ty2 in + (mkAppTy s1 s2, mkAppTy t1 t2) +coercionKind co@(TyConApp tc args) + | Just (ar, desc) <- isCoercionTyCon_maybe tc + -- CoercionTyCons carry their kinding rule, so we use it here + = WARN( not (length args >= ar), ppr co ) -- Always saturated + (let (ty1, ty2) = coTyConAppKind desc (take ar 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) + +coercionKind (FunTy ty1 ty2) + = let (t1, t2) = coercionKind ty1 + (s1, s2) = coercionKind ty2 in + (mkFunTy t1 s1, mkFunTy t2 s2) + +coercionKind (ForAllTy tv ty) + | isCoVar tv +-- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2 +-- ---------------------------------------------- +-- c1~c2 => c3 :: (s1~t1) => r1 ~ (s2~t2) => r2 +-- or +-- forall (_:c1~c2) + = let (c1,c2) = coVarKind tv + (s1,s2) = coercionKind c1 + (t1,t2) = coercionKind c2 + (r1,r2) = coercionKind ty + in + (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2) + + | otherwise +-- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2 +-- ---------------------------------------------- +-- forall a:k. c :: forall a:k. t1 ~ forall a:k. t2 + = let (ty1, ty2) = coercionKind ty in + (ForAllTy tv ty1, ForAllTy tv ty2) + +coercionKind (PredTy (ClassP cl args)) + = let (lArgs, rArgs) = coercionKinds args in + (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs)) +coercionKind (PredTy (IParam name ty)) + = let (ty1, ty2) = coercionKind ty in + (PredTy (IParam name ty1), PredTy (IParam name ty2)) +coercionKind (PredTy (EqPred c1 c2)) + = pprTrace "coercionKind" (pprEqPred (c1,c2)) $ + -- These should not show up in coercions at all + -- becuase they are in the form of for-alls + let k1 = coercionKindPredTy c1 + k2 = coercionKindPredTy c2 in + (k1,k2) + where + coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2 + +------------------ +-- | Apply 'coercionKind' to multiple 'Coercion's +coercionKinds :: [Coercion] -> ([Type], [Type]) +coercionKinds tys = unzip $ map coercionKind tys + +------------------ +-- | 'coTyConAppKind' is given a list of the type arguments to the 'CoTyCon', +-- and constructs the types that the resulting coercion relates. +-- Fails (in the monad) if ill-kinded. +-- Typically the monad is +-- either the Lint monad (with the consistency-check flag = True), +-- or the ID monad with a panic on failure (and the consistency-check flag = False) +coTyConAppKind + :: CoTyConDesc + -> [Type] -- Exactly right number of args + -> (Type, Type) -- Kind of this application +coTyConAppKind CoUnsafe (ty1:ty2:_) + = (ty1,ty2) +coTyConAppKind CoSym (co:_) + | (ty1,ty2) <- coercionKind co = (ty2,ty1) +coTyConAppKind CoTrans (co1:co2:_) + = (fst (coercionKind co1), snd (coercionKind co2)) +coTyConAppKind CoLeft (co:_) + | Just (res,_) <- decompLR_maybe (coercionKind co) = res +coTyConAppKind CoRight (co:_) + | Just (_,res) <- decompLR_maybe (coercionKind co) = res +coTyConAppKind CoCsel1 (co:_) + | Just (res,_,_) <- decompCsel_maybe (coercionKind co) = res +coTyConAppKind CoCsel2 (co:_) + | Just (_,res,_) <- decompCsel_maybe (coercionKind co) = res +coTyConAppKind CoCselR (co:_) + | Just (_,_,res) <- decompCsel_maybe (coercionKind co) = res +coTyConAppKind CoInst (co:ty:_) + | Just ((tv1,tv2), (ty1,ty2)) <- decompInst_maybe (coercionKind co) + = (substTyWith [tv1] [ty] ty1, substTyWith [tv2] [ty] ty2) +coTyConAppKind (CoAxiom { co_ax_tvs = tvs + , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos + = (substTyWith tvs tys1 lhs_ty, substTyWith tvs tys2 rhs_ty) where - (s1,t1) `eq` (s2,t2) = s1 `coreEqType` s2 && t1 `coreEqType` t2 - - (result,_,_) = go co - -- optimized, changed?, identity? - go :: Coercion -> ( Coercion, Bool, Bool ) - -- traverse coercion term bottom up and return - -- - -- 1) equivalent coercion, in optimized form - -- - -- 2) whether the output coercion differs from - -- the input coercion - -- - -- 3) whether the coercion is an identity coercion - -- - -- Performs the following optimizations: - -- - -- sym id >-> id - -- trans id co >-> co - -- trans co id >-> co - -- - go ty@(TyVarTy a) | isCoVar a = let (ty1,ty2) = coercionKind ty - in (ty, False, ty1 `coreEqType` ty2) - | otherwise = (ty, False, True) - go ty@(AppTy ty1 ty2) - = let (ty1', chan1, id1) = go ty1 - (ty2', chan2, id2) = go ty2 - in if chan1 || chan2 - then (AppTy ty1' ty2', True, id1 && id2) - else (ty , False, id1 && id2) - go ty@(TyConApp tc args) - | tc == symCoercionTyCon, [ty1] <- args - = case go ty1 of - (ty1', _ , True) -> (ty1', True, True) - (ty1', True, _ ) -> (TyConApp tc [ty1'], True, False) - (_ , _ , _ ) -> (ty, False, False) - | tc == transCoercionTyCon, [ty1,ty2] <- args - = let (ty1', chan1, id1) = go ty1 - (ty2', chan2, id2) = go ty2 - in if id1 - then (ty2', True, id2) - else if id2 - then (ty1', True, False) - else if chan1 || chan2 - then (TyConApp tc [ty1',ty2'], True , False) - else (ty , False, False) - | tc == leftCoercionTyCon, [ty1] <- args - = let (ty1', chan1, id1) = go ty1 - in if chan1 - then (TyConApp tc [ty1'], True , id1) - else (ty , False, id1) - | tc == rightCoercionTyCon, [ty1] <- args - = let (ty1', chan1, id1) = go ty1 - in if chan1 - then (TyConApp tc [ty1'], True , id1) - else (ty , False, id1) - | not (isCoercionTyCon tc) - = let (args', chans, ids) = mapAndUnzip3 go args - in if or chans - then (TyConApp tc args', True , and ids) - else (ty , False, and ids) - | otherwise - = (ty, False, False) - go ty@(FunTy ty1 ty2) - = let (ty1',chan1,id1) = go ty1 - (ty2',chan2,id2) = go ty2 - in if chan1 || chan2 - then (FunTy ty1' ty2', True , id1 && id2) - else (ty , False, id1 && id2) - go ty@(ForAllTy tv ty1) - = let (ty1', chan1, id1) = go ty1 - in if chan1 - then (ForAllTy tv ty1', True , id1) - else (ty , False, id1) - go ty@(PredTy (EqPred ty1 ty2)) - = let (ty1', chan1, id1) = go ty1 - (ty2', chan2, id2) = go ty2 - in if chan1 || chan2 - then (PredTy (EqPred ty1' ty2'), True , id1 && id2) - else (ty , False, id1 && id2) - go ty@(PredTy (ClassP cl args)) - = let (args', chans, ids) = mapAndUnzip3 go args - in if or chans - then (PredTy (ClassP cl args'), True , and ids) - else (ty , False, and ids) - go ty@(PredTy (IParam name ty1)) - = let (ty1', chan1, id1) = go ty1 - in if chan1 - then (PredTy (IParam name ty1'), True , id1) - else (ty , False, id1) + (tys1, tys2) = coercionKinds cos +coTyConAppKind desc cos = pprTrace "coTyConAppKind" (ppr desc $$ braces (vcat + [ ppr co <+> dcolon <+> pprEqPred (coercionKind co) + | co <- cos ])) $ + coercionKind (head cos) \end{code}