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:<any>. String -> a
  48         (->)  :: ?? -> ? -> *
  49         (\(x::t) -> ...)        Here t::<any> (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 instantaited 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 In the olden days, when we generalise, we make generic type variables
 101 whose kind is simple.  So generic type variables (other than built-in
 102 constants like 'error') always have simple kinds.  But I don't see any
 103 reason to do that any more (TcMType.zapTcTyVarToTyVar).
 104
 105
 106 \begin{code}
 107 liftedTypeKind   = LiftedTypeKind
 108 unliftedTypeKind = UnliftedTypeKind
 109 openTypeKind     = OpenTypeKind
 110 argTypeKind      = ArgTypeKind
 111 ubxTupleKind     = UbxTupleKind
 112
 113 mkArrowKind :: Kind -> Kind -> Kind
 114 mkArrowKind k1 k2 = k1 `FunKind` k2
 115
 116 mkArrowKinds :: [Kind] -> Kind -> Kind
 117 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
 118 \end{code}
 119
 120 %************************************************************************
 121 %*                                                                      *
 122         Functions over Kinds
 123 %*                                                                      *
 124 %************************************************************************
 125
 126 \begin{code}
 127 kindFunResult :: Kind -> Kind
 128 kindFunResult (FunKind _ k) = k
 129 kindFunResult k = pprPanic "kindFunResult" (ppr k)
 130
 131 splitKindFunTys :: Kind -> ([Kind],Kind)
 132 splitKindFunTys (FunKind k1 k2) = case splitKindFunTys k2 of
 133                                     (as, r) -> (k1:as, r)
 134 splitKindFunTys k = ([], k)
 135
 136 isLiftedTypeKind, isUnliftedTypeKind :: Kind -> Bool
 137 isLiftedTypeKind LiftedTypeKind = True
 138 isLiftedTypeKind other          = False
 139
 140 isUnliftedTypeKind UnliftedTypeKind = True
 141 isUnliftedTypeKind other            = False
 142
 143 isArgTypeKind :: Kind -> Bool
 144 -- True of any sub-kind of ArgTypeKind
 145 isArgTypeKind LiftedTypeKind   = True
 146 isArgTypeKind UnliftedTypeKind = True
 147 isArgTypeKind ArgTypeKind      = True
 148 isArgTypeKind other            = False
 149
 150 isOpenTypeKind :: Kind -> Bool
 151 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
 152 isOpenTypeKind (FunKind _ _) = False
 153 isOpenTypeKind other         = True
 154
 155 isSubKind :: Kind -> Kind -> Bool
 156 -- (k1 `isSubKind` k2) checks that k1 <: k2
 157 isSubKind LiftedTypeKind   LiftedTypeKind   = True
 158 isSubKind UnliftedTypeKind UnliftedTypeKind = True
 159 isSubKind UbxTupleKind     UbxTupleKind     = True
 160 isSubKind k1               OpenTypeKind     = isOpenTypeKind k1
 161 isSubKind k1               ArgTypeKind      = isArgTypeKind k1
 162 isSubKind (FunKind a1 r1) (FunKind a2 r2)
 163   = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
 164 isSubKind k1 k2 = False
 165
 166 defaultKind :: Kind -> Kind
 167 -- Used when generalising: default kind '?' and '??' to '*'
 168 defaultKind OpenTypeKind = LiftedTypeKind
 169 defaultKind ArgTypeKind  = LiftedTypeKind
 170 defaultKind kind         = kind
 171 \end{code}
 172
 173
 174 %************************************************************************
 175 %*                                                                      *
 176                 Pretty printing
 177 %*                                                                      *
 178 %************************************************************************
 179
 180 \begin{code}
 181 instance Outputable KindVar where
 182   ppr (KVar uniq _) = text "k_" <> ppr uniq
 183
 184 instance Outputable Kind where
 185   ppr k = pprKind k
 186
 187 pprParendKind :: Kind -> SDoc
 188 pprParendKind k@(FunKind _ _) = parens (pprKind k)
 189 pprParendKind k               = pprKind k
 190
 191 pprKind (KindVar v)      = ppr v
 192 pprKind LiftedTypeKind   = ptext SLIT("*")
 193 pprKind UnliftedTypeKind = ptext SLIT("#")
 194 pprKind OpenTypeKind     = ptext SLIT("?")
 195 pprKind ArgTypeKind      = ptext SLIT("??")
 196 pprKind UbxTupleKind     = ptext SLIT("(#)")
 197 pprKind (FunKind k1 k2)  = sep [ pprKind k1, arrow <+> pprParendKind k2]
 198 \end{code}
 199
 200
 201