ghc/compiler/typecheck/TcKind.lhs

   1 \begin{code}
   2 module TcKind (
   3
   4         Kind, mkTypeKind, mkBoxedTypeKind, mkUnboxedTypeKind, mkArrowKind,
   5         hasMoreBoxityInfo,      -- Kind -> Kind -> Bool
   6         resultKind,             -- Kind -> Kind
   7
   8         TcKind,
   9         newKindVar,     -- NF_TcM s (TcKind s)
  10         newKindVars,    -- Int -> NF_TcM s [TcKind s]
  11         unifyKind,      -- TcKind s -> TcKind s -> TcM s ()
  12         unifyKinds,     -- [TcKind s] -> [TcKind s] -> TcM s ()
  13
  14         kindToTcKind,   -- Kind     -> TcKind s
  15         tcDefaultKind   -- TcKind s -> NF_TcM s Kind
  16   ) where
  17
  18 #include "HsVersions.h"
  19
  20 import Kind
  21 import TcMonad
  22
  23 import Unique   ( Unique )
  24 import Util     ( nOfThem, panic )
  25 import Outputable
  26 \end{code}
  27
  28
  29 \begin{code}
  30 type TcKind s = GenKind (TcRef s (TcMaybe s))
  31 data TcMaybe s = Unbound
  32                | BoundTo (TcKind s)     -- Always ArrowKind or BoxedTypeKind
  33
  34 newKindVar :: NF_TcM s (TcKind s)
  35 newKindVar = tcGetUnique                `thenNF_Tc` \ uniq ->
  36              tcNewMutVar Unbound        `thenNF_Tc` \ box ->
  37              returnNF_Tc (VarKind uniq box)
  38
  39 newKindVars :: Int -> NF_TcM s [TcKind s]
  40 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
  41 \end{code}
  42
  43
  44 Kind unification
  45 ~~~~~~~~~~~~~~~~
  46 \begin{code}
  47 unifyKinds :: [TcKind s] -> [TcKind s] -> TcM s ()
  48 unifyKinds [] [] = returnTc ()
  49 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2  `thenTc_`
  50                                unifyKinds ks1 ks2
  51 unifyKinds _ _ = panic "unifyKinds: length mis-match"
  52
  53 unifyKind :: TcKind s               -- Expected
  54           -> TcKind s               -- Actual
  55           -> TcM s ()
  56
  57 unifyKind kind1 kind2
  58   = tcAddErrCtxtM ctxt (unify_kind kind1 kind2)
  59   where
  60     ctxt = zonkTcKind kind1     `thenNF_Tc` \ kind1' ->
  61            zonkTcKind kind2     `thenNF_Tc` \ kind2' ->
  62            returnNF_Tc (unifyKindCtxt kind1' kind2')
  63
  64
  65 -- TypeKind expected => the actual can be boxed or unboxed
  66 unify_kind TypeKind        TypeKind        = returnTc ()
  67 unify_kind TypeKind        BoxedTypeKind   = returnTc ()
  68 unify_kind TypeKind        UnboxedTypeKind = returnTc ()
  69
  70 unify_kind BoxedTypeKind   BoxedTypeKind   = returnTc ()
  71 unify_kind UnboxedTypeKind UnboxedTypeKind = returnTc ()
  72
  73 unify_kind (ArrowKind fun1 arg1)
  74            (ArrowKind fun2 arg2)
  75
  76   = unify_kind fun1 fun2        `thenTc_`
  77     unify_kind arg1 arg2
  78
  79 unify_kind kind1@(VarKind uniq box) kind2 = unify_var False kind1 uniq box kind2
  80 unify_kind kind1 kind2@(VarKind uniq box) = unify_var True  kind2 uniq box kind1
  81
  82 unify_kind kind1 kind2
  83   = failWithTc (kindMisMatchErr kind1 kind2)
  84 \end{code}
  85
  86 We could probably do some "shorting out" in unifyVarKind, but
  87 I'm not convinced it would save time, and it's a little tricky to get right.
  88
  89 \begin{code}
  90 unify_var swap_vars kind1 uniq1 box1 kind2
  91   = tcReadMutVar box1   `thenNF_Tc` \ maybe_kind1 ->
  92     case maybe_kind1 of
  93       Unbound          -> unify_unbound_var False kind1 uniq1 box1 kind2
  94       BoundTo TypeKind -> unify_unbound_var True  kind1 uniq1 box1 kind2
  95                           -- *** NB: BoundTo TypeKind is a kind of un-bound
  96                           --         It can get refined to BoundTo UnboxedTypeKind or BoxedTypeKind
  97
  98       BoundTo kind1' | swap_vars -> unify_kind kind2 kind1'
  99                      | otherwise -> unify_kind kind1' kind2
 100                      -- Keep them the right way round, so that
 101                      -- the asymettric boxed/unboxed stuff works
 102
 103
 104 unify_unbound_var type_kind kind1 uniq1 box1 kind2@(VarKind uniq2 box2)
 105   | uniq1 == uniq2      -- Binding to self is a no-op
 106   = returnTc ()
 107
 108   | otherwise           -- Distinct variables
 109   = tcReadMutVar box2   `thenNF_Tc` \ maybe_kind2 ->
 110     case maybe_kind2 of
 111         BoundTo kind2' -> unify_unbound_var type_kind kind1 uniq1 box1 kind2'
 112         Unbound        -> tcWriteMutVar box2 (BoundTo kind1)    `thenNF_Tc_`
 113                                 -- No need for occurs check here
 114                                 -- Kind1 is an unbound variable, or BoundToTypeKind
 115                           returnTc ()
 116
 117 -- If the variable was originally bound to TypeKind, we succeed
 118 -- unless the thing its bound to is an arrow.
 119 unify_unbound_var True kind1 uniq1 box1 kind2@(ArrowKind k1 k2)
 120   = failWithTc (kindMisMatchErr kind1 kind2)
 121
 122 unify_unbound_var type_kind kind1 uniq1 box1 non_var_or_arrow_kind2
 123   = occur_check non_var_or_arrow_kind2                  `thenTc_`
 124     tcWriteMutVar box1 (BoundTo non_var_or_arrow_kind2) `thenNF_Tc_`
 125     returnTc ()
 126   where
 127     occur_check TypeKind            = returnTc ()
 128     occur_check UnboxedTypeKind     = returnTc ()
 129     occur_check BoxedTypeKind       = returnTc ()
 130     occur_check (ArrowKind fun arg) = occur_check fun `thenTc_` occur_check arg
 131     occur_check kind@(VarKind uniq' box)
 132         | uniq1 == uniq'
 133         = failWithTc (kindOccurCheck kind non_var_or_arrow_kind2)
 134
 135         | otherwise     -- Different variable
 136         =  tcReadMutVar box             `thenNF_Tc` \ maybe_kind ->
 137            case maybe_kind of
 138                 Unbound       -> returnTc ()
 139                 BoundTo kind' -> occur_check kind'
 140 \end{code}
 141
 142 The "occurs check" is necessary to catch situation like
 143
 144         type T k = k k
 145
 146
 147 Kind flattening
 148 ~~~~~~~~~~~~~~~
 149 Coercions between TcKind and Kind.
 150
 151 \begin{code}
 152 -- This strange function is forced on us by the type system
 153 kindToTcKind :: Kind -> TcKind s
 154 kindToTcKind TypeKind          = TypeKind
 155 kindToTcKind BoxedTypeKind     = BoxedTypeKind
 156 kindToTcKind UnboxedTypeKind   = UnboxedTypeKind
 157 kindToTcKind (ArrowKind k1 k2) = ArrowKind (kindToTcKind k1) (kindToTcKind k2)
 158
 159
 160 -- Default all unbound kinds to TcTypeKind, and return the
 161 -- corresponding Kind as well.
 162 tcDefaultKind :: TcKind s -> NF_TcM s Kind
 163
 164 tcDefaultKind TypeKind        = returnNF_Tc TypeKind
 165 tcDefaultKind BoxedTypeKind   = returnNF_Tc BoxedTypeKind
 166 tcDefaultKind UnboxedTypeKind = returnNF_Tc UnboxedTypeKind
 167
 168 tcDefaultKind (ArrowKind kind1 kind2)
 169   = tcDefaultKind kind1 `thenNF_Tc` \ k1 ->
 170     tcDefaultKind kind2 `thenNF_Tc` \ k2 ->
 171     returnNF_Tc (ArrowKind k1 k2)
 172
 173         -- Here's where we "default" unbound kinds to BoxedTypeKind
 174 tcDefaultKind (VarKind uniq box)
 175   = tcReadMutVar box    `thenNF_Tc` \ maybe_kind ->
 176     case maybe_kind of
 177         BoundTo TypeKind -> bind_to_boxed
 178         Unbound          -> bind_to_boxed
 179         BoundTo kind     -> tcDefaultKind kind
 180   where
 181         -- Default unbound variables to kind BoxedTypeKind
 182     bind_to_boxed = tcWriteMutVar box (BoundTo BoxedTypeKind)   `thenNF_Tc_`
 183                     returnNF_Tc BoxedTypeKind
 184
 185
 186
 187 zonkTcKind :: TcKind s -> NF_TcM s (TcKind s)
 188 -- Removes variables that have now been bound.
 189 -- Mainly used just before an error message is printed,
 190 -- so that we don't need to follow through bound variables
 191 -- during error message construction.
 192
 193 zonkTcKind TypeKind        = returnNF_Tc TypeKind
 194 zonkTcKind BoxedTypeKind   = returnNF_Tc BoxedTypeKind
 195 zonkTcKind UnboxedTypeKind = returnNF_Tc UnboxedTypeKind
 196
 197 zonkTcKind (ArrowKind kind1 kind2)
 198   = zonkTcKind kind1    `thenNF_Tc` \ k1 ->
 199     zonkTcKind kind2    `thenNF_Tc` \ k2 ->
 200     returnNF_Tc (ArrowKind k1 k2)
 201
 202 zonkTcKind kind@(VarKind uniq box)
 203   = tcReadMutVar box    `thenNF_Tc` \ maybe_kind ->
 204     case maybe_kind of
 205         Unbound    -> returnNF_Tc kind
 206         BoundTo kind' -> zonkTcKind kind'
 207 \end{code}
 208
 209
 210 Errors and contexts
 211 ~~~~~~~~~~~~~~~~~~~
 212 \begin{code}
 213 unifyKindCtxt kind1 kind2
 214   = vcat [ptext SLIT("Expected:") <+> ppr kind1,
 215           ptext SLIT("Found:   ") <+> ppr kind2]
 216
 217 kindOccurCheck kind1 kind2
 218   = hang (ptext SLIT("Cannot construct the infinite kind:")) 4
 219         (sep [ppr kind1, equals, ppr kind1, ptext SLIT("(\"occurs check\")")])
 220
 221 kindMisMatchErr kind1 kind2
 222  = hang (ptext SLIT("Couldn't match the kind")) 4
 223         (sep [ppr kind1,
 224               ptext SLIT("against"),
 225               ppr kind2]
 226         )
 227 \end{code}