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