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 (KindVar _)   = False    -- This is a conservative answer
 149                                         -- It matters in the call to isSubKind in
 150                                         -- checkExpectedKind.
 151 isOpenTypeKind other         = True
 152
 153 isSubKind :: Kind -> Kind -> Bool
 154 -- (k1 `isSubKind` k2) checks that k1 <: k2
 155 isSubKind LiftedTypeKind   LiftedTypeKind   = True
 156 isSubKind UnliftedTypeKind UnliftedTypeKind = True
 157 isSubKind UbxTupleKind     UbxTupleKind     = True
 158 isSubKind k1               OpenTypeKind     = isOpenTypeKind k1
 159 isSubKind k1               ArgTypeKind      = isArgTypeKind k1
 160 isSubKind (FunKind a1 r1) (FunKind a2 r2)   = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
 161 isSubKind k1              k2                = False
 162
 163 defaultKind :: Kind -> Kind
 164 -- Used when generalising: default kind '?' and '??' to '*'
 165 --
 166 -- When we generalise, we make generic type variables whose kind is
 167 -- simple (* or *->* etc).  So generic type variables (other than
 168 -- built-in constants like 'error') always have simple kinds.  This is important;
 169 -- consider
 170 --      f x = True
 171 -- We want f to get type
 172 --      f :: forall (a::*). a -> Bool
 173 -- Not
 174 --      f :: forall (a::??). a -> Bool
 175 -- because that would allow a call like (f 3#) as well as (f True),
 176 --and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
 177 defaultKind OpenTypeKind = LiftedTypeKind
 178 defaultKind ArgTypeKind  = LiftedTypeKind
 179 defaultKind kind         = kind
 180 \end{code}
 181
 182
 183 %************************************************************************
 184 %*                                                                      *
 185                 Pretty printing
 186 %*                                                                      *
 187 %************************************************************************
 188
 189 \begin{code}
 190 instance Outputable KindVar where
 191   ppr (KVar uniq _) = text "k_" <> ppr uniq
 192
 193 instance Outputable Kind where
 194   ppr k = pprKind k
 195
 196 pprParendKind :: Kind -> SDoc
 197 pprParendKind k@(FunKind _ _) = parens (pprKind k)
 198 pprParendKind k               = pprKind k
 199
 200 pprKind (KindVar v)      = ppr v
 201 pprKind LiftedTypeKind   = ptext SLIT("*")
 202 pprKind UnliftedTypeKind = ptext SLIT("#")
 203 pprKind OpenTypeKind     = ptext SLIT("?")
 204 pprKind ArgTypeKind      = ptext SLIT("??")
 205 pprKind UbxTupleKind     = ptext SLIT("(#)")
 206 pprKind (FunKind k1 k2)  = sep [ pprParendKind k1, arrow <+> pprKind k2]
 207 \end{code}
 208
 209
 210