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