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