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