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