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