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