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