compiler/types/Kind.lhs

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