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