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