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