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