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