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