Add kind equalities to GHC.
[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, TupleSections, MultiWayIf #-}
9
10 module TcHsType (
11 -- Type signatures
12 kcHsSigType, tcClassSigType,
13 tcHsSigType, tcHsSigWcType,
14 funsSigCtxt, addSigCtxt,
15
16 tcHsClsInstType,
17 tcHsDeriv, tcHsVectInst,
18 UserTypeCtxt(..),
19 tcImplicitTKBndrs, tcImplicitTKBndrsType, tcHsTyVarBndrs,
20
21 -- Type checking type and class decls
22 kcLookupKind, kcTyClTyVars, tcTyClTyVars,
23 tcHsConArgType, tcDataKindSig,
24
25 -- Kind-checking types
26 -- No kind generalisation, no checkValidType
27 tcWildCardBinders,
28 kcHsTyVarBndrs,
29 tcHsLiftedType, tcHsOpenType,
30 tcHsLiftedTypeNC, tcHsOpenTypeNC,
31 tcLHsType, tcCheckLHsType,
32 tcHsContext, tcLHsPredType, tcInferApps, tcInferArgs,
33 solveEqualities, -- useful re-export
34
35 kindGeneralize,
36
37 -- Sort-checking kinds
38 tcLHsKind,
39
40 -- Pattern type signatures
41 tcHsPatSigType, tcPatSig, funAppCtxt
42 ) where
43
44 #include "HsVersions.h"
45
46 import HsSyn
47 import TcRnMonad
48 import TcEvidence
49 import TcEnv
50 import TcMType
51 import TcValidity
52 import TcUnify
53 import TcIface
54 import TcSimplify ( solveEqualities )
55 import TcType
56 import Type
57 import Kind
58 import RdrName( lookupLocalRdrOcc )
59 import Var
60 import VarSet
61 import TyCon
62 import ConLike
63 import DataCon
64 import TysPrim ( tYPE )
65 import Class
66 import Name
67 import NameEnv
68 import NameSet
69 import VarEnv
70 import TysWiredIn
71 import BasicTypes
72 import SrcLoc
73 import DynFlags ( ExtensionFlag( Opt_DataKinds, Opt_MonoLocalBinds
74 , Opt_TypeInType ) )
75 import Constants ( mAX_CTUPLE_SIZE )
76 import ErrUtils( MsgDoc )
77 import Unique
78 import Util
79 import UniqSupply
80 import Outputable
81 import FastString
82 import PrelNames hiding ( wildCardName )
83 import Pair
84
85 import Data.Maybe
86 import Control.Monad
87
88 {-
89 ----------------------------
90 General notes
91 ----------------------------
92
93 Unlike with expressions, type-checking types both does some checking and
94 desugars at the same time. This is necessary because we often want to perform
95 equality checks on the types right away, and it would be incredibly painful
96 to do this on un-desugared types. Luckily, desugared types are close enough
97 to HsTypes to make the error messages sane.
98
99 During type-checking, we perform as little validity checking as possible.
100 This is because some type-checking is done in a mutually-recursive knot, and
101 if we look too closely at the tycons, we'll loop. This is why we always must
102 use mkNakedTyConApp and mkNakedAppTys, etc., which never look at a tycon.
103 The mkNamed... functions don't uphold Type invariants, but zonkTcTypeToType
104 will repair this for us. Note that zonkTcType *is* safe within a knot, and
105 can be done repeatedly with no ill effect: it just squeezes out metavariables.
106
107 Generally, after type-checking, you will want to do validity checking, say
108 with TcValidity.checkValidType.
109
110 Validity checking
111 ~~~~~~~~~~~~~~~~~
112 Some of the validity check could in principle be done by the kind checker,
113 but not all:
114
115 - During desugaring, we normalise by expanding type synonyms. Only
116 after this step can we check things like type-synonym saturation
117 e.g. type T k = k Int
118 type S a = a
119 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
120 and then S is saturated. This is a GHC extension.
121
122 - Similarly, also a GHC extension, we look through synonyms before complaining
123 about the form of a class or instance declaration
124
125 - Ambiguity checks involve functional dependencies, and it's easier to wait
126 until knots have been resolved before poking into them
127
128 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
129 finished building the loop. So to keep things simple, we postpone most validity
130 checking until step (3).
131
132 Knot tying
133 ~~~~~~~~~~
134 During step (1) we might fault in a TyCon defined in another module, and it might
135 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
136 knot around type declarations with ARecThing, so that the fault-in code can get
137 the TyCon being defined.
138
139 %************************************************************************
140 %* *
141 Check types AND do validity checking
142 * *
143 ************************************************************************
144 -}
145
146 funsSigCtxt :: [Located Name] -> UserTypeCtxt
147 -- Returns FunSigCtxt, with no redundant-context-reporting,
148 -- form a list of located names
149 funsSigCtxt (L _ name1 : _) = FunSigCtxt name1 False
150 funsSigCtxt [] = panic "funSigCtxt"
151
152 addSigCtxt :: UserTypeCtxt -> LHsType Name -> TcM a -> TcM a
153 addSigCtxt ctxt sig_ty thing_inside
154 = setSrcSpan (getLoc sig_ty) $
155 addErrCtxt (pprSigCtxt ctxt empty (ppr sig_ty)) $
156 thing_inside
157
158 tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType Name -> TcM Type
159 -- This one is used when we have a LHsSigWcType, but in
160 -- a place where wildards aren't allowed. The renamer has
161 -- alrady checked this, so we can simply ignore it.
162 tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
163
164 kcHsSigType :: [Located Name] -> LHsSigType Name -> TcM ()
165 kcHsSigType names (HsIB { hsib_body = hs_ty
166 , hsib_vars = sig_vars })
167 = addSigCtxt (funsSigCtxt names) hs_ty $
168 discardResult $
169 tcImplicitTKBndrsType sig_vars $
170 tc_lhs_type typeLevelMode hs_ty liftedTypeKind
171
172 tcClassSigType :: [Located Name] -> LHsSigType Name -> TcM Type
173 -- Does not do validity checking; this must be done outside
174 -- the recursive class declaration "knot"
175 tcClassSigType names sig_ty
176 = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
177 do { ty <- tc_hs_sig_type sig_ty liftedTypeKind
178 ; kindGeneralizeType ty }
179
180 tcHsSigType :: UserTypeCtxt -> LHsSigType Name -> TcM Type
181 -- Does validity checking
182 tcHsSigType ctxt sig_ty
183 = addSigCtxt ctxt (hsSigType sig_ty) $
184 do { kind <- case expectedKindInCtxt ctxt of
185 AnythingKind -> newMetaKindVar
186 TheKind k -> return k
187 OpenKind -> do { lev <- newFlexiTyVarTy levityTy
188 ; return $ tYPE lev }
189 -- The kind is checked by checkValidType, and isn't necessarily
190 -- of kind * in a Template Haskell quote eg [t| Maybe |]
191
192 ; ty <- tc_hs_sig_type sig_ty kind
193 -- Generalise here: see Note [Kind generalisation]
194 ; ty <- maybeKindGeneralizeType ty -- also zonks
195 ; checkValidType ctxt ty
196 ; return ty }
197
198 tc_hs_sig_type :: LHsSigType Name -> Kind -> TcM Type
199 -- Does not do validity checking or zonking
200 tc_hs_sig_type (HsIB { hsib_body = hs_ty
201 , hsib_vars = sig_vars }) kind
202 = do { (tkvs, ty) <- solveEqualities $
203 tcImplicitTKBndrsType sig_vars $
204 tc_lhs_type typeLevelMode hs_ty kind
205 ; return (mkInvForAllTys tkvs ty) }
206
207 -----------------
208 tcHsDeriv :: LHsSigType Name -> TcM ([TyVar], Class, [Type], Kind)
209 -- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
210 -- Returns the C, [ty1, ty2, and the kind of C's *next* argument
211 -- E.g. class C (a::*) (b::k->k)
212 -- data T a b = ... deriving( C Int )
213 -- returns ([k], C, [k, Int], k->k)
214 -- Also checks that (C ty1 ty2 arg) :: Constraint
215 -- if arg has a suitable kind
216 tcHsDeriv hs_ty
217 = do { arg_kind <- newMetaKindVar
218 -- always safe to kind-generalize, because there
219 -- can be no covars in an outer scope
220 ; ty <- checkNoErrs $
221 -- avoid redundant error report with "illegal deriving", below
222 tc_hs_sig_type hs_ty (mkFunTy arg_kind constraintKind)
223 ; ty <- kindGeneralizeType ty -- also zonks
224 ; arg_kind <- zonkTcType arg_kind
225 ; let (tvs, pred) = splitForAllTys ty
226 ; case getClassPredTys_maybe pred of
227 Just (cls, tys) -> return (tvs, cls, tys, arg_kind)
228 Nothing -> failWithTc (ptext (sLit "Illegal deriving item") <+> quotes (ppr hs_ty)) }
229
230 tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt
231 -> LHsSigType Name
232 -> TcM ([TyVar], ThetaType, Class, [Type])
233 -- Like tcHsSigType, but for a class instance declaration
234 -- The significant difference is that we expect a /constraint/
235 -- not a /type/ for the bit after the '=>'.
236 tcHsClsInstType user_ctxt hs_inst_ty@(HsIB { hsib_vars = sig_vars
237 , hsib_body = hs_qual_ty })
238 -- An explicit forall in an instance declaration isn't
239 -- allowed, so there won't be any HsForAllTy here
240 = setSrcSpan (getLoc hs_qual_ty) $
241 do { (tkvs, phi_ty) <- solveEqualities $
242 tcImplicitTKBndrsType sig_vars $
243 do { theta <- tcHsContext cxt
244 ; head_ty' <- tc_lhs_type typeLevelMode
245 head_ty constraintKind
246 ; return (mkPhiTy theta head_ty') }
247 ; let inst_ty = mkInvForAllTys tkvs phi_ty
248 ; inst_ty <- kindGeneralizeType inst_ty
249 ; inst_ty <- zonkTcType inst_ty
250 ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
251 where
252 (cxt, head_ty) = splitLHsQualTy hs_qual_ty
253
254 -- Used for 'VECTORISE [SCALAR] instance' declarations
255 --
256 tcHsVectInst :: LHsSigType Name -> TcM (Class, [Type])
257 tcHsVectInst ty
258 | Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe (hsSigType ty)
259 -- Ignoring the binders looks pretty dodgy to me
260 = do { (cls, cls_kind) <- tcClass cls_name
261 ; (applied_class, _res_kind)
262 <- tcInferApps typeLevelMode cls_name (mkClassPred cls []) cls_kind tys
263 ; case tcSplitTyConApp_maybe applied_class of
264 Just (_tc, args) -> ASSERT( _tc == classTyCon cls )
265 return (cls, args)
266 _ -> failWithTc (text "Too many arguments passed to" <+> ppr cls_name) }
267 | otherwise
268 = failWithTc $ ptext (sLit "Malformed instance type")
269
270 {-
271 These functions are used during knot-tying in
272 type and class declarations, when we have to
273 separate kind-checking, desugaring, and validity checking
274
275
276 ************************************************************************
277 * *
278 The main kind checker: no validity checks here
279 %* *
280 %************************************************************************
281
282 First a couple of simple wrappers for kcHsType
283 -}
284
285 tcHsConArgType :: NewOrData -> LHsType Name -> TcM Type
286 -- Permit a bang, but discard it
287 tcHsConArgType NewType bty = tcHsLiftedType (getBangType bty)
288 -- Newtypes can't have bangs, but we don't check that
289 -- until checkValidDataCon, so do not want to crash here
290
291 tcHsConArgType DataType bty = tcHsOpenType (getBangType bty)
292 -- Can't allow an unlifted type for newtypes, because we're effectively
293 -- going to remove the constructor while coercing it to a lifted type.
294 -- And newtypes can't be bang'd
295
296 ---------------------------
297 tcHsOpenType, tcHsLiftedType,
298 tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType Name -> TcM TcType
299 -- Used for type signatures
300 -- Do not do validity checking
301 tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty
302 tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty
303
304 tcHsOpenTypeNC ty = do { ek <- ekOpen
305 ; tc_lhs_type typeLevelMode ty ek }
306 tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
307
308 -- Like tcHsType, but takes an expected kind
309 tcCheckLHsType :: LHsType Name -> Kind -> TcM Type
310 tcCheckLHsType hs_ty exp_kind
311 = addTypeCtxt hs_ty $
312 tc_lhs_type typeLevelMode hs_ty exp_kind
313
314 tcLHsType :: LHsType Name -> TcM (TcType, TcKind)
315 -- Called from outside: set the context
316 tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
317
318 ---------------------------
319 -- | Should we generalise the kind of this type?
320 -- We *should* generalise if the type is mentions no scoped type variables
321 -- or if NoMonoLocalBinds is set. Otherwise, nope.
322 decideKindGeneralisationPlan :: Type -> TcM Bool
323 decideKindGeneralisationPlan ty
324 = do { mono_locals <- xoptM Opt_MonoLocalBinds
325 ; in_scope <- getInLocalScope
326 ; let fvs = tyCoVarsOfTypeList ty
327 should_gen = not mono_locals || all (not . in_scope . getName) fvs
328 ; traceTc "decideKindGeneralisationPlan"
329 (vcat [ text "type:" <+> ppr ty
330 , text "ftvs:" <+> ppr fvs
331 , text "should gen?" <+> ppr should_gen ])
332 ; return should_gen }
333
334 maybeKindGeneralizeType :: TcType -> TcM Type
335 maybeKindGeneralizeType ty
336 = do { should_gen <- decideKindGeneralisationPlan ty
337 ; if should_gen
338 then kindGeneralizeType ty
339 else zonkTcType ty }
340
341 {-
342 ************************************************************************
343 * *
344 Type-checking modes
345 * *
346 ************************************************************************
347
348 The kind-checker is parameterised by a TcTyMode, which contains some
349 information about where we're checking a type.
350
351 The renamer issues errors about what it can. All errors issued here must
352 concern things that the renamer can't handle.
353
354 -}
355
356 data TcTyMode
357 = TcTyMode { mode_level :: TypeOrKind -- True <=> type, False <=> kind
358 -- used only for -XNoTypeInType errors
359 }
360
361 typeLevelMode :: TcTyMode
362 typeLevelMode = TcTyMode { mode_level = TypeLevel }
363
364 kindLevelMode :: TcTyMode
365 kindLevelMode = TcTyMode { mode_level = KindLevel }
366
367 -- switch to kind level
368 kindLevel :: TcTyMode -> TcTyMode
369 kindLevel mode = mode { mode_level = KindLevel }
370
371 {-
372 Note [Bidirectional type checking]
373 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
374 In expressions, whenever we see a polymorphic identifier, say `id`, we are
375 free to instantiate it with metavariables, knowing that we can always
376 re-generalize with type-lambdas when necessary. For example:
377
378 rank2 :: (forall a. a -> a) -> ()
379 x = rank2 id
380
381 When checking the body of `x`, we can instantiate `id` with a metavariable.
382 Then, when we're checking the application of `rank2`, we notice that we really
383 need a polymorphic `id`, and then re-generalize over the unconstrained
384 metavariable.
385
386 In types, however, we're not so lucky, because *we cannot re-generalize*!
387 There is no lambda. So, we must be careful only to instantiate at the last
388 possible moment, when we're sure we're never going to want the lost polymorphism
389 again. This is done in calls to tcInstBinders and tcInstBindersX.
390
391 To implement this behavior, we use bidirectional type checking, where we
392 explicitly think about whether we know the kind of the type we're checking
393 or not. Note that there is a difference between not knowing a kind and
394 knowing a metavariable kind: the metavariables are TauTvs, and cannot become
395 forall-quantified kinds. Previously (before dependent types), there were
396 no higher-rank kinds, and so we could instantiate early and be sure that
397 no types would have polymorphic kinds, and so we could always assume that
398 the kind of a type was a fresh metavariable. Not so anymore, thus the
399 need for two algorithms.
400
401 For HsType forms that can never be kind-polymorphic, we implement only the
402 "down" direction, where we safely assume a metavariable kind. For HsType forms
403 that *can* be kind-polymorphic, we implement just the "up" (functions with
404 "infer" in their name) version, as we gain nothing by also implementing the
405 "down" version.
406
407 Note [Future-proofing the type checker]
408 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
409 As discussed in Note [Bidirectional type checking], each HsType form is
410 handled in *either* tc_infer_hs_type *or* tc_hs_type. These functions
411 are mutually recursive, so that either one can work for any type former.
412 But, we want to make sure that our pattern-matches are complete. So,
413 we have a bunch of repetitive code just so that we get warnings if we're
414 missing any patterns.
415 -}
416
417 -- | Check and desugar a type, returning the core type and its
418 -- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
419 -- level.
420 tc_infer_lhs_type :: TcTyMode -> LHsType Name -> TcM (TcType, TcKind)
421 tc_infer_lhs_type mode (L span ty)
422 = setSrcSpan span $
423 do { traceTc "tc_infer_lhs_type:" (ppr ty)
424 ; tc_infer_hs_type mode ty }
425
426 -- | Infer the kind of a type and desugar. This is the "up" type-checker,
427 -- as described in Note [Bidirectional type checking]
428 tc_infer_hs_type :: TcTyMode -> HsType Name -> TcM (TcType, TcKind)
429 tc_infer_hs_type mode (HsTyVar (L _ tv)) = tcTyVar mode tv
430 tc_infer_hs_type mode (HsAppTy ty1 ty2)
431 = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
432 ; (fun_ty', fun_kind) <- tc_infer_lhs_type mode fun_ty
433 ; fun_kind' <- zonkTcType fun_kind
434 ; tcInferApps mode fun_ty fun_ty' fun_kind' arg_tys }
435 tc_infer_hs_type mode (HsParTy t) = tc_infer_lhs_type mode t
436 tc_infer_hs_type mode (HsOpTy lhs (L _ op) rhs)
437 | not (op `hasKey` funTyConKey)
438 = do { (op', op_kind) <- tcTyVar mode op
439 ; op_kind' <- zonkTcType op_kind
440 ; tcInferApps mode op op' op_kind' [lhs, rhs] }
441 tc_infer_hs_type mode (HsKindSig ty sig)
442 = do { sig' <- tc_lhs_kind (kindLevel mode) sig
443 ; ty' <- tc_lhs_type mode ty sig'
444 ; return (ty', sig') }
445 tc_infer_hs_type mode (HsDocTy ty _) = tc_infer_lhs_type mode ty
446 tc_infer_hs_type _ (HsCoreTy ty) = return (ty, typeKind ty)
447 tc_infer_hs_type mode other_ty
448 = do { kv <- newMetaKindVar
449 ; ty' <- tc_hs_type mode other_ty kv
450 ; return (ty', kv) }
451
452 tc_lhs_type :: TcTyMode -> LHsType Name -> TcKind -> TcM TcType
453 tc_lhs_type mode (L span ty) exp_kind
454 = setSrcSpan span $
455 do { traceTc "tc_lhs_type:" (ppr ty $$ ppr exp_kind)
456 ; tc_hs_type mode ty exp_kind }
457
458 ------------------------------------------
459 tc_fun_type :: TcTyMode -> LHsType Name -> LHsType Name -> TcKind -> TcM TcType
460 tc_fun_type mode ty1 ty2 exp_kind
461 = do { arg_lev <- newFlexiTyVarTy levityTy
462 ; res_lev <- newFlexiTyVarTy levityTy
463 ; ty1' <- tc_lhs_type mode ty1 (tYPE arg_lev)
464 ; ty2' <- tc_lhs_type mode ty2 (tYPE res_lev)
465 ; checkExpectedKind (mkNakedFunTy ty1' ty2') liftedTypeKind exp_kind }
466
467 ------------------------------------------
468 -- See also Note [Bidirectional type checking]
469 tc_hs_type :: TcTyMode -> HsType Name -> TcKind -> TcM TcType
470 tc_hs_type mode (HsParTy ty) exp_kind = tc_lhs_type mode ty exp_kind
471 tc_hs_type mode (HsDocTy ty _) exp_kind = tc_lhs_type mode ty exp_kind
472 tc_hs_type _ ty@(HsBangTy {}) _
473 -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
474 -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
475 -- bangs are invalid, so fail. (#7210)
476 = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
477 tc_hs_type _ ty@(HsRecTy _) _
478 -- Record types (which only show up temporarily in constructor
479 -- signatures) should have been removed by now
480 = failWithTc (ptext (sLit "Record syntax is illegal here:") <+> ppr ty)
481
482 -- This should never happen; type splices are expanded by the renamer
483 tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind
484 = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
485
486 ---------- Functions and applications
487 tc_hs_type mode (HsFunTy ty1 ty2) exp_kind
488 = tc_fun_type mode ty1 ty2 exp_kind
489
490 tc_hs_type mode (HsOpTy ty1 (L _ op) ty2) exp_kind
491 | op `hasKey` funTyConKey
492 = tc_fun_type mode ty1 ty2 exp_kind
493
494 --------- Foralls
495 tc_hs_type mode hs_ty@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
496 -- Do not kind-generalise here. See Note [Kind generalisation]
497 | isConstraintKind exp_kind
498 = failWithTc (hang (ptext (sLit "Illegal constraint:")) 2 (ppr hs_ty))
499
500 | otherwise
501 = fmap fst $
502 tcHsTyVarBndrs hs_tvs $ \ tvs' ->
503 -- Do not kind-generalise here! See Note [Kind generalisation]
504 -- Why exp_kind? See Note [Body kind of forall]
505 do { ty' <- tc_lhs_type mode ty exp_kind
506 ; let bound_vars = allBoundVariables ty'
507 ; return (mkNakedInvSigmaTy tvs' [] ty', bound_vars) }
508
509 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
510 = do { ctxt' <- tc_hs_context mode ctxt
511 ; ty' <- if null (unLoc ctxt) then -- Plain forall, no context
512 tc_lhs_type mode ty exp_kind
513 -- Why exp_kind? See Note [Body kind of forall]
514 else
515 -- If there is a context, then this forall is really a
516 -- _function_, so the kind of the result really is *
517 -- The body kind (result of the function) can be * or #, hence ekOpen
518 do { ek <- ekOpen
519 ; ty <- tc_lhs_type mode ty ek
520 ; checkExpectedKind ty liftedTypeKind exp_kind }
521
522 ; return (mkNakedPhiTy ctxt' ty') }
523
524 --------- Lists, arrays, and tuples
525 tc_hs_type mode (HsListTy elt_ty) exp_kind
526 = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
527 ; checkWiredInTyCon listTyCon
528 ; checkExpectedKind (mkListTy tau_ty) liftedTypeKind exp_kind }
529
530 tc_hs_type mode (HsPArrTy elt_ty) exp_kind
531 = do { MASSERT( isTypeLevel (mode_level mode) )
532 ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
533 ; checkWiredInTyCon parrTyCon
534 ; checkExpectedKind (mkPArrTy tau_ty) liftedTypeKind exp_kind }
535
536 -- See Note [Distinguishing tuple kinds] in HsTypes
537 -- See Note [Inferring tuple kinds]
538 tc_hs_type mode (HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind
539 -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
540 | Just tup_sort <- tupKindSort_maybe exp_kind
541 = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
542 tc_tuple mode tup_sort hs_tys exp_kind
543 | otherwise
544 = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
545 ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
546 ; kinds <- mapM zonkTcType kinds
547 -- Infer each arg type separately, because errors can be
548 -- confusing if we give them a shared kind. Eg Trac #7410
549 -- (Either Int, Int), we do not want to get an error saying
550 -- "the second argument of a tuple should have kind *->*"
551
552 ; let (arg_kind, tup_sort)
553 = case [ (k,s) | k <- kinds
554 , Just s <- [tupKindSort_maybe k] ] of
555 ((k,s) : _) -> (k,s)
556 [] -> (liftedTypeKind, BoxedTuple)
557 -- In the [] case, it's not clear what the kind is, so guess *
558
559 ; tys' <- sequence [ setSrcSpan loc $
560 checkExpectedKind ty kind arg_kind
561 | ((L loc _),ty,kind) <- zip3 hs_tys tys kinds ]
562
563 ; finish_tuple tup_sort tys' (map (const arg_kind) tys') exp_kind }
564
565
566 tc_hs_type mode (HsTupleTy hs_tup_sort tys) exp_kind
567 = tc_tuple mode tup_sort tys exp_kind
568 where
569 tup_sort = case hs_tup_sort of -- Fourth case dealt with above
570 HsUnboxedTuple -> UnboxedTuple
571 HsBoxedTuple -> BoxedTuple
572 HsConstraintTuple -> ConstraintTuple
573 _ -> panic "tc_hs_type HsTupleTy"
574
575
576 --------- Promoted lists and tuples
577 tc_hs_type mode (HsExplicitListTy _k tys) exp_kind
578 = do { tks <- mapM (tc_infer_lhs_type mode) tys
579 ; (taus', kind) <- unifyKinds tks
580 ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
581 ; checkExpectedKind ty (mkListTy kind) exp_kind }
582 where
583 mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
584 mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k]
585
586 tc_hs_type mode (HsExplicitTupleTy _ tys) exp_kind
587 = do { tks <- mapM (tc_infer_lhs_type mode) tys
588 ; let n = length tys
589 kind_con = tupleTyCon Boxed n
590 ty_con = promotedTupleDataCon Boxed n
591 (taus, ks) = unzip tks
592 tup_k = mkTyConApp kind_con ks
593 ; checkExpectedKind (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
594
595 --------- Constraint types
596 tc_hs_type mode (HsIParamTy n ty) exp_kind
597 = do { MASSERT( isTypeLevel (mode_level mode) )
598 ; ty' <- tc_lhs_type mode ty liftedTypeKind
599 ; let n' = mkStrLitTy $ hsIPNameFS n
600 ; checkExpectedKind (mkClassPred ipClass [n',ty'])
601 constraintKind exp_kind }
602
603 tc_hs_type mode (HsEqTy ty1 ty2) exp_kind
604 = do { (ty1', kind1) <- tc_infer_lhs_type mode ty1
605 ; (ty2', kind2) <- tc_infer_lhs_type mode ty2
606 ; ty2'' <- checkExpectedKind ty2' kind2 kind1
607 ; eq_tc <- tcLookupTyCon eqTyConName
608 ; let ty' = mkNakedTyConApp eq_tc [kind1, ty1', ty2'']
609 ; checkExpectedKind ty' constraintKind exp_kind }
610
611 --------- Literals
612 tc_hs_type _ (HsTyLit (HsNumTy _ n)) exp_kind
613 = do { checkWiredInTyCon typeNatKindCon
614 ; checkExpectedKind (mkNumLitTy n) typeNatKind exp_kind }
615
616 tc_hs_type _ (HsTyLit (HsStrTy _ s)) exp_kind
617 = do { checkWiredInTyCon typeSymbolKindCon
618 ; checkExpectedKind (mkStrLitTy s) typeSymbolKind exp_kind }
619
620 --------- Potentially kind-polymorphic types: call the "up" checker
621 -- See Note [Future-proofing the type checker]
622 tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
623 tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek
624 tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
625 tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
626 tc_hs_type mode ty@(HsCoreTy {}) ek = tc_infer_hs_type_ek mode ty ek
627
628 tc_hs_type _ (HsWildCardTy wc) exp_kind
629 = do { let name = wildCardName wc
630 ; tv <- tcLookupTyVar name
631 ; checkExpectedKind (mkTyVarTy tv) (tyVarKind tv) exp_kind }
632
633 -- disposed of by renamer
634 tc_hs_type _ ty@(HsAppsTy {}) _
635 = pprPanic "tc_hs_tyep HsAppsTy" (ppr ty)
636
637 ---------------------------
638 -- | Call 'tc_infer_hs_type' and check its result against an expected kind.
639 tc_infer_hs_type_ek :: TcTyMode -> HsType Name -> TcKind -> TcM TcType
640 tc_infer_hs_type_ek mode ty ek
641 = do { (ty', k) <- tc_infer_hs_type mode ty
642 ; checkExpectedKind ty' k ek }
643
644 ---------------------------
645 tupKindSort_maybe :: TcKind -> Maybe TupleSort
646 tupKindSort_maybe k
647 | Just (k', _) <- tcSplitCastTy_maybe k = tupKindSort_maybe k'
648 | Just k' <- coreView k = tupKindSort_maybe k'
649 | isConstraintKind k = Just ConstraintTuple
650 | isLiftedTypeKind k = Just BoxedTuple
651 | otherwise = Nothing
652
653 tc_tuple :: TcTyMode -> TupleSort -> [LHsType Name] -> TcKind -> TcM TcType
654 tc_tuple mode tup_sort tys exp_kind
655 = do { arg_kinds <- case tup_sort of
656 BoxedTuple -> return (nOfThem arity liftedTypeKind)
657 UnboxedTuple -> do { levs <- newFlexiTyVarTys arity levityTy
658 ; return $ map tYPE levs }
659 ConstraintTuple -> return (nOfThem arity constraintKind)
660 ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
661 ; finish_tuple tup_sort tau_tys arg_kinds exp_kind }
662 where
663 arity = length tys
664
665 finish_tuple :: TupleSort
666 -> [TcType] -- ^ argument types
667 -> [TcKind] -- ^ of these kinds
668 -> TcKind -- ^ expected kind of the whole tuple
669 -> TcM TcType
670 finish_tuple tup_sort tau_tys tau_kinds exp_kind
671 = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
672 ; let arg_tys = case tup_sort of
673 -- See also Note [Unboxed tuple levity vars] in TyCon
674 UnboxedTuple -> map (getLevityFromKind "finish_tuple") tau_kinds
675 ++ tau_tys
676 BoxedTuple -> tau_tys
677 ConstraintTuple -> tau_tys
678 ; tycon <- case tup_sort of
679 ConstraintTuple
680 | arity > mAX_CTUPLE_SIZE
681 -> failWith (bigConstraintTuple arity)
682 | otherwise -> tcLookupTyCon (cTupleTyConName arity)
683 BoxedTuple -> do { let tc = tupleTyCon Boxed arity
684 ; checkWiredInTyCon tc
685 ; return tc }
686 UnboxedTuple -> return (tupleTyCon Unboxed arity)
687 ; checkExpectedKind (mkTyConApp tycon arg_tys) res_kind exp_kind }
688 where
689 arity = length tau_tys
690 res_kind = case tup_sort of
691 UnboxedTuple -> unliftedTypeKind
692 BoxedTuple -> liftedTypeKind
693 ConstraintTuple -> constraintKind
694
695 bigConstraintTuple :: Arity -> MsgDoc
696 bigConstraintTuple arity
697 = hang (ptext (sLit "Constraint tuple arity too large:") <+> int arity
698 <+> parens (ptext (sLit "max arity =") <+> int mAX_CTUPLE_SIZE))
699 2 (ptext (sLit "Instead, use a nested tuple"))
700
701 ---------------------------
702 -- | Apply a type of a given kind to a list of arguments. This instantiates
703 -- invisible parameters as necessary. However, it does *not* necessarily
704 -- apply all the arguments, if the kind runs out of binders.
705 -- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.
706 -- These kinds should be used to instantiate invisible kind variables;
707 -- they come from an enclosing class for an associated type/data family.
708 -- This version will instantiate all invisible arguments left over after
709 -- the visible ones.
710 tcInferArgs :: Outputable fun
711 => fun -- ^ the function
712 -> TcKind -- ^ function kind (zonked)
713 -> Maybe (VarEnv Kind) -- ^ possibly, kind info (see above)
714 -> [LHsType Name] -- ^ args
715 -> TcM (TcKind, [TcType], [LHsType Name], Int)
716 -- ^ (result kind, typechecked args, untypechecked args, n)
717 tcInferArgs fun fun_kind mb_kind_info args
718 = do { (res_kind, args', leftovers, n)
719 <- tc_infer_args typeLevelMode fun fun_kind mb_kind_info args 1
720 -- now, we need to instantiate any remaining invisible arguments
721 ; let (invis_bndrs, really_res_kind) = splitPiTysInvisible res_kind
722 ; (subst, invis_args)
723 <- tcInstBindersX emptyTCvSubst mb_kind_info invis_bndrs
724 ; return ( substTy subst really_res_kind, args' `chkAppend` invis_args
725 , leftovers, n ) }
726
727 -- | See comments for 'tcInferArgs'. But this version does not instantiate
728 -- any remaining invisible arguments.
729 tc_infer_args :: Outputable fun
730 => TcTyMode
731 -> fun -- ^ the function
732 -> TcKind -- ^ function kind (zonked)
733 -> Maybe (VarEnv Kind) -- ^ possibly, kind info (see above)
734 -> [LHsType Name] -- ^ args
735 -> Int -- ^ number to start arg counter at
736 -> TcM (TcKind, [TcType], [LHsType Name], Int)
737 tc_infer_args mode orig_ty ki mb_kind_info orig_args n0
738 = do { traceTc "tcInferApps" (ppr ki $$ ppr orig_args)
739 ; go emptyTCvSubst ki orig_args n0 [] }
740 where
741 go subst fun_kind [] n acc
742 = return ( substTy subst fun_kind, reverse acc, [], n )
743 -- when we call this when checking type family patterns, we really
744 -- do want to instantiate all invisible arguments. During other
745 -- typechecking, we don't.
746
747 go subst fun_kind all_args n acc
748 | Just fun_kind' <- coreView fun_kind
749 = go subst fun_kind' all_args n acc
750
751 | Just tv <- getTyVar_maybe fun_kind
752 , Just fun_kind' <- lookupTyVar subst tv
753 = go subst fun_kind' all_args n acc
754
755 | (inv_bndrs, res_k) <- splitPiTysInvisible fun_kind
756 , not (null inv_bndrs)
757 = do { (subst', args') <- tcInstBindersX subst mb_kind_info inv_bndrs
758 ; go subst' res_k all_args n (reverse args' ++ acc) }
759
760 | Just (bndr, res_k) <- splitPiTy_maybe fun_kind
761 , arg:args <- all_args -- this actually has to succeed
762 = ASSERT( isVisibleBinder bndr )
763 do { let mode' | isNamedBinder bndr = kindLevel mode
764 | otherwise = mode
765 ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
766 tc_lhs_type mode' arg (substTy subst $ binderType bndr)
767 ; let subst' = case binderVar_maybe bndr of
768 Just tv -> extendTCvSubst subst tv arg'
769 Nothing -> subst
770 ; go subst' res_k args (n+1) (arg' : acc) }
771
772 | otherwise
773 = return (substTy subst fun_kind, reverse acc, all_args, n)
774
775 -- | Applies a type to a list of arguments. Always consumes all the
776 -- arguments.
777 tcInferApps :: Outputable fun
778 => TcTyMode
779 -> fun -- ^ Function (for printing only)
780 -> TcType -- ^ Function (could be knot-tied)
781 -> TcKind -- ^ Function kind (zonked)
782 -> [LHsType Name] -- ^ Args
783 -> TcM (TcType, TcKind) -- ^ (f args, result kind)
784 tcInferApps mode orig_ty ty ki args = go ty ki args 1
785 where
786 go fun fun_kind [] _ = return (fun, fun_kind)
787 go fun fun_kind args n
788 | Just fun_kind' <- coreView fun_kind
789 = go fun fun_kind' args n
790
791 | isPiTy fun_kind
792 = do { (res_kind, args', leftover_args, n')
793 <- tc_infer_args mode orig_ty fun_kind Nothing args n
794 ; go (mkNakedAppTys fun args') res_kind leftover_args n' }
795
796 go fun fun_kind all_args@(arg:args) n
797 = do { (co, arg_k, res_k) <- matchExpectedFunKind (length all_args)
798 fun fun_kind
799 ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
800 tc_lhs_type mode arg arg_k
801 ; go (mkNakedAppTy (fun `mkNakedCastTy` co) arg')
802 res_k args (n+1) }
803
804 ---------------------------
805 -- | This is used to instantiate binders when type-checking *types* only.
806 -- Precondition: all binders are invisible. See also Note [Bidirectional type checking]
807 tcInstBinders :: [TyBinder] -> TcM (TCvSubst, [TcType])
808 tcInstBinders = tcInstBindersX emptyTCvSubst Nothing
809
810 -- | This is used to instantiate binders when type-checking *types* only.
811 -- Precondition: all binders are invisible.
812 -- The @VarEnv Kind@ gives some known instantiations.
813 -- See also Note [Bidirectional type checking]
814 tcInstBindersX :: TCvSubst -> Maybe (VarEnv Kind)
815 -> [TyBinder] -> TcM (TCvSubst, [TcType])
816 tcInstBindersX subst mb_kind_info bndrs
817 = do { (subst, args) <- mapAccumLM (tcInstBinderX mb_kind_info) subst bndrs
818 ; traceTc "instantiating implicit dependent vars:"
819 (vcat $ zipWith (\bndr arg -> ppr bndr <+> text ":=" <+> ppr arg)
820 bndrs args)
821 ; return (subst, args) }
822
823 -- | Used only in *types*
824 tcInstBinderX :: Maybe (VarEnv Kind)
825 -> TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
826 tcInstBinderX mb_kind_info subst binder
827 | Just tv <- binderVar_maybe binder
828 = case lookup_tv tv of
829 Just ki -> return (extendTCvSubst subst tv ki, ki)
830 Nothing -> do { (subst', tv') <- tcInstTyVarX subst tv
831 ; return (subst', mkTyVarTy tv') }
832
833 -- This is the *only* constraint currently handled in types.
834 | Just (mk, role, k1, k2) <- get_pred_tys_maybe substed_ty
835 = do { let origin = TypeEqOrigin { uo_actual = k1
836 , uo_expected = k2
837 , uo_thing = Nothing }
838 ; co <- case role of
839 Nominal -> unifyKind noThing k1 k2
840 Representational -> emitWantedEq origin KindLevel role k1 k2
841 Phantom -> pprPanic "tcInstBinderX Phantom" (ppr binder)
842 ; arg' <- mk co k1 k2
843 ; return (subst, arg') }
844
845 | otherwise
846 = do { let (env, tidy_ty) = tidyOpenType emptyTidyEnv substed_ty
847 ; addErrTcM (env, text "Illegal constraint in a type:" <+> ppr tidy_ty)
848
849 -- just invent a new variable so that we can continue
850 ; u <- newUnique
851 ; let name = mkSysTvName u (fsLit "dict")
852 ; return (subst, mkTyVarTy $ mkTyVar name substed_ty) }
853
854 where
855 substed_ty = substTy subst (binderType binder)
856
857 lookup_tv tv = do { env <- mb_kind_info -- `Maybe` monad
858 ; lookupVarEnv env tv }
859
860 -- handle boxed equality constraints, because it's so easy
861 get_pred_tys_maybe ty
862 | Just (r, k1, k2) <- getEqPredTys_maybe ty
863 = Just (\co _ _ -> return $ mkCoercionTy co, r, k1, k2)
864 | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
865 = if | tc `hasKey` heqTyConKey
866 -> Just (mkHEqBoxTy, Nominal, k1, k2)
867 | otherwise
868 -> Nothing
869 | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
870 = if | tc `hasKey` eqTyConKey
871 -> Just (mkEqBoxTy, Nominal, k1, k2)
872 | tc `hasKey` coercibleTyConKey
873 -> Just (mkCoercibleBoxTy, Representational, k1, k2)
874 | otherwise
875 -> Nothing
876 | otherwise
877 = Nothing
878
879 -------------------------------
880 -- | This takes @a ~# b@ and returns @a ~~ b@.
881 mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
882 -- monadic just for convenience with mkEqBoxTy
883 mkHEqBoxTy co ty1 ty2
884 = return $
885 mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
886 where k1 = typeKind ty1
887 k2 = typeKind ty2
888
889 -- | This takes @a ~# b@ and returns @a ~ b@.
890 mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
891 mkEqBoxTy co ty1 ty2
892 = do { eq_tc <- tcLookupTyCon eqTyConName
893 ; let [datacon] = tyConDataCons eq_tc
894 ; hetero <- mkHEqBoxTy co ty1 ty2
895 ; return $ mkTyConApp (promoteDataCon datacon) [k, ty1, ty2, hetero] }
896 where k = typeKind ty1
897
898 -- | This takes @a ~R# b@ and returns @Coercible a b@.
899 mkCoercibleBoxTy :: TcCoercion -> Type -> Type -> TcM Type
900 -- monadic just for convenience with mkEqBoxTy
901 mkCoercibleBoxTy co ty1 ty2
902 = do { return $
903 mkTyConApp (promoteDataCon coercibleDataCon)
904 [k, ty1, ty2, mkCoercionTy co] }
905 where k = typeKind ty1
906
907
908 --------------------------
909 checkExpectedKind :: TcType -- the type whose kind we're checking
910 -> TcKind -- the known kind of that type, k
911 -> TcKind -- the expected kind, exp_kind
912 -> TcM TcType -- a possibly-inst'ed, casted type :: exp_kind
913 -- Instantiate a kind (if necessary) and then call unifyType
914 -- (checkExpectedKind ty act_kind exp_kind)
915 -- checks that the actual kind act_kind is compatible
916 -- with the expected kind exp_kind
917 checkExpectedKind ty act_kind exp_kind
918 = do { (ty', act_kind') <- instantiate ty act_kind exp_kind
919 ; let origin = TypeEqOrigin { uo_actual = act_kind'
920 , uo_expected = exp_kind
921 , uo_thing = Just $ mkTypeErrorThing ty'
922 }
923 ; co_k <- uType origin KindLevel act_kind' exp_kind
924 ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
925 , ppr exp_kind
926 , ppr co_k ])
927 ; let result_ty = ty' `mkNakedCastTy` co_k
928 ; return result_ty }
929 where
930 -- we need to make sure that both kinds have the same number of implicit
931 -- foralls out front. If the actual kind has more, instantiate accordingly.
932 -- Otherwise, just pass the type & kind through -- the errors are caught
933 -- in unifyType.
934 instantiate :: TcType -- the type
935 -> TcKind -- of this kind
936 -> TcKind -- but expected to be of this one
937 -> TcM ( TcType -- the inst'ed type
938 , TcKind ) -- its new kind
939 instantiate ty act_ki exp_ki
940 = let (exp_bndrs, _) = splitPiTysInvisible exp_ki in
941 instantiateTyN (length exp_bndrs) ty act_ki
942
943 -- | Instantiate a type to have at most @n@ invisible arguments.
944 instantiateTyN :: Int -- ^ @n@
945 -> TcType -- ^ the type
946 -> TcKind -- ^ its kind
947 -> TcM (TcType, TcKind) -- ^ The inst'ed type with kind
948 instantiateTyN n ty ki
949 = let (bndrs, inner_ki) = splitPiTysInvisible ki
950 num_to_inst = length bndrs - n
951 -- NB: splitAt is forgiving with invalid numbers
952 (inst_bndrs, leftover_bndrs) = splitAt num_to_inst bndrs
953 in
954 if num_to_inst <= 0 then return (ty, ki) else
955 do { (subst, inst_args) <- tcInstBinders inst_bndrs
956 ; let rebuilt_ki = mkForAllTys leftover_bndrs inner_ki
957 ki' = substTy subst rebuilt_ki
958 ; return (mkNakedAppTys ty inst_args, ki') }
959
960 ---------------------------
961 tcHsContext :: LHsContext Name -> TcM [PredType]
962 tcHsContext = tc_hs_context typeLevelMode
963
964 tcLHsPredType :: LHsType Name -> TcM PredType
965 tcLHsPredType = tc_lhs_pred typeLevelMode
966
967 tc_hs_context :: TcTyMode -> LHsContext Name -> TcM [PredType]
968 tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)
969
970 tc_lhs_pred :: TcTyMode -> LHsType Name -> TcM PredType
971 tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
972
973 ---------------------------
974 tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
975 -- See Note [Type checking recursive type and class declarations]
976 -- in TcTyClsDecls
977 tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
978 = do { traceTc "lk1" (ppr name)
979 ; thing <- tcLookup name
980 ; case thing of
981 ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
982
983 AThing kind -> do { data_kinds <- xoptM Opt_DataKinds
984 ; unless (isTypeLevel (mode_level mode) ||
985 data_kinds) $
986 promotionErr name NoDataKinds
987 ; tc <- get_loopy_tc name
988 ; return (mkNakedTyConApp tc [], kind) }
989 -- mkNakedTyConApp: see Note [Type-checking inside the knot]
990 -- NB: we really should check if we're at the kind level
991 -- and if the tycon is promotable if -XNoTypeInType is set.
992 -- But this is a terribly large amount of work! Not worth it.
993
994 AGlobal (ATyCon tc)
995 -> do { type_in_type <- xoptM Opt_TypeInType
996 ; data_kinds <- xoptM Opt_DataKinds
997 ; unless (isTypeLevel (mode_level mode) ||
998 data_kinds ||
999 isKindTyCon tc) $
1000 promotionErr name NoDataKinds
1001 ; unless (isTypeLevel (mode_level mode) ||
1002 type_in_type ||
1003 isLegacyPromotableTyCon tc) $
1004 promotionErr name NoTypeInTypeTC
1005 ; return (mkTyConApp tc [], tyConKind tc) }
1006
1007 AGlobal (AConLike (RealDataCon dc))
1008 -> do { data_kinds <- xoptM Opt_DataKinds
1009 ; unless (data_kinds || specialPromotedDc dc) $
1010 promotionErr name NoDataKinds
1011 ; type_in_type <- xoptM Opt_TypeInType
1012 ; unless ( type_in_type ||
1013 ( isTypeLevel (mode_level mode) &&
1014 isLegacyPromotableDataCon dc ) ||
1015 ( isKindLevel (mode_level mode) &&
1016 specialPromotedDc dc ) ) $
1017 promotionErr name NoTypeInTypeDC
1018 ; let tc = promoteDataCon dc
1019 ; return (mkNakedTyConApp tc [], tyConKind tc) }
1020
1021 APromotionErr err -> promotionErr name err
1022
1023 _ -> wrongThingErr "type" thing name }
1024 where
1025 get_loopy_tc name
1026 = do { env <- getGblEnv
1027 ; case lookupNameEnv (tcg_type_env env) name of
1028 Just (ATyCon tc) -> return tc
1029 _ -> return (aThingErr "tcTyVar" name) }
1030
1031 tcClass :: Name -> TcM (Class, TcKind)
1032 tcClass cls -- Must be a class
1033 = do { thing <- tcLookup cls
1034 ; case thing of
1035 AThing kind -> return (aThingErr "tcClass" cls, kind)
1036 AGlobal (ATyCon tc)
1037 | Just cls <- tyConClass_maybe tc
1038 -> return (cls, tyConKind tc)
1039 _ -> wrongThingErr "class" thing cls }
1040
1041
1042 aThingErr :: String -> Name -> b
1043 -- The type checker for types is sometimes called simply to
1044 -- do *kind* checking; and in that case it ignores the type
1045 -- returned. Which is a good thing since it may not be available yet!
1046 aThingErr str x = pprPanic "AThing evaluated unexpectedly" (text str <+> ppr x)
1047
1048 {-
1049 Note [Type-checking inside the knot]
1050 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1051 Suppose we are checking the argument types of a data constructor. We
1052 must zonk the types before making the DataCon, because once built we
1053 can't change it. So we must traverse the type.
1054
1055 BUT the parent TyCon is knot-tied, so we can't look at it yet.
1056
1057 So we must be careful not to use "smart constructors" for types that
1058 look at the TyCon or Class involved.
1059
1060 * Hence the use of mkNakedXXX functions. These do *not* enforce
1061 the invariants (for example that we use (ForAllTy (Anon s) t) rather
1062 than (TyConApp (->) [s,t])).
1063
1064 * The zonking functions establish invariants (even zonkTcType, a change from
1065 previous behaviour). So we must never inspect the result of a
1066 zonk that might mention a knot-tied TyCon. This is generally OK
1067 because we zonk *kinds* while kind-checking types. And the TyCons
1068 in kinds shouldn't be knot-tied, because they come from a previous
1069 mutually recursive group.
1070
1071 * TcHsSyn.zonkTcTypeToType also can safely check/establish
1072 invariants.
1073
1074 This is horribly delicate. I hate it. A good example of how
1075 delicate it is can be seen in Trac #7903.
1076
1077 Note [Body kind of a forall]
1078 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1079 The body of a forall is usually a type, but in principle
1080 there's no reason to prohibit *unlifted* types.
1081 In fact, GHC can itself construct a function with an
1082 unboxed tuple inside a for-all (via CPR analyis; see
1083 typecheck/should_compile/tc170).
1084
1085 Moreover in instance heads we get forall-types with
1086 kind Constraint.
1087
1088 Moreover if we have a signature
1089 f :: Int#
1090 then we represent it as (HsForAll Implicit [] [] Int#). And this must
1091 be legal! We can't drop the empty forall until *after* typechecking
1092 the body because of kind polymorphism:
1093 Typeable :: forall k. k -> Constraint
1094 data Apply f t = Apply (f t)
1095 -- Apply :: forall k. (k -> *) -> k -> *
1096 instance Typeable Apply where ...
1097 Then the dfun has type
1098 df :: forall k. Typeable ((k->*) -> k -> *) (Apply k)
1099
1100 f :: Typeable Apply
1101
1102 f :: forall (t:k->*) (a:k). t a -> t a
1103
1104 class C a b where
1105 op :: a b -> Typeable Apply
1106
1107 data T a = MkT (Typeable Apply)
1108 | T2 a
1109 T :: * -> *
1110 MkT :: forall k. (Typeable ((k->*) -> k -> *) (Apply k)) -> T a
1111
1112 f :: (forall (k:*). forall (t:: k->*) (a:k). t a -> t a) -> Int
1113 f :: (forall a. a -> Typeable Apply) -> Int
1114
1115 So we *must* keep the HsForAll on the instance type
1116 HsForAll Implicit [] [] (Typeable Apply)
1117 so that we do kind generalisation on it.
1118
1119 It's tempting to check that the body kind is either * or #. But this is
1120 wrong. For example:
1121
1122 class C a b
1123 newtype N = Mk Foo deriving (C a)
1124
1125 We're doing newtype-deriving for C. But notice how `a` isn't in scope in
1126 the predicate `C a`. So we quantify, yielding `forall a. C a` even though
1127 `C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
1128 convenient. Bottom line: don't check for * or # here.
1129
1130 Note [Inferring tuple kinds]
1131 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1132 Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
1133 we try to figure out whether it's a tuple of kind * or Constraint.
1134 Step 1: look at the expected kind
1135 Step 2: infer argument kinds
1136
1137 If after Step 2 it's not clear from the arguments that it's
1138 Constraint, then it must be *. Once having decided that we re-check
1139 the Check the arguments again to give good error messages
1140 in eg. `(Maybe, Maybe)`
1141
1142 Note that we will still fail to infer the correct kind in this case:
1143
1144 type T a = ((a,a), D a)
1145 type family D :: Constraint -> Constraint
1146
1147 While kind checking T, we do not yet know the kind of D, so we will default the
1148 kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
1149
1150 Note [Desugaring types]
1151 ~~~~~~~~~~~~~~~~~~~~~~~
1152 The type desugarer is phase 2 of dealing with HsTypes. Specifically:
1153
1154 * It transforms from HsType to Type
1155
1156 * It zonks any kinds. The returned type should have no mutable kind
1157 or type variables (hence returning Type not TcType):
1158 - any unconstrained kind variables are defaulted to (Any *) just
1159 as in TcHsSyn.
1160 - there are no mutable type variables because we are
1161 kind-checking a type
1162 Reason: the returned type may be put in a TyCon or DataCon where
1163 it will never subsequently be zonked.
1164
1165 You might worry about nested scopes:
1166 ..a:kappa in scope..
1167 let f :: forall b. T '[a,b] -> Int
1168 In this case, f's type could have a mutable kind variable kappa in it;
1169 and we might then default it to (Any *) when dealing with f's type
1170 signature. But we don't expect this to happen because we can't get a
1171 lexically scoped type variable with a mutable kind variable in it. A
1172 delicate point, this. If it becomes an issue we might need to
1173 distinguish top-level from nested uses.
1174
1175 Moreover
1176 * it cannot fail,
1177 * it does no unifications
1178 * it does no validity checking, except for structural matters, such as
1179 (a) spurious ! annotations.
1180 (b) a class used as a type
1181
1182 Note [Kind of a type splice]
1183 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1184 Consider these terms, each with TH type splice inside:
1185 [| e1 :: Maybe $(..blah..) |]
1186 [| e2 :: $(..blah..) |]
1187 When kind-checking the type signature, we'll kind-check the splice
1188 $(..blah..); we want to give it a kind that can fit in any context,
1189 as if $(..blah..) :: forall k. k.
1190
1191 In the e1 example, the context of the splice fixes kappa to *. But
1192 in the e2 example, we'll desugar the type, zonking the kind unification
1193 variables as we go. When we encounter the unconstrained kappa, we
1194 want to default it to '*', not to (Any *).
1195
1196
1197 Help functions for type applications
1198 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1199 -}
1200
1201 addTypeCtxt :: LHsType Name -> TcM a -> TcM a
1202 -- Wrap a context around only if we want to show that contexts.
1203 -- Omit invisble ones and ones user's won't grok
1204 addTypeCtxt (L _ ty) thing
1205 = addErrCtxt doc thing
1206 where
1207 doc = ptext (sLit "In the type") <+> quotes (ppr ty)
1208
1209 {-
1210 ************************************************************************
1211 * *
1212 Type-variable binders
1213 %* *
1214 %************************************************************************
1215
1216 Note [Scope-check inferred kinds]
1217 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1218 Consider
1219
1220 data SameKind :: k -> k -> *
1221 foo :: forall a (b :: Proxy a) (c :: Proxy d). SameKind b c
1222
1223 d has no binding site. So it gets bound implicitly, at the top. The
1224 problem is that d's kind mentions `a`. So it's all ill-scoped.
1225
1226 The way we check for this is to gather all variables *bound* in a
1227 type variable's scope. The type variable's kind should not mention
1228 any of these variables. That is, d's kind can't mention a, b, or c.
1229 We can't just check to make sure that d's kind is in scope, because
1230 we might be about to kindGeneralize.
1231
1232 A little messy, but it works.
1233
1234 -}
1235
1236 tcWildCardBinders :: [Name]
1237 -> ([(Name, TcTyVar)] -> TcM a)
1238 -> TcM a
1239 -- Use the Unique form the specified Name; don't clone it. There is
1240 -- no need to clone, and not doing so avoids the need to return a list
1241 -- of pairs to bring into scope.
1242 tcWildCardBinders wcs thing_inside
1243 = do { wcs <- mapM new_wildcard wcs
1244 ; tcExtendTyVarEnv2 wcs $
1245 thing_inside wcs }
1246 where
1247 new_wildcard :: Name -> TcM (Name, TcTyVar)
1248 new_wildcard name = do { kind <- newMetaKindVar
1249 ; tv <- newFlexiTyVar kind
1250 ; return (name, tv) }
1251
1252 -- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
1253 -- user-supplied kind signature (CUSK), generalise the result.
1254 -- Used in 'getInitialKind' (for tycon kinds and other kinds)
1255 -- and in kind-checking (but not for tycon kinds, which are checked with
1256 -- tcTyClDecls). See also Note [Complete user-supplied kind signatures] in
1257 -- HsDecls.
1258 --
1259 -- This function does not do telescope checking.
1260 kcHsTyVarBndrs :: Bool -- ^ True <=> the decl being checked has a CUSK
1261 -> LHsQTyVars Name
1262 -> ([TyVar] -> [TyVar] -> TcM (Kind, r))
1263 -- ^ the result kind, possibly with other info
1264 -- ^ args are implicit vars, explicit vars
1265 -> TcM (Kind, r) -- ^ The full kind of the thing being declared,
1266 -- with the other info
1267 kcHsTyVarBndrs cusk (HsQTvs { hsq_implicit = kv_ns
1268 , hsq_explicit = hs_tvs }) thing_inside
1269 = do { meta_kvs <- mapM (const newMetaKindVar) kv_ns
1270 ; kvs <- if cusk
1271 then return $ zipWith new_skolem_tv kv_ns meta_kvs
1272 -- the names must line up in splitTelescopeTvs
1273 else zipWithM newSigTyVar kv_ns meta_kvs
1274 ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $
1275 do { (full_kind, _, stuff) <- bind_telescope hs_tvs (thing_inside kvs)
1276 ; let qkvs = filter (not . isMetaTyVar) $
1277 tyCoVarsOfTypeWellScoped full_kind
1278
1279 -- the free non-meta variables in the returned kind will
1280 -- contain both *mentioned* kind vars and *unmentioned* kind
1281 -- vars (See case (1) under Note [Typechecking telescopes])
1282 gen_kind = if cusk
1283 then mkInvForAllTys qkvs $ full_kind
1284 else full_kind
1285 ; return (gen_kind, stuff) } }
1286 where
1287 -- there may be dependency between the explicit "ty" vars. So, we have
1288 -- to handle them one at a time. We also need to build up a full kind
1289 -- here, because this is the place we know whether to use a FunTy or a
1290 -- ForAllTy. We prefer using an anonymous binder over a trivial named
1291 -- binder. If a user wants a trivial named one, use an explicit kind
1292 -- signature.
1293 bind_telescope :: [LHsTyVarBndr Name]
1294 -> ([TyVar] -> TcM (Kind, r))
1295 -> TcM (Kind, VarSet, r)
1296 bind_telescope [] thing
1297 = do { (res_kind, stuff) <- thing []
1298 ; return (res_kind, tyCoVarsOfType res_kind, stuff) }
1299 bind_telescope (L _ hs_tv : hs_tvs) thing
1300 = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
1301 ; (res_kind, fvs, stuff) <- bind_unless_scoped tv_pair $
1302 bind_telescope hs_tvs $ \tvs ->
1303 thing (tv:tvs)
1304 -- we must be *lazy* in res_kind and fvs (assuming that the
1305 -- caller of kcHsTyVarBndrs is, too), as sometimes these hold
1306 -- panics. See kcConDecl.
1307 ; k <- zonkTcType (tyVarKind tv)
1308 ; let k_fvs = tyCoVarsOfType k
1309 (bndr, fvs')
1310 | tv `elemVarSet` fvs
1311 = ( mkNamedBinder tv Visible
1312 , fvs `delVarSet` tv `unionVarSet` k_fvs )
1313 | otherwise
1314 = (mkAnonBinder k, fvs `unionVarSet` k_fvs)
1315
1316 ; return ( mkForAllTy bndr res_kind, fvs', stuff ) }
1317
1318 -- | Bind the tyvar in the env't unless the bool is True
1319 bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a
1320 bind_unless_scoped (_, True) thing_inside = thing_inside
1321 bind_unless_scoped (tv, False) thing_inside
1322 = tcExtendTyVarEnv [tv] thing_inside
1323
1324 kc_hs_tv :: HsTyVarBndr Name -> TcM (TcTyVar, Bool)
1325 kc_hs_tv hs_tvb
1326 = do { (tv, scoped) <- tcHsTyVarBndr_Scoped hs_tvb
1327
1328 -- in the CUSK case, we want to default any un-kinded tyvars
1329 -- See Note [Complete user-supplied kind signatures] in HsDecls
1330 ; case hs_tvb of
1331 UserTyVar {}
1332 | cusk
1333 , not scoped -- don't default class tyvars
1334 -> discardResult $
1335 unifyKind (Just (mkTyVarTy tv)) liftedTypeKind
1336 (tyVarKind tv)
1337 _ -> return ()
1338
1339 ; return (tv, scoped) }
1340
1341 tcImplicitTKBndrs :: [Name]
1342 -> TcM (a, TyVarSet) -- vars are bound somewhere in the scope
1343 -- see Note [Scope-check inferred kinds]
1344 -> TcM ([TcTyVar], a)
1345 tcImplicitTKBndrs = tcImplicitTKBndrsX tcHsTyVarName
1346
1347 -- | Convenient specialization
1348 tcImplicitTKBndrsType :: [Name]
1349 -> TcM Type
1350 -> TcM ([TcTyVar], Type)
1351 tcImplicitTKBndrsType var_ns thing_inside
1352 = tcImplicitTKBndrs var_ns $
1353 do { res_ty <- thing_inside
1354 ; return (res_ty, allBoundVariables res_ty) }
1355
1356 -- this more general variant is needed in tcHsPatSigType.
1357 -- See Note [Pattern signature binders]
1358 tcImplicitTKBndrsX :: (Name -> TcM (TcTyVar, Bool)) -- new_tv function
1359 -> [Name]
1360 -> TcM (a, TyVarSet)
1361 -> TcM ([TcTyVar], a)
1362 -- Returned TcTyVars have the supplied Names
1363 -- i.e. no cloning of fresh names
1364 tcImplicitTKBndrsX new_tv var_ns thing_inside
1365 = do { tkvs_pairs <- mapM new_tv var_ns
1366 ; let must_scope_tkvs = [ tkv | (tkv, False) <- tkvs_pairs ]
1367 tkvs = map fst tkvs_pairs
1368 ; (result, bound_tvs) <- tcExtendTyVarEnv must_scope_tkvs $
1369 thing_inside
1370
1371 -- it's possible that we guessed the ordering of variables
1372 -- wrongly. Adjust.
1373 ; tkvs <- mapM zonkTyCoVarKind tkvs
1374 ; let extra = text "NB: Implicitly-bound variables always come" <+>
1375 text "before other ones."
1376 ; checkValidInferredKinds tkvs bound_tvs extra
1377
1378 ; let final_tvs = toposortTyVars tkvs
1379 ; traceTc "tcImplicitTKBndrs" (ppr var_ns $$ ppr final_tvs)
1380
1381 ; return (final_tvs, result) }
1382
1383 tcHsTyVarBndrs :: [LHsTyVarBndr Name]
1384 -> ([TyVar] -> TcM (a, TyVarSet))
1385 -- ^ Thing inside returns the set of variables bound
1386 -- in the scope. See Note [Scope-check inferred kinds]
1387 -> TcM (a, TyVarSet) -- ^ returns augmented bound vars
1388 -- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
1389 tcHsTyVarBndrs orig_hs_tvs thing_inside
1390 = go orig_hs_tvs $ \ tvs ->
1391 do { (result, bound_tvs) <- thing_inside tvs
1392
1393 -- Issue an error if the ordering is bogus.
1394 -- See Note [Bad telescopes] in TcValidity.
1395 ; tvs <- checkZonkValidTelescope (interppSP orig_hs_tvs) tvs empty
1396 ; checkValidInferredKinds tvs bound_tvs empty
1397
1398 ; traceTc "tcHsTyVarBndrs" $
1399 vcat [ text "Hs vars:" <+> ppr orig_hs_tvs
1400 , text "tvs:" <+> sep (map pprTvBndr tvs) ]
1401
1402 ; return (result, bound_tvs `unionVarSet` mkVarSet tvs)
1403 }
1404 where
1405 go [] thing = thing []
1406 go (L _ hs_tv : hs_tvs) thing
1407 = do { tv <- tcHsTyVarBndr hs_tv
1408 ; tcExtendTyVarEnv [tv] $
1409 go hs_tvs $ \ tvs ->
1410 thing (tv : tvs) }
1411
1412 tcHsTyVarBndr :: HsTyVarBndr Name -> TcM TcTyVar
1413 -- Return a type variable initialised with a kind variable.
1414 -- Typically the Kind inside the HsTyVarBndr will be a tyvar
1415 -- with a mutable kind in it.
1416 -- NB: These variables must not be in scope. This function
1417 -- is not appropriate for use with associated types, for example.
1418 --
1419 -- Returned TcTyVar has the same name; no cloning
1420 --
1421 -- See also Note [Associated type tyvar names] in Class
1422 tcHsTyVarBndr (UserTyVar (L _ name))
1423 = do { kind <- newMetaKindVar
1424 ; return (mkTcTyVar name kind (SkolemTv False)) }
1425 tcHsTyVarBndr (KindedTyVar (L _ name) kind)
1426 = do { kind <- tcLHsKind kind
1427 ; return (mkTcTyVar name kind (SkolemTv False)) }
1428
1429 -- | Type-check a user-written TyVarBndr, which binds a variable
1430 -- that might already be in scope (e.g., in an associated type declaration)
1431 -- The second return value says whether the variable is in scope (True)
1432 -- or not (False).
1433 tcHsTyVarBndr_Scoped :: HsTyVarBndr Name -> TcM (TcTyVar, Bool)
1434 tcHsTyVarBndr_Scoped (UserTyVar (L _ name))
1435 = tcHsTyVarName name
1436 tcHsTyVarBndr_Scoped (KindedTyVar (L _ name) lhs_kind)
1437 = do { tv_pair@(tv, _) <- tcHsTyVarName name
1438 ; kind <- tcLHsKind lhs_kind
1439 -- for a scoped variable: make sure annotation is consistent
1440 -- for an unscoped variable: unify the meta-tyvar kind
1441 -- either way: we can ignore the resulting coercion
1442 ; discardResult $ unifyKind (Just (mkTyVarTy tv)) kind (tyVarKind tv)
1443 ; return tv_pair }
1444
1445 -- | Produce a tyvar of the given name (with a meta-tyvar kind). If
1446 -- the name is already in scope, return the scoped variable. The
1447 -- second return value says whether the variable is in scope (True)
1448 -- or not (False). (Use this for associated types, for example.)
1449 tcHsTyVarName :: Name -> TcM (TcTyVar, Bool)
1450 tcHsTyVarName name
1451 = do { mb_tv <- tcLookupLcl_maybe name
1452 ; case mb_tv of
1453 Just (ATyVar _ tv) -> return (tv, True)
1454 _ -> do { kind <- newMetaKindVar
1455 ; return (mkTcTyVar name kind vanillaSkolemTv, False) }}
1456
1457 -- makes a new skolem tv
1458 new_skolem_tv :: Name -> Kind -> TcTyVar
1459 new_skolem_tv n k = mkTcTyVar n k vanillaSkolemTv
1460
1461 ------------------
1462 kindGeneralizeType :: Type -> TcM Type
1463 kindGeneralizeType ty
1464 = do { kvs <- kindGeneralize ty
1465 ; zonkTcType (mkInvForAllTys kvs ty) }
1466
1467 kindGeneralize :: TcType -> TcM [KindVar]
1468 kindGeneralize ty
1469 = do { gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
1470 ; kvs <- zonkTcTypeAndFV ty
1471 ; quantifyTyVars gbl_tvs (Pair kvs emptyVarSet) }
1472
1473 {-
1474 Note [Kind generalisation]
1475 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1476 We do kind generalisation only at the outer level of a type signature.
1477 For example, consider
1478 T :: forall k. k -> *
1479 f :: (forall a. T a -> Int) -> Int
1480 When kind-checking f's type signature we generalise the kind at
1481 the outermost level, thus:
1482 f1 :: forall k. (forall (a:k). T k a -> Int) -> Int -- YES!
1483 and *not* at the inner forall:
1484 f2 :: (forall k. forall (a:k). T k a -> Int) -> Int -- NO!
1485 Reason: same as for HM inference on value level declarations,
1486 we want to infer the most general type. The f2 type signature
1487 would be *less applicable* than f1, because it requires a more
1488 polymorphic argument.
1489
1490 NB: There are no explicit kind variables written in f's signature.
1491 When there are, the renamer adds these kind variables to the list of
1492 variables bound by the forall, so you can indeed have a type that's
1493 higher-rank in its kind. But only by explicit request.
1494
1495 Note [Kinds of quantified type variables]
1496 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1497 tcTyVarBndrsGen quantifies over a specified list of type variables,
1498 *and* over the kind variables mentioned in the kinds of those tyvars.
1499
1500 Note that we must zonk those kinds (obviously) but less obviously, we
1501 must return type variables whose kinds are zonked too. Example
1502 (a :: k7) where k7 := k9 -> k9
1503 We must return
1504 [k9, a:k9->k9]
1505 and NOT
1506 [k9, a:k7]
1507 Reason: we're going to turn this into a for-all type,
1508 forall k9. forall (a:k7). blah
1509 which the type checker will then instantiate, and instantiate does not
1510 look through unification variables!
1511
1512 Hence using zonked_kinds when forming tvs'.
1513
1514 Note [Typechecking telescopes]
1515 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1516 The function tcTyClTyVars has to bind the scoped type and kind
1517 variables in a telescope. For example:
1518
1519 class Foo k (t :: Proxy k -> k2) where ...
1520
1521 By the time [kt]cTyClTyVars is called, we know *something* about the kind of Foo,
1522 at least that it has the form
1523
1524 Foo :: forall (k2 :: mk2). forall (k :: mk1) -> (Proxy mk1 k -> k2) -> Constraint
1525
1526 if it has a CUSK (Foo does not, in point of fact) or
1527
1528 Foo :: forall (k :: mk1) -> (Proxy mk1 k -> k2) -> Constraint
1529
1530 if it does not, where mk1 and mk2 are meta-kind variables (mk1, mk2 :: *).
1531
1532 When calling tcTyClTyVars, this kind is further generalized w.r.t. any
1533 free variables appearing in mk1 or mk2. So, mk_tvs must handle
1534 that possibility. Perhaps we discover that mk1 := Maybe k3 and mk2 := *,
1535 so we have
1536
1537 Foo :: forall (k3 :: *). forall (k2 :: *). forall (k :: Maybe k3) ->
1538 (Proxy (Maybe k3) k -> k2) -> Constraint
1539
1540 We now have several sorts of variables to think about:
1541 1) The variable k3 is not mentioned in the source at all. It is neither
1542 explicitly bound nor ever used. It is *not* a scoped kind variable,
1543 and should not be bound when type-checking the scope of the telescope.
1544
1545 2) The variable k2 is mentioned in the source, but it is not explicitly
1546 bound. It *is* a scoped kind variable, and will appear in the
1547 hsq_implicit field of a LHsTyVarBndrs.
1548
1549 2a) In the non-CUSK case, these variables won't have been generalized
1550 yet and don't appear in the looked-up kind. So we just return these
1551 in a NameSet.
1552
1553 3) The variable k is mentioned in the source with an explicit binding.
1554 It *is* a scoped type variable, and will appear in the
1555 hsq_explicit field of a LHsTyVarBndrs.
1556
1557 4) The variable t is bound in the source, but it is never mentioned later
1558 in the kind. It *is* a scoped variable (it can appear in the telescope
1559 scope, even though it is non-dependent), and will appear in the
1560 hsq_explicit field of a LHsTyVarBndrs.
1561
1562 splitTelescopeTvs walks through the output of a splitPiTys on the
1563 telescope head's kind (Foo, in our example), creating a list of tyvars
1564 to be bound within the telescope scope. It must simultaneously walk
1565 through the hsq_implicit and hsq_explicit fields of a LHsTyVarBndrs.
1566 Comments in the code refer back to the cases in this Note.
1567
1568 Cases (1) and (2) can be mixed together, but these cases must appear before
1569 cases (3) and (4) (the implicitly bound vars always precede the explicitly
1570 bound ones). So, we handle the lists in two stages (mk_tvs and
1571 mk_tvs2).
1572
1573 As a further wrinkle, it's possible that the variables in case (2) have
1574 been reordered. This is because hsq_implicit is ordered by the renamer,
1575 but there may be dependency among the variables. Of course, the order in
1576 the kind must take dependency into account. So we use a NameSet to keep
1577 these straightened out.
1578
1579 Note [Free-floating kind vars]
1580 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1581 Consider
1582
1583 data T = MkT (forall (a :: k). Proxy a)
1584
1585 This is not an existential datatype, but a higher-rank one. Note that
1586 the forall to the right of MkT. Also consider
1587
1588 data S a = MkS (Proxy (a :: k))
1589
1590 According to the rules around implicitly-bound kind variables, those
1591 k's scope over the whole declarations. The renamer grabs it and adds it
1592 to the hsq_implicits field of the HsQTyVars of the tycon. So it must
1593 be in scope during type-checking, but we want to reject T while accepting
1594 S.
1595
1596 Why reject T? Because the kind variable isn't fixed by anything. For
1597 a variable like k to be implicit, it needs to be mentioned in the kind
1598 of a tycon tyvar. But it isn't.
1599
1600 Why accept S? Because kind inference tells us that a has kind k, so it's
1601 all OK.
1602
1603 Here's the approach: in the first pass ("kind-checking") we just bring
1604 k into scope. In the second pass, we certainly hope that k has been
1605 integrated into the type's (generalized) kind, and so it should be found
1606 by splitTelescopeTvs. If it's not, then we must have a definition like
1607 T, and we reject.
1608
1609 -}
1610
1611 --------------------
1612 -- getInitialKind has made a suitably-shaped kind for the type or class
1613 -- Unpack it, and attribute those kinds to the type variables
1614 -- Extend the env with bindings for the tyvars, taken from
1615 -- the kind of the tycon/class. Give it to the thing inside, and
1616 -- check the result kind matches
1617 kcLookupKind :: Name -> TcM Kind
1618 kcLookupKind nm
1619 = do { tc_ty_thing <- tcLookup nm
1620 ; case tc_ty_thing of
1621 AThing k -> return k
1622 AGlobal (ATyCon tc) -> return (tyConKind tc)
1623 _ -> pprPanic "kcLookupKind" (ppr tc_ty_thing) }
1624
1625 -- See Note [Typechecking telescopes]
1626 splitTelescopeTvs :: Kind -- of the head of the telescope
1627 -> LHsQTyVars Name
1628 -> ( [TyVar] -- scoped type variables
1629 , NameSet -- ungeneralized implicit variables (case 2a)
1630 , [TyVar] -- implicit type variables (cases 1 & 2)
1631 , [TyVar] -- explicit type variables (cases 3 & 4)
1632 , Kind ) -- result kind
1633 splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs
1634 , hsq_explicit = hs_tvs })
1635 = let (bndrs, inner_ki) = splitPiTys kind
1636 (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, mk_kind)
1637 = mk_tvs [] [] bndrs (mkNameSet hs_kvs) hs_tvs
1638 in
1639 (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, mk_kind inner_ki)
1640 where
1641 mk_tvs :: [TyVar] -- scoped tv accum (reversed)
1642 -> [TyVar] -- implicit tv accum (reversed)
1643 -> [TyBinder]
1644 -> NameSet -- implicit variables
1645 -> [LHsTyVarBndr Name] -- explicit variables
1646 -> ( [TyVar] -- the tyvars to be lexically bound
1647 , NameSet -- Case 2a names
1648 , [TyVar] -- implicit tyvars
1649 , [TyVar] -- explicit tyvars
1650 , Type -> Type ) -- a function to create the result k
1651 mk_tvs scoped_tv_acc imp_tv_acc (bndr : bndrs) all_hs_kvs all_hs_tvs
1652 | Just tv <- binderVar_maybe bndr
1653 , isInvisibleBinder bndr
1654 , let tv_name = getName tv
1655 , tv_name `elemNameSet` all_hs_kvs
1656 = mk_tvs (tv : scoped_tv_acc) (tv : imp_tv_acc)
1657 bndrs (all_hs_kvs `delFromNameSet` tv_name) all_hs_tvs -- Case (2)
1658
1659 | Just tv <- binderVar_maybe bndr
1660 , isInvisibleBinder bndr
1661 = mk_tvs scoped_tv_acc (tv : imp_tv_acc)
1662 bndrs all_hs_kvs all_hs_tvs -- Case (1)
1663
1664 -- there may actually still be some hs_kvs, if we're kind checking
1665 -- a non-CUSK. The kinds *aren't* generalized, so we won't see them
1666 -- here.
1667 mk_tvs scoped_tv_acc imp_tv_acc all_bndrs all_hs_kvs all_hs_tvs
1668 = let (scoped, exp_tvs, mk_kind)
1669 = mk_tvs2 scoped_tv_acc [] all_bndrs all_hs_tvs in
1670 (scoped, all_hs_kvs, reverse imp_tv_acc, exp_tvs, mk_kind)
1671 -- no more Case (1) or (2)
1672
1673 -- This can't handle Case (1) or Case (2) from [Typechecking telescopes]
1674 mk_tvs2 :: [TyVar]
1675 -> [TyVar] -- new parameter: explicit tv accum (reversed)
1676 -> [TyBinder]
1677 -> [LHsTyVarBndr Name]
1678 -> ( [TyVar]
1679 , [TyVar] -- explicit tvs only
1680 , Type -> Type )
1681 mk_tvs2 scoped_tv_acc exp_tv_acc (bndr : bndrs) (hs_tv : hs_tvs)
1682 | Just tv <- binderVar_maybe bndr
1683 = ASSERT2( isVisibleBinder bndr, err_doc )
1684 ASSERT( getName tv == hsLTyVarName hs_tv )
1685 mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) bndrs hs_tvs -- Case (3)
1686
1687 | otherwise
1688 = ASSERT( isVisibleBinder bndr )
1689 let tv = mkTyVar (hsLTyVarName hs_tv) (binderType bndr) in
1690 mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) bndrs hs_tvs -- Case (4)
1691 where
1692 err_doc = vcat [ ppr (bndr : bndrs)
1693 , ppr (hs_tv : hs_tvs)
1694 , ppr kind
1695 , ppr tvbs ]
1696
1697 mk_tvs2 scoped_tv_acc exp_tv_acc all_bndrs [] -- All done!
1698 = ( reverse scoped_tv_acc
1699 , reverse exp_tv_acc
1700 , mkForAllTys all_bndrs )
1701
1702 mk_tvs2 _ _ all_bndrs all_hs_tvs
1703 = pprPanic "splitTelescopeTvs 2" (vcat [ ppr all_bndrs
1704 , ppr all_hs_tvs ])
1705
1706
1707 -----------------------
1708 -- used on first pass only ("kind checking")
1709 kcTyClTyVars :: Name -> LHsQTyVars Name
1710 -> TcM a -> TcM a
1711 kcTyClTyVars tycon hs_tvs thing_inside
1712 = tc_tycl_tyvars False tycon hs_tvs $ \_ _ _ _ -> thing_inside
1713
1714 -- used on second pass only ("type checking", really desugaring)
1715 tcTyClTyVars :: Name -> LHsQTyVars Name -- LHS of the type or class decl
1716 -> ([TyVar] -> [TyVar] -> Kind -> Kind -> TcM a) -> TcM a
1717 tcTyClTyVars = tc_tycl_tyvars True
1718
1719 tc_tycl_tyvars :: Bool -- are we doing the second pass?
1720 -> Name -> LHsQTyVars Name -- LHS of the type or class decl
1721 -> ([TyVar] -> [TyVar] -> Kind -> Kind -> TcM a) -> TcM a
1722 -- Used for the type variables of a type or class decl
1723 -- on both the first and second full passes in TcTyClDecls.
1724 -- *Not* used in the initial-kind run.
1725 --
1726 -- (tcTyClTyVars T [a,b] thing_inside)
1727 -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
1728 -- calls thing_inside with arguments
1729 -- [k1,k2] [a,b] (forall (k1:*) (k2:*) (a:k1 -> *) (b:k1). k2 -> *) (k2 -> *)
1730 -- having also extended the type environment with bindings
1731 -- for k1,k2,a,b
1732 --
1733 -- No need to freshen the k's because they are just skolem
1734 -- constants here, and we are at top level anyway.
1735 --
1736 -- Never emits constraints.
1737 --
1738 -- The LHsTyVarBndrs is always user-written, and the kind of the tycon
1739 -- is available in the local env.
1740 tc_tycl_tyvars second_pass tycon hs_tvs thing_inside
1741 = do { kind <- kcLookupKind tycon
1742 ; let (scoped_tvs, non_cusk_kv_name_set, all_kvs, all_tvs, res_k)
1743 = splitTelescopeTvs kind hs_tvs
1744 ; traceTc "tcTyClTyVars splitTelescopeTvs:"
1745 (vcat [ text "Tycon:" <+> ppr tycon
1746 , text "Kind:" <+> ppr kind
1747 , text "hs_tvs:" <+> ppr hs_tvs
1748 , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs
1749 , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs
1750 , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs
1751 , text "non-CUSK kvs:" <+> ppr non_cusk_kv_name_set
1752 , text "res_k:" <+> ppr res_k] )
1753
1754 -- need to look up the non-cusk kvs in order to get their
1755 -- kinds right, in case the kinds were informed by
1756 -- the getInitialKinds pass
1757 ; let non_cusk_kv_names = nameSetElems non_cusk_kv_name_set
1758 free_kvs = tyCoVarsOfTypes $
1759 map tyVarKind (all_kvs ++ all_tvs)
1760 lookup nm = case lookupVarSetByName free_kvs nm of
1761 Just tv -> Left tv
1762 Nothing -> Right nm
1763 (non_cusk_kvs, weirds) = partitionWith lookup non_cusk_kv_names
1764
1765 -- See Note [Free-floating kind vars] TODO (RAE): Write note.
1766 ; weird_kvs <- if second_pass
1767 then do { checkNoErrs $
1768 mapM_ (report_floating_kv all_tvs) weirds
1769 ; return [] }
1770 else do { ks <- mapM (const newMetaKindVar) weirds
1771 ; return (zipWith new_skolem_tv weirds ks) }
1772
1773 ; tcExtendTyVarEnv (non_cusk_kvs ++ weird_kvs ++ scoped_tvs) $
1774 thing_inside (non_cusk_kvs ++ weird_kvs ++ all_kvs) all_tvs kind res_k }
1775 where
1776 report_floating_kv all_tvs kv_name
1777 = addErr $
1778 vcat [ text "Kind variable" <+> quotes (ppr kv_name) <+>
1779 text "is implicitly bound in datatype"
1780 , quotes (ppr tycon) <> comma <+>
1781 text "but does not appear as the kind of any"
1782 , text "of its type variables. Perhaps you meant"
1783 , text "to bind it (with TypeInType) explicitly somewhere?"
1784 , if null all_tvs then empty else
1785 hang (text "Type variables with inferred kinds:")
1786 2 (pprTvBndrs all_tvs) ]
1787
1788 -----------------------------------
1789 tcDataKindSig :: Kind -> TcM [TyVar]
1790 -- GADT decls can have a (perhaps partial) kind signature
1791 -- e.g. data T :: * -> * -> * where ...
1792 -- This function makes up suitable (kinded) type variables for
1793 -- the argument kinds, and checks that the result kind is indeed *.
1794 -- We use it also to make up argument type variables for for data instances.
1795 -- Never emits constraints.
1796 tcDataKindSig kind
1797 = do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
1798 ; span <- getSrcSpanM
1799 ; us <- newUniqueSupply
1800 ; rdr_env <- getLocalRdrEnv
1801 ; let uniqs = uniqsFromSupply us
1802 occs = [ occ | str <- allNameStrings
1803 , let occ = mkOccName tvName str
1804 , isNothing (lookupLocalRdrOcc rdr_env occ) ]
1805 -- Note [Avoid name clashes for associated data types]
1806
1807 ; return [ mk_tv span uniq occ kind
1808 | ((kind, occ), uniq) <- arg_kinds `zip` occs `zip` uniqs ] }
1809 where
1810 (bndrs, res_kind) = splitPiTys kind
1811 arg_kinds = map binderType bndrs
1812 mk_tv loc uniq occ kind
1813 = mkTyVar (mkInternalName uniq occ loc) kind
1814
1815 badKindSig :: Kind -> SDoc
1816 badKindSig kind
1817 = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
1818 2 (ppr kind)
1819
1820 {-
1821 Note [Avoid name clashes for associated data types]
1822 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1823 Consider class C a b where
1824 data D b :: * -> *
1825 When typechecking the decl for D, we'll invent an extra type variable
1826 for D, to fill out its kind. Ideally we don't want this type variable
1827 to be 'a', because when pretty printing we'll get
1828 class C a b where
1829 data D b a0
1830 (NB: the tidying happens in the conversion to IfaceSyn, which happens
1831 as part of pretty-printing a TyThing.)
1832
1833 That's why we look in the LocalRdrEnv to see what's in scope. This is
1834 important only to get nice-looking output when doing ":info C" in GHCi.
1835 It isn't essential for correctness.
1836
1837
1838 ************************************************************************
1839 * *
1840 Scoped type variables
1841 * *
1842 ************************************************************************
1843
1844
1845 tcAddScopedTyVars is used for scoped type variables added by pattern
1846 type signatures
1847 e.g. \ ((x::a), (y::a)) -> x+y
1848 They never have explicit kinds (because this is source-code only)
1849 They are mutable (because they can get bound to a more specific type).
1850
1851 Usually we kind-infer and expand type splices, and then
1852 tupecheck/desugar the type. That doesn't work well for scoped type
1853 variables, because they scope left-right in patterns. (e.g. in the
1854 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
1855
1856 The current not-very-good plan is to
1857 * find all the types in the patterns
1858 * find their free tyvars
1859 * do kind inference
1860 * bring the kinded type vars into scope
1861 * BUT throw away the kind-checked type
1862 (we'll kind-check it again when we type-check the pattern)
1863
1864 This is bad because throwing away the kind checked type throws away
1865 its splices. But too bad for now. [July 03]
1866
1867 Historical note:
1868 We no longer specify that these type variables must be universally
1869 quantified (lots of email on the subject). If you want to put that
1870 back in, you need to
1871 a) Do a checkSigTyVars after thing_inside
1872 b) More insidiously, don't pass in expected_ty, else
1873 we unify with it too early and checkSigTyVars barfs
1874 Instead you have to pass in a fresh ty var, and unify
1875 it with expected_ty afterwards
1876 -}
1877
1878 tcHsPatSigType :: UserTypeCtxt
1879 -> LHsSigWcType Name -- The type signature
1880 -> TcM ( Type -- The signature
1881 , [TcTyVar] -- The new bit of type environment, binding
1882 -- the scoped type variables
1883 , [(Name, TcTyVar)] ) -- The wildcards
1884 -- Used for type-checking type signatures in
1885 -- (a) patterns e.g f (x::Int) = e
1886 -- (b) RULE forall bndrs e.g. forall (x::Int). f x = x
1887 --
1888 -- This may emit constraints
1889
1890 tcHsPatSigType ctxt sig_ty
1891 | HsIB { hsib_vars = sig_vars, hsib_body = wc_ty } <- sig_ty
1892 , HsWC { hswc_wcs = sig_wcs, hswc_ctx = extra, hswc_body = hs_ty } <- wc_ty
1893 = ASSERT( isNothing extra ) -- No extra-constraint wildcard in pattern sigs
1894 addSigCtxt ctxt hs_ty $
1895 tcWildCardBinders sig_wcs $ \ wcs ->
1896 do { emitWildCardHoleConstraints wcs
1897 ; (vars, sig_ty) <- tcImplicitTKBndrsX new_tkv sig_vars $
1898 do { ty <- tcHsLiftedType hs_ty
1899 ; return (ty, allBoundVariables ty) }
1900 ; sig_ty <- zonkTcType sig_ty
1901 -- don't use zonkTcTypeToType; it mistreats wildcards
1902 ; checkValidType ctxt sig_ty
1903 ; traceTc "tcHsPatSigType" (ppr sig_vars)
1904 ; return (sig_ty, vars, wcs) }
1905 where
1906 new_tkv name -- See Note [Pattern signature binders]
1907 = (, False) <$> -- "False" means that these tyvars aren't yet in scope
1908 do { kind <- newMetaKindVar
1909 ; case ctxt of
1910 RuleSigCtxt {} -> return $ new_skolem_tv name kind
1911 _ -> newSigTyVar name kind }
1912 -- See Note [Unifying SigTvs]
1913
1914 tcPatSig :: Bool -- True <=> pattern binding
1915 -> LHsSigWcType Name
1916 -> TcSigmaType
1917 -> TcM (TcType, -- The type to use for "inside" the signature
1918 [TcTyVar], -- The new bit of type environment, binding
1919 -- the scoped type variables
1920 [(Name, TcTyVar)], -- The wildcards
1921 HsWrapper) -- Coercion due to unification with actual ty
1922 -- Of shape: res_ty ~ sig_ty
1923 tcPatSig in_pat_bind sig res_ty
1924 = do { (sig_ty, sig_tvs, sig_wcs) <- tcHsPatSigType PatSigCtxt sig
1925 -- sig_tvs are the type variables free in 'sig',
1926 -- and not already in scope. These are the ones
1927 -- that should be brought into scope
1928
1929 ; if null sig_tvs then do {
1930 -- Just do the subsumption check and return
1931 wrap <- addErrCtxtM (mk_msg sig_ty) $
1932 tcSubType_NC PatSigCtxt res_ty sig_ty
1933 ; return (sig_ty, [], sig_wcs, wrap)
1934 } else do
1935 -- Type signature binds at least one scoped type variable
1936
1937 -- A pattern binding cannot bind scoped type variables
1938 -- It is more convenient to make the test here
1939 -- than in the renamer
1940 { when in_pat_bind (addErr (patBindSigErr sig_tvs))
1941
1942 -- Check that all newly-in-scope tyvars are in fact
1943 -- constrained by the pattern. This catches tiresome
1944 -- cases like
1945 -- type T a = Int
1946 -- f :: Int -> Int
1947 -- f (x :: T a) = ...
1948 -- Here 'a' doesn't get a binding. Sigh
1949 ; let bad_tvs = [ tv | tv <- sig_tvs
1950 , not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ]
1951 ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
1952
1953 -- Now do a subsumption check of the pattern signature against res_ty
1954 ; wrap <- addErrCtxtM (mk_msg sig_ty) $
1955 tcSubType_NC PatSigCtxt res_ty sig_ty
1956
1957 -- Phew!
1958 ; return (sig_ty, sig_tvs, sig_wcs, wrap)
1959 } }
1960 where
1961 mk_msg sig_ty tidy_env
1962 = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
1963 ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
1964 ; let msg = vcat [ hang (ptext (sLit "When checking that the pattern signature:"))
1965 4 (ppr sig_ty)
1966 , nest 2 (hang (ptext (sLit "fits the type of its context:"))
1967 2 (ppr res_ty)) ]
1968 ; return (tidy_env, msg) }
1969
1970 patBindSigErr :: [TcTyVar] -> SDoc
1971 patBindSigErr sig_tvs
1972 = hang (ptext (sLit "You cannot bind scoped type variable") <> plural sig_tvs
1973 <+> pprQuotedList sig_tvs)
1974 2 (ptext (sLit "in a pattern binding signature"))
1975
1976 {-
1977 Note [Pattern signature binders]
1978 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1979 Consider
1980 data T = forall a. T a (a->Int)
1981 f (T x (f :: a->Int) = blah)
1982
1983 Here
1984 * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk',
1985 It must be a skolem so that that it retains its identity, and
1986 TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
1987
1988 * The type signature pattern (f :: a->Int) binds "a" -> a_sig in the envt
1989
1990 * Then unificaiton makes a_sig := a_sk
1991
1992 That's why we must make a_sig a MetaTv (albeit a SigTv),
1993 not a SkolemTv, so that it can unify to a_sk.
1994
1995 For RULE binders, though, things are a bit different (yuk).
1996 RULE "foo" forall (x::a) (y::[a]). f x y = ...
1997 Here this really is the binding site of the type variable so we'd like
1998 to use a skolem, so that we get a complaint if we unify two of them
1999 together.
2000
2001 Note [Unifying SigTvs]
2002 ~~~~~~~~~~~~~~~~~~~~~~
2003 ALAS we have no decent way of avoiding two SigTvs getting unified.
2004 Consider
2005 f (x::(a,b)) (y::c)) = [fst x, y]
2006 Here we'd really like to complain that 'a' and 'c' are unified. But
2007 for the reasons above we can't make a,b,c into skolems, so they
2008 are just SigTvs that can unify. And indeed, this would be ok,
2009 f x (y::c) = case x of
2010 (x1 :: a1, True) -> [x,y]
2011 (x1 :: a2, False) -> [x,y,y]
2012 Here the type of x's first component is called 'a1' in one branch and
2013 'a2' in the other. We could try insisting on the same OccName, but
2014 they definitely won't have the sane lexical Name.
2015
2016 I think we could solve this by recording in a SigTv a list of all the
2017 in-scope variables that it should not unify with, but it's fiddly.
2018
2019
2020 ************************************************************************
2021 * *
2022 Checking kinds
2023 * *
2024 ************************************************************************
2025
2026 -}
2027
2028 -- | Produce an 'TcKind' suitable for a checking a type that can be * or #.
2029 ekOpen :: TcM TcKind
2030 ekOpen = do { lev <- newFlexiTyVarTy levityTy
2031 ; return (tYPE lev) }
2032
2033 unifyKinds :: [(TcType, TcKind)] -> TcM ([TcType], TcKind)
2034 unifyKinds act_kinds
2035 = do { kind <- newMetaKindVar
2036 ; let check (ty, act_kind) = checkExpectedKind ty act_kind kind
2037 ; tys' <- mapM check act_kinds
2038 ; return (tys', kind) }
2039
2040 {-
2041 ************************************************************************
2042 * *
2043 Sort checking kinds
2044 * *
2045 ************************************************************************
2046
2047 tcLHsKind converts a user-written kind to an internal, sort-checked kind.
2048 It does sort checking and desugaring at the same time, in one single pass.
2049 -}
2050
2051 tcLHsKind :: LHsKind Name -> TcM Kind
2052 tcLHsKind = tc_lhs_kind kindLevelMode
2053
2054 tc_lhs_kind :: TcTyMode -> LHsKind Name -> TcM Kind
2055 tc_lhs_kind mode k
2056 = addErrCtxt (ptext (sLit "In the kind") <+> quotes (ppr k)) $
2057 tc_lhs_type (kindLevel mode) k liftedTypeKind
2058
2059 promotionErr :: Name -> PromotionErr -> TcM a
2060 promotionErr name err
2061 = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> ptext (sLit "cannot be used here"))
2062 2 (parens reason))
2063 where
2064 reason = case err of
2065 FamDataConPE -> text "it comes from a data family instance"
2066 NoDataKinds -> text "Perhaps you intended to use DataKinds"
2067 NoTypeInTypeTC -> text "Perhaps you intended to use TypeInType"
2068 NoTypeInTypeDC -> text "Perhaps you intended to use TypeInType"
2069 _ -> text "it is defined and used in the same recursive group"
2070
2071 {-
2072 ************************************************************************
2073 * *
2074 Scoped type variables
2075 * *
2076 ************************************************************************
2077 -}
2078
2079 badPatSigTvs :: TcType -> [TyVar] -> SDoc
2080 badPatSigTvs sig_ty bad_tvs
2081 = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs,
2082 quotes (pprWithCommas ppr bad_tvs),
2083 ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
2084 ptext (sLit "but are actually discarded by a type synonym") ]
2085 , ptext (sLit "To fix this, expand the type synonym")
2086 , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
2087
2088 {-
2089 ************************************************************************
2090 * *
2091 Error messages and such
2092 * *
2093 ************************************************************************
2094 -}
2095
2096 -- | Make an appropriate message for an error in a function argument.
2097 -- Used for both expressions and types.
2098 funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
2099 funAppCtxt fun arg arg_no
2100 = hang (hsep [ ptext (sLit "In the"), speakNth arg_no, ptext (sLit "argument of"),
2101 quotes (ppr fun) <> text ", namely"])
2102 2 (quotes (ppr arg))