X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FType.lhs;h=f894cd304f1e0bac556c732613af689dbf0e647d;hp=63633e9694eb93cd752dafdc9d89c5f82ca226d2;hb=b06d623b2e367a572de5daf06d6a0b12c2740471;hpb=2cd930397966d27a221998c8ac060151e2027e90 diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index 63633e9..f894cd3 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -36,19 +36,18 @@ module Type ( mkTyConApp, mkTyConTy, tyConAppTyCon, tyConAppArgs, splitTyConApp_maybe, splitTyConApp, - splitNewTyConApp_maybe, splitNewTyConApp, mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, - applyTy, applyTys, isForAllTy, dropForAlls, + applyTy, applyTys, applyTysD, isForAllTy, dropForAlls, -- (Newtypes) - newTyConInstRhs, + newTyConInstRhs, carefullySplitNewType_maybe, -- (Type families) - tyFamInsts, + tyFamInsts, predFamInsts, -- (Source types) - mkPredTy, mkPredTys, mkFamilyTyConApp, + mkPredTy, mkPredTys, mkFamilyTyConApp, isEqPred, -- ** Common type constructors funTyCon, @@ -64,9 +63,6 @@ module Type ( -- $kind_subtyping Kind, SimpleKind, KindVar, - -- ** Deconstructing Kinds - kindFunResult, splitKindFunTys, splitKindFunTysN, - -- ** Common Kinds and SuperKinds liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind, @@ -77,18 +73,9 @@ module Type ( liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon, argTypeKindTyCon, ubxTupleKindTyCon, - -- ** Predicates on Kinds - isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, - isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, - isCoSuperKind, isSuperKind, isCoercionKind, isEqPred, - mkArrowKind, mkArrowKinds, - - isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind, - isSubKindCon, - -- * Type free variables tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta, - typeKind, + expandTypeSynonyms, -- * Tidying type related things up for printing tidyType, tidyTypes, @@ -99,7 +86,8 @@ module Type ( tidyKind, -- * Type comparison - coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, + coreEqType, coreEqType2, + tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, tcEqPred, tcEqPredX, tcCmpPred, tcEqTypeX, tcPartOfType, tcPartOfPred, -- * Forcing evaluation of types @@ -123,17 +111,18 @@ module Type ( emptyTvSubstEnv, emptyTvSubst, mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst, - getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, + getTvSubstEnv, setTvSubstEnv, zapTvSubstEnv, getTvInScope, + extendTvInScope, extendTvInScopeList, extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv, isEmptyTvSubst, -- ** Performing substitution on types - substTy, substTys, substTyWith, substTheta, + substTy, substTys, substTyWith, substTysWith, substTheta, substPred, substTyVar, substTyVars, substTyVarBndr, deShadowTy, lookupTyVar, -- * Pretty-printing pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll, - pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind, + pprPred, pprEqPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind, pprSourceTyCon ) where @@ -152,7 +141,6 @@ import VarSet import Name import Class -import PrelNames import TyCon -- others @@ -282,6 +270,29 @@ tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys tcView _ = Nothing ----------------------------------------------- +expandTypeSynonyms :: Type -> Type +-- ^ Expand out all type synonyms. Actually, it'd suffice to expand out +-- just the ones that discard type variables (e.g. type Funny a = Int) +-- But we don't know which those are currently, so we just expand all. +expandTypeSynonyms ty + = go ty + where + go (TyConApp tc tys) + | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys + = go (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys') + | otherwise + = TyConApp tc (map go tys) + go (TyVarTy tv) = TyVarTy tv + go (AppTy t1 t2) = AppTy (go t1) (go t2) + go (FunTy t1 t2) = FunTy (go t1) (go t2) + go (ForAllTy tv t) = ForAllTy tv (go t) + go (PredTy p) = PredTy (go_pred p) + + go_pred (ClassP c ts) = ClassP c (map go ts) + go_pred (IParam ip t) = IParam ip (go t) + go_pred (EqPred t1 t2) = EqPred (go t1) (go t2) + +----------------------------------------------- {-# INLINE kindView #-} kindView :: Kind -> Maybe Kind -- ^ Similar to 'coreView' or 'tcView', but works on 'Kind's @@ -381,7 +392,7 @@ repSplitAppTy_maybe :: Type -> Maybe (Type,Type) repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2) repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2) repSplitAppTy_maybe (TyConApp tc tys) - | not (isOpenSynTyCon tc) || length tys > tyConArity tc + | isDecomposableTyCon tc || length tys > tyConArity tc = case snocView tys of -- never create unsaturated type family apps Just (tys', ty') -> Just (TyConApp tc tys', ty') Nothing -> Nothing @@ -405,9 +416,9 @@ splitAppTys ty = split ty ty [] split _ (AppTy ty arg) args = split ty ty (arg:args) split _ (TyConApp tc tc_args) args = let -- keep type families saturated - n | isOpenSynTyCon tc = tyConArity tc - | otherwise = 0 - (tc_args1, tc_args2) = splitAt n tc_args + n | isDecomposableTyCon tc = 0 + | otherwise = tyConArity tc + (tc_args1, tc_args2) = splitAt n tc_args in (TyConApp tc tc_args1, tc_args2 ++ args) split _ (FunTy ty1 ty2) args = ASSERT( null args ) @@ -424,8 +435,8 @@ splitAppTys ty = split ty ty [] \begin{code} mkFunTy :: Type -> Type -> Type -- ^ Creates a function type from the given argument and result type -mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildCoVar (PredTy (EqPred ty1 ty2))) res -mkFunTy arg res = FunTy arg res +mkFunTy arg@(PredTy (EqPred {})) res = ForAllTy (mkWildCoVar arg) res +mkFunTy arg res = FunTy arg res mkFunTys :: [Type] -> Type -> Type mkFunTys tys ty = foldr mkFunTy ty tys @@ -534,22 +545,8 @@ splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res]) splitTyConApp_maybe _ = Nothing --- | Sometimes we do NOT want to look through a @newtype@. When case matching --- on a newtype we want a convenient way to access the arguments of a @newtype@ --- constructor so as to properly form a coercion, and so we use 'splitNewTyConApp' --- instead of 'splitTyConApp_maybe' -splitNewTyConApp :: Type -> (TyCon, [Type]) -splitNewTyConApp ty = case splitNewTyConApp_maybe ty of - Just stuff -> stuff - Nothing -> pprPanic "splitNewTyConApp" (ppr ty) -splitNewTyConApp_maybe :: Type -> Maybe (TyCon, [Type]) -splitNewTyConApp_maybe ty | Just ty' <- tcView ty = splitNewTyConApp_maybe ty' -splitNewTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) -splitNewTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res]) -splitNewTyConApp_maybe _ = Nothing - newTyConInstRhs :: TyCon -> [Type] -> Type --- ^ Unwrap one 'layer' of newtype on a type constructor and it's arguments, using an +-- ^ Unwrap one 'layer' of newtype on a type constructor and its arguments, using an -- eta-reduced version of the @newtype@ if possible newTyConInstRhs tycon tys = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs ) @@ -611,14 +608,9 @@ newtype at outermost level; and bale out if we see it again. -- | Looks through: -- -- 1. For-alls --- -- 2. Synonyms --- -- 3. Predicates --- --- 4. Usage annotations --- --- 5. All newtypes, including recursive ones, but not newtype families +-- 4. All newtypes, including recursive ones, but not newtype families -- -- It's useful in the back end of the compiler. repType :: Type -> Type @@ -633,19 +625,25 @@ repType ty go rec_nts (ForAllTy _ ty) -- Look through foralls = go rec_nts ty - go rec_nts ty@(TyConApp tc tys) -- Expand newtypes - | Just _co_con <- newTyConCo_maybe tc -- See Note [Expanding newtypes] - = if tc `elem` rec_nts -- in Type.lhs - then ty - else go rec_nts' nt_rhs - where - nt_rhs = newTyConInstRhs tc tys - rec_nts' | isRecursiveTyCon tc = tc:rec_nts - | otherwise = rec_nts + go rec_nts (TyConApp tc tys) -- Expand newtypes + | Just (rec_nts', ty') <- carefullySplitNewType_maybe rec_nts tc tys + = go rec_nts' ty' go _ ty = ty +carefullySplitNewType_maybe :: [TyCon] -> TyCon -> [Type] -> Maybe ([TyCon],Type) +-- Return the representation of a newtype, unless +-- we've seen it already: see Note [Expanding newtypes] +carefullySplitNewType_maybe rec_nts tc tys + | isNewTyCon tc + , not (tc `elem` rec_nts) = Just (rec_nts', newTyConInstRhs tc tys) + | otherwise = Nothing + where + rec_nts' | isRecursiveTyCon tc = tc:rec_nts + | otherwise = rec_nts + + -- ToDo: this could be moved to the code generator, using splitTyConApp instead -- of inspecting the type directly. @@ -672,7 +670,7 @@ typePrimRep ty = case repType ty of \begin{code} mkForAllTy :: TyVar -> Type -> Type mkForAllTy tyvar ty - = mkForAllTys [tyvar] ty + = ForAllTy tyvar ty -- | Wraps foralls over the type using the provided 'TyVar's from left to right mkForAllTys :: [TyVar] -> Type -> Type @@ -742,17 +740,20 @@ applyTys :: Type -> [Type] -> Type -- > foo = case undefined :: R of -- > R f -> f () -applyTys orig_fun_ty [] = orig_fun_ty -applyTys orig_fun_ty arg_tys +applyTys ty args = applyTysD empty ty args + +applyTysD :: SDoc -> Type -> [Type] -> Type -- Debug version +applyTysD _ orig_fun_ty [] = orig_fun_ty +applyTysD doc orig_fun_ty arg_tys | n_tvs == n_args -- The vastly common case = substTyWith tvs arg_tys rho_ty | n_tvs > n_args -- Too many for-alls = substTyWith (take n_args tvs) arg_tys (mkForAllTys (drop n_args tvs) rho_ty) | otherwise -- Too many type args - = ASSERT2( n_tvs > 0, ppr orig_fun_ty ) -- Zero case gives infnite loop! - applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty) - (drop n_tvs arg_tys) + = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty ) -- Zero case gives infnite loop! + applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty) + (drop n_tvs arg_tys) where (tvs, rho_ty) = splitForAllTys orig_fun_ty n_tvs = length tvs @@ -777,6 +778,10 @@ mkPredTy pred = PredTy pred mkPredTys :: ThetaType -> [Type] mkPredTys preds = map PredTy preds +isEqPred :: PredType -> Bool +isEqPred (EqPred _ _) = True +isEqPred _ = False + predTypeRep :: PredType -> Type -- ^ Convert a 'PredType' to its representation type. However, it unwraps -- only the outermost level; for example, the result might be a newtype application @@ -820,44 +825,10 @@ pprSourceTyCon tycon %************************************************************************ %* * -\subsection{Kinds and free variables} + The free variables of a type %* * %************************************************************************ ---------------------------------------------------------------------- - Finding the kind of a type - ~~~~~~~~~~~~~~~~~~~~~~~~~~ -\begin{code} -typeKind :: Type -> Kind -typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) ) - -- We should be looking for the coercion kind, - -- not the type kind - foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys -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 -\end{code} - - ---------------------------------------------------------------------- - Free variables of a type - ~~~~~~~~~~~~~~~~~~~~~~~~ \begin{code} tyVarsOfType :: Type -> TyVarSet -- ^ NB: for type synonyms tyVarsOfType does /not/ expand the synonym @@ -899,6 +870,14 @@ tyFamInsts (TyConApp tc tys) tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 tyFamInsts (ForAllTy _ ty) = tyFamInsts ty +tyFamInsts (PredTy pty) = predFamInsts pty + +-- | Finds type family instances occuring in a predicate type after expanding +-- synonyms. +predFamInsts :: PredType -> [(TyCon, [Type])] +predFamInsts (ClassP _cla tys) = concat (map tyFamInsts tys) +predFamInsts (IParam _ ty) = tyFamInsts ty +predFamInsts (EqPred ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 \end{code} @@ -1120,11 +1099,14 @@ See Note [Newtype eta] in TyCon.lhs \begin{code} -- | Type equality test for Core types (i.e. ignores predicate-types, synonyms etc.) coreEqType :: Type -> Type -> Bool -coreEqType t1 t2 - = eq rn_env t1 t2 +coreEqType t1 t2 = coreEqType2 rn_env t1 t2 where rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2)) +coreEqType2 :: RnEnv2 -> Type -> Type -> Bool +coreEqType2 rn_env t1 t2 + = eq rn_env t1 t2 + where eq env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2 eq env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2 eq env (AppTy s1 t1) (AppTy s2 t2) = eq env s1 s2 && eq env t1 t2 @@ -1159,14 +1141,16 @@ coreEqType t1 t2 \begin{code} tcEqType :: Type -> Type -> Bool --- ^ Type equality on source types. Does not look through @newtypes@ or 'PredType's +-- ^ Type equality on source types. Does not look through @newtypes@ or +-- 'PredType's, but it does look through type synonyms. tcEqType t1 t2 = isEqual $ cmpType t1 t2 tcEqTypes :: [Type] -> [Type] -> Bool tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2 tcCmpType :: Type -> Type -> Ordering --- ^ Type ordering on source types. Does not look through @newtypes@ or 'PredType's +-- ^ Type ordering on source types. Does not look through @newtypes@ or +-- 'PredType's, but it does look through type synonyms. tcCmpType t1 t2 = cmpType t1 t2 tcCmpTypes :: [Type] -> [Type] -> Ordering @@ -1411,8 +1395,14 @@ notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env) setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env -extendTvInScope :: TvSubst -> [Var] -> TvSubst -extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env +zapTvSubstEnv :: TvSubst -> TvSubst +zapTvSubstEnv (TvSubst in_scope _) = TvSubst in_scope emptyVarEnv + +extendTvInScope :: TvSubst -> Var -> TvSubst +extendTvInScope (TvSubst in_scope env) var = TvSubst (extendInScopeSet in_scope var) env + +extendTvInScopeList :: TvSubst -> [Var] -> TvSubst +extendTvInScopeList (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty) @@ -1511,6 +1501,12 @@ substTyWith :: [TyVar] -> [Type] -> Type -> Type substTyWith tvs tys = ASSERT( length tvs == length tys ) substTy (zipOpenTvSubst tvs tys) +-- | Type substitution making use of an 'TvSubst' that +-- is assumed to be open, see 'zipOpenTvSubst' +substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type] +substTysWith tvs tys = ASSERT( length tvs == length tys ) + substTys (zipOpenTvSubst tvs tys) + -- | Substitute within a 'Type' substTy :: TvSubst -> Type -> Type substTy subst ty | isEmptyTvSubst subst = ty @@ -1548,20 +1544,20 @@ subst_ty :: TvSubst -> Type -> Type subst_ty subst ty = go ty where - go (TyVarTy tv) = substTyVar subst tv - go (TyConApp tc tys) = let args = map go tys - in args `seqList` TyConApp tc args + go (TyVarTy tv) = substTyVar subst tv + go (TyConApp tc tys) = let args = map go tys + in args `seqList` TyConApp tc args - go (PredTy p) = PredTy $! (substPred subst p) + go (PredTy p) = PredTy $! (substPred subst p) - go (FunTy arg res) = (FunTy $! (go arg)) $! (go res) - go (AppTy fun arg) = mkAppTy (go fun) $! (go arg) + go (FunTy arg res) = (FunTy $! (go arg)) $! (go res) + go (AppTy fun arg) = mkAppTy (go fun) $! (go arg) -- The mkAppTy smart constructor is important -- we might be replacing (a Int), represented with App -- by [Int], represented with TyConApp - go (ForAllTy tv ty) = case substTyVarBndr subst tv of - (subst', tv') -> - ForAllTy tv' $! (subst_ty subst' ty) + go (ForAllTy tv ty) = case substTyVarBndr subst tv of + (subst', tv') -> + ForAllTy tv' $! (subst_ty subst' ty) substTyVar :: TvSubst -> TyVar -> Type substTyVar subst@(TvSubst _ _) tv @@ -1671,130 +1667,3 @@ When unifying two internal type variables, we collect their kind constraints by finding the GLB of the two. Since the partial order is a tree, they only have a glb if one is a sub-kind of the other. In that case, we bind the less-informative one to the more informative one. Neat, eh? - - -\begin{code} - -\end{code} - -%************************************************************************ -%* * - Functions over Kinds -%* * -%************************************************************************ - -\begin{code} --- | Essentially 'funResultTy' on kinds -kindFunResult :: Kind -> Kind -kindFunResult k = funResultTy k - --- | Essentially 'splitFunTys' on kinds -splitKindFunTys :: Kind -> ([Kind],Kind) -splitKindFunTys k = splitFunTys k - --- | Essentially 'splitFunTysN' on kinds -splitKindFunTysN :: Int -> Kind -> ([Kind],Kind) -splitKindFunTysN k = splitFunTysN k - --- | 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 - -isEqPred :: PredType -> Bool -isEqPred (EqPred _ _) = True -isEqPred _ = False -\end{code}