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