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