(Another) minor refactoring of substitutions
[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 -> extendTvSubst 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 (extendTvSubstAndInScope 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 { check_tc tc_tc
988 ; tc <- get_loopy_tc name tc_tc
989 ; handle_tyfams tc tc_tc }
990 -- mkNakedTyConApp: see Note [Type-checking inside the knot]
991 -- NB: we really should check if we're at the kind level
992 -- and if the tycon is promotable if -XNoTypeInType is set.
993 -- But this is a terribly large amount of work! Not worth it.
994
995 AGlobal (ATyCon tc)
996 -> do { check_tc tc
997 ; handle_tyfams tc tc }
998
999 AGlobal (AConLike (RealDataCon dc))
1000 -> do { data_kinds <- xoptM LangExt.DataKinds
1001 ; unless (data_kinds || specialPromotedDc dc) $
1002 promotionErr name NoDataKindsDC
1003 ; type_in_type <- xoptM LangExt.TypeInType
1004 ; unless ( type_in_type ||
1005 ( isTypeLevel (mode_level mode) &&
1006 isLegacyPromotableDataCon dc ) ||
1007 ( isKindLevel (mode_level mode) &&
1008 specialPromotedDc dc ) ) $
1009 promotionErr name NoTypeInTypeDC
1010 ; let tc = promoteDataCon dc
1011 ; return (mkNakedTyConApp tc [], tyConKind tc) }
1012
1013 APromotionErr err -> promotionErr name err
1014
1015 _ -> wrongThingErr "type" thing name }
1016 where
1017 check_tc :: TyCon -> TcM ()
1018 check_tc tc = do { type_in_type <- xoptM LangExt.TypeInType
1019 ; data_kinds <- xoptM LangExt.DataKinds
1020 ; unless (isTypeLevel (mode_level mode) ||
1021 data_kinds ||
1022 isKindTyCon tc) $
1023 promotionErr name NoDataKindsTC
1024 ; unless (isTypeLevel (mode_level mode) ||
1025 type_in_type ||
1026 isLegacyPromotableTyCon tc) $
1027 promotionErr name NoTypeInTypeTC }
1028
1029 -- if we are type-checking a type family tycon, we must instantiate
1030 -- any invisible arguments right away. Otherwise, we get #11246
1031 handle_tyfams :: TyCon -- the tycon to instantiate (might be loopy)
1032 -> TyCon -- a non-loopy version of the tycon
1033 -> TcM (TcType, TcKind)
1034 handle_tyfams tc tc_tc
1035 | mightBeUnsaturatedTyCon tc_tc
1036 = return (ty, tc_kind)
1037
1038 | otherwise
1039 = instantiateTyN 0 ty tc_kind
1040 where
1041 ty = mkNakedTyConApp tc []
1042 tc_kind = tyConKind tc_tc
1043
1044 get_loopy_tc :: Name -> TyCon -> TcM TyCon
1045 -- Return the knot-tied global TyCon if there is one
1046 -- Otherwise the local TcTyCon; we must be doing kind checking
1047 -- but we still want to return a TyCon of some sort to use in
1048 -- error messages
1049 get_loopy_tc name tc_tc
1050 = do { env <- getGblEnv
1051 ; case lookupNameEnv (tcg_type_env env) name of
1052 Just (ATyCon tc) -> return tc
1053 _ -> do { traceTc "lk1 (loopy)" (ppr name)
1054 ; return tc_tc } }
1055
1056 tcClass :: Name -> TcM (Class, TcKind)
1057 tcClass cls -- Must be a class
1058 = do { thing <- tcLookup cls
1059 ; case thing of
1060 ATcTyCon tc -> return (aThingErr "tcClass" cls, tyConKind tc)
1061 AGlobal (ATyCon tc)
1062 | Just cls <- tyConClass_maybe tc
1063 -> return (cls, tyConKind tc)
1064 _ -> wrongThingErr "class" thing cls }
1065
1066
1067 aThingErr :: String -> Name -> b
1068 -- The type checker for types is sometimes called simply to
1069 -- do *kind* checking; and in that case it ignores the type
1070 -- returned. Which is a good thing since it may not be available yet!
1071 aThingErr str x = pprPanic "AThing evaluated unexpectedly" (text str <+> ppr x)
1072
1073 {-
1074 Note [Type-checking inside the knot]
1075 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1076 Suppose we are checking the argument types of a data constructor. We
1077 must zonk the types before making the DataCon, because once built we
1078 can't change it. So we must traverse the type.
1079
1080 BUT the parent TyCon is knot-tied, so we can't look at it yet.
1081
1082 So we must be careful not to use "smart constructors" for types that
1083 look at the TyCon or Class involved.
1084
1085 * Hence the use of mkNakedXXX functions. These do *not* enforce
1086 the invariants (for example that we use (ForAllTy (Anon s) t) rather
1087 than (TyConApp (->) [s,t])).
1088
1089 * The zonking functions establish invariants (even zonkTcType, a change from
1090 previous behaviour). So we must never inspect the result of a
1091 zonk that might mention a knot-tied TyCon. This is generally OK
1092 because we zonk *kinds* while kind-checking types. And the TyCons
1093 in kinds shouldn't be knot-tied, because they come from a previous
1094 mutually recursive group.
1095
1096 * TcHsSyn.zonkTcTypeToType also can safely check/establish
1097 invariants.
1098
1099 This is horribly delicate. I hate it. A good example of how
1100 delicate it is can be seen in Trac #7903.
1101
1102 Note [Body kind of a HsForAllTy]
1103 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1104 The body of a forall is usually a type, but in principle
1105 there's no reason to prohibit *unlifted* types.
1106 In fact, GHC can itself construct a function with an
1107 unboxed tuple inside a for-all (via CPR analyis; see
1108 typecheck/should_compile/tc170).
1109
1110 Moreover in instance heads we get forall-types with
1111 kind Constraint.
1112
1113 It's tempting to check that the body kind is either * or #. But this is
1114 wrong. For example:
1115
1116 class C a b
1117 newtype N = Mk Foo deriving (C a)
1118
1119 We're doing newtype-deriving for C. But notice how `a` isn't in scope in
1120 the predicate `C a`. So we quantify, yielding `forall a. C a` even though
1121 `C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
1122 convenient. Bottom line: don't check for * or # here.
1123
1124 Note [Body kind of a HsQualTy]
1125 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1126 If ctxt is non-empty, the HsQualTy really is a /function/, so the
1127 kind of the result really is '*', and in that case the kind of the
1128 body-type can be lifted or unlifted.
1129
1130 However, consider
1131 instance Eq a => Eq [a] where ...
1132 or
1133 f :: (Eq a => Eq [a]) => blah
1134 Here both body-kind of the HsQualTy is Constraint rather than *.
1135 Rather crudely we tell the difference by looking at exp_kind. It's
1136 very convenient to typecheck instance types like any other HsSigType.
1137
1138 Admittedly the '(Eq a => Eq [a]) => blah' case is erroneous, but it's
1139 better to reject in checkValidType. If we say that the body kind
1140 should be '*' we risk getting TWO error messages, one saying that Eq
1141 [a] doens't have kind '*', and one saying that we need a Constraint to
1142 the left of the outer (=>).
1143
1144 How do we figure out the right body kind? Well, it's a bit of a
1145 kludge: I just look at the expected kind. If it's Constraint, we
1146 must be in this instance situation context. It's a kludge because it
1147 wouldn't work if any unification was involved to compute that result
1148 kind -- but it isn't. (The true way might be to use the 'mode'
1149 parameter, but that seemed like a sledgehammer to crack a nut.)
1150
1151 Note [Inferring tuple kinds]
1152 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1153 Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
1154 we try to figure out whether it's a tuple of kind * or Constraint.
1155 Step 1: look at the expected kind
1156 Step 2: infer argument kinds
1157
1158 If after Step 2 it's not clear from the arguments that it's
1159 Constraint, then it must be *. Once having decided that we re-check
1160 the Check the arguments again to give good error messages
1161 in eg. `(Maybe, Maybe)`
1162
1163 Note that we will still fail to infer the correct kind in this case:
1164
1165 type T a = ((a,a), D a)
1166 type family D :: Constraint -> Constraint
1167
1168 While kind checking T, we do not yet know the kind of D, so we will default the
1169 kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
1170
1171 Note [Desugaring types]
1172 ~~~~~~~~~~~~~~~~~~~~~~~
1173 The type desugarer is phase 2 of dealing with HsTypes. Specifically:
1174
1175 * It transforms from HsType to Type
1176
1177 * It zonks any kinds. The returned type should have no mutable kind
1178 or type variables (hence returning Type not TcType):
1179 - any unconstrained kind variables are defaulted to (Any *) just
1180 as in TcHsSyn.
1181 - there are no mutable type variables because we are
1182 kind-checking a type
1183 Reason: the returned type may be put in a TyCon or DataCon where
1184 it will never subsequently be zonked.
1185
1186 You might worry about nested scopes:
1187 ..a:kappa in scope..
1188 let f :: forall b. T '[a,b] -> Int
1189 In this case, f's type could have a mutable kind variable kappa in it;
1190 and we might then default it to (Any *) when dealing with f's type
1191 signature. But we don't expect this to happen because we can't get a
1192 lexically scoped type variable with a mutable kind variable in it. A
1193 delicate point, this. If it becomes an issue we might need to
1194 distinguish top-level from nested uses.
1195
1196 Moreover
1197 * it cannot fail,
1198 * it does no unifications
1199 * it does no validity checking, except for structural matters, such as
1200 (a) spurious ! annotations.
1201 (b) a class used as a type
1202
1203 Note [Kind of a type splice]
1204 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1205 Consider these terms, each with TH type splice inside:
1206 [| e1 :: Maybe $(..blah..) |]
1207 [| e2 :: $(..blah..) |]
1208 When kind-checking the type signature, we'll kind-check the splice
1209 $(..blah..); we want to give it a kind that can fit in any context,
1210 as if $(..blah..) :: forall k. k.
1211
1212 In the e1 example, the context of the splice fixes kappa to *. But
1213 in the e2 example, we'll desugar the type, zonking the kind unification
1214 variables as we go. When we encounter the unconstrained kappa, we
1215 want to default it to '*', not to (Any *).
1216
1217
1218 Help functions for type applications
1219 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1220 -}
1221
1222 addTypeCtxt :: LHsType Name -> TcM a -> TcM a
1223 -- Wrap a context around only if we want to show that contexts.
1224 -- Omit invisble ones and ones user's won't grok
1225 addTypeCtxt (L _ ty) thing
1226 = addErrCtxt doc thing
1227 where
1228 doc = text "In the type" <+> quotes (ppr ty)
1229
1230 {-
1231 ************************************************************************
1232 * *
1233 Type-variable binders
1234 %* *
1235 %************************************************************************
1236
1237 Note [Scope-check inferred kinds]
1238 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1239 Consider
1240
1241 data SameKind :: k -> k -> *
1242 foo :: forall a (b :: Proxy a) (c :: Proxy d). SameKind b c
1243
1244 d has no binding site. So it gets bound implicitly, at the top. The
1245 problem is that d's kind mentions `a`. So it's all ill-scoped.
1246
1247 The way we check for this is to gather all variables *bound* in a
1248 type variable's scope. The type variable's kind should not mention
1249 any of these variables. That is, d's kind can't mention a, b, or c.
1250 We can't just check to make sure that d's kind is in scope, because
1251 we might be about to kindGeneralize.
1252
1253 A little messy, but it works.
1254
1255 -}
1256
1257 tcWildCardBinders :: [Name]
1258 -> ([(Name, TcTyVar)] -> TcM a)
1259 -> TcM a
1260 -- Use the Unique form the specified Name; don't clone it. There is
1261 -- no need to clone, and not doing so avoids the need to return a list
1262 -- of pairs to bring into scope.
1263 tcWildCardBinders wcs thing_inside
1264 = do { wcs <- mapM new_wildcard wcs
1265 ; tcExtendTyVarEnv2 wcs $
1266 thing_inside wcs }
1267 where
1268 new_wildcard :: Name -> TcM (Name, TcTyVar)
1269 new_wildcard name = do { kind <- newMetaKindVar
1270 ; tv <- newFlexiTyVar kind
1271 ; return (name, tv) }
1272
1273 -- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
1274 -- user-supplied kind signature (CUSK), generalise the result.
1275 -- Used in 'getInitialKind' (for tycon kinds and other kinds)
1276 -- and in kind-checking (but not for tycon kinds, which are checked with
1277 -- tcTyClDecls). See also Note [Complete user-supplied kind signatures] in
1278 -- HsDecls.
1279 --
1280 -- This function does not do telescope checking.
1281 kcHsTyVarBndrs :: Bool -- ^ True <=> the decl being checked has a CUSK
1282 -> LHsQTyVars Name
1283 -> ([TyVar] -> [TyVar] -> TcM (Kind, r))
1284 -- ^ the result kind, possibly with other info
1285 -- ^ args are implicit vars, explicit vars
1286 -> TcM (Kind, r) -- ^ The full kind of the thing being declared,
1287 -- with the other info
1288 kcHsTyVarBndrs cusk (HsQTvs { hsq_implicit = kv_ns
1289 , hsq_explicit = hs_tvs }) thing_inside
1290 = do { meta_kvs <- mapM (const newMetaKindVar) kv_ns
1291 ; kvs <- if cusk
1292 then return $ zipWith new_skolem_tv kv_ns meta_kvs
1293 -- the names must line up in splitTelescopeTvs
1294 else zipWithM newSigTyVar kv_ns meta_kvs
1295 ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $
1296 do { (full_kind, _, stuff) <- bind_telescope hs_tvs (thing_inside kvs)
1297 ; let qkvs = filter (not . isMetaTyVar) $
1298 tyCoVarsOfTypeWellScoped full_kind
1299 -- these have to be the vars made with new_skolem_tv
1300 -- above. Thus, they are known to the user and should
1301 -- be Specified, not Invisible, when kind-generalizing
1302
1303 -- the free non-meta variables in the returned kind will
1304 -- contain both *mentioned* kind vars and *unmentioned* kind
1305 -- vars (See case (1) under Note [Typechecking telescopes])
1306 gen_kind = if cusk
1307 then mkSpecForAllTys qkvs $ full_kind
1308 else full_kind
1309 ; return (gen_kind, stuff) } }
1310 where
1311 -- there may be dependency between the explicit "ty" vars. So, we have
1312 -- to handle them one at a time. We also need to build up a full kind
1313 -- here, because this is the place we know whether to use a FunTy or a
1314 -- ForAllTy. We prefer using an anonymous binder over a trivial named
1315 -- binder. If a user wants a trivial named one, use an explicit kind
1316 -- signature.
1317 bind_telescope :: [LHsTyVarBndr Name]
1318 -> ([TyVar] -> TcM (Kind, r))
1319 -> TcM (Kind, VarSet, r)
1320 bind_telescope [] thing
1321 = do { (res_kind, stuff) <- thing []
1322 ; return (res_kind, tyCoVarsOfType res_kind, stuff) }
1323 bind_telescope (L _ hs_tv : hs_tvs) thing
1324 = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
1325 ; (res_kind, fvs, stuff) <- bind_unless_scoped tv_pair $
1326 bind_telescope hs_tvs $ \tvs ->
1327 thing (tv:tvs)
1328 -- we must be *lazy* in res_kind and fvs (assuming that the
1329 -- caller of kcHsTyVarBndrs is, too), as sometimes these hold
1330 -- panics. See kcConDecl.
1331 ; k <- zonkTcType (tyVarKind tv)
1332 ; let k_fvs = tyCoVarsOfType k
1333 (bndr, fvs')
1334 | tv `elemVarSet` fvs
1335 = ( mkNamedBinder Visible tv
1336 , fvs `delVarSet` tv `unionVarSet` k_fvs )
1337 | otherwise
1338 = (mkAnonBinder k, fvs `unionVarSet` k_fvs)
1339
1340 ; return ( mkForAllTy bndr res_kind, fvs', stuff ) }
1341
1342 -- | Bind the tyvar in the env't unless the bool is True
1343 bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a
1344 bind_unless_scoped (_, True) thing_inside = thing_inside
1345 bind_unless_scoped (tv, False) thing_inside
1346 = tcExtendTyVarEnv [tv] thing_inside
1347
1348 kc_hs_tv :: HsTyVarBndr Name -> TcM (TcTyVar, Bool)
1349 kc_hs_tv hs_tvb
1350 = do { (tv, scoped) <- tcHsTyVarBndr_Scoped hs_tvb
1351
1352 -- in the CUSK case, we want to default any un-kinded tyvars
1353 -- See Note [Complete user-supplied kind signatures] in HsDecls
1354 ; case hs_tvb of
1355 UserTyVar {}
1356 | cusk
1357 , not scoped -- don't default class tyvars
1358 -> discardResult $
1359 unifyKind (Just (mkTyVarTy tv)) liftedTypeKind
1360 (tyVarKind tv)
1361 _ -> return ()
1362
1363 ; return (tv, scoped) }
1364
1365 tcImplicitTKBndrs :: [Name]
1366 -> TcM (a, TyVarSet) -- vars are bound somewhere in the scope
1367 -- see Note [Scope-check inferred kinds]
1368 -> TcM ([TcTyVar], a)
1369 tcImplicitTKBndrs = tcImplicitTKBndrsX tcHsTyVarName
1370
1371 -- | Convenient specialization
1372 tcImplicitTKBndrsType :: [Name]
1373 -> TcM Type
1374 -> TcM ([TcTyVar], Type)
1375 tcImplicitTKBndrsType var_ns thing_inside
1376 = tcImplicitTKBndrs var_ns $
1377 do { res_ty <- thing_inside
1378 ; return (res_ty, allBoundVariables res_ty) }
1379
1380 -- this more general variant is needed in tcHsPatSigType.
1381 -- See Note [Pattern signature binders]
1382 tcImplicitTKBndrsX :: (Name -> TcM (TcTyVar, Bool)) -- new_tv function
1383 -> [Name]
1384 -> TcM (a, TyVarSet)
1385 -> TcM ([TcTyVar], a)
1386 -- Returned TcTyVars have the supplied Names
1387 -- i.e. no cloning of fresh names
1388 tcImplicitTKBndrsX new_tv var_ns thing_inside
1389 = do { tkvs_pairs <- mapM new_tv var_ns
1390 ; let must_scope_tkvs = [ tkv | (tkv, False) <- tkvs_pairs ]
1391 tkvs = map fst tkvs_pairs
1392 ; (result, bound_tvs) <- tcExtendTyVarEnv must_scope_tkvs $
1393 thing_inside
1394
1395 -- it's possible that we guessed the ordering of variables
1396 -- wrongly. Adjust.
1397 ; tkvs <- mapM zonkTyCoVarKind tkvs
1398 ; let extra = text "NB: Implicitly-bound variables always come" <+>
1399 text "before other ones."
1400 ; checkValidInferredKinds tkvs bound_tvs extra
1401
1402 ; let final_tvs = toposortTyVars tkvs
1403 ; traceTc "tcImplicitTKBndrs" (ppr var_ns $$ ppr final_tvs)
1404
1405 ; return (final_tvs, result) }
1406
1407 tcExplicitTKBndrs :: [LHsTyVarBndr Name]
1408 -> ([TyVar] -> TcM (a, TyVarSet))
1409 -- ^ Thing inside returns the set of variables bound
1410 -- in the scope. See Note [Scope-check inferred kinds]
1411 -> TcM (a, TyVarSet) -- ^ returns augmented bound vars
1412 -- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
1413 tcExplicitTKBndrs orig_hs_tvs thing_inside
1414 = go orig_hs_tvs $ \ tvs ->
1415 do { (result, bound_tvs) <- thing_inside tvs
1416
1417 -- Issue an error if the ordering is bogus.
1418 -- See Note [Bad telescopes] in TcValidity.
1419 ; tvs <- checkZonkValidTelescope (interppSP orig_hs_tvs) tvs empty
1420 ; checkValidInferredKinds tvs bound_tvs empty
1421
1422 ; traceTc "tcExplicitTKBndrs" $
1423 vcat [ text "Hs vars:" <+> ppr orig_hs_tvs
1424 , text "tvs:" <+> sep (map pprTvBndr tvs) ]
1425
1426 ; return (result, bound_tvs `unionVarSet` mkVarSet tvs)
1427 }
1428 where
1429 go [] thing = thing []
1430 go (L _ hs_tv : hs_tvs) thing
1431 = do { tv <- tcHsTyVarBndr hs_tv
1432 ; tcExtendTyVarEnv [tv] $
1433 go hs_tvs $ \ tvs ->
1434 thing (tv : tvs) }
1435
1436 tcHsTyVarBndr :: HsTyVarBndr Name -> TcM TcTyVar
1437 -- Return a SkolemTv TcTyVar, initialised with a kind variable.
1438 -- Typically the Kind inside the HsTyVarBndr will be a tyvar
1439 -- with a mutable kind in it.
1440 -- NB: These variables must not be in scope. This function
1441 -- is not appropriate for use with associated types, for example.
1442 --
1443 -- Returned TcTyVar has the same name; no cloning
1444 --
1445 -- See also Note [Associated type tyvar names] in Class
1446 tcHsTyVarBndr (UserTyVar (L _ name))
1447 = do { kind <- newMetaKindVar
1448 ; return (mkTcTyVar name kind (SkolemTv False)) }
1449 tcHsTyVarBndr (KindedTyVar (L _ name) kind)
1450 = do { kind <- tcLHsKind kind
1451 ; return (mkTcTyVar name kind (SkolemTv False)) }
1452
1453 -- | Type-check a user-written TyVarBndr, which binds a variable
1454 -- that might already be in scope (e.g., in an associated type declaration)
1455 -- The second return value says whether the variable is in scope (True)
1456 -- or not (False).
1457 tcHsTyVarBndr_Scoped :: HsTyVarBndr Name -> TcM (TcTyVar, Bool)
1458 tcHsTyVarBndr_Scoped (UserTyVar (L _ name))
1459 = tcHsTyVarName name
1460 tcHsTyVarBndr_Scoped (KindedTyVar (L _ name) lhs_kind)
1461 = do { tv_pair@(tv, _) <- tcHsTyVarName name
1462 ; kind <- tcLHsKind lhs_kind
1463 -- for a scoped variable: make sure annotation is consistent
1464 -- for an unscoped variable: unify the meta-tyvar kind
1465 -- either way: we can ignore the resulting coercion
1466 ; discardResult $ unifyKind (Just (mkTyVarTy tv)) kind (tyVarKind tv)
1467 ; return tv_pair }
1468
1469 -- | Produce a tyvar of the given name (with a meta-tyvar kind). If
1470 -- the name is already in scope, return the scoped variable. The
1471 -- second return value says whether the variable is in scope (True)
1472 -- or not (False). (Use this for associated types, for example.)
1473 tcHsTyVarName :: Name -> TcM (TcTyVar, Bool)
1474 tcHsTyVarName name
1475 = do { mb_tv <- tcLookupLcl_maybe name
1476 ; case mb_tv of
1477 Just (ATyVar _ tv) -> return (tv, True)
1478 _ -> do { kind <- newMetaKindVar
1479 ; return (mkTcTyVar name kind vanillaSkolemTv, False) }}
1480
1481 -- makes a new skolem tv
1482 new_skolem_tv :: Name -> Kind -> TcTyVar
1483 new_skolem_tv n k = mkTcTyVar n k vanillaSkolemTv
1484
1485 ------------------
1486 kindGeneralizeType :: Type -> TcM Type
1487 -- Result is zonked
1488 kindGeneralizeType ty
1489 = do { kvs <- kindGeneralize ty
1490 ; zonkTcType (mkInvForAllTys kvs ty) }
1491
1492 kindGeneralize :: TcType -> TcM [KindVar]
1493 kindGeneralize ty
1494 = do { gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
1495 ; kvs <- zonkTcTypeAndFV ty
1496 ; quantifyTyVars gbl_tvs (Pair kvs emptyVarSet) }
1497
1498 {-
1499 Note [Kind generalisation]
1500 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1501 We do kind generalisation only at the outer level of a type signature.
1502 For example, consider
1503 T :: forall k. k -> *
1504 f :: (forall a. T a -> Int) -> Int
1505 When kind-checking f's type signature we generalise the kind at
1506 the outermost level, thus:
1507 f1 :: forall k. (forall (a:k). T k a -> Int) -> Int -- YES!
1508 and *not* at the inner forall:
1509 f2 :: (forall k. forall (a:k). T k a -> Int) -> Int -- NO!
1510 Reason: same as for HM inference on value level declarations,
1511 we want to infer the most general type. The f2 type signature
1512 would be *less applicable* than f1, because it requires a more
1513 polymorphic argument.
1514
1515 NB: There are no explicit kind variables written in f's signature.
1516 When there are, the renamer adds these kind variables to the list of
1517 variables bound by the forall, so you can indeed have a type that's
1518 higher-rank in its kind. But only by explicit request.
1519
1520 Note [Kinds of quantified type variables]
1521 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1522 tcTyVarBndrsGen quantifies over a specified list of type variables,
1523 *and* over the kind variables mentioned in the kinds of those tyvars.
1524
1525 Note that we must zonk those kinds (obviously) but less obviously, we
1526 must return type variables whose kinds are zonked too. Example
1527 (a :: k7) where k7 := k9 -> k9
1528 We must return
1529 [k9, a:k9->k9]
1530 and NOT
1531 [k9, a:k7]
1532 Reason: we're going to turn this into a for-all type,
1533 forall k9. forall (a:k7). blah
1534 which the type checker will then instantiate, and instantiate does not
1535 look through unification variables!
1536
1537 Hence using zonked_kinds when forming tvs'.
1538
1539 Note [Typechecking telescopes]
1540 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1541 The function tcTyClTyVars has to bind the scoped type and kind
1542 variables in a telescope. For example:
1543
1544 class Foo k (t :: Proxy k -> k2) where ...
1545
1546 By the time [kt]cTyClTyVars is called, we know *something* about the kind of Foo,
1547 at least that it has the form
1548
1549 Foo :: forall (k2 :: mk2). forall (k :: mk1) -> (Proxy mk1 k -> k2) -> Constraint
1550
1551 if it has a CUSK (Foo does not, in point of fact) or
1552
1553 Foo :: forall (k :: mk1) -> (Proxy mk1 k -> k2) -> Constraint
1554
1555 if it does not, where mk1 and mk2 are meta-kind variables (mk1, mk2 :: *).
1556
1557 When calling tcTyClTyVars, this kind is further generalized w.r.t. any
1558 free variables appearing in mk1 or mk2. So, mk_tvs must handle
1559 that possibility. Perhaps we discover that mk1 := Maybe k3 and mk2 := *,
1560 so we have
1561
1562 Foo :: forall (k3 :: *). forall (k2 :: *). forall (k :: Maybe k3) ->
1563 (Proxy (Maybe k3) k -> k2) -> Constraint
1564
1565 We now have several sorts of variables to think about:
1566 1) The variable k3 is not mentioned in the source at all. It is neither
1567 explicitly bound nor ever used. It is *not* a scoped kind variable,
1568 and should not be bound when type-checking the scope of the telescope.
1569
1570 2) The variable k2 is mentioned in the source, but it is not explicitly
1571 bound. It *is* a scoped kind variable, and will appear in the
1572 hsq_implicit field of a LHsTyVarBndrs.
1573
1574 2a) In the non-CUSK case, these variables won't have been generalized
1575 yet and don't appear in the looked-up kind. So we just return these
1576 in a NameSet.
1577
1578 3) The variable k is mentioned in the source with an explicit binding.
1579 It *is* a scoped type variable, and will appear in the
1580 hsq_explicit field of a LHsTyVarBndrs.
1581
1582 4) The variable t is bound in the source, but it is never mentioned later
1583 in the kind. It *is* a scoped variable (it can appear in the telescope
1584 scope, even though it is non-dependent), and will appear in the
1585 hsq_explicit field of a LHsTyVarBndrs.
1586
1587 splitTelescopeTvs walks through the output of a splitPiTys on the
1588 telescope head's kind (Foo, in our example), creating a list of tyvars
1589 to be bound within the telescope scope. It must simultaneously walk
1590 through the hsq_implicit and hsq_explicit fields of a LHsTyVarBndrs.
1591 Comments in the code refer back to the cases in this Note.
1592
1593 Cases (1) and (2) can be mixed together, but these cases must appear before
1594 cases (3) and (4) (the implicitly bound vars always precede the explicitly
1595 bound ones). So, we handle the lists in two stages (mk_tvs and
1596 mk_tvs2).
1597
1598 As a further wrinkle, it's possible that the variables in case (2) have
1599 been reordered. This is because hsq_implicit is ordered by the renamer,
1600 but there may be dependency among the variables. Of course, the order in
1601 the kind must take dependency into account. So we use a NameSet to keep
1602 these straightened out.
1603
1604 Note [Free-floating kind vars]
1605 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1606 Consider
1607
1608 data T = MkT (forall (a :: k). Proxy a)
1609 -- from test ghci/scripts/T7873
1610
1611 This is not an existential datatype, but a higher-rank one. Note that
1612 the forall to the right of MkT. Also consider
1613
1614 data S a = MkS (Proxy (a :: k))
1615
1616 According to the rules around implicitly-bound kind variables, those
1617 k's scope over the whole declarations. The renamer grabs it and adds it
1618 to the hsq_implicits field of the HsQTyVars of the tycon. So it must
1619 be in scope during type-checking, but we want to reject T while accepting
1620 S.
1621
1622 Why reject T? Because the kind variable isn't fixed by anything. For
1623 a variable like k to be implicit, it needs to be mentioned in the kind
1624 of a tycon tyvar. But it isn't.
1625
1626 Why accept S? Because kind inference tells us that a has kind k, so it's
1627 all OK.
1628
1629 Here's the approach: in the first pass ("kind-checking") we just bring
1630 k into scope. In the second pass, we certainly hope that k has been
1631 integrated into the type's (generalized) kind, and so it should be found
1632 by splitTelescopeTvs. If it's not, then we must have a definition like
1633 T, and we reject. (But see Note [Tiresome kind checking] about some extra
1634 processing necessary in the second pass.)
1635
1636 Note [Tiresome kind matching]
1637 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1638 Because of the use of SigTvs in kind inference (see #11203, for example)
1639 sometimes kind variables come into tcTClTyVars (the second, desugaring
1640 pass in TcTyClDecls) with the wrong names. The best way to fix this up
1641 is just to unify the kinds, again. So we return HsKind/Kind pairs from
1642 splitTelescopeTvs that can get unified in tcTyClTyVars, but only if there
1643 are kind vars the didn't link up in splitTelescopeTvs.
1644
1645 -}
1646
1647 --------------------
1648 -- getInitialKind has made a suitably-shaped kind for the type or class
1649 -- Unpack it, and attribute those kinds to the type variables
1650 -- Extend the env with bindings for the tyvars, taken from
1651 -- the kind of the tycon/class. Give it to the thing inside, and
1652 -- check the result kind matches
1653 kcLookupKind :: Name -> TcM Kind
1654 kcLookupKind nm
1655 = do { tc_ty_thing <- tcLookup nm
1656 ; case tc_ty_thing of
1657 ATcTyCon tc -> return (tyConKind tc)
1658 AGlobal (ATyCon tc) -> return (tyConKind tc)
1659 _ -> pprPanic "kcLookupKind" (ppr tc_ty_thing) }
1660
1661 -- See Note [Typechecking telescopes]
1662 splitTelescopeTvs :: Kind -- of the head of the telescope
1663 -> LHsQTyVars Name
1664 -> ( [TyVar] -- scoped type variables
1665 , NameSet -- ungeneralized implicit variables (case 2a)
1666 , [TyVar] -- implicit type variables (cases 1 & 2)
1667 , [TyVar] -- explicit type variables (cases 3 & 4)
1668 , [(LHsKind Name, Kind)] -- see Note [Tiresome kind matching]
1669 , Kind ) -- result kind
1670 splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs
1671 , hsq_explicit = hs_tvs })
1672 = let (bndrs, inner_ki) = splitPiTys kind
1673 (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, kind_matches, mk_kind)
1674 = mk_tvs [] [] bndrs (mkNameSet hs_kvs) hs_tvs
1675 in
1676 (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, kind_matches, mk_kind inner_ki)
1677 where
1678 mk_tvs :: [TyVar] -- scoped tv accum (reversed)
1679 -> [TyVar] -- implicit tv accum (reversed)
1680 -> [TyBinder]
1681 -> NameSet -- implicit variables
1682 -> [LHsTyVarBndr Name] -- explicit variables
1683 -> ( [TyVar] -- the tyvars to be lexically bound
1684 , NameSet -- Case 2a names
1685 , [TyVar] -- implicit tyvars
1686 , [TyVar] -- explicit tyvars
1687 , [(LHsKind Name, Kind)] -- tiresome kind matches
1688 , Type -> Type ) -- a function to create the result k
1689 mk_tvs scoped_tv_acc imp_tv_acc (bndr : bndrs) all_hs_kvs all_hs_tvs
1690 | Just tv <- binderVar_maybe bndr
1691 , isInvisibleBinder bndr
1692 , let tv_name = getName tv
1693 , tv_name `elemNameSet` all_hs_kvs
1694 = mk_tvs (tv : scoped_tv_acc) (tv : imp_tv_acc)
1695 bndrs (all_hs_kvs `delFromNameSet` tv_name) all_hs_tvs -- Case (2)
1696
1697 | Just tv <- binderVar_maybe bndr
1698 , isInvisibleBinder bndr
1699 = mk_tvs scoped_tv_acc (tv : imp_tv_acc)
1700 bndrs all_hs_kvs all_hs_tvs -- Case (1)
1701
1702 -- there may actually still be some hs_kvs, if we're kind checking
1703 -- a non-CUSK. The kinds *aren't* generalized, so we won't see them
1704 -- here.
1705 mk_tvs scoped_tv_acc imp_tv_acc all_bndrs all_hs_kvs all_hs_tvs
1706 = let (scoped, exp_tvs, kind_matches, mk_kind)
1707 = mk_tvs2 scoped_tv_acc [] [] all_bndrs all_hs_tvs in
1708 (scoped, all_hs_kvs, reverse imp_tv_acc, exp_tvs, kind_matches, mk_kind)
1709 -- no more Case (1) or (2)
1710
1711 -- This can't handle Case (1) or Case (2) from [Typechecking telescopes]
1712 mk_tvs2 :: [TyVar]
1713 -> [TyVar] -- new parameter: explicit tv accum (reversed)
1714 -> [(LHsKind Name, Kind)] -- tiresome kind matches accum
1715 -> [TyBinder]
1716 -> [LHsTyVarBndr Name]
1717 -> ( [TyVar]
1718 , [TyVar] -- explicit tvs only
1719 , [(LHsKind Name, Kind)] -- tiresome kind matches
1720 , Type -> Type )
1721 mk_tvs2 scoped_tv_acc exp_tv_acc kind_match_acc (bndr : bndrs) (hs_tv : hs_tvs)
1722 | Just tv <- binderVar_maybe bndr
1723 = ASSERT2( isVisibleBinder bndr, err_doc )
1724 ASSERT( getName tv == hsLTyVarName hs_tv )
1725 mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) kind_match_acc' bndrs hs_tvs
1726 -- Case (3)
1727
1728 | otherwise
1729 = ASSERT( isVisibleBinder bndr )
1730 let tv = mkTyVar (hsLTyVarName hs_tv) (binderType bndr) in
1731 mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) kind_match_acc' bndrs hs_tvs
1732 -- Case (4)
1733 where
1734 err_doc = vcat [ ppr (bndr : bndrs)
1735 , ppr (hs_tv : hs_tvs)
1736 , ppr kind
1737 , ppr tvbs ]
1738
1739 kind_match_acc' = case hs_tv of
1740 L _ (UserTyVar {}) -> kind_match_acc
1741 L _ (KindedTyVar _ hs_kind) -> (hs_kind, kind) : kind_match_acc
1742 where kind = binderType bndr
1743
1744 mk_tvs2 scoped_tv_acc exp_tv_acc kind_match_acc all_bndrs [] -- All done!
1745 = ( reverse scoped_tv_acc
1746 , reverse exp_tv_acc
1747 , kind_match_acc -- no need to reverse; it's not ordered
1748 , mkForAllTys all_bndrs )
1749
1750 mk_tvs2 _ _ _ all_bndrs all_hs_tvs
1751 = pprPanic "splitTelescopeTvs 2" (vcat [ ppr all_bndrs
1752 , ppr all_hs_tvs ])
1753
1754
1755 -----------------------
1756 -- | "Kind check" the tyvars to a tycon. This is used during the "kind-checking"
1757 -- pass in TcTyClsDecls. (Never in getInitialKind, never in the
1758 -- "type-checking"/desugaring pass.) It works only for LHsQTyVars associated
1759 -- with a tycon, whose kind is known (partially) via getInitialKinds.
1760 -- Never emits constraints, though the thing_inside might.
1761 kcTyClTyVars :: Name -- ^ of the tycon
1762 -> LHsQTyVars Name
1763 -> TcM a -> TcM a
1764 kcTyClTyVars tycon hs_tvs thing_inside
1765 = do { kind <- kcLookupKind tycon
1766 ; let (scoped_tvs, non_cusk_kv_name_set, all_kvs, all_tvs, _, res_k)
1767 = splitTelescopeTvs kind hs_tvs
1768 ; traceTc "kcTyClTyVars splitTelescopeTvs:"
1769 (vcat [ text "Tycon:" <+> ppr tycon
1770 , text "Kind:" <+> ppr kind
1771 , text "hs_tvs:" <+> ppr hs_tvs
1772 , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs
1773 , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs
1774 , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs
1775 , text "non-CUSK kvs:" <+> ppr non_cusk_kv_name_set
1776 , text "res_k:" <+> ppr res_k] )
1777
1778 -- need to look up the non-cusk kvs in order to get their
1779 -- kinds right, in case the kinds were informed by
1780 -- the getInitialKinds pass
1781 ; let non_cusk_kv_names = nameSetElems non_cusk_kv_name_set
1782 free_kvs = tyCoVarsOfTypes $
1783 map tyVarKind (all_kvs ++ all_tvs)
1784 mk_kv kv_name = case lookupVarSetByName free_kvs kv_name of
1785 Just kv -> return kv
1786 Nothing ->
1787 -- this kv isn't mentioned in the
1788 -- LHsQTyVars at all. But maybe
1789 -- it's mentioned in the body
1790 -- In any case, just gin up a
1791 -- meta-kind for it
1792 do { kv_kind <- newMetaKindVar
1793 ; return (new_skolem_tv kv_name kv_kind) }
1794 ; non_cusk_kvs <- mapM mk_kv non_cusk_kv_names
1795
1796 -- The non_cusk_kvs are still scoped; they are mentioned by
1797 -- name by the user
1798 ; tcExtendTyVarEnv (non_cusk_kvs ++ scoped_tvs) $
1799 thing_inside }
1800
1801 tcTyClTyVars :: Name -> LHsQTyVars Name -- LHS of the type or class decl
1802 -> ([TyVar] -> [TyVar] -> Kind -> Kind -> TcM a) -> TcM a
1803 -- ^ Used for the type variables of a type or class decl
1804 -- on the second full pass (type-checking/desugaring) in TcTyClDecls.
1805 -- This is *not* used in the initial-kind run, nor in the "kind-checking" pass.
1806 --
1807 -- (tcTyClTyVars T [a,b] thing_inside)
1808 -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
1809 -- calls thing_inside with arguments
1810 -- [k1,k2] [a,b] (forall (k1:*) (k2:*) (a:k1 -> *) (b:k1). k2 -> *) (k2 -> *)
1811 -- having also extended the type environment with bindings
1812 -- for k1,k2,a,b
1813 --
1814 -- Never emits constraints.
1815 --
1816 -- The LHsTyVarBndrs is always user-written, and the full, generalised
1817 -- kind of the tycon is available in the local env.
1818 tcTyClTyVars tycon hs_tvs thing_inside
1819 = do { kind <- kcLookupKind tycon
1820 ; let ( scoped_tvs, float_kv_name_set, all_kvs
1821 , all_tvs, kind_matches, res_k )
1822 = splitTelescopeTvs kind hs_tvs
1823 ; traceTc "tcTyClTyVars splitTelescopeTvs:"
1824 (vcat [ text "Tycon:" <+> ppr tycon
1825 , text "Kind:" <+> ppr kind
1826 , text "hs_tvs:" <+> ppr hs_tvs
1827 , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs
1828 , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs
1829 , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs
1830 , text "floating kvs:" <+> ppr float_kv_name_set
1831 , text "Tiresome kind matches:" <+> ppr kind_matches
1832 , text "res_k:" <+> ppr res_k] )
1833
1834 ; float_kvs <- deal_with_float_kvs float_kv_name_set kind_matches
1835 scoped_tvs all_tvs
1836
1837 ; tcExtendTyVarEnv (float_kvs ++ scoped_tvs) $
1838 -- the float_kvs are already in the all_kvs
1839 thing_inside all_kvs all_tvs kind res_k }
1840 where
1841 -- See Note [Free-floating kind vars]
1842 deal_with_float_kvs float_kv_name_set kind_matches scoped_tvs all_tvs
1843 | isEmptyNameSet float_kv_name_set
1844 = return []
1845
1846 | otherwise
1847 = do { -- the floating kvs might just be renamed
1848 -- see Note [Tiresome kind matching]
1849 ; let float_kv_names = nameSetElems float_kv_name_set
1850 ; float_kv_kinds <- mapM (const newMetaKindVar) float_kv_names
1851 ; float_kvs <- zipWithM newSigTyVar float_kv_names float_kv_kinds
1852 ; discardResult $
1853 tcExtendTyVarEnv (float_kvs ++ scoped_tvs) $
1854 solveEqualities $
1855 forM kind_matches $ \ (hs_kind, kind) ->
1856 do { tc_kind <- tcLHsKind hs_kind
1857 ; unifyKind noThing tc_kind kind }
1858
1859 ; zonked_kvs <- mapM ((return . tcGetTyVar "tcTyClTyVars") <=< zonkTcTyVar)
1860 float_kvs
1861 ; let (still_sigs, matched_up) = partition isSigTyVar zonked_kvs
1862 -- the still_sigs didn't match with anything. They must be
1863 -- "free-floating", as in Note [Free-floating kind vars]
1864 ; checkNoErrs $ mapM_ (report_floating_kv all_tvs) still_sigs
1865
1866 -- the matched up kvs are proper scoped kvs.
1867 ; return matched_up }
1868
1869 report_floating_kv all_tvs kv
1870 = addErr $
1871 vcat [ text "Kind variable" <+> quotes (ppr kv) <+>
1872 text "is implicitly bound in datatype"
1873 , quotes (ppr tycon) <> comma <+>
1874 text "but does not appear as the kind of any"
1875 , text "of its type variables. Perhaps you meant"
1876 , text "to bind it (with TypeInType) explicitly somewhere?"
1877 , if null all_tvs then empty else
1878 hang (text "Type variables with inferred kinds:")
1879 2 (pprTvBndrs all_tvs) ]
1880
1881 -----------------------------------
1882 tcDataKindSig :: Kind -> TcM [TyVar]
1883 -- GADT decls can have a (perhaps partial) kind signature
1884 -- e.g. data T :: * -> * -> * where ...
1885 -- This function makes up suitable (kinded) type variables for
1886 -- the argument kinds, and checks that the result kind is indeed *.
1887 -- We use it also to make up argument type variables for for data instances.
1888 -- Never emits constraints.
1889 tcDataKindSig kind
1890 = do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
1891 ; span <- getSrcSpanM
1892 ; us <- newUniqueSupply
1893 ; rdr_env <- getLocalRdrEnv
1894 ; let uniqs = uniqsFromSupply us
1895 occs = [ occ | str <- allNameStrings
1896 , let occ = mkOccName tvName str
1897 , isNothing (lookupLocalRdrOcc rdr_env occ) ]
1898 -- Note [Avoid name clashes for associated data types]
1899
1900 ; return [ mk_tv span uniq occ kind
1901 | ((kind, occ), uniq) <- arg_kinds `zip` occs `zip` uniqs ] }
1902 where
1903 (bndrs, res_kind) = splitPiTys kind
1904 arg_kinds = map binderType bndrs
1905 mk_tv loc uniq occ kind
1906 = mkTyVar (mkInternalName uniq occ loc) kind
1907
1908 badKindSig :: Kind -> SDoc
1909 badKindSig kind
1910 = hang (text "Kind signature on data type declaration has non-* return kind")
1911 2 (ppr kind)
1912
1913 {-
1914 Note [Avoid name clashes for associated data types]
1915 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1916 Consider class C a b where
1917 data D b :: * -> *
1918 When typechecking the decl for D, we'll invent an extra type variable
1919 for D, to fill out its kind. Ideally we don't want this type variable
1920 to be 'a', because when pretty printing we'll get
1921 class C a b where
1922 data D b a0
1923 (NB: the tidying happens in the conversion to IfaceSyn, which happens
1924 as part of pretty-printing a TyThing.)
1925
1926 That's why we look in the LocalRdrEnv to see what's in scope. This is
1927 important only to get nice-looking output when doing ":info C" in GHCi.
1928 It isn't essential for correctness.
1929
1930
1931 ************************************************************************
1932 * *
1933 Scoped type variables
1934 * *
1935 ************************************************************************
1936
1937
1938 tcAddScopedTyVars is used for scoped type variables added by pattern
1939 type signatures
1940 e.g. \ ((x::a), (y::a)) -> x+y
1941 They never have explicit kinds (because this is source-code only)
1942 They are mutable (because they can get bound to a more specific type).
1943
1944 Usually we kind-infer and expand type splices, and then
1945 tupecheck/desugar the type. That doesn't work well for scoped type
1946 variables, because they scope left-right in patterns. (e.g. in the
1947 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
1948
1949 The current not-very-good plan is to
1950 * find all the types in the patterns
1951 * find their free tyvars
1952 * do kind inference
1953 * bring the kinded type vars into scope
1954 * BUT throw away the kind-checked type
1955 (we'll kind-check it again when we type-check the pattern)
1956
1957 This is bad because throwing away the kind checked type throws away
1958 its splices. But too bad for now. [July 03]
1959
1960 Historical note:
1961 We no longer specify that these type variables must be universally
1962 quantified (lots of email on the subject). If you want to put that
1963 back in, you need to
1964 a) Do a checkSigTyVars after thing_inside
1965 b) More insidiously, don't pass in expected_ty, else
1966 we unify with it too early and checkSigTyVars barfs
1967 Instead you have to pass in a fresh ty var, and unify
1968 it with expected_ty afterwards
1969 -}
1970
1971 tcHsPatSigType :: UserTypeCtxt
1972 -> LHsSigWcType Name -- The type signature
1973 -> TcM ( Type -- The signature
1974 , [TcTyVar] -- The new bit of type environment, binding
1975 -- the scoped type variables
1976 , [(Name, TcTyVar)] ) -- The wildcards
1977 -- Used for type-checking type signatures in
1978 -- (a) patterns e.g f (x::Int) = e
1979 -- (b) RULE forall bndrs e.g. forall (x::Int). f x = x
1980 --
1981 -- This may emit constraints
1982
1983 tcHsPatSigType ctxt sig_ty
1984 | HsIB { hsib_vars = sig_vars, hsib_body = wc_ty } <- sig_ty
1985 , HsWC { hswc_wcs = sig_wcs, hswc_ctx = extra, hswc_body = hs_ty } <- wc_ty
1986 = ASSERT( isNothing extra ) -- No extra-constraint wildcard in pattern sigs
1987 addSigCtxt ctxt hs_ty $
1988 tcWildCardBinders sig_wcs $ \ wcs ->
1989 do { emitWildCardHoleConstraints wcs
1990 ; (vars, sig_ty) <- tcImplicitTKBndrsX new_tkv sig_vars $
1991 do { ty <- tcHsLiftedType hs_ty
1992 ; return (ty, allBoundVariables ty) }
1993 ; sig_ty <- zonkTcType sig_ty
1994 -- don't use zonkTcTypeToType; it mistreats wildcards
1995 ; checkValidType ctxt sig_ty
1996 ; traceTc "tcHsPatSigType" (ppr sig_vars)
1997 ; return (sig_ty, vars, wcs) }
1998 where
1999 new_tkv name -- See Note [Pattern signature binders]
2000 = (, False) <$> -- "False" means that these tyvars aren't yet in scope
2001 do { kind <- newMetaKindVar
2002 ; case ctxt of
2003 RuleSigCtxt {} -> return $ new_skolem_tv name kind
2004 _ -> newSigTyVar name kind }
2005 -- See Note [Unifying SigTvs]
2006
2007 tcPatSig :: Bool -- True <=> pattern binding
2008 -> LHsSigWcType Name
2009 -> ExpSigmaType
2010 -> TcM (TcType, -- The type to use for "inside" the signature
2011 [TcTyVar], -- The new bit of type environment, binding
2012 -- the scoped type variables
2013 [(Name, TcTyVar)], -- The wildcards
2014 HsWrapper) -- Coercion due to unification with actual ty
2015 -- Of shape: res_ty ~ sig_ty
2016 tcPatSig in_pat_bind sig res_ty
2017 = do { (sig_ty, sig_tvs, sig_wcs) <- tcHsPatSigType PatSigCtxt sig
2018 -- sig_tvs are the type variables free in 'sig',
2019 -- and not already in scope. These are the ones
2020 -- that should be brought into scope
2021
2022 ; if null sig_tvs then do {
2023 -- Just do the subsumption check and return
2024 wrap <- addErrCtxtM (mk_msg sig_ty) $
2025 tcSubTypeET_NC PatSigCtxt res_ty sig_ty
2026 ; return (sig_ty, [], sig_wcs, wrap)
2027 } else do
2028 -- Type signature binds at least one scoped type variable
2029
2030 -- A pattern binding cannot bind scoped type variables
2031 -- It is more convenient to make the test here
2032 -- than in the renamer
2033 { when in_pat_bind (addErr (patBindSigErr sig_tvs))
2034
2035 -- Check that all newly-in-scope tyvars are in fact
2036 -- constrained by the pattern. This catches tiresome
2037 -- cases like
2038 -- type T a = Int
2039 -- f :: Int -> Int
2040 -- f (x :: T a) = ...
2041 -- Here 'a' doesn't get a binding. Sigh
2042 ; let bad_tvs = [ tv | tv <- sig_tvs
2043 , not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ]
2044 ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
2045
2046 -- Now do a subsumption check of the pattern signature against res_ty
2047 ; wrap <- addErrCtxtM (mk_msg sig_ty) $
2048 tcSubTypeET_NC PatSigCtxt res_ty sig_ty
2049
2050 -- Phew!
2051 ; return (sig_ty, sig_tvs, sig_wcs, wrap)
2052 } }
2053 where
2054 mk_msg sig_ty tidy_env
2055 = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
2056 ; res_ty <- readExpType res_ty -- should be filled in by now
2057 ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
2058 ; let msg = vcat [ hang (text "When checking that the pattern signature:")
2059 4 (ppr sig_ty)
2060 , nest 2 (hang (text "fits the type of its context:")
2061 2 (ppr res_ty)) ]
2062 ; return (tidy_env, msg) }
2063
2064 patBindSigErr :: [TcTyVar] -> SDoc
2065 patBindSigErr sig_tvs
2066 = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
2067 <+> pprQuotedList sig_tvs)
2068 2 (text "in a pattern binding signature")
2069
2070 {-
2071 Note [Pattern signature binders]
2072 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2073 Consider
2074 data T = forall a. T a (a->Int)
2075 f (T x (f :: a->Int) = blah)
2076
2077 Here
2078 * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk',
2079 It must be a skolem so that that it retains its identity, and
2080 TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
2081
2082 * The type signature pattern (f :: a->Int) binds "a" -> a_sig in the envt
2083
2084 * Then unification makes a_sig := a_sk
2085
2086 That's why we must make a_sig a MetaTv (albeit a SigTv),
2087 not a SkolemTv, so that it can unify to a_sk.
2088
2089 For RULE binders, though, things are a bit different (yuk).
2090 RULE "foo" forall (x::a) (y::[a]). f x y = ...
2091 Here this really is the binding site of the type variable so we'd like
2092 to use a skolem, so that we get a complaint if we unify two of them
2093 together.
2094
2095 Note [Unifying SigTvs]
2096 ~~~~~~~~~~~~~~~~~~~~~~
2097 ALAS we have no decent way of avoiding two SigTvs getting unified.
2098 Consider
2099 f (x::(a,b)) (y::c)) = [fst x, y]
2100 Here we'd really like to complain that 'a' and 'c' are unified. But
2101 for the reasons above we can't make a,b,c into skolems, so they
2102 are just SigTvs that can unify. And indeed, this would be ok,
2103 f x (y::c) = case x of
2104 (x1 :: a1, True) -> [x,y]
2105 (x1 :: a2, False) -> [x,y,y]
2106 Here the type of x's first component is called 'a1' in one branch and
2107 'a2' in the other. We could try insisting on the same OccName, but
2108 they definitely won't have the sane lexical Name.
2109
2110 I think we could solve this by recording in a SigTv a list of all the
2111 in-scope variables that it should not unify with, but it's fiddly.
2112
2113
2114 ************************************************************************
2115 * *
2116 Checking kinds
2117 * *
2118 ************************************************************************
2119
2120 -}
2121
2122 -- | Produce an 'TcKind' suitable for a checking a type that can be * or #.
2123 ekOpen :: TcM TcKind
2124 ekOpen = do { lev <- newFlexiTyVarTy levityTy
2125 ; return (tYPE lev) }
2126
2127 unifyKinds :: [(TcType, TcKind)] -> TcM ([TcType], TcKind)
2128 unifyKinds act_kinds
2129 = do { kind <- newMetaKindVar
2130 ; let check (ty, act_kind) = checkExpectedKind ty act_kind kind
2131 ; tys' <- mapM check act_kinds
2132 ; return (tys', kind) }
2133
2134 {-
2135 ************************************************************************
2136 * *
2137 Sort checking kinds
2138 * *
2139 ************************************************************************
2140
2141 tcLHsKind converts a user-written kind to an internal, sort-checked kind.
2142 It does sort checking and desugaring at the same time, in one single pass.
2143 -}
2144
2145 tcLHsKind :: LHsKind Name -> TcM Kind
2146 tcLHsKind = tc_lhs_kind kindLevelMode
2147
2148 tc_lhs_kind :: TcTyMode -> LHsKind Name -> TcM Kind
2149 tc_lhs_kind mode k
2150 = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $
2151 tc_lhs_type (kindLevel mode) k liftedTypeKind
2152
2153 promotionErr :: Name -> PromotionErr -> TcM a
2154 promotionErr name err
2155 = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here")
2156 2 (parens reason))
2157 where
2158 reason = case err of
2159 FamDataConPE -> text "it comes from a data family instance"
2160 NoDataKindsTC -> text "Perhaps you intended to use DataKinds"
2161 NoDataKindsDC -> text "Perhaps you intended to use DataKinds"
2162 NoTypeInTypeTC -> text "Perhaps you intended to use TypeInType"
2163 NoTypeInTypeDC -> text "Perhaps you intended to use TypeInType"
2164 PatSynPE -> text "Pattern synonyms cannot be promoted"
2165 _ -> text "it is defined and used in the same recursive group"
2166
2167 {-
2168 ************************************************************************
2169 * *
2170 Scoped type variables
2171 * *
2172 ************************************************************************
2173 -}
2174
2175 badPatSigTvs :: TcType -> [TyVar] -> SDoc
2176 badPatSigTvs sig_ty bad_tvs
2177 = vcat [ fsep [text "The type variable" <> plural bad_tvs,
2178 quotes (pprWithCommas ppr bad_tvs),
2179 text "should be bound by the pattern signature" <+> quotes (ppr sig_ty),
2180 text "but are actually discarded by a type synonym" ]
2181 , text "To fix this, expand the type synonym"
2182 , text "[Note: I hope to lift this restriction in due course]" ]
2183
2184 {-
2185 ************************************************************************
2186 * *
2187 Error messages and such
2188 * *
2189 ************************************************************************
2190 -}
2191
2192 -- | Make an appropriate message for an error in a function argument.
2193 -- Used for both expressions and types.
2194 funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
2195 funAppCtxt fun arg arg_no
2196 = hang (hsep [ text "In the", speakNth arg_no, ptext (sLit "argument of"),
2197 quotes (ppr fun) <> text ", namely"])
2198 2 (quotes (ppr arg))