Track specified/invisible more carefully.
[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 ; quantifyTyVars 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 --
1750 -- (tcTyClTyVars T [a,b] thing_inside)
1751 -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
1752 -- calls thing_inside with arguments
1753 -- [k1,k2] [a,b] [k1:*, k2:*, a:k1 -> *, b:k1] (k2 -> *)
1754 -- having also extended the type environment with bindings
1755 -- for k1,k2,a,b
1756 --
1757 -- Never emits constraints.
1758 --
1759 -- The LHsTyVarBndrs is always user-written, and the full, generalised
1760 -- kind of the tycon is available in the local env.
1761 tcTyClTyVars tycon hs_tvs thing_inside
1762 = do { (binders, res_kind) <- kcLookupKind tycon
1763 ; let ( scoped_tvs, float_kv_name_set, all_kvs
1764 , all_tvs, kind_matches )
1765 = splitTelescopeTvs binders hs_tvs
1766 ; traceTc "tcTyClTyVars splitTelescopeTvs:"
1767 (vcat [ text "Tycon:" <+> ppr tycon
1768 , text "Binders:" <+> ppr binders
1769 , text "res_kind:" <+> ppr res_kind
1770 , text "hs_tvs.hsq_implicit:" <+> ppr (hsq_implicit hs_tvs)
1771 , text "hs_tvs.hsq_explicit:" <+> ppr (hsq_explicit hs_tvs)
1772 , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs
1773 , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs
1774 , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs
1775 , text "floating kvs:" <+> ppr float_kv_name_set
1776 , text "Tiresome kind matches:" <+> ppr kind_matches ] )
1777
1778 ; float_kvs <- deal_with_float_kvs float_kv_name_set kind_matches
1779 scoped_tvs all_tvs
1780
1781 ; tcExtendTyVarEnv (float_kvs ++ scoped_tvs) $
1782 -- the float_kvs are already in the all_kvs
1783 thing_inside all_kvs all_tvs binders res_kind }
1784 where
1785 -- See Note [Free-floating kind vars]
1786 deal_with_float_kvs float_kv_name_set kind_matches scoped_tvs all_tvs
1787 | isEmptyNameSet float_kv_name_set
1788 = return []
1789
1790 | otherwise
1791 = do { -- the floating kvs might just be renamed
1792 -- see Note [Tiresome kind matching]
1793 ; let float_kv_names = nameSetElems float_kv_name_set
1794 ; float_kv_kinds <- mapM (const newMetaKindVar) float_kv_names
1795 ; float_kvs <- zipWithM newSigTyVar float_kv_names float_kv_kinds
1796 ; discardResult $
1797 tcExtendTyVarEnv (float_kvs ++ scoped_tvs) $
1798 solveEqualities $
1799 forM kind_matches $ \ (hs_kind, kind) ->
1800 do { tc_kind <- tcLHsKind hs_kind
1801 ; unifyKind noThing tc_kind kind }
1802
1803 ; zonked_kvs <- mapM ((return . tcGetTyVar "tcTyClTyVars") <=< zonkTcTyVar)
1804 float_kvs
1805 ; let (still_sigs, matched_up) = partition isSigTyVar zonked_kvs
1806 -- the still_sigs didn't match with anything. They must be
1807 -- "free-floating", as in Note [Free-floating kind vars]
1808 ; checkNoErrs $ mapM_ (report_floating_kv all_tvs) still_sigs
1809
1810 -- the matched up kvs are proper scoped kvs.
1811 ; return matched_up }
1812
1813 report_floating_kv all_tvs kv
1814 = addErr $
1815 vcat [ text "Kind variable" <+> quotes (ppr kv) <+>
1816 text "is implicitly bound in datatype"
1817 , quotes (ppr tycon) <> comma <+>
1818 text "but does not appear as the kind of any"
1819 , text "of its type variables. Perhaps you meant"
1820 , text "to bind it (with TypeInType) explicitly somewhere?"
1821 , if null all_tvs then empty else
1822 hang (text "Type variables with inferred kinds:")
1823 2 (pprTvBndrs all_tvs) ]
1824
1825 -----------------------------------
1826 tcDataKindSig :: Kind -> TcM ([TyVar], [TyBinder], Kind)
1827 -- GADT decls can have a (perhaps partial) kind signature
1828 -- e.g. data T :: * -> * -> * where ...
1829 -- This function makes up suitable (kinded) type variables for
1830 -- the argument kinds, and checks that the result kind is indeed *.
1831 -- We use it also to make up argument type variables for for data instances.
1832 -- Never emits constraints.
1833 -- Returns the new TyVars, the extracted TyBinders, and the new, reduced
1834 -- result kind (which should always be Type or a synonym thereof)
1835 tcDataKindSig kind
1836 = do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
1837 ; span <- getSrcSpanM
1838 ; us <- newUniqueSupply
1839 ; rdr_env <- getLocalRdrEnv
1840 ; let uniqs = uniqsFromSupply us
1841 occs = [ occ | str <- allNameStrings
1842 , let occ = mkOccName tvName str
1843 , isNothing (lookupLocalRdrOcc rdr_env occ) ]
1844 -- Note [Avoid name clashes for associated data types]
1845
1846 -- NB: Use the tv from a binder if there is one. Otherwise,
1847 -- we end up inventing a new Unique for it, and any other tv
1848 -- that mentions the first ends up with the wrong kind.
1849 ; return ( [ tv
1850 | ((bndr, occ), uniq) <- bndrs `zip` occs `zip` uniqs
1851 , let tv | Just bndr_tv <- binderVar_maybe bndr
1852 = bndr_tv
1853 | otherwise
1854 = mk_tv span uniq occ (binderType bndr) ]
1855 , bndrs, res_kind ) }
1856 where
1857 (bndrs, res_kind) = splitPiTys kind
1858 mk_tv loc uniq occ kind
1859 = mkTyVar (mkInternalName uniq occ loc) kind
1860
1861 badKindSig :: Kind -> SDoc
1862 badKindSig kind
1863 = hang (text "Kind signature on data type declaration has non-* return kind")
1864 2 (ppr kind)
1865
1866 {-
1867 Note [Avoid name clashes for associated data types]
1868 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1869 Consider class C a b where
1870 data D b :: * -> *
1871 When typechecking the decl for D, we'll invent an extra type variable
1872 for D, to fill out its kind. Ideally we don't want this type variable
1873 to be 'a', because when pretty printing we'll get
1874 class C a b where
1875 data D b a0
1876 (NB: the tidying happens in the conversion to IfaceSyn, which happens
1877 as part of pretty-printing a TyThing.)
1878
1879 That's why we look in the LocalRdrEnv to see what's in scope. This is
1880 important only to get nice-looking output when doing ":info C" in GHCi.
1881 It isn't essential for correctness.
1882
1883
1884 ************************************************************************
1885 * *
1886 Scoped type variables
1887 * *
1888 ************************************************************************
1889
1890
1891 tcAddScopedTyVars is used for scoped type variables added by pattern
1892 type signatures
1893 e.g. \ ((x::a), (y::a)) -> x+y
1894 They never have explicit kinds (because this is source-code only)
1895 They are mutable (because they can get bound to a more specific type).
1896
1897 Usually we kind-infer and expand type splices, and then
1898 tupecheck/desugar the type. That doesn't work well for scoped type
1899 variables, because they scope left-right in patterns. (e.g. in the
1900 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
1901
1902 The current not-very-good plan is to
1903 * find all the types in the patterns
1904 * find their free tyvars
1905 * do kind inference
1906 * bring the kinded type vars into scope
1907 * BUT throw away the kind-checked type
1908 (we'll kind-check it again when we type-check the pattern)
1909
1910 This is bad because throwing away the kind checked type throws away
1911 its splices. But too bad for now. [July 03]
1912
1913 Historical note:
1914 We no longer specify that these type variables must be universally
1915 quantified (lots of email on the subject). If you want to put that
1916 back in, you need to
1917 a) Do a checkSigTyVars after thing_inside
1918 b) More insidiously, don't pass in expected_ty, else
1919 we unify with it too early and checkSigTyVars barfs
1920 Instead you have to pass in a fresh ty var, and unify
1921 it with expected_ty afterwards
1922 -}
1923
1924 tcHsPatSigType :: UserTypeCtxt
1925 -> LHsSigWcType Name -- The type signature
1926 -> TcM ( Type -- The signature
1927 , [TcTyVar] -- The new bit of type environment, binding
1928 -- the scoped type variables
1929 , [(Name, TcTyVar)] ) -- The wildcards
1930 -- Used for type-checking type signatures in
1931 -- (a) patterns e.g f (x::Int) = e
1932 -- (b) RULE forall bndrs e.g. forall (x::Int). f x = x
1933 --
1934 -- This may emit constraints
1935
1936 tcHsPatSigType ctxt sig_ty
1937 | HsIB { hsib_vars = sig_vars, hsib_body = wc_ty } <- sig_ty
1938 , HsWC { hswc_wcs = sig_wcs, hswc_ctx = extra, hswc_body = hs_ty } <- wc_ty
1939 = ASSERT( isNothing extra ) -- No extra-constraint wildcard in pattern sigs
1940 addSigCtxt ctxt hs_ty $
1941 tcWildCardBinders sig_wcs $ \ wcs ->
1942 do { emitWildCardHoleConstraints wcs
1943 ; (vars, sig_ty) <- tcImplicitTKBndrsX new_tkv sig_vars $
1944 do { ty <- tcHsLiftedType hs_ty
1945 ; return (ty, allBoundVariables ty) }
1946 ; sig_ty <- zonkTcType sig_ty
1947 -- don't use zonkTcTypeToType; it mistreats wildcards
1948 ; checkValidType ctxt sig_ty
1949 ; traceTc "tcHsPatSigType" (ppr sig_vars)
1950 ; return (sig_ty, vars, wcs) }
1951 where
1952 new_tkv name -- See Note [Pattern signature binders]
1953 = (, False) <$> -- "False" means that these tyvars aren't yet in scope
1954 do { kind <- newMetaKindVar
1955 ; case ctxt of
1956 RuleSigCtxt {} -> return $ new_skolem_tv name kind
1957 _ -> newSigTyVar name kind }
1958 -- See Note [Unifying SigTvs]
1959
1960 tcPatSig :: Bool -- True <=> pattern binding
1961 -> LHsSigWcType Name
1962 -> ExpSigmaType
1963 -> TcM (TcType, -- The type to use for "inside" the signature
1964 [TcTyVar], -- The new bit of type environment, binding
1965 -- the scoped type variables
1966 [(Name, TcTyVar)], -- The wildcards
1967 HsWrapper) -- Coercion due to unification with actual ty
1968 -- Of shape: res_ty ~ sig_ty
1969 tcPatSig in_pat_bind sig res_ty
1970 = do { (sig_ty, sig_tvs, sig_wcs) <- tcHsPatSigType PatSigCtxt sig
1971 -- sig_tvs are the type variables free in 'sig',
1972 -- and not already in scope. These are the ones
1973 -- that should be brought into scope
1974
1975 ; if null sig_tvs then do {
1976 -- Just do the subsumption check and return
1977 wrap <- addErrCtxtM (mk_msg sig_ty) $
1978 tcSubTypeET_NC PatSigCtxt res_ty sig_ty
1979 ; return (sig_ty, [], sig_wcs, wrap)
1980 } else do
1981 -- Type signature binds at least one scoped type variable
1982
1983 -- A pattern binding cannot bind scoped type variables
1984 -- It is more convenient to make the test here
1985 -- than in the renamer
1986 { when in_pat_bind (addErr (patBindSigErr sig_tvs))
1987
1988 -- Check that all newly-in-scope tyvars are in fact
1989 -- constrained by the pattern. This catches tiresome
1990 -- cases like
1991 -- type T a = Int
1992 -- f :: Int -> Int
1993 -- f (x :: T a) = ...
1994 -- Here 'a' doesn't get a binding. Sigh
1995 ; let bad_tvs = [ tv | tv <- sig_tvs
1996 , not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ]
1997 ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
1998
1999 -- Now do a subsumption check of the pattern signature against res_ty
2000 ; wrap <- addErrCtxtM (mk_msg sig_ty) $
2001 tcSubTypeET_NC PatSigCtxt res_ty sig_ty
2002
2003 -- Phew!
2004 ; return (sig_ty, sig_tvs, sig_wcs, wrap)
2005 } }
2006 where
2007 mk_msg sig_ty tidy_env
2008 = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
2009 ; res_ty <- readExpType res_ty -- should be filled in by now
2010 ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
2011 ; let msg = vcat [ hang (text "When checking that the pattern signature:")
2012 4 (ppr sig_ty)
2013 , nest 2 (hang (text "fits the type of its context:")
2014 2 (ppr res_ty)) ]
2015 ; return (tidy_env, msg) }
2016
2017 patBindSigErr :: [TcTyVar] -> SDoc
2018 patBindSigErr sig_tvs
2019 = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
2020 <+> pprQuotedList sig_tvs)
2021 2 (text "in a pattern binding signature")
2022
2023 {-
2024 Note [Pattern signature binders]
2025 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2026 Consider
2027 data T = forall a. T a (a->Int)
2028 f (T x (f :: a->Int) = blah)
2029
2030 Here
2031 * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk',
2032 It must be a skolem so that that it retains its identity, and
2033 TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
2034
2035 * The type signature pattern (f :: a->Int) binds "a" -> a_sig in the envt
2036
2037 * Then unification makes a_sig := a_sk
2038
2039 That's why we must make a_sig a MetaTv (albeit a SigTv),
2040 not a SkolemTv, so that it can unify to a_sk.
2041
2042 For RULE binders, though, things are a bit different (yuk).
2043 RULE "foo" forall (x::a) (y::[a]). f x y = ...
2044 Here this really is the binding site of the type variable so we'd like
2045 to use a skolem, so that we get a complaint if we unify two of them
2046 together.
2047
2048 Note [Unifying SigTvs]
2049 ~~~~~~~~~~~~~~~~~~~~~~
2050 ALAS we have no decent way of avoiding two SigTvs getting unified.
2051 Consider
2052 f (x::(a,b)) (y::c)) = [fst x, y]
2053 Here we'd really like to complain that 'a' and 'c' are unified. But
2054 for the reasons above we can't make a,b,c into skolems, so they
2055 are just SigTvs that can unify. And indeed, this would be ok,
2056 f x (y::c) = case x of
2057 (x1 :: a1, True) -> [x,y]
2058 (x1 :: a2, False) -> [x,y,y]
2059 Here the type of x's first component is called 'a1' in one branch and
2060 'a2' in the other. We could try insisting on the same OccName, but
2061 they definitely won't have the sane lexical Name.
2062
2063 I think we could solve this by recording in a SigTv a list of all the
2064 in-scope variables that it should not unify with, but it's fiddly.
2065
2066
2067 ************************************************************************
2068 * *
2069 Checking kinds
2070 * *
2071 ************************************************************************
2072
2073 -}
2074
2075 -- | Produce an 'TcKind' suitable for a checking a type that can be * or #.
2076 ekOpen :: TcM TcKind
2077 ekOpen = do { rr <- newFlexiTyVarTy runtimeRepTy
2078 ; return (tYPE rr) }
2079
2080 unifyKinds :: [(TcType, TcKind)] -> TcM ([TcType], TcKind)
2081 unifyKinds act_kinds
2082 = do { kind <- newMetaKindVar
2083 ; let check (ty, act_kind) = checkExpectedKind ty act_kind kind
2084 ; tys' <- mapM check act_kinds
2085 ; return (tys', kind) }
2086
2087 {-
2088 ************************************************************************
2089 * *
2090 Sort checking kinds
2091 * *
2092 ************************************************************************
2093
2094 tcLHsKind converts a user-written kind to an internal, sort-checked kind.
2095 It does sort checking and desugaring at the same time, in one single pass.
2096 -}
2097
2098 tcLHsKind :: LHsKind Name -> TcM Kind
2099 tcLHsKind = tc_lhs_kind kindLevelMode
2100
2101 tc_lhs_kind :: TcTyMode -> LHsKind Name -> TcM Kind
2102 tc_lhs_kind mode k
2103 = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $
2104 tc_lhs_type (kindLevel mode) k liftedTypeKind
2105
2106 promotionErr :: Name -> PromotionErr -> TcM a
2107 promotionErr name err
2108 = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here")
2109 2 (parens reason))
2110 where
2111 reason = case err of
2112 FamDataConPE -> text "it comes from a data family instance"
2113 NoDataKindsTC -> text "Perhaps you intended to use DataKinds"
2114 NoDataKindsDC -> text "Perhaps you intended to use DataKinds"
2115 NoTypeInTypeTC -> text "Perhaps you intended to use TypeInType"
2116 NoTypeInTypeDC -> text "Perhaps you intended to use TypeInType"
2117 PatSynPE -> text "Pattern synonyms cannot be promoted"
2118 _ -> text "it is defined and used in the same recursive group"
2119
2120 {-
2121 ************************************************************************
2122 * *
2123 Scoped type variables
2124 * *
2125 ************************************************************************
2126 -}
2127
2128 badPatSigTvs :: TcType -> [TyVar] -> SDoc
2129 badPatSigTvs sig_ty bad_tvs
2130 = vcat [ fsep [text "The type variable" <> plural bad_tvs,
2131 quotes (pprWithCommas ppr bad_tvs),
2132 text "should be bound by the pattern signature" <+> quotes (ppr sig_ty),
2133 text "but are actually discarded by a type synonym" ]
2134 , text "To fix this, expand the type synonym"
2135 , text "[Note: I hope to lift this restriction in due course]" ]
2136
2137 {-
2138 ************************************************************************
2139 * *
2140 Error messages and such
2141 * *
2142 ************************************************************************
2143 -}
2144
2145 -- | Make an appropriate message for an error in a function argument.
2146 -- Used for both expressions and types.
2147 funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
2148 funAppCtxt fun arg arg_no
2149 = hang (hsep [ text "In the", speakNth arg_no, ptext (sLit "argument of"),
2150 quotes (ppr fun) <> text ", namely"])
2151 2 (quotes (ppr arg))