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