ghc/compiler/types/Kind.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
   3 %
   4
   5 \begin{code}
   6 module Kind (
   7         Kind(..), KindVar(..), SimpleKind,
   8         openTypeKind, liftedTypeKind, unliftedTypeKind,
   9         argTypeKind, ubxTupleKind,
  10
  11         isLiftedTypeKind, isUnliftedTypeKind,
  12         isArgTypeKind, isOpenTypeKind,
  13         mkArrowKind, mkArrowKinds,
  14
  15         isSubKind, defaultKind,
  16         kindFunResult, splitKindFunTys, mkKindVar,
  17
  18         pprKind, pprParendKind
  19      ) where
  20
  21 #include "HsVersions.h"
  22
  23 import Unique   ( Unique )
  24 import Outputable
  25 import DATA_IOREF
  26 \end{code}
  27
  28 Kinds
  29 ~~~~~
  30 There's a little subtyping at the kind level:
  31
  32                  ?
  33                 / \
  34                /   \
  35               ??   (#)
  36              /  \
  37             *   #
  38
  39 where   *    [LiftedTypeKind]   means boxed type
  40         #    [UnliftedTypeKind] means unboxed type
  41         (#)  [UbxTupleKind]     means unboxed tuple
  42         ??   [ArgTypeKind]      is the lub of *,#
  43         ?    [OpenTypeKind]     means any type at all
  44
  45 In particular:
  46
  47         error :: forall a:?. String -> a
  48         (->)  :: ?? -> ? -> *
  49         (\(x::t) -> ...)        Here t::?? (i.e. not unboxed tuple)
  50
  51 \begin{code}
  52 data Kind
  53   = LiftedTypeKind      -- *
  54   | OpenTypeKind        -- ?
  55   | UnliftedTypeKind    -- #
  56   | UbxTupleKind        -- (##)
  57   | ArgTypeKind         -- ??
  58   | FunKind Kind Kind   -- k1 -> k2
  59   | KindVar KindVar
  60   deriving( Eq )
  61
  62 data KindVar = KVar Unique (IORef (Maybe SimpleKind))
  63   -- INVARIANT: a KindVar can only be instantiated by a SimpleKind
  64
  65 type SimpleKind = Kind
  66   -- A SimpleKind has no ? or # kinds in it:
  67   -- sk ::= * | sk1 -> sk2 | kvar
  68
  69 instance Eq KindVar where
  70   (KVar u1 _) == (KVar u2 _) = u1 == u2
  71
  72 mkKindVar :: Unique -> IORef (Maybe Kind) -> KindVar
  73 mkKindVar = KVar
  74 \end{code}
  75
  76 Kind inference
  77 ~~~~~~~~~~~~~~
  78 During kind inference, a kind variable unifies only with
  79 a "simple kind", sk
  80         sk ::= * | sk1 -> sk2
  81 For example
  82         data T a = MkT a (T Int#)
  83 fails.  We give T the kind (k -> *), and the kind variable k won't unify
  84 with # (the kind of Int#).
  85
  86 Type inference
  87 ~~~~~~~~~~~~~~
  88 When creating a fresh internal type variable, we give it a kind to express
  89 constraints on it.  E.g. in (\x->e) we make up a fresh type variable for x,
  90 with kind ??.
  91
  92 During unification we only bind an internal type variable to a type
  93 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
  94
  95 When unifying two internal type variables, we collect their kind constraints by
  96 finding the GLB of the two.  Since the partial order is a tree, they only
  97 have a glb if one is a sub-kind of the other.  In that case, we bind the
  98 less-informative one to the more informative one.  Neat, eh?
  99
 100
 101 \begin{code}
 102 liftedTypeKind   = LiftedTypeKind
 103 unliftedTypeKind = UnliftedTypeKind
 104 openTypeKind     = OpenTypeKind
 105 argTypeKind      = ArgTypeKind
 106 ubxTupleKind     = UbxTupleKind
 107
 108 mkArrowKind :: Kind -> Kind -> Kind
 109 mkArrowKind k1 k2 = k1 `FunKind` k2
 110
 111 mkArrowKinds :: [Kind] -> Kind -> Kind
 112 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 113 \end{code}
 114
 115 %************************************************************************
 116 %*                                                                      *
 117         Functions over Kinds
 118 %*                                                                      *
 119 %************************************************************************
 120
 121 \begin{code}
 122 kindFunResult :: Kind -> Kind
 123 kindFunResult (FunKind _ k) = k
 124 kindFunResult k = pprPanic "kindFunResult" (ppr k)
 125
 126 splitKindFunTys :: Kind -> ([Kind],Kind)
 127 splitKindFunTys (FunKind k1 k2) = case splitKindFunTys k2 of
 128                                     (as, r) -> (k1:as, r)
 129 splitKindFunTys k = ([], k)
 130
 131 isLiftedTypeKind, isUnliftedTypeKind :: Kind -> Bool
 132 isLiftedTypeKind LiftedTypeKind = True
 133 isLiftedTypeKind other          = False
 134
 135 isUnliftedTypeKind UnliftedTypeKind = True
 136 isUnliftedTypeKind other            = False
 137
 138 isArgTypeKind :: Kind -> Bool
 139 -- True of any sub-kind of ArgTypeKind
 140 isArgTypeKind LiftedTypeKind   = True
 141 isArgTypeKind UnliftedTypeKind = True
 142 isArgTypeKind ArgTypeKind      = True
 143 isArgTypeKind other            = False
 144
 145 isOpenTypeKind :: Kind -> Bool
 146 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
 147 isOpenTypeKind (FunKind _ _) = False
 148 isOpenTypeKind other         = True
 149
 150 isSubKind :: Kind -> Kind -> Bool
 151 -- (k1 `isSubKind` k2) checks that k1 <: k2
 152 isSubKind LiftedTypeKind   LiftedTypeKind   = True
 153 isSubKind UnliftedTypeKind UnliftedTypeKind = True
 154 isSubKind UbxTupleKind     UbxTupleKind     = True
 155 isSubKind k1               OpenTypeKind     = isOpenTypeKind k1
 156 isSubKind k1               ArgTypeKind      = isArgTypeKind k1
 157 isSubKind (FunKind a1 r1) (FunKind a2 r2)
 158   = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
 159 isSubKind k1 k2 = False
 160
 161 defaultKind :: Kind -> Kind
 162 -- Used when generalising: default kind '?' and '??' to '*'
 163 --
 164 -- When we generalise, we make generic type variables whose kind is
 165 -- simple (* or *->* etc).  So generic type variables (other than
 166 -- built-in constants like 'error') always have simple kinds.  This is important;
 167 -- consider
 168 --      f x = True
 169 -- We want f to get type
 170 --      f :: forall (a::*). a -> Bool
 171 -- Not
 172 --      f :: forall (a::??). a -> Bool
 173 -- because that would allow a call like (f 3#) as well as (f True),
 174 --and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
 175 defaultKind OpenTypeKind = LiftedTypeKind
 176 defaultKind ArgTypeKind  = LiftedTypeKind
 177 defaultKind kind         = kind
 178 \end{code}
 179
 180
 181 %************************************************************************
 182 %*                                                                      *
 183                 Pretty printing
 184 %*                                                                      *
 185 %************************************************************************
 186
 187 \begin{code}
 188 instance Outputable KindVar where
 189   ppr (KVar uniq _) = text "k_" <> ppr uniq
 190
 191 instance Outputable Kind where
 192   ppr k = pprKind k
 193
 194 pprParendKind :: Kind -> SDoc
 195 pprParendKind k@(FunKind _ _) = parens (pprKind k)
 196 pprParendKind k               = pprKind k
 197
 198 pprKind (KindVar v)      = ppr v
 199 pprKind LiftedTypeKind   = ptext SLIT("*")
 200 pprKind UnliftedTypeKind = ptext SLIT("#")
 201 pprKind OpenTypeKind     = ptext SLIT("?")
 202 pprKind ArgTypeKind      = ptext SLIT("??")
 203 pprKind UbxTupleKind     = ptext SLIT("(#)")
 204 pprKind (FunKind k1 k2)  = sep [ pprParendKind k1, arrow <+> pprKind k2]
 205 \end{code}
 206
 207
 208