compiler/types/Kind.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 %
   4
   5 \begin{code}
   6 module Kind (
   7         -- * Main data type
   8         Kind, typeKind,
   9
  10         -- Kinds
  11         liftedTypeKind, unliftedTypeKind, openTypeKind,
  12         argTypeKind, ubxTupleKind,
  13         mkArrowKind, mkArrowKinds,
  14
  15         -- Kind constructors...
  16         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
  17         argTypeKindTyCon, ubxTupleKindTyCon,
  18         ecKind,
  19
  20         -- Super Kinds
  21         tySuperKind, tySuperKindTyCon,
  22
  23         pprKind, pprParendKind,
  24
  25         -- ** Deconstructing Kinds
  26         kindFunResult, kindAppResult, synTyConResKind,
  27         splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
  28
  29         -- ** Predicates on Kinds
  30         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
  31         isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
  32         isSuperKind, isCoercionKind,
  33         isLiftedTypeKindCon,
  34
  35         isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind,
  36         isSubKindCon,
  37
  38        ) where
  39
  40 #include "HsVersions.h"
  41
  42 import TypeRep
  43 import TysPrim
  44 import TyCon
  45 import Var
  46 import PrelNames
  47 import Outputable
  48 \end{code}
  49
  50 %************************************************************************
  51 %*                                                                      *
  52         Predicates over Kinds
  53 %*                                                                      *
  54 %************************************************************************
  55
  56 \begin{code}
  57 isTySuperKind :: SuperKind -> Bool
  58 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
  59 isTySuperKind _                = False
  60
  61 -------------------
  62 -- Lastly we need a few functions on Kinds
  63
  64 isLiftedTypeKindCon :: TyCon -> Bool
  65 isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
  66 \end{code}
  67
  68 %************************************************************************
  69 %*                                                                      *
  70         The kind of a type
  71 %*                                                                      *
  72 %************************************************************************
  73
  74 \begin{code}
  75 typeKind :: Type -> Kind
  76 typeKind _ty@(TyConApp tc tys)
  77   = ASSERT2( not (tc `hasKey` eqPredPrimTyConKey) || length tys == 2, ppr _ty )
  78              -- Assertion checks for unsaturated application of (~)
  79              -- See Note [The (~) TyCon] in TysPrim
  80     kindAppResult (tyConKind tc) tys
  81
  82 typeKind (PredTy pred)        = predKind pred
  83 typeKind (AppTy fun _)        = kindFunResult (typeKind fun)
  84 typeKind (ForAllTy _ ty)      = typeKind ty
  85 typeKind (TyVarTy tyvar)      = tyVarKind tyvar
  86 typeKind (FunTy _arg res)
  87     -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*),
  88     --              not unliftedTypKind (#)
  89     -- The only things that can be after a function arrow are
  90     --   (a) types (of kind openTypeKind or its sub-kinds)
  91     --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
  92     | isTySuperKind k         = k
  93     | otherwise               = ASSERT( isSubOpenTypeKind k) liftedTypeKind
  94     where
  95       k = typeKind res
  96
  97 ------------------
  98 predKind :: PredType -> Kind
  99 predKind (EqPred {}) = unliftedTypeKind -- Coercions are unlifted
 100 predKind (ClassP {}) = liftedTypeKind   -- Class and implicitPredicates are
 101 predKind (IParam {}) = liftedTypeKind   -- always represented by lifted types
 102 \end{code}
 103
 104 %************************************************************************
 105 %*                                                                      *
 106         Functions over Kinds
 107 %*                                                                      *
 108 %************************************************************************
 109
 110 \begin{code}
 111 -- | Essentially 'funResultTy' on kinds
 112 kindFunResult :: Kind -> Kind
 113 kindFunResult (FunTy _ res) = res
 114 kindFunResult k = pprPanic "kindFunResult" (ppr k)
 115
 116 kindAppResult :: Kind -> [arg] -> Kind
 117 kindAppResult k []     = k
 118 kindAppResult k (_:as) = kindAppResult (kindFunResult k) as
 119
 120 -- | Essentially 'splitFunTys' on kinds
 121 splitKindFunTys :: Kind -> ([Kind],Kind)
 122 splitKindFunTys (FunTy a r) = case splitKindFunTys r of
 123                               (as, k) -> (a:as, k)
 124 splitKindFunTys k = ([], k)
 125
 126 splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
 127 splitKindFunTy_maybe (FunTy a r) = Just (a,r)
 128 splitKindFunTy_maybe _           = Nothing
 129
 130 -- | Essentially 'splitFunTysN' on kinds
 131 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
 132 splitKindFunTysN 0 k           = ([], k)
 133 splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of
 134                                    (as, k) -> (a:as, k)
 135 splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k)
 136
 137 -- | Find the result 'Kind' of a type synonym,
 138 -- after applying it to its 'arity' number of type variables
 139 -- Actually this function works fine on data types too,
 140 -- but they'd always return '*', so we never need to ask
 141 synTyConResKind :: TyCon -> Kind
 142 synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)
 143
 144 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
 145 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
 146 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
 147         isUnliftedTypeKindCon, isSubArgTypeKindCon      :: TyCon -> Bool
 148
 149 isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
 150
 151 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
 152 isOpenTypeKind _               = False
 153
 154 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
 155
 156 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
 157 isUbxTupleKind _               = False
 158
 159 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
 160
 161 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
 162 isArgTypeKind _               = False
 163
 164 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
 165
 166 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
 167 isUnliftedTypeKind _               = False
 168
 169 isSubOpenTypeKind :: Kind -> Bool
 170 -- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
 171 isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
 172                                      ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
 173                                      False
 174 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
 175 isSubOpenTypeKind other            = ASSERT( isKind other ) False
 176          -- This is a conservative answer
 177          -- It matters in the call to isSubKind in
 178          -- checkExpectedKind.
 179
 180 isSubArgTypeKindCon kc
 181   | isUnliftedTypeKindCon kc = True
 182   | isLiftedTypeKindCon kc   = True
 183   | isArgTypeKindCon kc      = True
 184   | otherwise                = False
 185
 186 isSubArgTypeKind :: Kind -> Bool
 187 -- ^ True of any sub-kind of ArgTypeKind
 188 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
 189 isSubArgTypeKind _                = False
 190
 191 -- | Is this a super-kind (i.e. a type-of-kinds)?
 192 isSuperKind :: Type -> Bool
 193 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
 194 isSuperKind _                   = False
 195
 196 -- | Is this a kind (i.e. a type-of-types)?
 197 isKind :: Kind -> Bool
 198 isKind k = isSuperKind (typeKind k)
 199
 200 isSubKind :: Kind -> Kind -> Bool
 201 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
 202 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
 203 isSubKind (FunTy a1 r1) (FunTy a2 r2)         = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
 204 isSubKind _             _                     = False
 205
 206 isSubKindCon :: TyCon -> TyCon -> Bool
 207 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
 208 isSubKindCon kc1 kc2
 209   | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
 210   | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
 211   | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
 212   | isOpenTypeKindCon kc2                                  = True
 213                            -- we already know kc1 is not a fun, its a TyCon
 214   | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
 215   | otherwise                                              = False
 216
 217 defaultKind :: Kind -> Kind
 218 -- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
 219 -- information on what that means
 220
 221 -- When we generalise, we make generic type variables whose kind is
 222 -- simple (* or *->* etc).  So generic type variables (other than
 223 -- built-in constants like 'error') always have simple kinds.  This is important;
 224 -- consider
 225 --      f x = True
 226 -- We want f to get type
 227 --      f :: forall (a::*). a -> Bool
 228 -- Not
 229 --      f :: forall (a::??). a -> Bool
 230 -- because that would allow a call like (f 3#) as well as (f True),
 231 --and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
 232 defaultKind k
 233   | isSubOpenTypeKind k = liftedTypeKind
 234   | isSubArgTypeKind k  = liftedTypeKind
 235   | otherwise        = k
 236
 237 ecKind           = liftedTypeKind `mkArrowKind` (liftedTypeKind `mkArrowKind` liftedTypeKind)
 238 \end{code}