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