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