2f427916b47c3bb04f25c94dcd6bb6f871fed3f2
[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( 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 ; 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 tcWildcardBinders :: [Name]
926 -> ([(Name,TcTyVar)] -> TcM a)
927 -> TcM a
928 tcWildcardBinders wcs thing_inside
929 = do { wc_prs <- mapM new_wildcard wcs
930 ; tcExtendTyVarEnv2 wc_prs $
931 thing_inside wc_prs }
932 where
933 new_wildcard :: Name -> TcM (Name, TcTyVar)
934 new_wildcard name = do { kind <- newMetaKindVar
935 ; tv <- newFlexiTyVar kind
936 ; return (name, tv) }
937
938 mkKindSigVar :: Name -> TcM KindVar
939 -- Use the specified name; don't clone it
940 mkKindSigVar n
941 = do { mb_thing <- tcLookupLcl_maybe n
942 ; case mb_thing of
943 Just (AThing k)
944 | Just kvar <- getTyVar_maybe k
945 -> return kvar
946 _ -> return $ mkTcTyVar n superKind (SkolemTv False) }
947
948 kcScopedKindVars :: [Name] -> TcM a -> TcM a
949 -- Given some tyvar binders like [a (b :: k -> *) (c :: k)]
950 -- bind each scoped kind variable (k in this case) to a fresh
951 -- kind skolem variable
952 kcScopedKindVars kv_ns thing_inside
953 = do { kvs <- mapM newSigKindVar kv_ns
954 -- NB: use mutable signature variables
955 ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) thing_inside }
956
957 -- | Kind-check a 'LHsTyVarBndrs'. If the decl under consideration has a complete,
958 -- user-supplied kind signature (CUSK), generalise the result. Used in 'getInitialKind'
959 -- and in kind-checking. See also Note [Complete user-supplied kind signatures] in
960 -- HsDecls.
961 kcHsTyVarBndrs :: Bool -- ^ True <=> the decl being checked has a CUSK
962 -> LHsTyVarBndrs Name
963 -> TcM (Kind, r) -- ^ the result kind, possibly with other info
964 -> TcM (Kind, r) -- ^ The full kind of the thing being declared,
965 -- with the other info
966 kcHsTyVarBndrs cusk (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
967 = do { kvs <- if cusk
968 then mapM mkKindSigVar kv_ns
969 else mapM newSigKindVar kv_ns
970 ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $
971 do { nks <- mapM (kc_hs_tv . unLoc) hs_tvs
972 ; (res_kind, stuff) <- tcExtendKindEnv nks thing_inside
973 ; let full_kind = mkArrowKinds (map snd nks) res_kind
974 kvs = filter (not . isMetaTyVar) $
975 varSetElems $ tyVarsOfType full_kind
976 gen_kind = if cusk
977 then mkForAllTys kvs full_kind
978 else full_kind
979 ; return (gen_kind, stuff) } }
980 where
981 kc_hs_tv :: HsTyVarBndr Name -> TcM (Name, TcKind)
982 kc_hs_tv (UserTyVar n)
983 = do { mb_thing <- tcLookupLcl_maybe n
984 ; kind <- case mb_thing of
985 Just (AThing k) -> return k
986 _ | cusk -> return liftedTypeKind
987 | otherwise -> newMetaKindVar
988 ; return (n, kind) }
989 kc_hs_tv (KindedTyVar (L _ n) k)
990 = do { kind <- tcLHsKind k
991 -- In an associated type decl, the type variable may already
992 -- be in scope; in that case we want to make sure its kind
993 -- matches the one declared here
994 ; mb_thing <- tcLookupLcl_maybe n
995 ; case mb_thing of
996 Nothing -> return ()
997 Just (AThing ks) -> checkKind kind ks
998 Just thing -> pprPanic "check_in_scope" (ppr thing)
999 ; return (n, kind) }
1000
1001 tcHsTyVarBndrs :: LHsTyVarBndrs Name
1002 -> ([TcTyVar] -> TcM r)
1003 -> TcM r
1004 -- Bind the kind variables to fresh skolem variables
1005 -- and type variables to skolems, each with a meta-kind variable kind
1006 tcHsTyVarBndrs (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
1007 = do { kvs <- mapM mkKindSigVar kv_ns
1008 ; tcExtendTyVarEnv kvs $ do
1009 { tvs <- mapM tcHsTyVarBndr hs_tvs
1010 ; traceTc "tcHsTyVarBndrs {" (vcat [ text "Hs kind vars:" <+> ppr kv_ns
1011 , text "Hs type vars:" <+> ppr hs_tvs
1012 , text "Kind vars:" <+> ppr kvs
1013 , text "Type vars:" <+> ppr tvs ])
1014 ; res <- tcExtendTyVarEnv tvs (thing_inside (kvs ++ tvs))
1015 ; traceTc "tcHsTyVarBndrs }" (vcat [ text "Hs kind vars:" <+> ppr kv_ns
1016 , text "Hs type vars:" <+> ppr hs_tvs
1017 , text "Kind vars:" <+> ppr kvs
1018 , text "Type vars:" <+> ppr tvs ])
1019 ; return res } }
1020
1021 tcHsTyVarBndr :: LHsTyVarBndr Name -> TcM TcTyVar
1022 -- Return a type variable
1023 -- initialised with a kind variable.
1024 -- Typically the Kind inside the HsTyVarBndr will be a tyvar with a mutable kind
1025 -- in it.
1026 --
1027 -- If the variable is already in scope return it, instead of introducing a new
1028 -- one. This can occur in
1029 -- instance C (a,b) where
1030 -- type F (a,b) c = ...
1031 -- Here a,b will be in scope when processing the associated type instance for F.
1032 -- See Note [Associated type tyvar names] in Class
1033 tcHsTyVarBndr (L _ hs_tv)
1034 = do { let name = hsTyVarName hs_tv
1035 ; mb_tv <- tcLookupLcl_maybe name
1036 ; case mb_tv of {
1037 Just (ATyVar _ tv) -> return tv ;
1038 _ -> do
1039 { kind <- case hs_tv of
1040 UserTyVar {} -> newMetaKindVar
1041 KindedTyVar _ kind -> tcLHsKind kind
1042 ; return ( mkTcTyVar name kind (SkolemTv False)) } } }
1043
1044 ------------------
1045 kindGeneralize :: TyVarSet -> TcM [KindVar]
1046 kindGeneralize tkvs
1047 = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
1048 ; quantifyTyVars gbl_tvs (filterVarSet isKindVar tkvs) }
1049 -- ToDo: remove the (filter isKindVar)
1050 -- Any type variables in tkvs will be in scope,
1051 -- and hence in gbl_tvs, so after removing gbl_tvs
1052 -- we should only have kind variables left
1053 --
1054 -- BUT there is a smelly case (to be fixed when TH is reorganised)
1055 -- f t = [| e :: $t |]
1056 -- When typechecking the body of the bracket, we typecheck $t to a
1057 -- unification variable 'alpha', with no biding forall. We don't
1058 -- want to kind-quantify it!
1059
1060 {-
1061 Note [Kind generalisation]
1062 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1063 We do kind generalisation only at the outer level of a type signature.
1064 For example, consider
1065 T :: forall k. k -> *
1066 f :: (forall a. T a -> Int) -> Int
1067 When kind-checking f's type signature we generalise the kind at
1068 the outermost level, thus:
1069 f1 :: forall k. (forall (a:k). T k a -> Int) -> Int -- YES!
1070 and *not* at the inner forall:
1071 f2 :: (forall k. forall (a:k). T k a -> Int) -> Int -- NO!
1072 Reason: same as for HM inference on value level declarations,
1073 we want to infer the most general type. The f2 type signature
1074 would be *less applicable* than f1, because it requires a more
1075 polymorphic argument.
1076
1077 Note [Kinds of quantified type variables]
1078 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1079 tcTyVarBndrsGen quantifies over a specified list of type variables,
1080 *and* over the kind variables mentioned in the kinds of those tyvars.
1081
1082 Note that we must zonk those kinds (obviously) but less obviously, we
1083 must return type variables whose kinds are zonked too. Example
1084 (a :: k7) where k7 := k9 -> k9
1085 We must return
1086 [k9, a:k9->k9]
1087 and NOT
1088 [k9, a:k7]
1089 Reason: we're going to turn this into a for-all type,
1090 forall k9. forall (a:k7). blah
1091 which the type checker will then instantiate, and instantiate does not
1092 look through unification variables!
1093
1094 Hence using zonked_kinds when forming tvs'.
1095 -}
1096
1097 --------------------
1098 -- getInitialKind has made a suitably-shaped kind for the type or class
1099 -- Unpack it, and attribute those kinds to the type variables
1100 -- Extend the env with bindings for the tyvars, taken from
1101 -- the kind of the tycon/class. Give it to the thing inside, and
1102 -- check the result kind matches
1103 kcLookupKind :: Name -> TcM Kind
1104 kcLookupKind nm
1105 = do { tc_ty_thing <- tcLookup nm
1106 ; case tc_ty_thing of
1107 AThing k -> return k
1108 AGlobal (ATyCon tc) -> return (tyConKind tc)
1109 _ -> pprPanic "kcLookupKind" (ppr tc_ty_thing) }
1110
1111 kcTyClTyVars :: Name -> LHsTyVarBndrs Name -> TcM a -> TcM a
1112 -- Used for the type variables of a type or class decl,
1113 -- when doing the initial kind-check.
1114 kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
1115 = kcScopedKindVars kvs $
1116 do { tc_kind <- kcLookupKind name
1117 ; let (_, mono_kind) = splitForAllTys tc_kind
1118 -- if we have a FullKindSignature, the tc_kind may already
1119 -- be generalized. The kvs get matched up while kind-checking
1120 -- the types in kc_tv, below
1121 (arg_ks, _res_k) = splitKindFunTysN (length hs_tvs) mono_kind
1122 -- There should be enough arrows, because
1123 -- getInitialKinds used the tcdTyVars
1124 ; name_ks <- zipWithM kc_tv hs_tvs arg_ks
1125 ; tcExtendKindEnv name_ks thing_inside }
1126 where
1127 -- getInitialKind has already gotten the kinds of these type
1128 -- variables, but tiresomely we need to check them *again*
1129 -- to match the kind variables they mention against the ones
1130 -- we've freshly brought into scope
1131 kc_tv :: LHsTyVarBndr Name -> Kind -> TcM (Name, Kind)
1132 kc_tv (L _ (UserTyVar n)) exp_k
1133 = return (n, exp_k)
1134 kc_tv (L _ (KindedTyVar (L _ n) hs_k)) exp_k
1135 = do { k <- tcLHsKind hs_k
1136 ; checkKind k exp_k
1137 ; return (n, exp_k) }
1138
1139 -----------------------
1140 tcTyClTyVars :: Name -> LHsTyVarBndrs Name -- LHS of the type or class decl
1141 -> ([TyVar] -> Kind -> TcM a) -> TcM a
1142 -- Used for the type variables of a type or class decl,
1143 -- on the second pass when constructing the final result
1144 -- (tcTyClTyVars T [a,b] thing_inside)
1145 -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
1146 -- calls thing_inside with arguments
1147 -- [k1,k2,a,b] (k2 -> *)
1148 -- having also extended the type environment with bindings
1149 -- for k1,k2,a,b
1150 --
1151 -- No need to freshen the k's because they are just skolem
1152 -- constants here, and we are at top level anyway.
1153 tcTyClTyVars tycon (HsQTvs { hsq_kvs = hs_kvs, hsq_tvs = hs_tvs }) thing_inside
1154 = kcScopedKindVars hs_kvs $ -- Bind scoped kind vars to fresh kind univ vars
1155 -- There may be fewer of these than the kvs of
1156 -- the type constructor, of course
1157 do { thing <- tcLookup tycon
1158 ; let { kind = case thing of -- The kind of the tycon has been worked out
1159 -- by the previous pass, and is fully zonked
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
1176 = return (mkTyVar n kind)
1177 tc_hs_tv (L _ (KindedTyVar (L _ n) hs_k)) kind
1178 = do { tc_kind <- tcLHsKind hs_k
1179 ; checkKind kind tc_kind
1180 ; return (mkTyVar n kind) }
1181
1182 -----------------------------------
1183 tcDataKindSig :: Kind -> TcM [TyVar]
1184 -- GADT decls can have a (perhaps partial) kind signature
1185 -- e.g. data T :: * -> * -> * where ...
1186 -- This function makes up suitable (kinded) type variables for
1187 -- the argument kinds, and checks that the result kind is indeed *.
1188 -- We use it also to make up argument type variables for for data instances.
1189 tcDataKindSig kind
1190 = do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
1191 ; span <- getSrcSpanM
1192 ; us <- newUniqueSupply
1193 ; rdr_env <- getLocalRdrEnv
1194 ; let uniqs = uniqsFromSupply us
1195 occs = [ occ | str <- allNameStrings
1196 , let occ = mkOccName tvName str
1197 , isNothing (lookupLocalRdrOcc rdr_env occ) ]
1198 -- Note [Avoid name clashes for associated data types]
1199
1200 ; return [ mk_tv span uniq occ kind
1201 | ((kind, occ), uniq) <- arg_kinds `zip` occs `zip` uniqs ] }
1202 where
1203 (arg_kinds, res_kind) = splitKindFunTys kind
1204 mk_tv loc uniq occ kind
1205 = mkTyVar (mkInternalName uniq occ loc) kind
1206
1207 badKindSig :: Kind -> SDoc
1208 badKindSig kind
1209 = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
1210 2 (ppr kind)
1211
1212 {-
1213 Note [Avoid name clashes for associated data types]
1214 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1215 Consider class C a b where
1216 data D b :: * -> *
1217 When typechecking the decl for D, we'll invent an extra type variable
1218 for D, to fill out its kind. Ideally we don't want this type variable
1219 to be 'a', because when pretty printing we'll get
1220 class C a b where
1221 data D b a0
1222 (NB: the tidying happens in the conversion to IfaceSyn, which happens
1223 as part of pretty-printing a TyThing.)
1224
1225 That's why we look in the LocalRdrEnv to see what's in scope. This is
1226 important only to get nice-looking output when doing ":info C" in GHCi.
1227 It isn't essential for correctness.
1228
1229
1230 ************************************************************************
1231 * *
1232 Scoped type variables
1233 * *
1234 ************************************************************************
1235
1236
1237 tcAddScopedTyVars is used for scoped type variables added by pattern
1238 type signatures
1239 e.g. \ ((x::a), (y::a)) -> x+y
1240 They never have explicit kinds (because this is source-code only)
1241 They are mutable (because they can get bound to a more specific type).
1242
1243 Usually we kind-infer and expand type splices, and then
1244 tupecheck/desugar the type. That doesn't work well for scoped type
1245 variables, because they scope left-right in patterns. (e.g. in the
1246 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
1247
1248 The current not-very-good plan is to
1249 * find all the types in the patterns
1250 * find their free tyvars
1251 * do kind inference
1252 * bring the kinded type vars into scope
1253 * BUT throw away the kind-checked type
1254 (we'll kind-check it again when we type-check the pattern)
1255
1256 This is bad because throwing away the kind checked type throws away
1257 its splices. But too bad for now. [July 03]
1258
1259 Historical note:
1260 We no longer specify that these type variables must be universally
1261 quantified (lots of email on the subject). If you want to put that
1262 back in, you need to
1263 a) Do a checkSigTyVars after thing_inside
1264 b) More insidiously, don't pass in expected_ty, else
1265 we unify with it too early and checkSigTyVars barfs
1266 Instead you have to pass in a fresh ty var, and unify
1267 it with expected_ty afterwards
1268 -}
1269
1270 tcHsPatSigType :: UserTypeCtxt
1271 -> HsWithBndrs Name (LHsType Name) -- The type signature
1272 -> TcM ( Type -- The signature
1273 , [(Name, TcTyVar)] -- The new bit of type environment, binding
1274 -- the scoped type variables
1275 , [(Name, TcTyVar)] ) -- The wildcards
1276 -- Used for type-checking type signatures in
1277 -- (a) patterns e.g f (x::Int) = e
1278 -- (b) result signatures e.g. g x :: Int = e
1279 -- (c) RULE forall bndrs e.g. forall (x::Int). f x = x
1280
1281 tcHsPatSigType ctxt (HsWB { hswb_cts = hs_ty, hswb_kvs = sig_kvs,
1282 hswb_tvs = sig_tvs, hswb_wcs = sig_wcs })
1283 = addErrCtxt (pprSigCtxt ctxt empty (ppr hs_ty)) $
1284 tcWildcardBinders sig_wcs $ \ nwc_binds ->
1285 do { emitWildcardHoleConstraints nwc_binds
1286 ; kvs <- mapM new_kv sig_kvs
1287 ; tvs <- mapM new_tv sig_tvs
1288 ; let ktv_binds = (sig_kvs `zip` kvs) ++ (sig_tvs `zip` tvs)
1289 ; sig_ty <- tcExtendTyVarEnv2 ktv_binds $
1290 tcHsLiftedType hs_ty
1291 ; sig_ty <- zonkSigType sig_ty
1292 ; checkValidType ctxt sig_ty
1293 ; return (sig_ty, ktv_binds, nwc_binds) }
1294 where
1295 new_kv name = new_tkv name superKind
1296 new_tv name = do { kind <- newMetaKindVar
1297 ; new_tkv name kind }
1298
1299 new_tkv name kind -- See Note [Pattern signature binders]
1300 = case ctxt of
1301 RuleSigCtxt {} -> return (mkTcTyVar name kind (SkolemTv False))
1302 _ -> newSigTyVar name kind -- See Note [Unifying SigTvs]
1303
1304 tcPatSig :: Bool -- True <=> pattern binding
1305 -> HsWithBndrs Name (LHsType Name)
1306 -> TcSigmaType
1307 -> TcM (TcType, -- The type to use for "inside" the signature
1308 [(Name, TcTyVar)], -- The new bit of type environment, binding
1309 -- the scoped type variables
1310 [(Name, TcTyVar)], -- The wildcards
1311 HsWrapper) -- Coercion due to unification with actual ty
1312 -- Of shape: res_ty ~ sig_ty
1313 tcPatSig in_pat_bind sig res_ty
1314 = do { (sig_ty, sig_tvs, sig_nwcs) <- tcHsPatSigType PatSigCtxt sig
1315 -- sig_tvs are the type variables free in 'sig',
1316 -- and not already in scope. These are the ones
1317 -- that should be brought into scope
1318
1319 ; if null sig_tvs then do {
1320 -- Just do the subsumption check and return
1321 wrap <- addErrCtxtM (mk_msg sig_ty) $
1322 tcSubType_NC PatSigCtxt res_ty sig_ty
1323 ; return (sig_ty, [], sig_nwcs, wrap)
1324 } else do
1325 -- Type signature binds at least one scoped type variable
1326
1327 -- A pattern binding cannot bind scoped type variables
1328 -- It is more convenient to make the test here
1329 -- than in the renamer
1330 { when in_pat_bind (addErr (patBindSigErr sig_tvs))
1331
1332 -- Check that all newly-in-scope tyvars are in fact
1333 -- constrained by the pattern. This catches tiresome
1334 -- cases like
1335 -- type T a = Int
1336 -- f :: Int -> Int
1337 -- f (x :: T a) = ...
1338 -- Here 'a' doesn't get a binding. Sigh
1339 ; let bad_tvs = [ tv | (_, tv) <- sig_tvs
1340 , not (tv `elemVarSet` exactTyVarsOfType sig_ty) ]
1341 ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
1342
1343 -- Now do a subsumption check of the pattern signature against res_ty
1344 ; wrap <- addErrCtxtM (mk_msg sig_ty) $
1345 tcSubType_NC PatSigCtxt res_ty sig_ty
1346
1347 -- Phew!
1348 ; return (sig_ty, sig_tvs, sig_nwcs, wrap)
1349 } }
1350 where
1351 mk_msg sig_ty tidy_env
1352 = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
1353 ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
1354 ; let msg = vcat [ hang (ptext (sLit "When checking that the pattern signature:"))
1355 4 (ppr sig_ty)
1356 , nest 2 (hang (ptext (sLit "fits the type of its context:"))
1357 2 (ppr res_ty)) ]
1358 ; return (tidy_env, msg) }
1359
1360 patBindSigErr :: [(Name, TcTyVar)] -> SDoc
1361 patBindSigErr sig_tvs
1362 = hang (ptext (sLit "You cannot bind scoped type variable") <> plural sig_tvs
1363 <+> pprQuotedList (map fst sig_tvs))
1364 2 (ptext (sLit "in a pattern binding signature"))
1365
1366 {-
1367 Note [Pattern signature binders]
1368 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1369 Consider
1370 data T = forall a. T a (a->Int)
1371 f (T x (f :: a->Int) = blah)
1372
1373 Here
1374 * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk',
1375 It must be a skolem so that that it retains its identity, and
1376 TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
1377
1378 * The type signature pattern (f :: a->Int) binds "a" -> a_sig in the envt
1379
1380 * Then unificaiton makes a_sig := a_sk
1381
1382 That's why we must make a_sig a MetaTv (albeit a SigTv),
1383 not a SkolemTv, so that it can unify to a_sk.
1384
1385 For RULE binders, though, things are a bit different (yuk).
1386 RULE "foo" forall (x::a) (y::[a]). f x y = ...
1387 Here this really is the binding site of the type variable so we'd like
1388 to use a skolem, so that we get a complaint if we unify two of them
1389 together.
1390
1391 Note [Unifying SigTvs]
1392 ~~~~~~~~~~~~~~~~~~~~~~
1393 ALAS we have no decent way of avoiding two SigTvs getting unified.
1394 Consider
1395 f (x::(a,b)) (y::c)) = [fst x, y]
1396 Here we'd really like to complain that 'a' and 'c' are unified. But
1397 for the reasons above we can't make a,b,c into skolems, so they
1398 are just SigTvs that can unify. And indeed, this would be ok,
1399 f x (y::c) = case x of
1400 (x1 :: a1, True) -> [x,y]
1401 (x1 :: a2, False) -> [x,y,y]
1402 Here the type of x's first component is called 'a1' in one branch and
1403 'a2' in the other. We could try insisting on the same OccName, but
1404 they definitely won't have the sane lexical Name.
1405
1406 I think we could solve this by recording in a SigTv a list of all the
1407 in-scope variables that it should not unify with, but it's fiddly.
1408
1409
1410 ************************************************************************
1411 * *
1412 Checking kinds
1413 * *
1414 ************************************************************************
1415
1416 We would like to get a decent error message from
1417 (a) Under-applied type constructors
1418 f :: (Maybe, Maybe)
1419 (b) Over-applied type constructors
1420 f :: Int x -> Int x
1421 -}
1422
1423 -- The ExpKind datatype means "expected kind" and contains
1424 -- some info about just why that kind is expected, to improve
1425 -- the error message on a mis-match
1426 data ExpKind = EK TcKind (TcKind -> SDoc)
1427 -- The second arg is function that takes a *tidied* version
1428 -- of the first arg, and produces something like
1429 -- "Expected kind k"
1430 -- "Expected a constraint"
1431 -- "The argument of Maybe should have kind k"
1432
1433 instance Outputable ExpKind where
1434 ppr (EK k f) = f k
1435
1436 ekLifted, ekOpen, ekConstraint :: ExpKind
1437 ekLifted = EK liftedTypeKind expectedKindMsg
1438 ekOpen = EK openTypeKind expectedKindMsg
1439 ekConstraint = EK constraintKind expectedKindMsg
1440
1441 expectedKindMsg :: TcKind -> SDoc
1442 expectedKindMsg pkind
1443 | isConstraintKind pkind = ptext (sLit "Expected a constraint")
1444 | isOpenTypeKind pkind = ptext (sLit "Expected a type")
1445 | otherwise = ptext (sLit "Expected kind") <+> quotes (pprKind pkind)
1446
1447 -- Build an ExpKind for arguments
1448 expArgKind :: SDoc -> TcKind -> Int -> ExpKind
1449 expArgKind exp kind arg_no = EK kind msg_fn
1450 where
1451 msg_fn pkind
1452 = sep [ ptext (sLit "The") <+> speakNth arg_no
1453 <+> ptext (sLit "argument of") <+> exp
1454 , nest 2 $ ptext (sLit "should have kind")
1455 <+> quotes (pprKind pkind) ]
1456
1457 unifyKinds :: SDoc -> [(TcType, TcKind)] -> TcM TcKind
1458 unifyKinds fun act_kinds
1459 = do { kind <- newMetaKindVar
1460 ; let check (arg_no, (ty, act_kind))
1461 = checkExpectedKind ty act_kind (expArgKind (quotes fun) kind arg_no)
1462 ; mapM_ check (zip [1..] act_kinds)
1463 ; return kind }
1464
1465 checkKind :: TcKind -> TcKind -> TcM ()
1466 checkKind act_kind exp_kind
1467 = do { mb_subk <- unifyKindX act_kind exp_kind
1468 ; case mb_subk of
1469 Just EQ -> return ()
1470 _ -> unifyKindMisMatch act_kind exp_kind }
1471
1472 checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
1473 -- A fancy wrapper for 'unifyKindX', which tries
1474 -- to give decent error messages.
1475 -- (checkExpectedKind ty act_kind exp_kind)
1476 -- checks that the actual kind act_kind is compatible
1477 -- with the expected kind exp_kind
1478 -- The first argument, ty, is used only in the error message generation
1479 checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
1480 = do { mb_subk <- unifyKindX act_kind exp_kind
1481
1482 -- Kind unification only generates definite errors
1483 ; case mb_subk of {
1484 Just LT -> return () ; -- act_kind is a sub-kind of exp_kind
1485 Just EQ -> return () ; -- The two are equal
1486 _other -> do
1487
1488 { -- So there's an error
1489 -- Now to find out what sort
1490 exp_kind <- zonkTcKind exp_kind
1491 ; act_kind <- zonkTcKind act_kind
1492 ; traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind $$ ppr exp_kind)
1493 ; env0 <- tcInitTidyEnv
1494 ; dflags <- getDynFlags
1495 ; let (exp_as, _) = splitKindFunTys exp_kind
1496 (act_as, _) = splitKindFunTys act_kind
1497 n_exp_as = length exp_as
1498 n_act_as = length act_as
1499 n_diff_as = n_act_as - n_exp_as
1500
1501 (env1, tidy_exp_kind) = tidyOpenKind env0 exp_kind
1502 (env2, tidy_act_kind) = tidyOpenKind env1 act_kind
1503
1504 occurs_check
1505 | Just act_tv <- tcGetTyVar_maybe act_kind
1506 = check_occ act_tv exp_kind
1507 | Just exp_tv <- tcGetTyVar_maybe exp_kind
1508 = check_occ exp_tv act_kind
1509 | otherwise
1510 = False
1511
1512 check_occ tv k = case occurCheckExpand dflags tv k of
1513 OC_Occurs -> True
1514 _bad -> False
1515
1516 err | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1517 = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
1518 <+> ptext (sLit "is unlifted")
1519
1520 | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1521 = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
1522 <+> ptext (sLit "is lifted")
1523
1524 | occurs_check -- Must precede the "more args expected" check
1525 = ptext (sLit "Kind occurs check") $$ more_info
1526
1527 | n_exp_as < n_act_as -- E.g. [Maybe]
1528 = vcat [ ptext (sLit "Expecting") <+>
1529 speakN n_diff_as <+> ptext (sLit "more argument")
1530 <> (if n_diff_as > 1 then char 's' else empty)
1531 <+> ptext (sLit "to") <+> quotes (ppr ty)
1532 , more_info ]
1533
1534 -- Now n_exp_as >= n_act_as. In the next two cases,
1535 -- n_exp_as == 0, and hence so is n_act_as
1536 | otherwise -- E.g. Monad [Int]
1537 = more_info
1538
1539 more_info = sep [ ek_ctxt tidy_exp_kind <> comma
1540 , nest 2 $ ptext (sLit "but") <+> quotes (ppr ty)
1541 <+> ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
1542
1543 ; traceTc "checkExpectedKind 1" (ppr ty $$ ppr tidy_act_kind $$ ppr tidy_exp_kind $$ ppr env1 $$ ppr env2)
1544 ; failWithTcM (env2, err) } } }
1545
1546 {-
1547 ************************************************************************
1548 * *
1549 Sort checking kinds
1550 * *
1551 ************************************************************************
1552
1553 tcLHsKind converts a user-written kind to an internal, sort-checked kind.
1554 It does sort checking and desugaring at the same time, in one single pass.
1555 It fails when the kinds are not well-formed (eg. data A :: * Int), or if there
1556 are non-promotable or non-fully applied kinds.
1557 -}
1558
1559 tcLHsKind :: LHsKind Name -> TcM Kind
1560 tcLHsKind k = addErrCtxt (ptext (sLit "In the kind") <+> quotes (ppr k)) $
1561 tc_lhs_kind k
1562
1563 tc_lhs_kind :: LHsKind Name -> TcM Kind
1564 tc_lhs_kind (L span ki) = setSrcSpan span (tc_hs_kind ki)
1565
1566 -- The main worker
1567 tc_hs_kind :: HsKind Name -> TcM Kind
1568 tc_hs_kind (HsTyVar tc) = tc_kind_var_app tc []
1569 tc_hs_kind k@(HsAppTy _ _) = tc_kind_app k []
1570
1571 tc_hs_kind (HsParTy ki) = tc_lhs_kind ki
1572
1573 tc_hs_kind (HsFunTy ki1 ki2) =
1574 do kappa_ki1 <- tc_lhs_kind ki1
1575 kappa_ki2 <- tc_lhs_kind ki2
1576 return (mkArrowKind kappa_ki1 kappa_ki2)
1577
1578 tc_hs_kind (HsListTy ki) =
1579 do kappa <- tc_lhs_kind ki
1580 checkWiredInTyCon listTyCon
1581 return $ mkPromotedListTy kappa
1582
1583 tc_hs_kind (HsTupleTy _ kis) =
1584 do kappas <- mapM tc_lhs_kind kis
1585 checkWiredInTyCon tycon
1586 return $ mkTyConApp tycon kappas
1587 where
1588 tycon = promotedTupleTyCon Boxed (length kis)
1589
1590 -- Argument not kind-shaped
1591 tc_hs_kind k = pprPanic "tc_hs_kind" (ppr k)
1592
1593 -- Special case for kind application
1594 tc_kind_app :: HsKind Name -> [LHsKind Name] -> TcM Kind
1595 tc_kind_app (HsAppTy ki1 ki2) kis = tc_kind_app (unLoc ki1) (ki2:kis)
1596 tc_kind_app (HsTyVar tc) kis = do { arg_kis <- mapM tc_lhs_kind kis
1597 ; tc_kind_var_app tc arg_kis }
1598 tc_kind_app ki _ = failWithTc (quotes (ppr ki) <+>
1599 ptext (sLit "is not a kind constructor"))
1600
1601 tc_kind_var_app :: Name -> [Kind] -> TcM Kind
1602 -- Special case for * and Constraint kinds
1603 -- They are kinds already, so we don't need to promote them
1604 tc_kind_var_app name arg_kis
1605 | name == liftedTypeKindTyConName
1606 || name == constraintKindTyConName
1607 = do { unless (null arg_kis)
1608 (failWithTc (text "Kind" <+> ppr name <+> text "cannot be applied"))
1609 ; thing <- tcLookup name
1610 ; case thing of
1611 AGlobal (ATyCon tc) -> return (mkTyConApp tc [])
1612 _ -> panic "tc_kind_var_app 1" }
1613
1614 -- General case
1615 tc_kind_var_app name arg_kis
1616 = do { thing <- tcLookup name
1617 ; case thing of
1618 AGlobal (ATyCon tc)
1619 -> do { data_kinds <- xoptM Opt_DataKinds
1620 ; unless data_kinds $ addErr (dataKindsErr name)
1621 ; case promotableTyCon_maybe tc of
1622 Just prom_tc | arg_kis `lengthIs` tyConArity prom_tc
1623 -> return (mkTyConApp prom_tc arg_kis)
1624 Just _ -> tycon_err tc "is not fully applied"
1625 Nothing -> tycon_err tc "is not promotable" }
1626
1627 -- A lexically scoped kind variable
1628 ATyVar _ kind_var
1629 | not (isKindVar kind_var)
1630 -> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr kind_var)
1631 <+> ptext (sLit "used as a kind"))
1632 | not (null arg_kis) -- Kind variables always have kind BOX,
1633 -- so cannot be applied to anything
1634 -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr name)
1635 <+> ptext (sLit "cannot appear in a function position"))
1636 | otherwise
1637 -> return (mkAppTys (mkTyVarTy kind_var) arg_kis)
1638
1639 -- It is in scope, but not what we expected
1640 AThing _
1641 | isTyVarName name
1642 -> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr name)
1643 <+> ptext (sLit "used in a kind"))
1644 | otherwise
1645 -> failWithTc (hang (ptext (sLit "Type constructor") <+> quotes (ppr name)
1646 <+> ptext (sLit "used in a kind"))
1647 2 (ptext (sLit "inside its own recursive group")))
1648
1649 APromotionErr err -> promotionErr name err
1650
1651 _ -> wrongThingErr "promoted type" thing name
1652 -- This really should not happen
1653 }
1654 where
1655 tycon_err tc msg = failWithTc (quotes (ppr tc) <+> ptext (sLit "of kind")
1656 <+> quotes (ppr (tyConKind tc)) <+> ptext (sLit msg))
1657
1658 dataKindsErr :: Name -> SDoc
1659 dataKindsErr name
1660 = hang (ptext (sLit "Illegal kind:") <+> quotes (ppr name))
1661 2 (ptext (sLit "Perhaps you intended to use DataKinds"))
1662
1663 promotionErr :: Name -> PromotionErr -> TcM a
1664 promotionErr name err
1665 = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> ptext (sLit "cannot be used here"))
1666 2 (parens reason))
1667 where
1668 reason = case err of
1669 FamDataConPE -> ptext (sLit "it comes from a data family instance")
1670 NoDataKinds -> ptext (sLit "Perhaps you intended to use DataKinds")
1671 _ -> ptext (sLit "it is defined and used in the same recursive group")
1672
1673 {-
1674 ************************************************************************
1675 * *
1676 Scoped type variables
1677 * *
1678 ************************************************************************
1679 -}
1680
1681 badPatSigTvs :: TcType -> [TyVar] -> SDoc
1682 badPatSigTvs sig_ty bad_tvs
1683 = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs,
1684 quotes (pprWithCommas ppr bad_tvs),
1685 ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
1686 ptext (sLit "but are actually discarded by a type synonym") ]
1687 , ptext (sLit "To fix this, expand the type synonym")
1688 , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
1689
1690 unifyKindMisMatch :: TcKind -> TcKind -> TcM a
1691 unifyKindMisMatch ki1 ki2 = do
1692 ki1' <- zonkTcKind ki1
1693 ki2' <- zonkTcKind ki2
1694 let msg = hang (ptext (sLit "Couldn't match kind"))
1695 2 (sep [quotes (ppr ki1'),
1696 ptext (sLit "against"),
1697 quotes (ppr ki2')])
1698 failWithTc msg