Commit 94496fce authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

More simplification of the sub-kinding story

parent 9789b032
......@@ -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) }
......
......@@ -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
......
......@@ -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
......
......@@ -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}
......
......@@ -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
......
......@@ -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
......
......@@ -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,
--------------------------------
......
......@@ -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
......
......@@ -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}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment