ghc/compiler/typecheck/TcKind.lhs

   1 \begin{code}
   2 #include "HsVersions.h"
   3
   4 module TcKind (
   5
   6         Kind, mkTypeKind, mkBoxedTypeKind, mkUnboxedTypeKind, mkArrowKind,
   7         hasMoreBoxityInfo,      -- Kind -> Kind -> Bool
   8         resultKind,             -- Kind -> Kind
   9
  10         TcKind, mkTcTypeKind, mkTcArrowKind, mkTcVarKind,
  11         newKindVar,     -- NF_TcM s (TcKind s)
  12         newKindVars,    -- Int -> NF_TcM s [TcKind s]
  13         unifyKind,      -- TcKind s -> TcKind s -> TcM s ()
  14
  15         kindToTcKind,   -- Kind     -> TcKind s
  16         tcDefaultKind   -- TcKind s -> NF_TcM s Kind
  17   ) where
  18
  19 IMP_Ubiq(){-uitous-}
  20
  21 import Kind
  22 import TcMonad
  23
  24 import Unique   ( Unique, pprUnique10 )
  25 import Pretty
  26 import Util     ( nOfThem )
  27 import Outputable
  28 \end{code}
  29
  30
  31 \begin{code}
  32 data TcKind s           -- Used for kind inference
  33   = TcTypeKind
  34   | TcArrowKind (TcKind s) (TcKind s)
  35   | TcVarKind Unique (MutableVar s (Maybe (TcKind s)))
  36
  37 mkTcTypeKind  = TcTypeKind
  38 mkTcArrowKind = TcArrowKind
  39 mkTcVarKind   = TcVarKind
  40
  41 newKindVar :: NF_TcM s (TcKind s)
  42 newKindVar = tcGetUnique                `thenNF_Tc` \ uniq ->
  43              tcNewMutVar Nothing        `thenNF_Tc` \ box ->
  44              returnNF_Tc (TcVarKind uniq box)
  45
  46 newKindVars :: Int -> NF_TcM s [TcKind s]
  47 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
  48 \end{code}
  49
  50
  51 Kind unification
  52 ~~~~~~~~~~~~~~~~
  53 \begin{code}
  54 unifyKind :: TcKind s -> TcKind s -> TcM s ()
  55 unifyKind kind1 kind2
  56   = tcAddErrCtxtM ctxt (unify_kind kind1 kind2)
  57   where
  58     ctxt = zonkTcKind kind1     `thenNF_Tc` \ kind1' ->
  59            zonkTcKind kind2     `thenNF_Tc` \ kind2' ->
  60            returnNF_Tc (unifyKindCtxt kind1' kind2')
  61
  62
  63 unify_kind TcTypeKind TcTypeKind = returnTc ()
  64
  65 unify_kind (TcArrowKind fun1 arg1)
  66            (TcArrowKind fun2 arg2)
  67
  68   = unify_kind fun1 fun2        `thenTc_`
  69     unify_kind arg1 arg2
  70
  71 unify_kind (TcVarKind uniq box) kind = unify_var uniq box kind
  72 unify_kind kind (TcVarKind uniq box) = unify_var uniq box kind
  73
  74 unify_kind kind1 kind2
  75   = failTc (kindMisMatchErr kind1 kind2)
  76 \end{code}
  77
  78 We could probably do some "shorting out" in unifyVarKind, but
  79 I'm not convinced it would save time, and it's a little tricky to get right.
  80
  81 \begin{code}
  82 unify_var uniq1 box1 kind2
  83   = tcReadMutVar box1   `thenNF_Tc` \ maybe_kind1 ->
  84     case maybe_kind1 of
  85       Just kind1 -> unify_kind kind1 kind2
  86       Nothing    -> unify_unbound_var uniq1 box1 kind2
  87
  88 unify_unbound_var uniq1 box1 kind2@(TcVarKind uniq2 box2)
  89   | uniq1 == uniq2      -- Binding to self is a no-op
  90   = returnTc ()
  91
  92   | otherwise           -- Distinct variables
  93   = tcReadMutVar box2   `thenNF_Tc` \ maybe_kind2 ->
  94     case maybe_kind2 of
  95         Just kind2' -> unify_unbound_var uniq1 box1 kind2'
  96         Nothing     -> tcWriteMutVar box1 (Just kind2)  `thenNF_Tc_`
  97                                 -- No need for occurs check here
  98                        returnTc ()
  99
 100 unify_unbound_var uniq1 box1 non_var_kind2
 101   = occur_check non_var_kind2                   `thenTc_`
 102     tcWriteMutVar box1 (Just non_var_kind2)     `thenNF_Tc_`
 103     returnTc ()
 104   where
 105     occur_check TcTypeKind            = returnTc ()
 106     occur_check (TcArrowKind fun arg) = occur_check fun `thenTc_` occur_check arg
 107     occur_check kind1@(TcVarKind uniq' box)
 108         | uniq1 == uniq'
 109         = failTc (kindOccurCheck kind1 non_var_kind2)
 110
 111         | otherwise     -- Different variable
 112         =  tcReadMutVar box             `thenNF_Tc` \ maybe_kind ->
 113            case maybe_kind of
 114                 Nothing   -> returnTc ()
 115                 Just kind -> occur_check kind
 116 \end{code}
 117
 118 The "occurs check" is necessary to catch situation like
 119
 120         type T k = k k
 121
 122
 123 Kind flattening
 124 ~~~~~~~~~~~~~~~
 125 Coercions between TcKind and Kind
 126
 127 \begin{code}
 128 kindToTcKind :: Kind -> TcKind s
 129 kindToTcKind TypeKind          = TcTypeKind
 130 kindToTcKind BoxedTypeKind     = TcTypeKind
 131 kindToTcKind UnboxedTypeKind   = TcTypeKind
 132 kindToTcKind (ArrowKind k1 k2) = TcArrowKind (kindToTcKind k1) (kindToTcKind k2)
 133
 134
 135 -- Default all unbound kinds to TcTypeKind, and return the
 136 -- corresponding Kind as well.
 137 tcDefaultKind :: TcKind s -> NF_TcM s Kind
 138
 139 tcDefaultKind TcTypeKind
 140   = returnNF_Tc BoxedTypeKind
 141
 142 tcDefaultKind (TcArrowKind kind1 kind2)
 143   = tcDefaultKind kind1 `thenNF_Tc` \ k1 ->
 144     tcDefaultKind kind2 `thenNF_Tc` \ k2 ->
 145     returnNF_Tc (ArrowKind k1 k2)
 146
 147         -- Here's where we "default" unbound kinds to BoxedTypeKind
 148 tcDefaultKind (TcVarKind uniq box)
 149   = tcReadMutVar box    `thenNF_Tc` \ maybe_kind ->
 150     case maybe_kind of
 151         Just kind -> tcDefaultKind kind
 152
 153         Nothing   ->    -- Default unbound variables to kind Type
 154                      tcWriteMutVar box (Just TcTypeKind)        `thenNF_Tc_`
 155                      returnNF_Tc BoxedTypeKind
 156
 157 zonkTcKind :: TcKind s -> NF_TcM s (TcKind s)
 158 -- Removes variables that have now been bound.
 159 -- Mainly used just before an error message is printed,
 160 -- so that we don't need to follow through bound variables
 161 -- during error message construction.
 162
 163 zonkTcKind TcTypeKind = returnNF_Tc TcTypeKind
 164
 165 zonkTcKind (TcArrowKind kind1 kind2)
 166   = zonkTcKind kind1    `thenNF_Tc` \ k1 ->
 167     zonkTcKind kind2    `thenNF_Tc` \ k2 ->
 168     returnNF_Tc (TcArrowKind k1 k2)
 169
 170 zonkTcKind kind@(TcVarKind uniq box)
 171   = tcReadMutVar box    `thenNF_Tc` \ maybe_kind ->
 172     case maybe_kind of
 173         Nothing    -> returnNF_Tc kind
 174         Just kind' -> zonkTcKind kind'
 175 \end{code}
 176
 177
 178 \begin{code}
 179 instance Outputable (TcKind s) where
 180   ppr sty kind = pprQuote sty $ \ sty -> ppr_kind sty kind
 181
 182 ppr_kind sty TcTypeKind
 183   = char '*'
 184 ppr_kind sty (TcArrowKind kind1 kind2)
 185   = sep [ppr_parend sty kind1, ptext SLIT("->"), ppr_kind sty kind2]
 186 ppr_kind sty (TcVarKind uniq box)
 187   = hcat [char 'k', pprUnique10 uniq]
 188
 189 ppr_parend sty kind@(TcArrowKind _ _) = hcat [char '(', ppr_kind sty kind, char ')']
 190 ppr_parend sty other_kind             = ppr_kind sty other_kind
 191 \end{code}
 192
 193
 194
 195 Errors and contexts
 196 ~~~~~~~~~~~~~~~~~~~
 197 \begin{code}
 198 unifyKindCtxt kind1 kind2 sty
 199   = hang (ptext SLIT("When unifying two kinds")) 4
 200            (sep [ppr sty kind1, ptext SLIT("and"), ppr sty kind2])
 201
 202 kindOccurCheck kind1 kind2 sty
 203   = hang (ptext SLIT("Cannot construct the infinite kind:")) 4
 204         (sep [ppr sty kind1, equals, ppr sty kind1, ptext SLIT("(\"occurs check\")")])
 205
 206 kindMisMatchErr kind1 kind2 sty
 207  = hang (ptext SLIT("Couldn't match the kind")) 4
 208         (sep [ppr sty kind1,
 209               ptext SLIT("against"),
 210               ppr sty kind2]
 211         )
 212 \end{code}