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