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         tcKindToKind    -- 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 kind1
  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 tcKindToKind :: TcKind s -> NF_TcM s Kind
 131
 132 tcKindToKind TcTypeKind
 133   = returnNF_Tc TypeKind
 134
 135 tcKindToKind (TcArrowKind kind1 kind2)
 136   = tcKindToKind kind1  `thenNF_Tc` \ k1 ->
 137     tcKindToKind kind2  `thenNF_Tc` \ k2 ->
 138     returnNF_Tc (ArrowKind k1 k2)
 139
 140         -- Here's where we "default" unbound kinds to BoxedTypeKind
 141 tcKindToKind (TcVarKind uniq box)
 142   = tcReadMutVar box    `thenNF_Tc` \ maybe_kind ->
 143     case maybe_kind of
 144         Nothing   -> returnNF_Tc BoxedTypeKind  -- Default is kind Type for unbound
 145         Just kind -> tcKindToKind kind
 146
 147 zonkTcKind :: TcKind s -> NF_TcM s (TcKind s)
 148 -- Removes variables that have now been bound.
 149 -- Mainly used just before an error message is printed,
 150 -- so that we don't need to follow through bound variables
 151 -- during error message construction.
 152
 153 zonkTcKind TcTypeKind = returnNF_Tc TcTypeKind
 154
 155 zonkTcKind (TcArrowKind kind1 kind2)
 156   = zonkTcKind kind1    `thenNF_Tc` \ k1 ->
 157     zonkTcKind kind2    `thenNF_Tc` \ k2 ->
 158     returnNF_Tc (TcArrowKind k1 k2)
 159
 160 zonkTcKind kind@(TcVarKind uniq box)
 161   = tcReadMutVar box    `thenNF_Tc` \ maybe_kind ->
 162     case maybe_kind of
 163         Nothing    -> returnNF_Tc kind
 164         Just kind' -> zonkTcKind kind'
 165 \end{code}
 166
 167
 168 \begin{code}
 169 instance Outputable (TcKind s) where
 170   ppr sty kind = ppr_kind sty kind
 171
 172 ppr_kind sty TcTypeKind
 173   = ppStr "*"
 174 ppr_kind sty (TcArrowKind kind1 kind2)
 175   = ppSep [ppr_parend sty kind1, ppStr "->", ppr_kind sty kind2]
 176 ppr_kind sty (TcVarKind uniq box)
 177   = ppBesides [ppStr "k", pprUnique10 uniq]
 178
 179 ppr_parend sty kind@(TcArrowKind _ _) = ppBesides [ppChar '(', ppr_kind sty kind, ppChar ')']
 180 ppr_parend sty other_kind             = ppr_kind sty other_kind
 181 \end{code}
 182
 183
 184
 185 Errors and contexts
 186 ~~~~~~~~~~~~~~~~~~~
 187 \begin{code}
 188 unifyKindCtxt kind1 kind2 sty
 189   = ppHang (ppStr "When unifying two kinds") 4
 190            (ppSep [ppr sty kind1, ppStr "and", ppr sty kind2])
 191
 192 kindOccurCheck kind1 kind2 sty
 193   = ppHang (ppStr "Cannot construct the infinite kind:") 4
 194         (ppSep [ppBesides [ppStr "`", ppr sty kind1, ppStr "'"],
 195                 ppStr "=",
 196                 ppBesides [ppStr "`", ppr sty kind1, ppStr "'"],
 197                 ppStr "(\"occurs check\")"])
 198
 199 kindMisMatchErr kind1 kind2 sty
 200  = ppHang (ppStr "Couldn't match the kind") 4
 201         (ppSep [ppBesides [ppStr "`", ppr sty kind1, ppStr "'"],
 202                 ppStr "against",
 203                 ppBesides [ppStr "`", ppr sty kind1, ppStr "'"]
 204         ])
 205 \end{code}