ghc/compiler/typecheck/TcKind.lhs

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