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