diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2012-02-17 13:59:17 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2012-02-17 13:59:17 +0000 |
commit | 94496fcedfddc4d399e274424546a03d1c8f274b (patch) | |
tree | 35c47c458bdac04dc90f5353328176c8e5d575e9 | |
parent | 9789b032e9ce7a5030d534847ec94e5398b38def (diff) | |
download | haskell-94496fcedfddc4d399e274424546a03d1c8f274b.tar.gz |
More simplification of the sub-kinding story
-rw-r--r-- | compiler/coreSyn/CoreLint.lhs | 53 | ||||
-rw-r--r-- | compiler/typecheck/TcErrors.lhs | 2 | ||||
-rw-r--r-- | compiler/typecheck/TcHsType.lhs | 4 | ||||
-rw-r--r-- | compiler/typecheck/TcMType.lhs | 38 | ||||
-rw-r--r-- | compiler/typecheck/TcSimplify.lhs | 2 | ||||
-rw-r--r-- | compiler/typecheck/TcTyClsDecls.lhs | 2 | ||||
-rw-r--r-- | compiler/typecheck/TcType.lhs | 3 | ||||
-rw-r--r-- | compiler/types/Kind.lhs | 218 | ||||
-rw-r--r-- | compiler/types/Type.lhs | 27 |
9 files changed, 149 insertions, 200 deletions
diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs index cd4e2523ac..47e25839fa 100644 --- a/compiler/coreSyn/CoreLint.lhs +++ b/compiler/coreSyn/CoreLint.lhs @@ -689,8 +689,8 @@ lintArrow what k1 k2 -- Eg lintArrow "type or kind `blah'" k1 k2 | isSuperKind k1 = return superKind | otherwise - = do { unless (k1 `isSubKind` argTypeKind) (addErrL (msg (ptext (sLit "argument")) k1)) - ; unless (k2 `isSubKind` openTypeKind) (addErrL (msg (ptext (sLit "result")) k2)) + = do { unless (okArrowArgKind k1) (addErrL (msg (ptext (sLit "argument")) k1)) + ; unless (okArrowResultKind k2) (addErrL (msg (ptext (sLit "result")) k2)) ; return liftedTypeKind } where msg ar k @@ -791,7 +791,11 @@ lintCoercion (CoVarCo cv) = do { checkTyCoVarInScope cv ; cv' <- lookupIdInScope cv ; let (s,t) = coVarKind cv' - ; return (typeKind s, s, t) } + k = typeKind s + ; when (isSuperKind k) $ + checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality")) + 2 (ppr cv)) + ; return (k, s, t) } lintCoercion (UnsafeCo ty1 ty2) = do { k1 <- lintType ty1 @@ -846,33 +850,27 @@ lintCoercion co@(AxiomInstCo (CoAxiom { co_ax_tvs = ktvs , co_ax_rhs = rhs }) cos) = do { -- See Note [Kind instantiation in coercions] - let (kvs, tvs) = splitKiTyVars ktvs - (kcos, tcos) = splitAt (length kvs) cos - ; unless (not (any isKiVar tvs) - && kvs `equalLength` kcos - && tvs `equalLength` tcos) (bad_ax (ptext (sLit "lengths"))) - - ; kis <- mapM check_ki kcos - ; let tvs' = map (updateTyVarKind (Type.substTy subst)) tvs - subst = zipOpenTvSubst kvs kis - ; (tks, tys1, tys2) <- mapAndUnzip3M lintCoercion tcos - - ; zipWithM_ check_ki2 tvs' tks - ; let lhs' = substTyWith ktvs (kis ++ tys1) lhs - rhs' = substTyWith ktvs (kis ++ tys2) rhs - + unless (equalLength ktvs cos) (bad_ax (ptext (sLit "lengths"))) + ; in_scope <- getInScope + ; let empty_subst = mkTvSubst in_scope emptyTvSubstEnv + ; (subst_l, subst_r) <- foldlM check_ki + (empty_subst, empty_subst) + (ktvs `zip` cos) + ; let lhs' = Type.substTy subst_l lhs + rhs' = Type.substTy subst_r rhs ; return (typeKind lhs', lhs', rhs') } where bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what) 2 (ppr co)) - check_ki co - = do { (k, k1, k2) <- lintCoercion co - ; unless (isSuperKind k) (bad_ax (ptext (sLit "check_ki1a"))) - ; unless (k1 `eqKind` k2) (bad_ax (ptext (sLit "check_ki1b"))) - ; return k1 } -- Kind coercions must be refl - - check_ki2 tv k = unless (k `isSubKind` tyVarKind tv) - (bad_ax (ptext (sLit "check_ki2"))) + + check_ki (subst_l, subst_r) (ktv, co) + = do { (k, t1, t2) <- lintCoercion co + ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv) + -- Using subst_l is ok, because subst_l and subst_r + -- must agree on kind equalities + ; unless (k `isSubKind` ktv_kind) (bad_ax (ptext (sLit "check_ki2"))) + ; return (Type.extendTvSubst subst_l ktv t1, + Type.extendTvSubst subst_r ktv t2) } \end{code} %************************************************************************ @@ -993,6 +991,9 @@ updateTvSubst subst' m = getTvSubst :: LintM TvSubst getTvSubst = LintM (\ _ subst errs -> (Just subst, errs)) +getInScope :: LintM InScopeSet +getInScope = LintM (\ _ subst errs -> (Just (getTvInScope subst), errs)) + applySubstTy :: InType -> LintM OutType applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) } diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs index 0fb9d43a6e..cb388ff057 100644 --- a/compiler/typecheck/TcErrors.lhs +++ b/compiler/typecheck/TcErrors.lhs @@ -481,7 +481,7 @@ mkTyVarEqErr ctxt ct oriented tv1 ty2 -- So tv is a meta tyvar, and presumably it is -- an *untouchable* meta tyvar, else it'd have been unified - | not (k2 `isSubKind` k1) -- Kind error + | not (k2 `tcIsSubKind` k1) -- Kind error = mkErrorReport ctxt $ (kindErrorMsg (mkTyVarTy tv1) ty2) -- Occurs check diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index fe13f76140..f26bfbbf9a 100644 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -887,7 +887,6 @@ tcTyVarBndrs bndrs thing_inside = do where zonk (name, kind) = do { kind' <- zonkTcKind kind - ; checkTc (noHashInKind kind') (ptext (sLit "Kind signature contains # or (#)")) ; return (mkTyVar name kind') } tcTyVarBndrsKindGen :: [LHsTyVarBndr Name] -> ([TyVar] -> TcM r) -> TcM r @@ -964,8 +963,9 @@ kindGeneralizeKinds kinds `minusVarSet` gbl_tvs) (_, tidy_kvs_to_quantify) = tidyTyVarBndrs tidy_env kvs_to_quantify + -- We do not get a later chance to tidy! - ; kvs <- ASSERT2 (all isKiVar kvs_to_quantify, ppr kvs_to_quantify) + ; kvs <- ASSERT2 (all isKindVar kvs_to_quantify, ppr kvs_to_quantify) zonkQuantifiedTyVars tidy_kvs_to_quantify -- Zonk the kinds again, to pick up either the kind diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index cee7bc9ef4..518a40363c 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -70,8 +70,6 @@ module TcMType ( zonkTcTypeAndSubst, tcGetGlobalTyVars, - - compatKindTcM, isSubKindTcM ) where #include "HsVersions.h" @@ -389,7 +387,7 @@ writeMetaTyVarRef tyvar ref ty ; writeMutVar ref (Indirect ty) ; when ( not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables - && not (zonked_ty_kind `isSubKind` zonked_tv_kind)) + && not (zonked_ty_kind `tcIsSubKind` zonked_tv_kind)) $ WARN( True, hang (text "Ill-kinded update to meta tyvar") 2 ( ppr tyvar <+> text "::" <+> ppr tv_kind <+> text ":=" @@ -419,22 +417,26 @@ newFlexiTyVarTy kind = do newFlexiTyVarTys :: Int -> Kind -> TcM [TcType] newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind) -tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst) +tcInstTyVars :: [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst) -- Instantiate with META type variables +-- Note that this works for a sequence of kind and type +-- variables. Eg [ (k:BOX), (a:k->k) ] +-- Gives [ (k7:BOX), (a8:k7->k7) ] tcInstTyVars tyvars = tcInstTyVarsX emptyTvSubst tyvars -- emptyTvSubst has an empty in-scope set, but that's fine here -- Since the tyvars are freshly made, they cannot possibly be -- captured by any existing for-alls. -tcInstTyVarsX :: TvSubst -> [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst) +tcInstTyVarsX :: TvSubst -> [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst) +-- The "X" part is because of extending the substitution tcInstTyVarsX subst tyvars = - do { (subst', tyvars') <- mapAccumLM tcInstTyVar subst tyvars + do { (subst', tyvars') <- mapAccumLM tcInstTyVarX subst tyvars ; return (tyvars', mkTyVarTys tyvars', subst') } -tcInstTyVar :: TvSubst -> TyVar -> TcM (TvSubst, TcTyVar) +tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar) -- Make a new unification variable tyvar whose Name and Kind come from -- an existing TyVar. We substitute kind variables in the kind. -tcInstTyVar subst tyvar +tcInstTyVarX subst tyvar = do { uniq <- newMetaUnique ; ref <- newMutVar Flexi ; let name = mkSystemName uniq (getOccName tyvar) @@ -563,15 +565,14 @@ zonkTcPredType = zonkTcType defaultKindVarToStar :: TcTyVar -> TcM Kind -- We have a meta-kind: unify it with '*' defaultKindVarToStar kv - = do { ASSERT ( isKiVar kv && isMetaTyVar kv ) + = do { ASSERT ( isKindVar kv && isMetaTyVar kv ) writeMetaTyVar kv liftedTypeKind ; return liftedTypeKind } zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar] --- Precondition: a kind variable occurs before a type --- variable mentioning it in its kind +-- A kind variable k may occur *after* a tyvar mentioning k in its kind zonkQuantifiedTyVars tyvars - = do { let (kvs, tvs) = partitionKiTyVars tyvars + = do { let (kvs, tvs) = partition isKindVar tyvars ; poly_kinds <- xoptM Opt_PolyKinds ; if poly_kinds then mapM zonkQuantifiedTyVar (kvs ++ tvs) @@ -820,19 +821,6 @@ zonkType zonk_tc_tyvar ty %************************************************************************ \begin{code} -compatKindTcM :: Kind -> Kind -> TcM Bool -compatKindTcM k1 k2 - = do { k1' <- zonkTcKind k1 - ; k2' <- zonkTcKind k2 - ; return $ k1' `isSubKind` k2' || k2' `isSubKind` k1' } - -isSubKindTcM :: Kind -> Kind -> TcM Bool -isSubKindTcM k1 k2 - = do { k1' <- zonkTcKind k1 - ; k2' <- zonkTcKind k2 - ; return $ k1' `isSubKind` k2' } - -------------- zonkTcKind :: TcKind -> TcM TcKind zonkTcKind k = zonkTcType k \end{code} diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 6bd8dd90d8..ae948b5f95 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -1130,7 +1130,7 @@ getSolvableCTyFunEqs untch cts , isTouchableMetaTyVar_InRange untch tv -- And it's a *touchable* unification variable - , typeKind xi `isSubKind` tyVarKind tv + , typeKind xi `tcIsSubKind` tyVarKind tv -- Must do a small kind check since TcCanonical invariants -- on family equations only impose compatibility, not subkinding diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index 322506ff3f..8fa79e9148 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -1367,7 +1367,7 @@ checkValidClass cls ; mapM_ check_at_defs at_stuff } where (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls - unary = isSingleton (snd (splitKiTyVars tyvars)) -- IA0_NOTE: only count type arguments + unary = count isTypeVar tyvars == 1 -- Ignore kind variables check_op constrained_class_methods (sel_id, dm) = addErrCtxt (classOpCtxt sel_id tau) $ do diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index e0d5f63722..c94752111c 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -37,6 +37,7 @@ module TcType ( isSigTyVar, isOverlappableTyVar, isTyConableTyVar, isAmbiguousTyVar, metaTvRef, isFlexi, isIndirect, isRuntimeUnkSkol, + isTypeVar, isKindVar, -------------------------------- -- Builders @@ -118,7 +119,7 @@ module TcType ( unliftedTypeKind, liftedTypeKind, argTypeKind, openTypeKind, constraintKind, mkArrowKind, mkArrowKinds, isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind, - isSubArgTypeKind, isSubKind, splitKindFunTys, defaultKind, + isSubArgTypeKind, tcIsSubKind, splitKindFunTys, defaultKind, mkMetaKindVar, -------------------------------- diff --git a/compiler/types/Kind.lhs b/compiler/types/Kind.lhs index 3fda25c592..b3684151b1 100644 --- a/compiler/types/Kind.lhs +++ b/compiler/types/Kind.lhs @@ -36,18 +36,18 @@ module Kind ( -- ** Predicates on Kinds isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, isUbxTupleKind, isArgTypeKind, isConstraintKind, - isConstraintOrLiftedKind, isKind, - isSuperKind, isSuperKindTyCon, noHashInKind, + isConstraintOrLiftedKind, isKind, isKindVar, + isSuperKind, isSuperKindTyCon, isLiftedTypeKindCon, isConstraintKindCon, isAnyKind, isAnyKindCon, + okArrowArgKind, okArrowResultKind, - isSubArgTypeKind, tcIsSubArgTypeKind, - isSubOpenTypeKind, tcIsSubOpenTypeKind, - isSubKind, tcIsSubKind, defaultKind, - isSubKindCon, tcIsSubKindCon, isSubOpenTypeKindCon, + isSubArgTypeKind, isSubOpenTypeKind, + isSubKind, isSubKindCon, + tcIsSubKind, tcIsSubKindCon, + defaultKind, -- ** Functions on variables - isKiVar, splitKiTyVars, partitionKiTyVars, kiVarsOfKind, kiVarsOfKinds ) where @@ -59,38 +59,9 @@ import {-# SOURCE #-} Type ( typeKind, substKiWith, eqKind ) import TypeRep import TysPrim import TyCon -import Var import VarSet import PrelNames import Outputable - -import Data.List ( partition ) -\end{code} - -%************************************************************************ -%* * - Predicates over Kinds -%* * -%************************************************************************ - -\begin{code} -------------------- --- Lastly we need a few functions on Kinds - -isLiftedTypeKindCon :: TyCon -> Bool -isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey - --- This checks that its argument does not contain # or (#). --- It is used in tcTyVarBndrs. -noHashInKind :: Kind -> Bool -noHashInKind (TyVarTy {}) = True -noHashInKind (FunTy k1 k2) = noHashInKind k1 && noHashInKind k2 -noHashInKind (ForAllTy _ ki) = noHashInKind ki -noHashInKind (TyConApp kc kis) - = not (kc `hasKey` unliftedTypeKindTyConKey) - && not (kc `hasKey` ubxTupleKindTyConKey) - && all noHashInKind kis -noHashInKind _ = panic "noHashInKind" \end{code} %************************************************************************ @@ -139,37 +110,34 @@ isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind, isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon, - isUnliftedTypeKindCon, isSubArgTypeKindCon, tcIsSubArgTypeKindCon, - isSubOpenTypeKindCon, tcIsSubOpenTypeKindCon, isConstraintKindCon, - isAnyKindCon :: TyCon -> Bool + isUnliftedTypeKindCon, isSubArgTypeKindCon, + isSubOpenTypeKindCon, isConstraintKindCon, + isLiftedTypeKindCon, isAnyKindCon :: TyCon -> Bool -isAnyKindCon tc = tyConUnique tc == anyKindTyConKey + +isLiftedTypeKindCon tc = tyConUnique tc == liftedTypeKindTyConKey +isAnyKindCon tc = tyConUnique tc == anyKindTyConKey +isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey +isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey +isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey +isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey +isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey isAnyKind (TyConApp tc _) = isAnyKindCon tc isAnyKind _ = False -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 -isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey - isConstraintKind (TyConApp tc _) = isConstraintKindCon tc isConstraintKind _ = False @@ -177,106 +145,120 @@ isConstraintOrLiftedKind (TyConApp tc _) = isConstraintKindCon tc || isLiftedTypeKindCon tc isConstraintOrLiftedKind _ = False --- Subkinding +-------------------------------------------- +-- Kinding for arrow (->) +-- Says when a kind is acceptable on lhs or rhs of an arrow +-- arg -> res + +okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool +okArrowArgKindCon kc + | isLiftedTypeKindCon kc = True + | isUnliftedTypeKindCon kc = True + | isConstraintKindCon kc = True + | otherwise = False + +okArrowResultKindCon kc + | okArrowArgKindCon kc = True + | isUbxTupleKindCon kc = True + | otherwise = False + +okArrowArgKind, okArrowResultKind :: Kind -> Bool +okArrowArgKind (TyConApp kc []) = okArrowArgKindCon kc +okArrowArgKind _ = False + +okArrowResultKind (TyConApp kc []) = okArrowResultKindCon kc +okArrowResultKind _ = False + +----------------------------------------- +-- Subkinding -- The tc variants are used during type-checking, where we don't want the -- Constraint kind to be a subkind of anything -- After type-checking (in core), Constraint is a subkind of argTypeKind -isSubOpenTypeKind, tcIsSubOpenTypeKind :: Kind -> Bool +isSubOpenTypeKind :: Kind -> Bool -- ^ True of any sub-kind of OpenTypeKind isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc isSubOpenTypeKind _ = False --- ^ True of any sub-kind of OpenTypeKind -tcIsSubOpenTypeKind (TyConApp kc []) = tcIsSubOpenTypeKindCon kc -tcIsSubOpenTypeKind _ = False - isSubOpenTypeKindCon kc - | isSubArgTypeKindCon kc = True - | isUbxTupleKindCon kc = True - | isOpenTypeKindCon kc = True - | otherwise = False - -tcIsSubOpenTypeKindCon kc - | tcIsSubArgTypeKindCon kc = True - | isUbxTupleKindCon kc = True - | isOpenTypeKindCon kc = True - | otherwise = False + = isSubArgTypeKindCon kc + || isUbxTupleKindCon kc + || isOpenTypeKindCon kc + || isConstraintKindCon kc -- Needed for error (Num a) "blah" + -- and so that (Ord a -> Eq a) is well-kinded isSubArgTypeKindCon kc - | isUnliftedTypeKindCon kc = True - | isLiftedTypeKindCon kc = True - | isArgTypeKindCon kc = True - | isConstraintKindCon kc = True - | otherwise = False + = isUnliftedTypeKindCon kc + || isLiftedTypeKindCon kc + || isArgTypeKindCon kc -tcIsSubArgTypeKindCon kc - | isConstraintKindCon kc = False - | otherwise = isSubArgTypeKindCon kc - -isSubArgTypeKind, tcIsSubArgTypeKind :: Kind -> Bool +isSubArgTypeKind :: Kind -> Bool -- ^ True of any sub-kind of ArgTypeKind isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc isSubArgTypeKind _ = False -tcIsSubArgTypeKind (TyConApp kc []) = tcIsSubArgTypeKindCon kc -tcIsSubArgTypeKind _ = False - --- | Is this a super-kind (i.e. a type-of-kinds)? -isSuperKind :: Type -> Bool -isSuperKind (TyConApp skc []) = isSuperKindTyCon skc -isSuperKind _ = False - -isSuperKindTyCon :: TyCon -> Bool -isSuperKindTyCon tc = tc `hasKey` superKindTyConKey - -- | Is this a kind (i.e. a type-of-types)? isKind :: Kind -> Bool isKind k = isSuperKind (typeKind k) -isSubKind, tcIsSubKind :: Kind -> Kind -> Bool -isSubKind = isSubKind' False -tcIsSubKind = isSubKind' True - --- The first argument denotes whether we are in the type-checking phase or not -isSubKind' :: Bool -> Kind -> Kind -> Bool +isSubKind :: Kind -> Kind -> Bool -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@ -isSubKind' duringTc (FunTy a1 r1) (FunTy a2 r2) - = (isSubKind' duringTc a2 a1) && (isSubKind' duringTc r1 r2) +isSuperKindTyCon :: TyCon -> Bool +isSuperKindTyCon tc = tc `hasKey` superKindTyConKey + +isSubKind (FunTy a1 r1) (FunTy a2 r2) + = (isSubKind a2 a1) && (isSubKind r1 r2) -isSubKind' duringTc k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s) +isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s) | isPromotedTypeTyCon kc1 || isPromotedTypeTyCon kc2 -- handles promoted kinds (List *, Nat, etc.) - = eqKind k1 k2 + = eqKind k1 k2 | isSuperKindTyCon kc1 || isSuperKindTyCon kc2 -- handles BOX - = WARN( not (isSuperKindTyCon kc2 && isSuperKindTyCon kc2 - && null k1s && null k2s), + = ASSERT2( isSuperKindTyCon kc2 && isSuperKindTyCon kc2 + && null k1s && null k2s, ppr kc1 <+> ppr kc2 ) - kc1 == kc2 + True -- If one is BOX, the other must be too | otherwise = -- handles usual kinds (*, #, (#), etc.) ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 ) - if duringTc then kc1 `tcIsSubKindCon` kc2 - else kc1 `isSubKindCon` kc2 + kc1 `isSubKindCon` kc2 -isSubKind' _duringTc k1 k2 = eqKind k1 k2 +isSubKind k1 k2 = eqKind k1 k2 isSubKindCon :: TyCon -> TyCon -> Bool -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@ isSubKindCon kc1 kc2 - | kc1 == kc2 = True - | isSubArgTypeKindCon kc1 && isArgTypeKindCon kc2 = True - | isSubOpenTypeKindCon kc1 && isOpenTypeKindCon kc2 = True - | otherwise = False + | kc1 == kc2 = True + | isArgTypeKindCon kc2 = isSubArgTypeKindCon kc1 + | isOpenTypeKindCon kc2 = isSubOpenTypeKindCon kc1 + | otherwise = False + +------------------------- +-- Hack alert: we need a tiny variant for the typechecker +-- Reason: f :: Int -> (a~b) +-- g :: forall (c::Constraint). Int -> c +-- We want to reject these, even though Constraint is +-- a sub-kind of OpenTypeKind. It must be a sub-kind of OpenTypeKind +-- *after* the typechecker +-- a) So that (Ord a -> Eq a) is a legal type +-- b) So that the simplifer can generate (error (Eq a) "urk") +-- +-- Easiest way to reject is simply to make Constraint not +-- below OpenTypeKind when type checking + +tcIsSubKind :: Kind -> Kind -> Bool +tcIsSubKind k1 k2 + | isConstraintKind k1 = isConstraintKind k2 + | otherwise = isSubKind k1 k2 tcIsSubKindCon :: TyCon -> TyCon -> Bool tcIsSubKindCon kc1 kc2 - | kc1 == kc2 = True - | isConstraintKindCon kc1 || isConstraintKindCon kc2 = False - | otherwise = isSubKindCon kc1 kc2 + | isConstraintKindCon kc1 = isConstraintKindCon kc2 + | otherwise = isSubKindCon kc1 kc2 +------------------------- defaultKind :: Kind -> Kind -- ^ Used when generalising: default OpenKind and ArgKind to *. -- See "Type#kind_subtyping" for more information on what that means @@ -294,20 +276,8 @@ defaultKind :: Kind -> Kind -- and the calling conventions differ. -- This defaulting is done in TcMType.zonkTcTyVarBndr. defaultKind k - | tcIsSubOpenTypeKind k = liftedTypeKind - | otherwise = k - -splitKiTyVars :: [TyVar] -> ([KindVar], [TyVar]) --- Precondition: kind variables should precede type variables --- Postcondition: appending the two result lists gives the input! -splitKiTyVars = span (isSuperKind . tyVarKind) - -partitionKiTyVars :: [TyVar] -> ([KindVar], [TyVar]) -partitionKiTyVars = partition (isSuperKind . tyVarKind) - --- Checks if this "type or kind" variable is a kind variable -isKiVar :: TyVar -> Bool -isKiVar v = isSuperKind (varType v) + | isSubOpenTypeKind k = liftedTypeKind + | otherwise = k -- Returns the free kind variables in a kind kiVarsOfKind :: Kind -> VarSet diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index dbb2c5e0bb..114e3e9cfc 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -63,6 +63,7 @@ module Type ( funTyCon, -- ** Predicates on types + isTypeVar, isKindVar, isTyVarTy, isFunTy, isDictTy, isPredTy, isKindTy, -- (Lifting and boxity) @@ -89,7 +90,7 @@ module Type ( -- * Type free variables tyVarsOfType, tyVarsOfTypes, expandTypeSynonyms, - typeSize, varSetElemsKvsFirst, sortQuantVars, + typeSize, varSetElemsKvsFirst, -- * Type comparison eqType, eqTypeX, eqTypes, cmpType, cmpTypes, @@ -165,6 +166,7 @@ import Util import Outputable import FastString +import Data.List ( partition ) import Maybes ( orElse ) import Data.Maybe ( isJust ) @@ -689,8 +691,8 @@ mkPiKinds :: [TyVar] -> Kind -> Kind -- returns forall k1 k2. (k1 -> *) -> k2 mkPiKinds [] res = res mkPiKinds (tv:tvs) res - | isKiVar tv = ForAllTy tv (mkPiKinds tvs res) - | otherwise = FunTy (tyVarKind tv) (mkPiKinds tvs res) + | isKindVar tv = ForAllTy tv (mkPiKinds tvs res) + | otherwise = FunTy (tyVarKind tv) (mkPiKinds tvs res) mkPiType :: Var -> Type -> Type -- ^ Makes a @(->)@ type or a forall type, depending @@ -975,23 +977,10 @@ typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts) varSetElemsKvsFirst :: VarSet -> [TyVar] -- {k1,a,k2,b} --> [k1,k2,a,b] -varSetElemsKvsFirst set = uncurry (++) $ partitionKiTyVars (varSetElems set) - -sortQuantVars :: [Var] -> [Var] --- Sort the variables so the true kind then type variables come first -sortQuantVars = sortLe le +varSetElemsKvsFirst set + = kvs ++ tvs where - v1 `le` v2 = case (is_tv v1, is_tv v2) of - (True, False) -> True - (False, True) -> False - (True, True) -> - case (is_kv v1, is_kv v2) of - (True, False) -> True - (False, True) -> False - _ -> v1 <= v2 -- Same family - (False, False) -> v1 <= v2 - is_tv v = isTyVar v - is_kv v = isSuperKind (tyVarKind v) + (kvs, tvs) = partition isKindVar (varSetElems set) \end{code} |