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