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