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