722d162ecb7b9a7ff43d601b74d074e6ba141a3b
[ghc.git] / compiler / typecheck / TcHsType.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 %
5 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
6
7 \begin{code}
8 {-# LANGUAGE CPP #-}
9
10 module TcHsType (
11         tcHsSigType, tcHsSigTypeNC, tcHsDeriv, tcHsVectInst,
12         tcHsInstHead,
13         UserTypeCtxt(..),
14
15                 -- Type checking type and class decls
16         kcLookupKind, kcTyClTyVars, tcTyClTyVars,
17         tcHsConArgType, tcDataKindSig,
18         tcClassSigType,
19
20                 -- Kind-checking types
21                 -- No kind generalisation, no checkValidType
22         kcHsTyVarBndrs, tcHsTyVarBndrs,
23         tcHsLiftedType, tcHsOpenType,
24         tcLHsType, tcCheckLHsType,
25         tcHsContext, tcInferApps, tcHsArgTys,
26
27         kindGeneralize, checkKind,
28
29                 -- Sort-checking kinds
30         tcLHsKind,
31
32                 -- Pattern type signatures
33         tcHsPatSigType, tcPatSig
34    ) where
35
36 #include "HsVersions.h"
37
38 import HsSyn
39 import TcRnMonad
40 import TcEvidence( HsWrapper )
41 import TcEnv
42 import TcMType
43 import TcValidity
44 import TcUnify
45 import TcIface
46 import TcType
47 import Type
48 import TypeRep( Type(..) )  -- For the mkNakedXXX stuff
49 import Kind
50 import RdrName( lookupLocalRdrOcc )
51 import Var
52 import VarSet
53 import TyCon
54 import ConLike
55 import DataCon
56 import TysPrim ( liftedTypeKindTyConName, constraintKindTyConName )
57 import Class
58 import Name
59 import NameEnv
60 import TysWiredIn
61 import BasicTypes
62 import SrcLoc
63 import DynFlags ( ExtensionFlag( Opt_DataKinds ), getDynFlags )
64 import Unique
65 import UniqSupply
66 import Outputable
67 import FastString
68 import Util
69
70 import Data.Maybe( isNothing )
71 import Control.Monad ( unless, when, zipWithM )
72 import PrelNames( ipClassName, funTyConKey, allNameStrings )
73 \end{code}
74
75
76         ----------------------------
77                 General notes
78         ----------------------------
79
80 Generally speaking we now type-check types in three phases
81
82   1.  kcHsType: kind check the HsType
83         *includes* performing any TH type splices;
84         so it returns a translated, and kind-annotated, type
85
86   2.  dsHsType: convert from HsType to Type:
87         perform zonking
88         expand type synonyms [mkGenTyApps]
89         hoist the foralls [tcHsType]
90
91   3.  checkValidType: check the validity of the resulting type
92
93 Often these steps are done one after the other (tcHsSigType).
94 But in mutually recursive groups of type and class decls we do
95         1 kind-check the whole group
96         2 build TyCons/Classes in a knot-tied way
97         3 check the validity of types in the now-unknotted TyCons/Classes
98
99 For example, when we find
100         (forall a m. m a -> m a)
101 we bind a,m to kind varibles and kind-check (m a -> m a).  This makes
102 a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a) in
103 an environment that binds a and m suitably.
104
105 The kind checker passed to tcHsTyVars needs to look at enough to
106 establish the kind of the tyvar:
107   * For a group of type and class decls, it's just the group, not
108         the rest of the program
109   * For a tyvar bound in a pattern type signature, its the types
110         mentioned in the other type signatures in that bunch of patterns
111   * For a tyvar bound in a RULE, it's the type signatures on other
112         universally quantified variables in the rule
113
114 Note that this may occasionally give surprising results.  For example:
115
116         data T a b = MkT (a b)
117
118 Here we deduce                  a::*->*,       b::*
119 But equally valid would be      a::(*->*)-> *, b::*->*
120
121
122 Validity checking
123 ~~~~~~~~~~~~~~~~~
124 Some of the validity check could in principle be done by the kind checker,
125 but not all:
126
127 - During desugaring, we normalise by expanding type synonyms.  Only
128   after this step can we check things like type-synonym saturation
129   e.g.  type T k = k Int
130         type S a = a
131   Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
132   and then S is saturated.  This is a GHC extension.
133
134 - Similarly, also a GHC extension, we look through synonyms before complaining
135   about the form of a class or instance declaration
136
137 - Ambiguity checks involve functional dependencies, and it's easier to wait
138   until knots have been resolved before poking into them
139
140 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
141 finished building the loop.  So to keep things simple, we postpone most validity
142 checking until step (3).
143
144 Knot tying
145 ~~~~~~~~~~
146 During step (1) we might fault in a TyCon defined in another module, and it might
147 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
148 knot around type declarations with ARecThing, so that the fault-in code can get
149 the TyCon being defined.
150
151
152 %************************************************************************
153 %*                                                                      *
154               Check types AND do validity checking
155 %*                                                                      *
156 %************************************************************************
157
158 \begin{code}
159 tcHsSigType, tcHsSigTypeNC :: UserTypeCtxt -> LHsType Name -> TcM Type
160   -- NB: it's important that the foralls that come from the top-level
161   --     HsForAllTy in hs_ty occur *first* in the returned type.
162   --     See Note [Scoped] with TcSigInfo
163 tcHsSigType ctxt hs_ty
164   = addErrCtxt (pprSigCtxt ctxt empty (ppr hs_ty)) $
165     tcHsSigTypeNC ctxt hs_ty
166
167 tcHsSigTypeNC ctxt (L loc hs_ty)
168   = setSrcSpan loc $    -- The "In the type..." context
169                         -- comes from the caller; hence "NC"
170     do  { kind <- case expectedKindInCtxt ctxt of
171                     Nothing -> newMetaKindVar
172                     Just k  -> return k
173           -- The kind is checked by checkValidType, and isn't necessarily
174           -- of kind * in a Template Haskell quote eg [t| Maybe |]
175
176           -- Generalise here: see Note [Kind generalisation]
177         ; ty <- tcCheckHsTypeAndGen hs_ty kind
178
179           -- Zonk to expose kind information to checkValidType
180         ; ty <- zonkSigType ty
181         ; checkValidType ctxt ty
182         ; return ty }
183
184 -----------------
185 tcHsInstHead :: UserTypeCtxt -> LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type])
186 -- Like tcHsSigTypeNC, but for an instance head.
187 tcHsInstHead user_ctxt lhs_ty@(L loc hs_ty)
188   = setSrcSpan loc $    -- The "In the type..." context comes from the caller
189     do { inst_ty <- tc_inst_head hs_ty
190        ; kvs     <- zonkTcTypeAndFV inst_ty
191        ; kvs     <- kindGeneralize kvs
192        ; inst_ty <- zonkSigType (mkForAllTys kvs inst_ty)
193        ; checkValidInstance user_ctxt lhs_ty inst_ty }
194
195 tc_inst_head :: HsType Name -> TcM TcType
196 tc_inst_head (HsForAllTy _ hs_tvs hs_ctxt hs_ty)
197   = tcHsTyVarBndrs hs_tvs $ \ tvs ->
198     do { ctxt <- tcHsContext hs_ctxt
199        ; ty   <- tc_lhs_type hs_ty ekConstraint    -- Body for forall has kind Constraint
200        ; return (mkSigmaTy tvs ctxt ty) }
201
202 tc_inst_head hs_ty
203   = tc_hs_type hs_ty ekConstraint
204
205 -----------------
206 tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type], Kind)
207 -- Like tcHsSigTypeNC, but for the ...deriving( C t1 ty2 ) clause
208 -- Returns the C, [ty1, ty2, and the kind of C's *next* argument
209 -- E.g.    class C (a::*) (b::k->k)
210 --         data T a b = ... deriving( C Int )
211 --    returns ([k], C, [k, Int],  k->k)
212 -- Also checks that (C ty1 ty2 arg) :: Constraint
213 -- if arg has a suitable kind
214 tcHsDeriv hs_ty
215   = do { arg_kind <- newMetaKindVar
216        ; ty <- tcCheckHsTypeAndGen hs_ty (mkArrowKind arg_kind constraintKind)
217        ; ty       <- zonkSigType ty
218        ; arg_kind <- zonkSigType arg_kind
219        ; let (tvs, pred) = splitForAllTys ty
220        ; case getClassPredTys_maybe pred of
221            Just (cls, tys) -> return (tvs, cls, tys, arg_kind)
222            Nothing -> failWithTc (ptext (sLit "Illegal deriving item") <+> quotes (ppr hs_ty)) }
223
224 -- Used for 'VECTORISE [SCALAR] instance' declarations
225 --
226 tcHsVectInst :: LHsType Name -> TcM (Class, [Type])
227 tcHsVectInst ty
228   | Just (L _ cls_name, tys) <- splitLHsClassTy_maybe ty
229   = do { (cls, cls_kind) <- tcClass cls_name
230        ; (arg_tys, _res_kind) <- tcInferApps cls_name cls_kind tys
231        ; return (cls, arg_tys) }
232   | otherwise
233   = failWithTc $ ptext (sLit "Malformed instance type")
234 \end{code}
235
236         These functions are used during knot-tying in
237         type and class declarations, when we have to
238         separate kind-checking, desugaring, and validity checking
239
240
241 %************************************************************************
242 %*                                                                      *
243             The main kind checker: no validity checks here
244 %*                                                                      *
245 %************************************************************************
246
247         First a couple of simple wrappers for kcHsType
248
249 \begin{code}
250 tcClassSigType :: LHsType Name -> TcM Type
251 tcClassSigType lhs_ty@(L _ hs_ty)
252   = addTypeCtxt lhs_ty $
253     do { ty <- tcCheckHsTypeAndGen hs_ty liftedTypeKind
254        ; zonkSigType ty }
255
256 tcHsConArgType :: NewOrData ->  LHsType Name -> TcM Type
257 -- Permit a bang, but discard it
258 tcHsConArgType NewType  bty = tcHsLiftedType (getBangType bty)
259   -- Newtypes can't have bangs, but we don't check that
260   -- until checkValidDataCon, so do not want to crash here
261
262 tcHsConArgType DataType bty = tcHsOpenType (getBangType bty)
263   -- Can't allow an unlifted type for newtypes, because we're effectively
264   -- going to remove the constructor while coercing it to a lifted type.
265   -- And newtypes can't be bang'd
266
267 ---------------------------
268 tcHsArgTys :: SDoc -> [LHsType Name] -> [Kind] -> TcM [TcType]
269 tcHsArgTys what tys kinds
270   = sequence [ addTypeCtxt ty $
271                tc_lhs_type ty (expArgKind what kind n)
272              | (ty,kind,n) <- zip3 tys kinds [1..] ]
273
274 tc_hs_arg_tys :: SDoc -> [LHsType Name] -> [Kind] -> TcM [TcType]
275 -- Just like tcHsArgTys but without the addTypeCtxt
276 tc_hs_arg_tys what tys kinds
277   = sequence [ tc_lhs_type ty (expArgKind what kind n)
278              | (ty,kind,n) <- zip3 tys kinds [1..] ]
279
280 ---------------------------
281 tcHsOpenType, tcHsLiftedType :: LHsType Name -> TcM TcType
282 -- Used for type signatures
283 -- Do not do validity checking
284 tcHsOpenType ty   = addTypeCtxt ty $ tc_lhs_type ty ekOpen
285 tcHsLiftedType ty = addTypeCtxt ty $ tc_lhs_type ty ekLifted
286
287 -- Like tcHsType, but takes an expected kind
288 tcCheckLHsType :: LHsType Name -> Kind -> TcM Type
289 tcCheckLHsType hs_ty exp_kind
290   = addTypeCtxt hs_ty $
291     tc_lhs_type hs_ty (EK exp_kind expectedKindMsg)
292
293 tcLHsType :: LHsType Name -> TcM (TcType, TcKind)
294 -- Called from outside: set the context
295 tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type ty)
296
297 ---------------------------
298 tcCheckHsTypeAndGen :: HsType Name -> Kind -> TcM Type
299 -- Input type is HsType, not LhsType; the caller adds the context
300 -- Typecheck a type signature, and kind-generalise it
301 -- The result is not necessarily zonked, and has not been checked for validity
302 tcCheckHsTypeAndGen hs_ty kind
303   = do { ty  <- tc_hs_type hs_ty (EK kind expectedKindMsg)
304        ; traceTc "tcCheckHsTypeAndGen" (ppr hs_ty)
305        ; kvs <- zonkTcTypeAndFV ty
306        ; kvs <- kindGeneralize kvs
307        ; return (mkForAllTys kvs ty) }
308 \end{code}
309
310 Like tcExpr, tc_hs_type takes an expected kind which it unifies with
311 the kind it figures out. When we don't know what kind to expect, we use
312 tc_lhs_type_fresh, to first create a new meta kind variable and use that as
313 the expected kind.
314
315 \begin{code}
316 tc_infer_lhs_type :: LHsType Name -> TcM (TcType, TcKind)
317 tc_infer_lhs_type ty =
318   do { kv <- newMetaKindVar
319      ; r <- tc_lhs_type ty (EK kv expectedKindMsg)
320      ; return (r, kv) }
321
322 tc_lhs_type :: LHsType Name -> ExpKind -> TcM TcType
323 tc_lhs_type (L span ty) exp_kind
324   = setSrcSpan span $
325     do { traceTc "tc_lhs_type:" (ppr ty $$ ppr exp_kind)
326        ; tc_hs_type ty exp_kind }
327
328 tc_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [TcType]
329 tc_lhs_types tys_w_kinds = mapM (uncurry tc_lhs_type) tys_w_kinds
330
331 ------------------------------------------
332 tc_fun_type :: HsType Name -> LHsType Name -> LHsType Name -> ExpKind -> TcM TcType
333 -- We need to recognise (->) so that we can construct a FunTy,
334 -- *and* we need to do by looking at the Name, not the TyCon
335 -- (see Note [Zonking inside the knot]).  For example,
336 -- consider  f :: (->) Int Int  (Trac #7312)
337 tc_fun_type ty ty1 ty2 exp_kind@(EK _ ctxt)
338   = do { ty1' <- tc_lhs_type ty1 (EK openTypeKind ctxt)
339        ; ty2' <- tc_lhs_type ty2 (EK openTypeKind ctxt)
340        ; checkExpectedKind ty liftedTypeKind exp_kind
341        ; return (mkFunTy ty1' ty2') }
342
343 ------------------------------------------
344 tc_hs_type :: HsType Name -> ExpKind -> TcM TcType
345 tc_hs_type (HsParTy ty)        exp_kind = tc_lhs_type ty exp_kind
346 tc_hs_type (HsDocTy ty _)      exp_kind = tc_lhs_type ty exp_kind
347 tc_hs_type (HsQuasiQuoteTy {}) _ = panic "tc_hs_type: qq"       -- Eliminated by renamer
348 tc_hs_type ty@(HsBangTy {})    _
349     -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
350     -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
351     -- bangs are invalid, so fail. (#7210)
352     = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
353 tc_hs_type (HsRecTy _)         _ = panic "tc_hs_type: record" -- Unwrapped by con decls
354       -- Record types (which only show up temporarily in constructor
355       -- signatures) should have been removed by now
356
357 ---------- Functions and applications
358 tc_hs_type hs_ty@(HsTyVar name) exp_kind
359   = do { (ty, k) <- tcTyVar name
360        ; checkExpectedKind hs_ty k exp_kind
361        ; return ty }
362
363 tc_hs_type ty@(HsFunTy ty1 ty2) exp_kind
364   = tc_fun_type ty ty1 ty2 exp_kind
365
366 tc_hs_type hs_ty@(HsOpTy ty1 (_, l_op@(L _ op)) ty2) exp_kind
367   | op `hasKey` funTyConKey
368   = tc_fun_type hs_ty ty1 ty2 exp_kind
369   | otherwise
370   = do { (op', op_kind) <- tcTyVar op
371        ; tys' <- tcCheckApps hs_ty l_op op_kind [ty1,ty2] exp_kind
372        ; return (mkNakedAppTys op' tys') }
373          -- mkNakedAppTys: see Note [Zonking inside the knot]
374
375 tc_hs_type hs_ty@(HsAppTy ty1 ty2) exp_kind
376 --  | L _ (HsTyVar fun) <- fun_ty
377 --  , fun `hasKey` funTyConKey
378 --  , [fty1,fty2] <- arg_tys
379 --  = tc_fun_type hs_ty fty1 fty2 exp_kind
380 --  | otherwise
381   = do { (fun_ty', fun_kind) <- tc_infer_lhs_type fun_ty
382        ; arg_tys' <- tcCheckApps hs_ty fun_ty fun_kind arg_tys exp_kind
383        ; return (mkNakedAppTys fun_ty' arg_tys') }
384          -- mkNakedAppTys: see Note [Zonking inside the knot]
385          -- This looks fragile; how do we *know* that fun_ty isn't
386          -- a TyConApp, say (which is never supposed to appear in the
387          -- function position of an AppTy)?
388   where
389     (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
390
391 --------- Foralls
392 tc_hs_type hs_ty@(HsForAllTy _ hs_tvs context ty) exp_kind@(EK exp_k _)
393   | isConstraintKind exp_k
394   = failWithTc (hang (ptext (sLit "Illegal constraint:")) 2 (ppr hs_ty))
395
396   | otherwise
397   = tcHsTyVarBndrs hs_tvs $ \ tvs' ->
398     -- Do not kind-generalise here!  See Note [Kind generalisation]
399     do { ctxt' <- tcHsContext context
400        ; ty' <- if null (unLoc context) then  -- Plain forall, no context
401                    tc_lhs_type ty exp_kind    -- Why exp_kind?  See Note [Body kind of forall]
402                 else
403                    -- If there is a context, then this forall is really a
404                    -- _function_, so the kind of the result really is *
405                    -- The body kind (result of the function can be * or #, hence ekOpen
406                    do { checkExpectedKind hs_ty liftedTypeKind exp_kind
407                       ; tc_lhs_type ty ekOpen }
408        ; return (mkSigmaTy tvs' ctxt' ty') }
409
410 --------- Lists, arrays, and tuples
411 tc_hs_type hs_ty@(HsListTy elt_ty) exp_kind
412   = do { tau_ty <- tc_lhs_type elt_ty ekLifted
413        ; checkExpectedKind hs_ty liftedTypeKind exp_kind
414        ; checkWiredInTyCon listTyCon
415        ; return (mkListTy tau_ty) }
416
417 tc_hs_type hs_ty@(HsPArrTy elt_ty) exp_kind
418   = do { tau_ty <- tc_lhs_type elt_ty ekLifted
419        ; checkExpectedKind hs_ty liftedTypeKind exp_kind
420        ; checkWiredInTyCon parrTyCon
421        ; return (mkPArrTy tau_ty) }
422
423 -- See Note [Distinguishing tuple kinds] in HsTypes
424 -- See Note [Inferring tuple kinds]
425 tc_hs_type hs_ty@(HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind@(EK exp_k _ctxt)
426      -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
427   | Just tup_sort <- tupKindSort_maybe exp_k
428   = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
429     tc_tuple hs_ty tup_sort hs_tys exp_kind
430   | otherwise
431   = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys) 
432        ; (tys, kinds) <- mapAndUnzipM tc_infer_lhs_type hs_tys
433        ; kinds <- mapM zonkTcKind kinds
434            -- Infer each arg type separately, because errors can be
435            -- confusing if we give them a shared kind.  Eg Trac #7410
436            -- (Either Int, Int), we do not want to get an error saying
437            -- "the second argument of a tuple should have kind *->*"
438
439        ; let (arg_kind, tup_sort)
440                = case [ (k,s) | k <- kinds
441                               , Just s <- [tupKindSort_maybe k] ] of
442                     ((k,s) : _) -> (k,s)
443                     [] -> (liftedTypeKind, BoxedTuple)
444          -- In the [] case, it's not clear what the kind is, so guess *
445
446        ; sequence_ [ setSrcSpan loc $
447                      checkExpectedKind ty kind
448                         (expArgKind (ptext (sLit "a tuple")) arg_kind n)
449                    | (ty@(L loc _),kind,n) <- zip3 hs_tys kinds [1..] ]
450
451        ; finish_tuple hs_ty tup_sort tys exp_kind }
452
453
454 tc_hs_type hs_ty@(HsTupleTy hs_tup_sort tys) exp_kind
455   = tc_tuple hs_ty tup_sort tys exp_kind
456   where
457     tup_sort = case hs_tup_sort of  -- Fourth case dealt with above
458                   HsUnboxedTuple    -> UnboxedTuple
459                   HsBoxedTuple      -> BoxedTuple
460                   HsConstraintTuple -> ConstraintTuple
461                   _                 -> panic "tc_hs_type HsTupleTy"
462
463
464 --------- Promoted lists and tuples
465 tc_hs_type hs_ty@(HsExplicitListTy _k tys) exp_kind
466   = do { tks <- mapM tc_infer_lhs_type tys
467        ; let taus = map fst tks
468        ; kind <- unifyKinds (ptext (sLit "In a promoted list")) tks
469        ; checkExpectedKind hs_ty (mkPromotedListTy kind) exp_kind
470        ; return (foldr (mk_cons kind) (mk_nil kind) taus) }
471   where
472     mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
473     mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
474
475 tc_hs_type hs_ty@(HsExplicitTupleTy _ tys) exp_kind
476   = do { tks <- mapM tc_infer_lhs_type tys
477        ; let n          = length tys
478              kind_con   = promotedTupleTyCon   BoxedTuple n
479              ty_con     = promotedTupleDataCon BoxedTuple n
480              (taus, ks) = unzip tks
481              tup_k      = mkTyConApp kind_con ks
482        ; checkExpectedKind hs_ty tup_k exp_kind
483        ; return (mkTyConApp ty_con (ks ++ taus)) }
484
485 --------- Constraint types
486 tc_hs_type ipTy@(HsIParamTy n ty) exp_kind
487   = do { ty' <- tc_lhs_type ty ekLifted
488        ; checkExpectedKind ipTy constraintKind exp_kind
489        ; ipClass <- tcLookupClass ipClassName
490        ; let n' = mkStrLitTy $ hsIPNameFS n
491        ; return (mkClassPred ipClass [n',ty'])
492        }
493
494 tc_hs_type ty@(HsEqTy ty1 ty2) exp_kind
495   = do { (ty1', kind1) <- tc_infer_lhs_type ty1
496        ; (ty2', kind2) <- tc_infer_lhs_type ty2
497        ; checkExpectedKind ty2 kind2
498               (EK kind1 msg_fn)
499        ; checkExpectedKind ty constraintKind exp_kind
500        ; return (mkNakedTyConApp eqTyCon [kind1, ty1', ty2']) }
501   where
502     msg_fn pkind = ptext (sLit "The left argument of the equality had kind")
503                    <+> quotes (pprKind pkind)
504
505 --------- Misc
506 tc_hs_type (HsKindSig ty sig_k) exp_kind
507   = do { sig_k' <- tcLHsKind sig_k
508        ; checkExpectedKind ty sig_k' exp_kind
509        ; tc_lhs_type ty (EK sig_k' msg_fn) }
510   where
511     msg_fn pkind = ptext (sLit "The signature specified kind")
512                    <+> quotes (pprKind pkind)
513
514 tc_hs_type (HsCoreTy ty) exp_kind
515   = do { checkExpectedKind ty (typeKind ty) exp_kind
516        ; return ty }
517
518
519 -- This should never happen; type splices are expanded by the renamer
520 tc_hs_type ty@(HsSpliceTy {}) _exp_kind
521   = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
522
523 tc_hs_type (HsWrapTy {}) _exp_kind
524   = panic "tc_hs_type HsWrapTy"  -- We kind checked something twice
525
526 tc_hs_type hs_ty@(HsTyLit (HsNumTy n)) exp_kind
527   = do { checkExpectedKind hs_ty typeNatKind exp_kind
528        ; checkWiredInTyCon typeNatKindCon
529        ; return (mkNumLitTy n) }
530
531 tc_hs_type hs_ty@(HsTyLit (HsStrTy s)) exp_kind
532   = do { checkExpectedKind hs_ty typeSymbolKind exp_kind
533        ; checkWiredInTyCon typeSymbolKindCon
534        ; return (mkStrLitTy s) }
535
536 ---------------------------
537 tupKindSort_maybe :: TcKind -> Maybe TupleSort
538 tupKindSort_maybe k
539   | isConstraintKind k = Just ConstraintTuple
540   | isLiftedTypeKind k = Just BoxedTuple
541   | otherwise          = Nothing
542
543 tc_tuple :: HsType Name -> TupleSort -> [LHsType Name] -> ExpKind -> TcM TcType
544 tc_tuple hs_ty tup_sort tys exp_kind
545   = do { tau_tys <- tc_hs_arg_tys cxt_doc tys (repeat arg_kind)
546        ; finish_tuple hs_ty tup_sort tau_tys exp_kind }
547   where
548     arg_kind = case tup_sort of
549                  BoxedTuple      -> liftedTypeKind
550                  UnboxedTuple    -> openTypeKind
551                  ConstraintTuple -> constraintKind
552     cxt_doc = case tup_sort of
553                  BoxedTuple      -> ptext (sLit "a tuple")
554                  UnboxedTuple    -> ptext (sLit "an unboxed tuple")
555                  ConstraintTuple -> ptext (sLit "a constraint tuple")
556
557 finish_tuple :: HsType Name -> TupleSort -> [TcType] -> ExpKind -> TcM TcType
558 finish_tuple hs_ty tup_sort tau_tys exp_kind
559   = do { traceTc "finish_tuple" (ppr res_kind $$ ppr exp_kind $$ ppr exp_kind)
560        ; checkExpectedKind hs_ty res_kind exp_kind
561        ; checkWiredInTyCon tycon
562        ; return (mkTyConApp tycon tau_tys) }
563   where
564     tycon = tupleTyCon tup_sort (length tau_tys)
565     res_kind = case tup_sort of
566                  UnboxedTuple    -> unliftedTypeKind
567                  BoxedTuple      -> liftedTypeKind
568                  ConstraintTuple -> constraintKind
569
570 ---------------------------
571 tcInferApps :: Outputable a
572        => a
573        -> TcKind                        -- Function kind
574        -> [LHsType Name]                -- Arg types
575        -> TcM ([TcType], TcKind)        -- Kind-checked args
576 tcInferApps the_fun fun_kind args
577   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) fun_kind args
578        ; args' <- tc_lhs_types args_w_kinds
579        ; return (args', res_kind) }
580
581 tcCheckApps :: Outputable a
582             => HsType Name     -- The type being checked (for err messages only)
583             -> a               -- The function
584             -> TcKind -> [LHsType Name]   -- Fun kind and arg types
585             -> ExpKind                    -- Expected kind
586             -> TcM [TcType]
587 tcCheckApps hs_ty the_fun fun_kind args exp_kind
588   = do { (arg_tys, res_kind) <- tcInferApps the_fun fun_kind args
589        ; checkExpectedKind hs_ty res_kind exp_kind
590        ; return arg_tys }
591
592 ---------------------------
593 splitFunKind :: SDoc -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
594 splitFunKind the_fun fun_kind args
595   = go 1 fun_kind args
596   where
597     go _      fk [] = return ([], fk)
598     go arg_no fk (arg:args)
599        = do { mb_fk <- matchExpectedFunKind fk
600             ; case mb_fk of
601                  Nothing       -> failWithTc too_many_args
602                  Just (ak,fk') -> do { (aks, rk) <- go (arg_no+1) fk' args
603                                      ; let exp_kind = expArgKind (quotes the_fun) ak arg_no
604                                      ; return ((arg, exp_kind) : aks, rk) } }
605
606     too_many_args = quotes the_fun <+>
607                     ptext (sLit "is applied to too many type arguments")
608
609
610 ---------------------------
611 tcHsContext :: LHsContext Name -> TcM [PredType]
612 tcHsContext ctxt = mapM tcHsLPredType (unLoc ctxt)
613
614 tcHsLPredType :: LHsType Name -> TcM PredType
615 tcHsLPredType pred = tc_lhs_type pred ekConstraint
616
617 ---------------------------
618 tcTyVar :: Name -> TcM (TcType, TcKind)
619 -- See Note [Type checking recursive type and class declarations]
620 -- in TcTyClsDecls
621 tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
622   = do { traceTc "lk1" (ppr name)
623        ; thing <- tcLookup name
624        ; case thing of
625            ATyVar _ tv
626               | isKindVar tv
627               -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr tv)
628                              <+> ptext (sLit "used as a type"))
629               | otherwise
630               -> return (mkTyVarTy tv, tyVarKind tv)
631
632            AThing kind -> do { tc <- get_loopy_tc name
633                              ; inst_tycon (mkNakedTyConApp tc) kind }
634                              -- mkNakedTyConApp: see Note [Zonking inside the knot]
635
636            AGlobal (ATyCon tc) -> inst_tycon (mkTyConApp tc) (tyConKind tc)
637
638            AGlobal (AConLike (RealDataCon dc))
639              | Just tc <- promoteDataCon_maybe dc
640              -> do { data_kinds <- xoptM Opt_DataKinds
641                    ; unless data_kinds $ promotionErr name NoDataKinds
642                    ; inst_tycon (mkTyConApp tc) (tyConKind tc) }
643              | otherwise -> failWithTc (ptext (sLit "Data constructor") <+> quotes (ppr dc)
644                                         <+> ptext (sLit "comes from an un-promotable type")
645                                         <+> quotes (ppr (dataConTyCon dc)))
646
647            APromotionErr err -> promotionErr name err
648
649            _  -> wrongThingErr "type" thing name }
650   where
651     get_loopy_tc name
652       = do { env <- getGblEnv
653            ; case lookupNameEnv (tcg_type_env env) name of
654                 Just (ATyCon tc) -> return tc
655                 _                -> return (aThingErr "tcTyVar" name) }
656
657     inst_tycon :: ([Type] -> Type) -> Kind -> TcM (Type, Kind)
658     -- Instantiate the polymorphic kind
659     -- Lazy in the TyCon
660     inst_tycon mk_tc_app kind
661       | null kvs
662       = return (mk_tc_app [], ki_body)
663       | otherwise
664       = do { traceTc "lk4" (ppr name <+> dcolon <+> ppr kind)
665            ; ks <- mapM (const newMetaKindVar) kvs
666            ; return (mk_tc_app ks, substKiWith kvs ks ki_body) }
667       where
668         (kvs, ki_body) = splitForAllTys kind
669
670 tcClass :: Name -> TcM (Class, TcKind)
671 tcClass cls     -- Must be a class
672   = do { thing <- tcLookup cls
673        ; case thing of
674            AThing kind -> return (aThingErr "tcClass" cls, kind)
675            AGlobal (ATyCon tc)
676              | Just cls <- tyConClass_maybe tc
677              -> return (cls, tyConKind tc)
678            _ -> wrongThingErr "class" thing cls }
679
680
681 aThingErr :: String -> Name -> b
682 -- The type checker for types is sometimes called simply to
683 -- do *kind* checking; and in that case it ignores the type
684 -- returned. Which is a good thing since it may not be available yet!
685 aThingErr str x = pprPanic "AThing evaluated unexpectedly" (text str <+> ppr x)
686 \end{code}
687
688 Note [Zonking inside the knot]
689 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
690 Suppose we are checking the argument types of a data constructor.  We
691 must zonk the types before making the DataCon, because once built we
692 can't change it.  So we must traverse the type.
693
694 BUT the parent TyCon is knot-tied, so we can't look at it yet.
695
696 So we must be careful not to use "smart constructors" for types that
697 look at the TyCon or Class involved.
698
699   * Hence the use of mkNakedXXX functions. These do *not* enforce
700     the invariants (for example that we use (FunTy s t) rather
701     than (TyConApp (->) [s,t])).
702
703   * Ditto in zonkTcType (which may be applied more than once, eg to
704     squeeze out kind meta-variables), we are careful not to look at
705     the TyCon.
706
707   * We arrange to call zonkSigType *once* right at the end, and it
708     does establish the invariants.  But in exchange we can't look
709     at the result (not even its structure) until we have emerged
710     from the "knot".
711
712   * TcHsSyn.zonkTcTypeToType also can safely check/establish
713     invariants.
714
715 This is horribly delicate.  I hate it.  A good example of how
716 delicate it is can be seen in Trac #7903.
717
718 \begin{code}
719 mkNakedTyConApp :: TyCon -> [Type] -> Type
720 -- Builds a TyConApp
721 --   * without being strict in TyCon,
722 --   * without satisfying the invariants of TyConApp
723 -- A subsequent zonking will establish the invariants
724 mkNakedTyConApp tc tys = TyConApp tc tys
725
726 mkNakedAppTys :: Type -> [Type] -> Type
727 mkNakedAppTys ty1                []   = ty1
728 mkNakedAppTys (TyConApp tc tys1) tys2 = mkNakedTyConApp tc (tys1 ++ tys2)
729 mkNakedAppTys ty1                tys2 = foldl AppTy ty1 tys2
730
731 zonkSigType :: TcType -> TcM TcType
732 -- Zonk the result of type-checking a user-written type signature
733 -- It may have kind variables in it, but no meta type variables
734 -- Because of knot-typing (see Note [Zonking inside the knot])
735 -- it may need to establish the Type invariants;
736 -- hence the use of mkTyConApp and mkAppTy
737 zonkSigType ty
738   = go ty
739   where
740     go (TyConApp tc tys) = do tys' <- mapM go tys
741                               return (mkTyConApp tc tys')
742                 -- Key point: establish Type invariants!
743                 -- See Note [Zonking inside the knot]
744
745     go (LitTy n)         = return (LitTy n)
746
747     go (FunTy arg res)   = do arg' <- go arg
748                               res' <- go res
749                               return (FunTy arg' res')
750
751     go (AppTy fun arg)   = do fun' <- go fun
752                               arg' <- go arg
753                               return (mkAppTy fun' arg')
754                 -- NB the mkAppTy; we might have instantiated a
755                 -- type variable to a type constructor, so we need
756                 -- to pull the TyConApp to the top.
757
758         -- The two interesting cases!
759     go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
760                        | otherwise       = TyVarTy <$> updateTyVarKindM go tyvar
761                 -- Ordinary (non Tc) tyvars occur inside quantified types
762
763     go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
764                              ; ty' <- go ty
765                              ; return (ForAllTy tv' ty') }
766 \end{code}
767
768 Note [Body kind of a forall]
769 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
770 The body of a forall is usually a type, but in principle
771 there's no reason to prohibit *unlifted* types.
772 In fact, GHC can itself construct a function with an
773 unboxed tuple inside a for-all (via CPR analyis; see
774 typecheck/should_compile/tc170).
775
776 Moreover in instance heads we get forall-types with
777 kind Constraint.
778
779 Moreover if we have a signature
780    f :: Int#
781 then we represent it as (HsForAll Implicit [] [] Int#).  And this must
782 be legal!  We can't drop the empty forall until *after* typechecking
783 the body because of kind polymorphism:
784    Typeable :: forall k. k -> Constraint
785    data Apply f t = Apply (f t)
786    -- Apply :: forall k. (k -> *) -> k -> *
787    instance Typeable Apply where ...
788 Then the dfun has type
789    df :: forall k. Typeable ((k->*) -> k -> *) (Apply k)
790
791    f :: Typeable Apply
792
793    f :: forall (t:k->*) (a:k).  t a -> t a
794
795    class C a b where
796       op :: a b -> Typeable Apply
797
798    data T a = MkT (Typeable Apply)
799             | T2 a
800       T :: * -> *
801       MkT :: forall k. (Typeable ((k->*) -> k -> *) (Apply k)) -> T a
802
803    f :: (forall (k:BOX). forall (t:: k->*) (a:k). t a -> t a) -> Int
804    f :: (forall a. a -> Typeable Apply) -> Int
805
806 So we *must* keep the HsForAll on the instance type
807    HsForAll Implicit [] [] (Typeable Apply)
808 so that we do kind generalisation on it.
809
810 Really we should check that it's a type of value kind
811 {*, Constraint, #}, but I'm not doing that yet
812 Example that should be rejected:
813          f :: (forall (a:*->*). a) Int
814
815 Note [Inferring tuple kinds]
816 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
817 Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
818 we try to figure out whether it's a tuple of kind * or Constraint.
819   Step 1: look at the expected kind
820   Step 2: infer argument kinds
821
822 If after Step 2 it's not clear from the arguments that it's
823 Constraint, then it must be *.  Once having decided that we re-check
824 the Check the arguments again to give good error messages
825 in eg. `(Maybe, Maybe)`
826
827 Note that we will still fail to infer the correct kind in this case:
828
829   type T a = ((a,a), D a)
830   type family D :: Constraint -> Constraint
831
832 While kind checking T, we do not yet know the kind of D, so we will default the
833 kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
834
835 Note [Desugaring types]
836 ~~~~~~~~~~~~~~~~~~~~~~~
837 The type desugarer is phase 2 of dealing with HsTypes.  Specifically:
838
839   * It transforms from HsType to Type
840
841   * It zonks any kinds.  The returned type should have no mutable kind
842     or type variables (hence returning Type not TcType):
843       - any unconstrained kind variables are defaulted to AnyK just
844         as in TcHsSyn.
845       - there are no mutable type variables because we are
846         kind-checking a type
847     Reason: the returned type may be put in a TyCon or DataCon where
848     it will never subsequently be zonked.
849
850 You might worry about nested scopes:
851         ..a:kappa in scope..
852             let f :: forall b. T '[a,b] -> Int
853 In this case, f's type could have a mutable kind variable kappa in it;
854 and we might then default it to AnyK when dealing with f's type
855 signature.  But we don't expect this to happen because we can't get a
856 lexically scoped type variable with a mutable kind variable in it.  A
857 delicate point, this.  If it becomes an issue we might need to
858 distinguish top-level from nested uses.
859
860 Moreover
861   * it cannot fail,
862   * it does no unifications
863   * it does no validity checking, except for structural matters, such as
864         (a) spurious ! annotations.
865         (b) a class used as a type
866
867 Note [Kind of a type splice]
868 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
869 Consider these terms, each with TH type splice inside:
870      [| e1 :: Maybe $(..blah..) |]
871      [| e2 :: $(..blah..) |]
872 When kind-checking the type signature, we'll kind-check the splice
873 $(..blah..); we want to give it a kind that can fit in any context,
874 as if $(..blah..) :: forall k. k.
875
876 In the e1 example, the context of the splice fixes kappa to *.  But
877 in the e2 example, we'll desugar the type, zonking the kind unification
878 variables as we go.  When we encounter the unconstrained kappa, we
879 want to default it to '*', not to AnyK.
880
881
882 Help functions for type applications
883 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
884
885 \begin{code}
886 addTypeCtxt :: LHsType Name -> TcM a -> TcM a
887         -- Wrap a context around only if we want to show that contexts.
888         -- Omit invisble ones and ones user's won't grok
889 addTypeCtxt (L _ ty) thing
890   = addErrCtxt doc thing
891   where
892     doc = ptext (sLit "In the type") <+> quotes (ppr ty)
893 \end{code}
894
895 %************************************************************************
896 %*                                                                      *
897                 Type-variable binders
898 %*                                                                      *
899 %************************************************************************
900
901 \begin{code}
902
903 mkKindSigVar :: Name -> TcM KindVar
904 -- Use the specified name; don't clone it
905 mkKindSigVar n
906   = do { mb_thing <- tcLookupLcl_maybe n
907        ; case mb_thing of
908            Just (AThing k)
909              | Just kvar <- getTyVar_maybe k
910              -> return kvar
911            _ -> return $ mkTcTyVar n superKind (SkolemTv False) }
912
913 kcScopedKindVars :: [Name] -> TcM a -> TcM a
914 -- Given some tyvar binders like [a (b :: k -> *) (c :: k)]
915 -- bind each scoped kind variable (k in this case) to a fresh
916 -- kind skolem variable
917 kcScopedKindVars kv_ns thing_inside
918   = do { kvs <- mapM (\n -> newSigTyVar n superKind) kv_ns
919                      -- NB: use mutable signature variables
920        ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) thing_inside }
921
922 -- | Kind-check a 'LHsTyVarBndrs'. If the decl under consideration has a complete,
923 -- user-supplied kind signature (CUSK), generalise the result. Used in 'getInitialKind'
924 -- and in kind-checking. See also Note [Complete user-supplied kind signatures] in
925 -- HsDecls.
926 kcHsTyVarBndrs :: Bool    -- ^ True <=> the decl being checked has a CUSK
927                -> LHsTyVarBndrs Name
928                -> TcM (Kind, r)   -- ^ the result kind, possibly with other info
929                -> TcM (Kind, r)   -- ^ The full kind of the thing being declared,
930                                   -- with the other info
931 kcHsTyVarBndrs cusk (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
932   = do { kvs <- if cusk
933                 then mapM mkKindSigVar kv_ns
934                 else mapM (\n -> newSigTyVar n superKind) kv_ns
935        ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $
936     do { nks <- mapM (kc_hs_tv . unLoc) hs_tvs
937        ; (res_kind, stuff) <- tcExtendKindEnv nks thing_inside
938        ; let full_kind = mkArrowKinds (map snd nks) res_kind
939              kvs       = filter (not . isMetaTyVar) $
940                          varSetElems $ tyVarsOfType full_kind
941              gen_kind  = if cusk
942                          then mkForAllTys kvs full_kind
943                          else full_kind
944        ; return (gen_kind, stuff) } }
945   where
946     kc_hs_tv :: HsTyVarBndr Name -> TcM (Name, TcKind)
947     kc_hs_tv (UserTyVar n)
948       = do { mb_thing <- tcLookupLcl_maybe n
949            ; kind <- case mb_thing of
950                        Just (AThing k) -> return k
951                        _ | cusk        -> return liftedTypeKind
952                          | otherwise   -> newMetaKindVar
953            ; return (n, kind) }
954     kc_hs_tv (KindedTyVar n k)
955       = do { kind <- tcLHsKind k
956                -- In an associated type decl, the type variable may already
957                -- be in scope; in that case we want to make sure its kind
958                -- matches the one declared here
959            ; mb_thing <- tcLookupLcl_maybe n
960            ; case mb_thing of
961                Nothing          -> return ()
962                Just (AThing ks) -> checkKind kind ks
963                Just thing       -> pprPanic "check_in_scope" (ppr thing)
964            ; return (n, kind) }
965
966 tcHsTyVarBndrs :: LHsTyVarBndrs Name
967                -> ([TcTyVar] -> TcM r)
968                -> TcM r
969 -- Bind the kind variables to fresh skolem variables
970 -- and type variables to skolems, each with a meta-kind variable kind
971 tcHsTyVarBndrs (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
972   = do { kvs <- mapM mkKindSigVar kv_ns
973        ; tcExtendTyVarEnv kvs $ do
974        { tvs <- mapM tcHsTyVarBndr hs_tvs
975        ; traceTc "tcHsTyVarBndrs {" (vcat [ text "Hs kind vars:" <+> ppr kv_ns
976                                         , text "Hs type vars:" <+> ppr hs_tvs
977                                         , text "Kind vars:" <+> ppr kvs
978                                         , text "Type vars:" <+> ppr tvs ])
979        ; res <- tcExtendTyVarEnv tvs (thing_inside (kvs ++ tvs))
980        ; traceTc "tcHsTyVarBndrs }" (vcat [ text "Hs kind vars:" <+> ppr kv_ns
981                                         , text "Hs type vars:" <+> ppr hs_tvs
982                                         , text "Kind vars:" <+> ppr kvs
983                                         , text "Type vars:" <+> ppr tvs ])
984        ; return res  } }
985
986 tcHsTyVarBndr :: LHsTyVarBndr Name -> TcM TcTyVar
987 -- Return a type variable
988 -- initialised with a kind variable.
989 -- Typically the Kind inside the HsTyVarBndr will be a tyvar with a mutable kind
990 -- in it.
991 --
992 -- If the variable is already in scope return it, instead of introducing a new
993 -- one. This can occur in
994 --   instance C (a,b) where
995 --     type F (a,b) c = ...
996 -- Here a,b will be in scope when processing the associated type instance for F.
997 -- See Note [Associated type tyvar names] in Class
998 tcHsTyVarBndr (L _ hs_tv)
999   = do { let name = hsTyVarName hs_tv
1000        ; mb_tv <- tcLookupLcl_maybe name
1001        ; case mb_tv of {
1002            Just (ATyVar _ tv) -> return tv ;
1003            _ -> do
1004        { kind <- case hs_tv of
1005                    UserTyVar {}       -> newMetaKindVar
1006                    KindedTyVar _ kind -> tcLHsKind kind
1007        ; return ( mkTcTyVar name kind (SkolemTv False)) } } }
1008
1009 ------------------
1010 kindGeneralize :: TyVarSet -> TcM [KindVar]
1011 kindGeneralize tkvs
1012   = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
1013        ; quantifyTyVars gbl_tvs (filterVarSet isKindVar tkvs) }
1014                 -- ToDo: remove the (filter isKindVar)
1015                 -- Any type variables in tkvs will be in scope,
1016                 -- and hence in gbl_tvs, so after removing gbl_tvs
1017                 -- we should only have kind variables left
1018                 --
1019                 -- BUT there is a smelly case (to be fixed when TH is reorganised)
1020                 --     f t = [| e :: $t |]
1021                 -- When typechecking the body of the bracket, we typecheck $t to a
1022                 -- unification variable 'alpha', with no biding forall.  We don't
1023                 -- want to kind-quantify it!
1024 \end{code}
1025
1026 Note [Kind generalisation]
1027 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1028 We do kind generalisation only at the outer level of a type signature.
1029 For example, consider
1030   T :: forall k. k -> *
1031   f :: (forall a. T a -> Int) -> Int
1032 When kind-checking f's type signature we generalise the kind at
1033 the outermost level, thus:
1034   f1 :: forall k. (forall (a:k). T k a -> Int) -> Int  -- YES!
1035 and *not* at the inner forall:
1036   f2 :: (forall k. forall (a:k). T k a -> Int) -> Int  -- NO!
1037 Reason: same as for HM inference on value level declarations,
1038 we want to infer the most general type.  The f2 type signature
1039 would be *less applicable* than f1, because it requires a more
1040 polymorphic argument.
1041
1042 Note [Kinds of quantified type variables]
1043 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1044 tcTyVarBndrsGen quantifies over a specified list of type variables,
1045 *and* over the kind variables mentioned in the kinds of those tyvars.
1046
1047 Note that we must zonk those kinds (obviously) but less obviously, we
1048 must return type variables whose kinds are zonked too. Example
1049     (a :: k7)  where  k7 := k9 -> k9
1050 We must return
1051     [k9, a:k9->k9]
1052 and NOT
1053     [k9, a:k7]
1054 Reason: we're going to turn this into a for-all type,
1055    forall k9. forall (a:k7). blah
1056 which the type checker will then instantiate, and instantiate does not
1057 look through unification variables!
1058
1059 Hence using zonked_kinds when forming tvs'.
1060
1061 \begin{code}
1062 --------------------
1063 -- getInitialKind has made a suitably-shaped kind for the type or class
1064 -- Unpack it, and attribute those kinds to the type variables
1065 -- Extend the env with bindings for the tyvars, taken from
1066 -- the kind of the tycon/class.  Give it to the thing inside, and
1067 -- check the result kind matches
1068 kcLookupKind :: Name -> TcM Kind
1069 kcLookupKind nm
1070   = do { tc_ty_thing <- tcLookup nm
1071        ; case tc_ty_thing of
1072            AThing k            -> return k
1073            AGlobal (ATyCon tc) -> return (tyConKind tc)
1074            _                   -> pprPanic "kcLookupKind" (ppr tc_ty_thing) }
1075
1076 kcTyClTyVars :: Name -> LHsTyVarBndrs Name -> TcM a -> TcM a
1077 -- Used for the type variables of a type or class decl,
1078 -- when doing the initial kind-check.
1079 kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
1080   = kcScopedKindVars kvs $
1081     do  { tc_kind <- kcLookupKind name
1082         ; let (_, mono_kind)   = splitForAllTys tc_kind
1083                      -- if we have a FullKindSignature, the tc_kind may already
1084                      -- be generalized. The kvs get matched up while kind-checking
1085                      -- the types in kc_tv, below
1086               (arg_ks, _res_k) = splitKindFunTysN (length hs_tvs) mono_kind
1087                      -- There should be enough arrows, because
1088                      -- getInitialKinds used the tcdTyVars
1089         ; name_ks <- zipWithM kc_tv hs_tvs arg_ks
1090         ; tcExtendKindEnv name_ks thing_inside }
1091   where
1092     -- getInitialKind has already gotten the kinds of these type
1093     -- variables, but tiresomely we need to check them *again*
1094     -- to match the kind variables they mention against the ones
1095     -- we've freshly brought into scope
1096     kc_tv :: LHsTyVarBndr Name -> Kind -> TcM (Name, Kind)
1097     kc_tv (L _ (UserTyVar n)) exp_k
1098       = return (n, exp_k)
1099     kc_tv (L _ (KindedTyVar n hs_k)) exp_k
1100       = do { k <- tcLHsKind hs_k
1101            ; checkKind k exp_k
1102            ; return (n, exp_k) }
1103
1104 -----------------------
1105 tcTyClTyVars :: Name -> LHsTyVarBndrs Name      -- LHS of the type or class decl
1106              -> ([TyVar] -> Kind -> TcM a) -> TcM a
1107 -- Used for the type variables of a type or class decl,
1108 -- on the second pass when constructing the final result
1109 -- (tcTyClTyVars T [a,b] thing_inside)
1110 --   where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
1111 --   calls thing_inside with arguments
1112 --      [k1,k2,a,b] (k2 -> *)
1113 --   having also extended the type environment with bindings
1114 --   for k1,k2,a,b
1115 --
1116 -- No need to freshen the k's because they are just skolem
1117 -- constants here, and we are at top level anyway.
1118 tcTyClTyVars tycon (HsQTvs { hsq_kvs = hs_kvs, hsq_tvs = hs_tvs }) thing_inside
1119   = kcScopedKindVars hs_kvs $ -- Bind scoped kind vars to fresh kind univ vars
1120                               -- There may be fewer of these than the kvs of
1121                               -- the type constructor, of course
1122     do { thing <- tcLookup tycon
1123        ; let { kind = case thing of
1124                         AThing kind -> kind
1125                         _ -> panic "tcTyClTyVars"
1126                      -- We only call tcTyClTyVars during typechecking in
1127                      -- TcTyClDecls, where the local env is extended with
1128                      -- the generalized_env (mapping Names to AThings).
1129              ; (kvs, body)  = splitForAllTys kind
1130              ; (kinds, res) = splitKindFunTysN (length hs_tvs) body }
1131        ; tvs <- zipWithM tc_hs_tv hs_tvs kinds
1132        ; tcExtendTyVarEnv tvs (thing_inside (kvs ++ tvs) res) }
1133   where
1134     -- In the case of associated types, the renamer has
1135     -- ensured that the names are in commmon
1136     -- e.g.   class C a_29 where
1137     --           type T b_30 a_29 :: *
1138     -- Here the a_29 is shared
1139     tc_hs_tv (L _ (UserTyVar n))        kind = return (mkTyVar n kind)
1140     tc_hs_tv (L _ (KindedTyVar n hs_k)) kind = do { tc_kind <- tcLHsKind hs_k
1141                                                   ; checkKind kind tc_kind
1142                                                   ; return (mkTyVar n kind) }
1143
1144 -----------------------------------
1145 tcDataKindSig :: Kind -> TcM [TyVar]
1146 -- GADT decls can have a (perhaps partial) kind signature
1147 --      e.g.  data T :: * -> * -> * where ...
1148 -- This function makes up suitable (kinded) type variables for
1149 -- the argument kinds, and checks that the result kind is indeed *.
1150 -- We use it also to make up argument type variables for for data instances.
1151 tcDataKindSig kind
1152   = do  { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
1153         ; span <- getSrcSpanM
1154         ; us   <- newUniqueSupply
1155         ; rdr_env <- getLocalRdrEnv
1156         ; let uniqs = uniqsFromSupply us
1157               occs  = [ occ | str <- allNameStrings
1158                             , let occ = mkOccName tvName str
1159                             , isNothing (lookupLocalRdrOcc rdr_env occ) ]
1160                  -- Note [Avoid name clashes for associated data types]
1161
1162         ; return [ mk_tv span uniq occ kind
1163                  | ((kind, occ), uniq) <- arg_kinds `zip` occs `zip` uniqs ] }
1164   where
1165     (arg_kinds, res_kind) = splitKindFunTys kind
1166     mk_tv loc uniq occ kind
1167       = mkTyVar (mkInternalName uniq occ loc) kind
1168
1169 badKindSig :: Kind -> SDoc
1170 badKindSig kind
1171  = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
1172         2 (ppr kind)
1173 \end{code}
1174
1175 Note [Avoid name clashes for associated data types]
1176 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1177 Consider    class C a b where
1178                data D b :: * -> *
1179 When typechecking the decl for D, we'll invent an extra type variable
1180 for D, to fill out its kind.  Ideally we don't want this type variable
1181 to be 'a', because when pretty printing we'll get
1182             class C a b where
1183                data D b a0
1184 (NB: the tidying happens in the conversion to IfaceSyn, which happens
1185 as part of pretty-printing a TyThing.)
1186
1187 That's why we look in the LocalRdrEnv to see what's in scope. This is
1188 important only to get nice-looking output when doing ":info C" in GHCi.
1189 It isn't essential for correctness.
1190
1191
1192 %************************************************************************
1193 %*                                                                      *
1194                 Scoped type variables
1195 %*                                                                      *
1196 %************************************************************************
1197
1198
1199 tcAddScopedTyVars is used for scoped type variables added by pattern
1200 type signatures
1201         e.g.  \ ((x::a), (y::a)) -> x+y
1202 They never have explicit kinds (because this is source-code only)
1203 They are mutable (because they can get bound to a more specific type).
1204
1205 Usually we kind-infer and expand type splices, and then
1206 tupecheck/desugar the type.  That doesn't work well for scoped type
1207 variables, because they scope left-right in patterns.  (e.g. in the
1208 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
1209
1210 The current not-very-good plan is to
1211   * find all the types in the patterns
1212   * find their free tyvars
1213   * do kind inference
1214   * bring the kinded type vars into scope
1215   * BUT throw away the kind-checked type
1216         (we'll kind-check it again when we type-check the pattern)
1217
1218 This is bad because throwing away the kind checked type throws away
1219 its splices.  But too bad for now.  [July 03]
1220
1221 Historical note:
1222     We no longer specify that these type variables must be univerally
1223     quantified (lots of email on the subject).  If you want to put that
1224     back in, you need to
1225         a) Do a checkSigTyVars after thing_inside
1226         b) More insidiously, don't pass in expected_ty, else
1227            we unify with it too early and checkSigTyVars barfs
1228            Instead you have to pass in a fresh ty var, and unify
1229            it with expected_ty afterwards
1230
1231 \begin{code}
1232 tcHsPatSigType :: UserTypeCtxt
1233                -> HsWithBndrs Name (LHsType Name) -- The type signature
1234               -> TcM ( Type                       -- The signature
1235                       , [(Name, TcTyVar)] )   -- The new bit of type environment, binding
1236                                               -- the scoped type variables
1237 -- Used for type-checking type signatures in
1238 -- (a) patterns           e.g  f (x::Int) = e
1239 -- (b) result signatures  e.g. g x :: Int = e
1240 -- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x
1241
1242 tcHsPatSigType ctxt (HsWB { hswb_cts = hs_ty, hswb_kvs = sig_kvs, hswb_tvs = sig_tvs })
1243   = addErrCtxt (pprSigCtxt ctxt empty (ppr hs_ty)) $
1244     do  { kvs <- mapM new_kv sig_kvs
1245         ; tvs <- mapM new_tv sig_tvs
1246         ; let ktv_binds = (sig_kvs `zip` kvs) ++ (sig_tvs `zip` tvs)
1247         ; sig_ty <- tcExtendTyVarEnv2 ktv_binds $
1248                     tcHsLiftedType hs_ty
1249         ; sig_ty <- zonkSigType sig_ty
1250         ; checkValidType ctxt sig_ty
1251         ; return (sig_ty, ktv_binds) }
1252   where
1253     new_kv name = new_tkv name superKind
1254     new_tv name = do { kind <- newMetaKindVar
1255                      ; new_tkv name kind }
1256
1257     new_tkv name kind   -- See Note [Pattern signature binders]
1258       = case ctxt of
1259           RuleSigCtxt {} -> return (mkTcTyVar name kind (SkolemTv False))
1260           _              -> newSigTyVar name kind  -- See Note [Unifying SigTvs]
1261
1262 tcPatSig :: Bool                    -- True <=> pattern binding
1263          -> HsWithBndrs Name (LHsType Name)
1264          -> TcSigmaType
1265          -> TcM (TcType,            -- The type to use for "inside" the signature
1266                  [(Name, TcTyVar)], -- The new bit of type environment, binding
1267                                     -- the scoped type variables
1268                  HsWrapper)         -- Coercion due to unification with actual ty
1269                                     -- Of shape:  res_ty ~ sig_ty
1270 tcPatSig in_pat_bind sig res_ty
1271   = do  { (sig_ty, sig_tvs) <- tcHsPatSigType PatSigCtxt sig
1272         -- sig_tvs are the type variables free in 'sig',
1273         -- and not already in scope. These are the ones
1274         -- that should be brought into scope
1275
1276         ; if null sig_tvs then do {
1277                 -- Just do the subsumption check and return
1278                   wrap <- addErrCtxtM (mk_msg sig_ty) $
1279                           tcSubType_NC PatSigCtxt res_ty sig_ty
1280                 ; return (sig_ty, [], wrap)
1281         } else do
1282                 -- Type signature binds at least one scoped type variable
1283
1284                 -- A pattern binding cannot bind scoped type variables
1285                 -- It is more convenient to make the test here
1286                 -- than in the renamer
1287         { when in_pat_bind (addErr (patBindSigErr sig_tvs))
1288
1289                 -- Check that all newly-in-scope tyvars are in fact
1290                 -- constrained by the pattern.  This catches tiresome
1291                 -- cases like
1292                 --      type T a = Int
1293                 --      f :: Int -> Int
1294                 --      f (x :: T a) = ...
1295                 -- Here 'a' doesn't get a binding.  Sigh
1296         ; let bad_tvs = [ tv | (_, tv) <- sig_tvs
1297                              , not (tv `elemVarSet` exactTyVarsOfType sig_ty) ]
1298         ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
1299
1300         -- Now do a subsumption check of the pattern signature against res_ty
1301         ; wrap <- addErrCtxtM (mk_msg sig_ty) $
1302                   tcSubType_NC PatSigCtxt res_ty sig_ty
1303
1304         -- Phew!
1305         ; return (sig_ty, sig_tvs, wrap)
1306         } }
1307   where
1308     mk_msg sig_ty tidy_env
1309        = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
1310             ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
1311             ; let msg = vcat [ hang (ptext (sLit "When checking that the pattern signature:"))
1312                                   4 (ppr sig_ty)
1313                              , nest 2 (hang (ptext (sLit "fits the type of its context:"))
1314                                           2 (ppr res_ty)) ]
1315             ; return (tidy_env, msg) }
1316
1317 patBindSigErr :: [(Name, TcTyVar)] -> SDoc
1318 patBindSigErr sig_tvs
1319   = hang (ptext (sLit "You cannot bind scoped type variable") <> plural sig_tvs
1320           <+> pprQuotedList (map fst sig_tvs))
1321        2 (ptext (sLit "in a pattern binding signature"))
1322 \end{code}
1323
1324 Note [Pattern signature binders]
1325 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1326 Consider
1327    data T = forall a. T a (a->Int)
1328    f (T x (f :: a->Int) = blah)
1329
1330 Here
1331  * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk',
1332    It must be a skolem so that that it retains its identity, and
1333    TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
1334
1335  * The type signature pattern (f :: a->Int) binds "a" -> a_sig in the envt
1336
1337  * Then unificaiton makes a_sig := a_sk
1338
1339 That's why we must make a_sig a MetaTv (albeit a SigTv),
1340 not a SkolemTv, so that it can unify to a_sk.
1341
1342 For RULE binders, though, things are a bit different (yuk).
1343   RULE "foo" forall (x::a) (y::[a]).  f x y = ...
1344 Here this really is the binding site of the type variable so we'd like
1345 to use a skolem, so that we get a complaint if we unify two of them
1346 together.
1347
1348 Note [Unifying SigTvs]
1349 ~~~~~~~~~~~~~~~~~~~~~~
1350 ALAS we have no decent way of avoiding two SigTvs getting unified.
1351 Consider
1352   f (x::(a,b)) (y::c)) = [fst x, y]
1353 Here we'd really like to complain that 'a' and 'c' are unified. But
1354 for the reasons above we can't make a,b,c into skolems, so they
1355 are just SigTvs that can unify.  And indeed, this would be ok,
1356   f x (y::c) = case x of
1357                  (x1 :: a1, True) -> [x,y]
1358                  (x1 :: a2, False) -> [x,y,y]
1359 Here the type of x's first component is called 'a1' in one branch and
1360 'a2' in the other.  We could try insisting on the same OccName, but
1361 they definitely won't have the sane lexical Name.
1362
1363 I think we could solve this by recording in a SigTv a list of all the
1364 in-scope varaibles that it should not unify with, but it's fiddly.
1365
1366
1367 %************************************************************************
1368 %*                                                                      *
1369         Checking kinds
1370 %*                                                                      *
1371 %************************************************************************
1372
1373 We would like to get a decent error message from
1374   (a) Under-applied type constructors
1375              f :: (Maybe, Maybe)
1376   (b) Over-applied type constructors
1377              f :: Int x -> Int x
1378
1379 \begin{code}
1380 -- The ExpKind datatype means "expected kind" and contains
1381 -- some info about just why that kind is expected, to improve
1382 -- the error message on a mis-match
1383 data ExpKind = EK TcKind (TcKind -> SDoc)
1384    -- The second arg is function that takes a *tidied* version
1385    -- of the first arg, and produces something like
1386    --    "Expected kind k"
1387    --    "Expected a constraint"
1388    --    "The argument of Maybe should have kind k"
1389
1390 instance Outputable ExpKind where
1391   ppr (EK k f) = f k
1392
1393 ekLifted, ekOpen, ekConstraint :: ExpKind
1394 ekLifted     = EK liftedTypeKind expectedKindMsg
1395 ekOpen       = EK openTypeKind   expectedKindMsg
1396 ekConstraint = EK constraintKind expectedKindMsg
1397
1398 expectedKindMsg :: TcKind -> SDoc
1399 expectedKindMsg pkind
1400   | isConstraintKind pkind = ptext (sLit "Expected a constraint")
1401   | isOpenTypeKind   pkind = ptext (sLit "Expected a type")
1402   | otherwise = ptext (sLit "Expected kind") <+> quotes (pprKind pkind)
1403
1404 -- Build an ExpKind for arguments
1405 expArgKind :: SDoc -> TcKind -> Int -> ExpKind
1406 expArgKind exp kind arg_no = EK kind msg_fn
1407   where
1408     msg_fn pkind
1409       = sep [ ptext (sLit "The") <+> speakNth arg_no
1410               <+> ptext (sLit "argument of") <+> exp
1411             , nest 2 $ ptext (sLit "should have kind")
1412               <+> quotes (pprKind pkind) ]
1413
1414 unifyKinds :: SDoc -> [(TcType, TcKind)] -> TcM TcKind
1415 unifyKinds fun act_kinds
1416   = do { kind <- newMetaKindVar
1417        ; let check (arg_no, (ty, act_kind))
1418                = checkExpectedKind ty act_kind (expArgKind (quotes fun) kind arg_no)
1419        ; mapM_ check (zip [1..] act_kinds)
1420        ; return kind }
1421
1422 checkKind :: TcKind -> TcKind -> TcM ()
1423 checkKind act_kind exp_kind
1424   = do { mb_subk <- unifyKindX act_kind exp_kind
1425        ; case mb_subk of
1426            Just EQ -> return ()
1427            _       -> unifyKindMisMatch act_kind exp_kind }
1428
1429 checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
1430 -- A fancy wrapper for 'unifyKindX', which tries
1431 -- to give decent error messages.
1432 --      (checkExpectedKind ty act_kind exp_kind)
1433 -- checks that the actual kind act_kind is compatible
1434 --      with the expected kind exp_kind
1435 -- The first argument, ty, is used only in the error message generation
1436 checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
1437  = do { mb_subk <- unifyKindX act_kind exp_kind
1438
1439          -- Kind unification only generates definite errors
1440       ; case mb_subk of {
1441           Just LT -> return () ;    -- act_kind is a sub-kind of exp_kind
1442           Just EQ -> return () ;    -- The two are equal
1443           _other  -> do
1444
1445       {  -- So there's an error
1446          -- Now to find out what sort
1447         exp_kind <- zonkTcKind exp_kind
1448       ; act_kind <- zonkTcKind act_kind
1449       ; traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind $$ ppr exp_kind)
1450       ; env0 <- tcInitTidyEnv
1451       ; dflags <- getDynFlags
1452       ; let (exp_as, _) = splitKindFunTys exp_kind
1453             (act_as, _) = splitKindFunTys act_kind
1454             n_exp_as  = length exp_as
1455             n_act_as  = length act_as
1456             n_diff_as = n_act_as - n_exp_as
1457
1458             (env1, tidy_exp_kind) = tidyOpenKind env0 exp_kind
1459             (env2, tidy_act_kind) = tidyOpenKind env1 act_kind
1460
1461             occurs_check
1462                | Just act_tv <- tcGetTyVar_maybe act_kind
1463                = check_occ act_tv exp_kind
1464                | Just exp_tv <- tcGetTyVar_maybe exp_kind
1465                = check_occ exp_tv act_kind
1466                | otherwise
1467                = False
1468
1469             check_occ tv k = case occurCheckExpand dflags tv k of
1470                                 OC_Occurs -> True
1471                                 _bad      -> False
1472
1473             err | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1474                 = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
1475                     <+> ptext (sLit "is unlifted")
1476
1477                 | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1478                 = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
1479                     <+> ptext (sLit "is lifted")
1480
1481                 | occurs_check   -- Must precede the "more args expected" check
1482                 = ptext (sLit "Kind occurs check") $$ more_info
1483
1484                 | n_exp_as < n_act_as     -- E.g. [Maybe]
1485                 = vcat [ ptext (sLit "Expecting") <+>
1486                          speakN n_diff_as <+> ptext (sLit "more argument")
1487                          <> (if n_diff_as > 1 then char 's' else empty)
1488                          <+> ptext (sLit "to") <+> quotes (ppr ty)
1489                        , more_info ]
1490
1491                   -- Now n_exp_as >= n_act_as. In the next two cases,
1492                   -- n_exp_as == 0, and hence so is n_act_as
1493                 | otherwise               -- E.g. Monad [Int]
1494                 = more_info
1495
1496             more_info = sep [ ek_ctxt tidy_exp_kind <> comma
1497                             , nest 2 $ ptext (sLit "but") <+> quotes (ppr ty)
1498                               <+> ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
1499
1500       ; traceTc "checkExpectedKind 1" (ppr ty $$ ppr tidy_act_kind $$ ppr tidy_exp_kind $$ ppr env1 $$ ppr env2)
1501       ; failWithTcM (env2, err) } } }
1502
1503 \end{code}
1504
1505 %************************************************************************
1506 %*                                                                      *
1507         Sort checking kinds
1508 %*                                                                      *
1509 %************************************************************************
1510
1511 tcLHsKind converts a user-written kind to an internal, sort-checked kind.
1512 It does sort checking and desugaring at the same time, in one single pass.
1513 It fails when the kinds are not well-formed (eg. data A :: * Int), or if there
1514 are non-promotable or non-fully applied kinds.
1515
1516 \begin{code}
1517 tcLHsKind :: LHsKind Name -> TcM Kind
1518 tcLHsKind k = addErrCtxt (ptext (sLit "In the kind") <+> quotes (ppr k)) $
1519               tc_lhs_kind k
1520
1521 tc_lhs_kind :: LHsKind Name -> TcM Kind
1522 tc_lhs_kind (L span ki) = setSrcSpan span (tc_hs_kind ki)
1523
1524 -- The main worker
1525 tc_hs_kind :: HsKind Name -> TcM Kind
1526 tc_hs_kind (HsTyVar tc)    = tc_kind_var_app tc []
1527 tc_hs_kind k@(HsAppTy _ _) = tc_kind_app k []
1528
1529 tc_hs_kind (HsParTy ki) = tc_lhs_kind ki
1530
1531 tc_hs_kind (HsFunTy ki1 ki2) =
1532   do kappa_ki1 <- tc_lhs_kind ki1
1533      kappa_ki2 <- tc_lhs_kind ki2
1534      return (mkArrowKind kappa_ki1 kappa_ki2)
1535
1536 tc_hs_kind (HsListTy ki) =
1537   do kappa <- tc_lhs_kind ki
1538      checkWiredInTyCon listTyCon
1539      return $ mkPromotedListTy kappa
1540
1541 tc_hs_kind (HsTupleTy _ kis) =
1542   do kappas <- mapM tc_lhs_kind kis
1543      checkWiredInTyCon tycon
1544      return $ mkTyConApp tycon kappas
1545   where
1546      tycon = promotedTupleTyCon BoxedTuple (length kis)
1547
1548 -- Argument not kind-shaped
1549 tc_hs_kind k = pprPanic "tc_hs_kind" (ppr k)
1550
1551 -- Special case for kind application
1552 tc_kind_app :: HsKind Name -> [LHsKind Name] -> TcM Kind
1553 tc_kind_app (HsAppTy ki1 ki2) kis = tc_kind_app (unLoc ki1) (ki2:kis)
1554 tc_kind_app (HsTyVar tc)      kis = do { arg_kis <- mapM tc_lhs_kind kis
1555                                        ; tc_kind_var_app tc arg_kis }
1556 tc_kind_app ki                _   = failWithTc (quotes (ppr ki) <+>
1557                                     ptext (sLit "is not a kind constructor"))
1558
1559 tc_kind_var_app :: Name -> [Kind] -> TcM Kind
1560 -- Special case for * and Constraint kinds
1561 -- They are kinds already, so we don't need to promote them
1562 tc_kind_var_app name arg_kis
1563   |  name == liftedTypeKindTyConName
1564   || name == constraintKindTyConName
1565   = do { unless (null arg_kis)
1566            (failWithTc (text "Kind" <+> ppr name <+> text "cannot be applied"))
1567        ; thing <- tcLookup name
1568        ; case thing of
1569            AGlobal (ATyCon tc) -> return (mkTyConApp tc [])
1570            _                   -> panic "tc_kind_var_app 1" }
1571
1572 -- General case
1573 tc_kind_var_app name arg_kis
1574   = do { thing <- tcLookup name
1575        ; case thing of
1576            AGlobal (ATyCon tc)
1577              -> do { data_kinds <- xoptM Opt_DataKinds
1578                    ; unless data_kinds $ addErr (dataKindsErr name)
1579                    ; case promotableTyCon_maybe tc of
1580                        Just prom_tc | arg_kis `lengthIs` tyConArity prom_tc
1581                                -> return (mkTyConApp prom_tc arg_kis)
1582                        Just _  -> tycon_err tc "is not fully applied"
1583                        Nothing -> tycon_err tc "is not promotable" }
1584
1585            -- A lexically scoped kind variable
1586            ATyVar _ kind_var
1587              | not (isKindVar kind_var)
1588              -> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr kind_var)
1589                             <+> ptext (sLit "used as a kind"))
1590              | not (null arg_kis) -- Kind variables always have kind BOX,
1591                                   -- so cannot be applied to anything
1592              -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr name)
1593                             <+> ptext (sLit "cannot appear in a function position"))
1594              | otherwise
1595              -> return (mkAppTys (mkTyVarTy kind_var) arg_kis)
1596
1597            -- It is in scope, but not what we expected
1598            AThing _
1599              | isTyVarName name
1600              -> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr name)
1601                             <+> ptext (sLit "used in a kind"))
1602              | otherwise
1603              -> failWithTc (hang (ptext (sLit "Type constructor") <+> quotes (ppr name)
1604                                   <+> ptext (sLit "used in a kind"))
1605                                2 (ptext (sLit "inside its own recursive group")))
1606
1607            APromotionErr err -> promotionErr name err
1608
1609            _ -> wrongThingErr "promoted type" thing name
1610                 -- This really should not happen
1611      }
1612   where
1613    tycon_err tc msg = failWithTc (quotes (ppr tc) <+> ptext (sLit "of kind")
1614                                   <+> quotes (ppr (tyConKind tc)) <+> ptext (sLit msg))
1615
1616 dataKindsErr :: Name -> SDoc
1617 dataKindsErr name
1618   = hang (ptext (sLit "Illegal kind:") <+> quotes (ppr name))
1619        2 (ptext (sLit "Perhaps you intended to use DataKinds"))
1620
1621 promotionErr :: Name -> PromotionErr -> TcM a
1622 promotionErr name err
1623   = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> ptext (sLit "cannot be used here"))
1624                    2 (parens reason))
1625   where
1626     reason = case err of
1627                FamDataConPE -> ptext (sLit "it comes from a data family instance")
1628                NoDataKinds  -> ptext (sLit "Perhaps you intended to use DataKinds")
1629                _ -> ptext (sLit "it is defined and used in the same recursive group")
1630 \end{code}
1631
1632 %************************************************************************
1633 %*                                                                      *
1634                 Scoped type variables
1635 %*                                                                      *
1636 %************************************************************************
1637
1638 \begin{code}
1639 badPatSigTvs :: TcType -> [TyVar] -> SDoc
1640 badPatSigTvs sig_ty bad_tvs
1641   = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs,
1642                  quotes (pprWithCommas ppr bad_tvs),
1643                  ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
1644                  ptext (sLit "but are actually discarded by a type synonym") ]
1645          , ptext (sLit "To fix this, expand the type synonym")
1646          , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
1647
1648 unifyKindMisMatch :: TcKind -> TcKind -> TcM a
1649 unifyKindMisMatch ki1 ki2 = do
1650     ki1' <- zonkTcKind ki1
1651     ki2' <- zonkTcKind ki2
1652     let msg = hang (ptext (sLit "Couldn't match kind"))
1653               2 (sep [quotes (ppr ki1'),
1654                       ptext (sLit "against"),
1655                       quotes (ppr ki2')])
1656     failWithTc msg
1657 \end{code}
1658