Orient TyVar/TyVar equalities with deepest on the left
[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, RankNTypes #-}
9
10 module TcHsType (
11 -- Type signatures
12 kcHsSigType, tcClassSigType,
13 tcHsSigType, tcHsSigWcType,
14 tcHsPartialSigType,
15 funsSigCtxt, addSigCtxt, pprSigCtxt,
16
17 tcHsClsInstType,
18 tcHsDeriv, tcHsVectInst,
19 tcHsTypeApp,
20 UserTypeCtxt(..),
21 tcImplicitTKBndrs, tcImplicitTKBndrsX,
22 tcExplicitTKBndrs,
23 kcExplicitTKBndrs, kcImplicitTKBndrs,
24
25 -- Type checking type and class decls
26 kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars,
27 tcDataKindSig,
28
29 -- tyvars
30 scopeTyVars, scopeTyVars2,
31
32 -- Kind-checking types
33 -- No kind generalisation, no checkValidType
34 kcLHsQTyVars, kcLHsTyVarBndrs,
35 tcWildCardBinders,
36 tcHsLiftedType, tcHsOpenType,
37 tcHsLiftedTypeNC, tcHsOpenTypeNC,
38 tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
39 tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps,
40 solveEqualities, -- useful re-export
41
42 typeLevelMode, kindLevelMode,
43
44 kindGeneralize, checkExpectedKindX, instantiateTyUntilN,
45 reportFloatingKvs,
46
47 -- Sort-checking kinds
48 tcLHsKindSig, badKindSig,
49
50 -- Zonking and promoting
51 zonkPromoteType,
52
53 -- Pattern type signatures
54 tcHsPatSigType, tcPatSig, funAppCtxt
55 ) where
56
57 #include "HsVersions.h"
58
59 import GhcPrelude
60
61 import HsSyn
62 import TcRnMonad
63 import TcEvidence
64 import TcEnv
65 import TcMType
66 import TcValidity
67 import TcUnify
68 import TcIface
69 import TcSimplify
70 import TcType
71 import TcHsSyn( zonkSigType )
72 import Inst ( tcInstBinders, tcInstBinder )
73 import TyCoRep( TyBinder(..) ) -- Used in tcDataKindSig
74 import Type
75 import Coercion
76 import Kind
77 import RdrName( lookupLocalRdrOcc )
78 import Var
79 import VarSet
80 import TyCon
81 import ConLike
82 import DataCon
83 import Class
84 import Name
85 import NameEnv
86 import NameSet
87 import VarEnv
88 import TysWiredIn
89 import BasicTypes
90 import SrcLoc
91 import Constants ( mAX_CTUPLE_SIZE )
92 import ErrUtils( MsgDoc )
93 import Unique
94 import Util
95 import UniqSupply
96 import Outputable
97 import FastString
98 import PrelNames hiding ( wildCardName )
99 import qualified GHC.LanguageExtensions as LangExt
100
101 import Maybes
102 import Data.List ( partition, mapAccumR )
103 import Control.Monad
104
105 {-
106 ----------------------------
107 General notes
108 ----------------------------
109
110 Unlike with expressions, type-checking types both does some checking and
111 desugars at the same time. This is necessary because we often want to perform
112 equality checks on the types right away, and it would be incredibly painful
113 to do this on un-desugared types. Luckily, desugared types are close enough
114 to HsTypes to make the error messages sane.
115
116 During type-checking, we perform as little validity checking as possible.
117 This is because some type-checking is done in a mutually-recursive knot, and
118 if we look too closely at the tycons, we'll loop. This is why we always must
119 use mkNakedTyConApp and mkNakedAppTys, etc., which never look at a tycon.
120 The mkNamed... functions don't uphold Type invariants, but zonkTcTypeToType
121 will repair this for us. Note that zonkTcType *is* safe within a knot, and
122 can be done repeatedly with no ill effect: it just squeezes out metavariables.
123
124 Generally, after type-checking, you will want to do validity checking, say
125 with TcValidity.checkValidType.
126
127 Validity checking
128 ~~~~~~~~~~~~~~~~~
129 Some of the validity check could in principle be done by the kind checker,
130 but not all:
131
132 - During desugaring, we normalise by expanding type synonyms. Only
133 after this step can we check things like type-synonym saturation
134 e.g. type T k = k Int
135 type S a = a
136 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
137 and then S is saturated. This is a GHC extension.
138
139 - Similarly, also a GHC extension, we look through synonyms before complaining
140 about the form of a class or instance declaration
141
142 - Ambiguity checks involve functional dependencies, and it's easier to wait
143 until knots have been resolved before poking into them
144
145 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
146 finished building the loop. So to keep things simple, we postpone most validity
147 checking until step (3).
148
149 Knot tying
150 ~~~~~~~~~~
151 During step (1) we might fault in a TyCon defined in another module, and it might
152 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
153 knot around type declarations with ARecThing, so that the fault-in code can get
154 the TyCon being defined.
155
156 %************************************************************************
157 %* *
158 Check types AND do validity checking
159 * *
160 ************************************************************************
161 -}
162
163 funsSigCtxt :: [Located Name] -> UserTypeCtxt
164 -- Returns FunSigCtxt, with no redundant-context-reporting,
165 -- form a list of located names
166 funsSigCtxt (L _ name1 : _) = FunSigCtxt name1 False
167 funsSigCtxt [] = panic "funSigCtxt"
168
169 addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
170 addSigCtxt ctxt hs_ty thing_inside
171 = setSrcSpan (getLoc hs_ty) $
172 addErrCtxt (pprSigCtxt ctxt hs_ty) $
173 thing_inside
174
175 pprSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> SDoc
176 -- (pprSigCtxt ctxt <extra> <type>)
177 -- prints In the type signature for 'f':
178 -- f :: <type>
179 -- The <extra> is either empty or "the ambiguity check for"
180 pprSigCtxt ctxt hs_ty
181 | Just n <- isSigMaybe ctxt
182 = hang (text "In the type signature:")
183 2 (pprPrefixOcc n <+> dcolon <+> ppr hs_ty)
184
185 | otherwise
186 = hang (text "In" <+> pprUserTypeCtxt ctxt <> colon)
187 2 (ppr hs_ty)
188
189 tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
190 -- This one is used when we have a LHsSigWcType, but in
191 -- a place where wildards aren't allowed. The renamer has
192 -- already checked this, so we can simply ignore it.
193 tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
194
195 kcHsSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
196 kcHsSigType skol_info names (HsIB { hsib_body = hs_ty
197 , hsib_ext = HsIBRn { hsib_vars = sig_vars }})
198 = addSigCtxt (funsSigCtxt names) hs_ty $
199 discardResult $
200 tcImplicitTKBndrs skol_info sig_vars $
201 tc_lhs_type typeLevelMode hs_ty liftedTypeKind
202 kcHsSigType _ _ (XHsImplicitBndrs _) = panic "kcHsSigType"
203
204 tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
205 -- Does not do validity checking; this must be done outside
206 -- the recursive class declaration "knot"
207 tcClassSigType skol_info names sig_ty
208 = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
209 tc_hs_sig_type_and_gen skol_info sig_ty liftedTypeKind
210
211 tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
212 -- Does validity checking
213 -- See Note [Recipe for checking a signature]
214 tcHsSigType ctxt sig_ty
215 = addSigCtxt ctxt (hsSigType sig_ty) $
216 do { kind <- case expectedKindInCtxt ctxt of
217 AnythingKind -> newMetaKindVar
218 TheKind k -> return k
219 OpenKind -> newOpenTypeKind
220 -- The kind is checked by checkValidType, and isn't necessarily
221 -- of kind * in a Template Haskell quote eg [t| Maybe |]
222
223 -- Generalise here: see Note [Kind generalisation]
224 ; do_kind_gen <- decideKindGeneralisationPlan sig_ty
225 ; ty <- if do_kind_gen
226 then tc_hs_sig_type_and_gen skol_info sig_ty kind
227 else tc_hs_sig_type skol_info sig_ty kind
228
229 ; checkValidType ctxt ty
230 ; return ty }
231 where
232 skol_info = SigTypeSkol ctxt
233
234 tc_hs_sig_type_and_gen :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
235 -- Kind-checks/desugars an 'LHsSigType',
236 -- solve equalities,
237 -- and then kind-generalizes.
238 -- This will never emit constraints, as it uses solveEqualities interally.
239 -- No validity checking, but it does zonk en route to generalization
240 tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext
241 = HsIBRn { hsib_vars = sig_vars }
242 , hsib_body = hs_ty }) kind
243 = do { (tkvs, ty) <- solveEqualities $
244 tcImplicitTKBndrs skol_info sig_vars $
245 tc_lhs_type typeLevelMode hs_ty kind
246 -- NB the call to solveEqualities, which unifies all those
247 -- kind variables floating about, immediately prior to
248 -- kind generalisation
249
250 -- We use the "InKnot" zonker, because this is called
251 -- on class method sigs in the knot
252 ; ty1 <- zonkPromoteTypeInKnot $ mkSpecForAllTys tkvs ty
253 ; kvs <- kindGeneralize ty1
254 ; zonkSigType (mkInvForAllTys kvs ty1) }
255
256 tc_hs_sig_type_and_gen _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
257
258 tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
259 -- Kind-check/desugar a 'LHsSigType', but does not solve
260 -- the equalities that arise from doing so; instead it may
261 -- emit kind-equality constraints into the monad
262 -- Zonking, but no validity checking
263 tc_hs_sig_type skol_info (HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars }
264 , hsib_body = hs_ty }) kind
265 = do { (tkvs, ty) <- tcImplicitTKBndrs skol_info sig_vars $
266 tc_lhs_type typeLevelMode hs_ty kind
267
268 -- need to promote any remaining metavariables; test case:
269 -- dependent/should_fail/T14066e.
270 ; zonkPromoteType (mkSpecForAllTys tkvs ty) }
271
272 tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type"
273
274 -----------------
275 tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
276 -- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
277 -- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
278 -- E.g. class C (a::*) (b::k->k)
279 -- data T a b = ... deriving( C Int )
280 -- returns ([k], C, [k, Int], [k->k])
281 tcHsDeriv hs_ty
282 = do { cls_kind <- newMetaKindVar
283 -- always safe to kind-generalize, because there
284 -- can be no covars in an outer scope
285 ; ty <- checkNoErrs $
286 -- avoid redundant error report with "illegal deriving", below
287 tc_hs_sig_type_and_gen (SigTypeSkol DerivClauseCtxt) hs_ty cls_kind
288 ; cls_kind <- zonkTcType cls_kind
289 ; let (tvs, pred) = splitForAllTys ty
290 ; let (args, _) = splitFunTys cls_kind
291 ; case getClassPredTys_maybe pred of
292 Just (cls, tys) -> return (tvs, cls, tys, args)
293 Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
294
295 tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt
296 -> LHsSigType GhcRn
297 -> TcM ([TyVar], ThetaType, Class, [Type])
298 -- Like tcHsSigType, but for a class instance declaration
299 tcHsClsInstType user_ctxt hs_inst_ty
300 = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
301 do { inst_ty <- tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind
302 ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
303
304 -- Used for 'VECTORISE [SCALAR] instance' declarations
305 tcHsVectInst :: LHsSigType GhcRn -> TcM (Class, [Type])
306 tcHsVectInst ty
307 | let hs_cls_ty = hsSigType ty
308 , Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe hs_cls_ty
309 -- Ignoring the binders looks pretty dodgy to me
310 = do { (cls, cls_kind) <- tcClass cls_name
311 ; (applied_class, _res_kind)
312 <- tcTyApps typeLevelMode hs_cls_ty (mkClassPred cls []) cls_kind tys
313 ; case tcSplitTyConApp_maybe applied_class of
314 Just (_tc, args) -> ASSERT( _tc == classTyCon cls )
315 return (cls, args)
316 _ -> failWithTc (text "Too many arguments passed to" <+> ppr cls_name) }
317 | otherwise
318 = failWithTc $ text "Malformed instance type"
319
320 ----------------------------------------------
321 -- | Type-check a visible type application
322 tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
323 -- See Note [Recipe for checking a signature] in TcHsType
324 tcHsTypeApp wc_ty kind
325 | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
326 = do { ty <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ _ ->
327 tcCheckLHsType hs_ty kind
328 ; ty <- zonkPromoteType ty
329 ; checkValidType TypeAppCtxt ty
330 ; return ty }
331 -- NB: we don't call emitWildcardHoleConstraints here, because
332 -- we want any holes in visible type applications to be used
333 -- without fuss. No errors, warnings, extensions, etc.
334 tcHsTypeApp (XHsWildCardBndrs _) _ = panic "tcHsTypeApp"
335
336 {-
337 ************************************************************************
338 * *
339 The main kind checker: no validity checks here
340 * *
341 ************************************************************************
342
343 First a couple of simple wrappers for kcHsType
344 -}
345
346 ---------------------------
347 tcHsOpenType, tcHsLiftedType,
348 tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
349 -- Used for type signatures
350 -- Do not do validity checking
351 tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty
352 tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty
353
354 tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind
355 ; tc_lhs_type typeLevelMode ty ek }
356 tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
357
358 -- Like tcHsType, but takes an expected kind
359 tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
360 tcCheckLHsType hs_ty exp_kind
361 = addTypeCtxt hs_ty $
362 tc_lhs_type typeLevelMode hs_ty exp_kind
363
364 tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
365 -- Called from outside: set the context
366 tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
367
368 -- Like tcLHsType, but use it in a context where type synonyms and type families
369 -- do not need to be saturated, like in a GHCi :kind call
370 tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
371 tcLHsTypeUnsaturated ty = addTypeCtxt ty (tc_infer_lhs_type mode ty)
372 where
373 mode = allowUnsaturated typeLevelMode
374
375 ---------------------------
376 -- | Should we generalise the kind of this type signature?
377 -- We *should* generalise if the type is closed
378 -- or if NoMonoLocalBinds is set. Otherwise, nope.
379 -- See Note [Kind generalisation plan]
380 decideKindGeneralisationPlan :: LHsSigType GhcRn -> TcM Bool
381 decideKindGeneralisationPlan sig_ty@(HsIB { hsib_ext
382 = HsIBRn { hsib_closed = closed } })
383 = do { mono_locals <- xoptM LangExt.MonoLocalBinds
384 ; let should_gen = not mono_locals || closed
385 ; traceTc "decideKindGeneralisationPlan"
386 (ppr sig_ty $$ text "should gen?" <+> ppr should_gen)
387 ; return should_gen }
388 decideKindGeneralisationPlan(XHsImplicitBndrs _)
389 = panic "decideKindGeneralisationPlan"
390
391 {- Note [Kind generalisation plan]
392 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
393 When should we do kind-generalisation for user-written type signature?
394 Answer: we use the same rule as for value bindings:
395
396 * We always kind-generalise if the type signature is closed
397 * Additionally, we attempt to generalise if we have NoMonoLocalBinds
398
399 Trac #13337 shows the problem if we kind-generalise an open type (i.e.
400 one that mentions in-scope type variable
401 foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
402 => proxy a -> String
403 foo _ = case eqT :: Maybe (k :~: Type) of
404 Nothing -> ...
405 Just Refl -> case eqT :: Maybe (a :~: Int) of ...
406
407 In the expression type sig on the last line, we have (a :: k)
408 but (Int :: Type). Since (:~:) is kind-homogeneous, this requires
409 k ~ *, which is true in the Refl branch of the outer case.
410
411 That equality will be solved if we allow it to float out to the
412 implication constraint for the Refl match, but not not if we aggressively
413 attempt to solve all equalities the moment they occur; that is, when
414 checking (Maybe (a :~: Int)). (NB: solveEqualities fails unless it
415 solves all the kind equalities, which is the right thing at top level.)
416
417 So here the right thing is simply not to do kind generalisation!
418
419 ************************************************************************
420 * *
421 Type-checking modes
422 * *
423 ************************************************************************
424
425 The kind-checker is parameterised by a TcTyMode, which contains some
426 information about where we're checking a type.
427
428 The renamer issues errors about what it can. All errors issued here must
429 concern things that the renamer can't handle.
430
431 -}
432
433 -- | Info about the context in which we're checking a type. Currently,
434 -- differentiates only between types and kinds, but this will likely
435 -- grow, at least to include the distinction between patterns and
436 -- not-patterns.
437 data TcTyMode
438 = TcTyMode { mode_level :: TypeOrKind
439 , mode_unsat :: Bool -- True <=> allow unsaturated type families
440 }
441 -- The mode_unsat field is solely so that type families/synonyms can be unsaturated
442 -- in GHCi :kind calls
443
444 typeLevelMode :: TcTyMode
445 typeLevelMode = TcTyMode { mode_level = TypeLevel, mode_unsat = False }
446
447 kindLevelMode :: TcTyMode
448 kindLevelMode = TcTyMode { mode_level = KindLevel, mode_unsat = False }
449
450 allowUnsaturated :: TcTyMode -> TcTyMode
451 allowUnsaturated mode = mode { mode_unsat = True }
452
453 -- switch to kind level
454 kindLevel :: TcTyMode -> TcTyMode
455 kindLevel mode = mode { mode_level = KindLevel }
456
457 instance Outputable TcTyMode where
458 ppr = ppr . mode_level
459
460 {-
461 Note [Bidirectional type checking]
462 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
463 In expressions, whenever we see a polymorphic identifier, say `id`, we are
464 free to instantiate it with metavariables, knowing that we can always
465 re-generalize with type-lambdas when necessary. For example:
466
467 rank2 :: (forall a. a -> a) -> ()
468 x = rank2 id
469
470 When checking the body of `x`, we can instantiate `id` with a metavariable.
471 Then, when we're checking the application of `rank2`, we notice that we really
472 need a polymorphic `id`, and then re-generalize over the unconstrained
473 metavariable.
474
475 In types, however, we're not so lucky, because *we cannot re-generalize*!
476 There is no lambda. So, we must be careful only to instantiate at the last
477 possible moment, when we're sure we're never going to want the lost polymorphism
478 again. This is done in calls to tcInstBinders.
479
480 To implement this behavior, we use bidirectional type checking, where we
481 explicitly think about whether we know the kind of the type we're checking
482 or not. Note that there is a difference between not knowing a kind and
483 knowing a metavariable kind: the metavariables are TauTvs, and cannot become
484 forall-quantified kinds. Previously (before dependent types), there were
485 no higher-rank kinds, and so we could instantiate early and be sure that
486 no types would have polymorphic kinds, and so we could always assume that
487 the kind of a type was a fresh metavariable. Not so anymore, thus the
488 need for two algorithms.
489
490 For HsType forms that can never be kind-polymorphic, we implement only the
491 "down" direction, where we safely assume a metavariable kind. For HsType forms
492 that *can* be kind-polymorphic, we implement just the "up" (functions with
493 "infer" in their name) version, as we gain nothing by also implementing the
494 "down" version.
495
496 Note [Future-proofing the type checker]
497 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
498 As discussed in Note [Bidirectional type checking], each HsType form is
499 handled in *either* tc_infer_hs_type *or* tc_hs_type. These functions
500 are mutually recursive, so that either one can work for any type former.
501 But, we want to make sure that our pattern-matches are complete. So,
502 we have a bunch of repetitive code just so that we get warnings if we're
503 missing any patterns.
504
505 Note [The tcType invariant]
506 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
507 If tc_ty = tc_hs_type hs_ty exp_kind
508 then
509 typeKind tc_ty = exp_kind
510 without any zonking needed. The reason for this is that in
511 tcInferApps we see (F ty), and we kind-check 'ty' with an
512 expected-kind coming from F. Then, to make the resulting application
513 well kinded --- see Note [Ensure well-kinded types] in TcType --- we
514 need the kind-checked 'ty' to have exactly the kind that F expects,
515 with no funny zonking nonsense in between.
516
517 The tcType invariant also applies to checkExpectedKind: if
518 (tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
519 then
520 typeKind tc_ty = exp_ki
521 -}
522
523 ------------------------------------------
524 -- | Check and desugar a type, returning the core type and its
525 -- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
526 -- level.
527 tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
528 tc_infer_lhs_type mode (L span ty)
529 = setSrcSpan span $
530 do { (ty', kind) <- tc_infer_hs_type mode ty
531 ; return (ty', kind) }
532
533 -- | Infer the kind of a type and desugar. This is the "up" type-checker,
534 -- as described in Note [Bidirectional type checking]
535 tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
536 tc_infer_hs_type mode (HsParTy _ t) = tc_infer_lhs_type mode t
537 tc_infer_hs_type mode (HsTyVar _ _ (L _ tv)) = tcTyVar mode tv
538
539 tc_infer_hs_type mode (HsAppTy _ ty1 ty2)
540 = do { let (hs_fun_ty, hs_arg_tys) = splitHsAppTys ty1 [ty2]
541 ; (fun_ty, fun_kind) <- tc_infer_lhs_type mode hs_fun_ty
542 -- A worry: what if fun_kind needs zoonking?
543 -- We used to zonk it here, but that got fun_ty and fun_kind
544 -- out of sync (see the precondition to tcTyApps), which caused
545 -- Trac #14873. So I'm now zonking in tcTyVar, and not here.
546 -- Is that enough? Seems so, but I can't see how to be certain.
547 ; tcTyApps mode hs_fun_ty fun_ty fun_kind hs_arg_tys }
548
549 tc_infer_hs_type mode (HsOpTy _ lhs lhs_op@(L _ hs_op) rhs)
550 | not (hs_op `hasKey` funTyConKey)
551 = do { (op, op_kind) <- tcTyVar mode hs_op
552 -- See "A worry" in the HsApp case
553 ; tcTyApps mode (noLoc $ HsTyVar noExt NotPromoted lhs_op) op op_kind
554 [lhs, rhs] }
555
556 tc_infer_hs_type mode (HsKindSig _ ty sig)
557 = do { sig' <- tc_lhs_kind (kindLevel mode) sig
558 ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
559 ; ty' <- tc_lhs_type mode ty sig'
560 ; return (ty', sig') }
561
562 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
563 -- the splice location to the typechecker. Here we skip over it in order to have
564 -- the same kind inferred for a given expression whether it was produced from
565 -- splices or not.
566 --
567 -- See Note [Delaying modFinalizers in untyped splices].
568 tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
569 = tc_infer_hs_type mode ty
570
571 tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
572 tc_infer_hs_type _ (XHsType (NHsCoreTy ty)) = return (ty, typeKind ty)
573 tc_infer_hs_type mode other_ty
574 = do { kv <- newMetaKindVar
575 ; ty' <- tc_hs_type mode other_ty kv
576 ; return (ty', kv) }
577
578 ------------------------------------------
579 tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
580 tc_lhs_type mode (L span ty) exp_kind
581 = setSrcSpan span $
582 tc_hs_type mode ty exp_kind
583
584 ------------------------------------------
585 tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
586 -> TcM TcType
587 tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
588 TypeLevel ->
589 do { arg_k <- newOpenTypeKind
590 ; res_k <- newOpenTypeKind
591 ; ty1' <- tc_lhs_type mode ty1 arg_k
592 ; ty2' <- tc_lhs_type mode ty2 res_k
593 ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
594 liftedTypeKind exp_kind }
595 KindLevel -> -- no representation polymorphism in kinds. yet.
596 do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
597 ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
598 ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
599 liftedTypeKind exp_kind }
600
601 ------------------------------------------
602 tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
603 -- See Note [The tcType invariant]
604 -- See Note [Bidirectional type checking]
605
606 tc_hs_type mode (HsParTy _ ty) exp_kind = tc_lhs_type mode ty exp_kind
607 tc_hs_type mode (HsDocTy _ ty _) exp_kind = tc_lhs_type mode ty exp_kind
608 tc_hs_type _ ty@(HsBangTy _ bang _) _
609 -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
610 -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
611 -- bangs are invalid, so fail. (#7210, #14761)
612 = do { let bangError err = failWith $
613 text "Unexpected" <+> text err <+> text "annotation:" <+> ppr ty $$
614 text err <+> text "annotation cannot appear nested inside a type"
615 ; case bang of
616 HsSrcBang _ SrcUnpack _ -> bangError "UNPACK"
617 HsSrcBang _ SrcNoUnpack _ -> bangError "NOUNPACK"
618 HsSrcBang _ NoSrcUnpack SrcLazy -> bangError "laziness"
619 HsSrcBang _ _ _ -> bangError "strictness" }
620 tc_hs_type _ ty@(HsRecTy {}) _
621 -- Record types (which only show up temporarily in constructor
622 -- signatures) should have been removed by now
623 = failWithTc (text "Record syntax is illegal here:" <+> ppr ty)
624
625 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType'.
626 -- Here we get rid of it and add the finalizers to the global environment
627 -- while capturing the local environment.
628 --
629 -- See Note [Delaying modFinalizers in untyped splices].
630 tc_hs_type mode (HsSpliceTy _ (HsSpliced _ mod_finalizers (HsSplicedTy ty)))
631 exp_kind
632 = do addModFinalizersWithLclEnv mod_finalizers
633 tc_hs_type mode ty exp_kind
634
635 -- This should never happen; type splices are expanded by the renamer
636 tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind
637 = failWithTc (text "Unexpected type splice:" <+> ppr ty)
638
639 ---------- Functions and applications
640 tc_hs_type mode (HsFunTy _ ty1 ty2) exp_kind
641 = tc_fun_type mode ty1 ty2 exp_kind
642
643 tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
644 | op `hasKey` funTyConKey
645 = tc_fun_type mode ty1 ty2 exp_kind
646
647 --------- Foralls
648 tc_hs_type mode forall@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
649 = do { (tvs', ty') <- tcExplicitTKBndrs (ForAllSkol (ppr forall)) hs_tvs $
650 tc_lhs_type mode ty exp_kind
651 -- Do not kind-generalise here! See Note [Kind generalisation]
652 -- Why exp_kind? See Note [Body kind of HsForAllTy]
653 ; let bndrs = mkTyVarBinders Specified tvs'
654 ; return (mkForAllTys bndrs ty') }
655
656 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
657 | null (unLoc ctxt)
658 = tc_lhs_type mode ty exp_kind
659
660 | otherwise
661 = do { ctxt' <- tc_hs_context mode ctxt
662
663 -- See Note [Body kind of a HsQualTy]
664 ; ty' <- if isConstraintKind exp_kind
665 then tc_lhs_type mode ty constraintKind
666 else do { ek <- newOpenTypeKind
667 -- The body kind (result of the function)
668 -- can be * or #, hence newOpenTypeKind
669 ; ty' <- tc_lhs_type mode ty ek
670 ; checkExpectedKind (unLoc ty) ty' liftedTypeKind exp_kind }
671
672 ; return (mkPhiTy ctxt' ty') }
673
674 --------- Lists, arrays, and tuples
675 tc_hs_type mode rn_ty@(HsListTy _ elt_ty) exp_kind
676 = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
677 ; checkWiredInTyCon listTyCon
678 ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
679
680 tc_hs_type mode rn_ty@(HsPArrTy _ elt_ty) exp_kind
681 = do { MASSERT( isTypeLevel (mode_level mode) )
682 ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
683 ; checkWiredInTyCon parrTyCon
684 ; checkExpectedKind rn_ty (mkPArrTy tau_ty) liftedTypeKind exp_kind }
685
686 -- See Note [Distinguishing tuple kinds] in HsTypes
687 -- See Note [Inferring tuple kinds]
688 tc_hs_type mode rn_ty@(HsTupleTy _ HsBoxedOrConstraintTuple hs_tys) exp_kind
689 -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
690 | Just tup_sort <- tupKindSort_maybe exp_kind
691 = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
692 tc_tuple rn_ty mode tup_sort hs_tys exp_kind
693 | otherwise
694 = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
695 ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
696 ; kinds <- mapM zonkTcType kinds
697 -- Infer each arg type separately, because errors can be
698 -- confusing if we give them a shared kind. Eg Trac #7410
699 -- (Either Int, Int), we do not want to get an error saying
700 -- "the second argument of a tuple should have kind *->*"
701
702 ; let (arg_kind, tup_sort)
703 = case [ (k,s) | k <- kinds
704 , Just s <- [tupKindSort_maybe k] ] of
705 ((k,s) : _) -> (k,s)
706 [] -> (liftedTypeKind, BoxedTuple)
707 -- In the [] case, it's not clear what the kind is, so guess *
708
709 ; tys' <- sequence [ setSrcSpan loc $
710 checkExpectedKind hs_ty ty kind arg_kind
711 | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
712
713 ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
714
715
716 tc_hs_type mode rn_ty@(HsTupleTy _ hs_tup_sort tys) exp_kind
717 = tc_tuple rn_ty mode tup_sort tys exp_kind
718 where
719 tup_sort = case hs_tup_sort of -- Fourth case dealt with above
720 HsUnboxedTuple -> UnboxedTuple
721 HsBoxedTuple -> BoxedTuple
722 HsConstraintTuple -> ConstraintTuple
723 _ -> panic "tc_hs_type HsTupleTy"
724
725 tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
726 = do { let arity = length hs_tys
727 ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
728 ; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
729 ; let arg_reps = map getRuntimeRepFromKind arg_kinds
730 arg_tys = arg_reps ++ tau_tys
731 ; checkExpectedKind rn_ty
732 (mkTyConApp (sumTyCon arity) arg_tys)
733 (unboxedSumKind arg_reps)
734 exp_kind
735 }
736
737 --------- Promoted lists and tuples
738 tc_hs_type mode rn_ty@(HsExplicitListTy _ _ tys) exp_kind
739 = do { tks <- mapM (tc_infer_lhs_type mode) tys
740 ; (taus', kind) <- unifyKinds tys tks
741 ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
742 ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
743 where
744 mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
745 mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k]
746
747 tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
748 -- using newMetaKindVar means that we force instantiations of any polykinded
749 -- types. At first, I just used tc_infer_lhs_type, but that led to #11255.
750 = do { ks <- replicateM arity newMetaKindVar
751 ; taus <- zipWithM (tc_lhs_type mode) tys ks
752 ; let kind_con = tupleTyCon Boxed arity
753 ty_con = promotedTupleDataCon Boxed arity
754 tup_k = mkTyConApp kind_con ks
755 ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
756 where
757 arity = length tys
758
759 --------- Constraint types
760 tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
761 = do { MASSERT( isTypeLevel (mode_level mode) )
762 ; ty' <- tc_lhs_type mode ty liftedTypeKind
763 ; let n' = mkStrLitTy $ hsIPNameFS n
764 ; ipClass <- tcLookupClass ipClassName
765 ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
766 constraintKind exp_kind }
767
768 tc_hs_type mode rn_ty@(HsEqTy _ ty1 ty2) exp_kind
769 = do { (ty1', kind1) <- tc_infer_lhs_type mode ty1
770 ; (ty2', kind2) <- tc_infer_lhs_type mode ty2
771 ; ty2'' <- checkExpectedKind (unLoc ty2) ty2' kind2 kind1
772 ; eq_tc <- tcLookupTyCon eqTyConName
773 ; let ty' = mkNakedTyConApp eq_tc [kind1, ty1', ty2'']
774 ; checkExpectedKind rn_ty ty' constraintKind exp_kind }
775
776 --------- Literals
777 tc_hs_type _ rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
778 = do { checkWiredInTyCon typeNatKindCon
779 ; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
780
781 tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
782 = do { checkWiredInTyCon typeSymbolKindCon
783 ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
784
785 --------- Potentially kind-polymorphic types: call the "up" checker
786 -- See Note [Future-proofing the type checker]
787 tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
788 tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek
789 tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
790 tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
791 tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
792
793 tc_hs_type _ (HsWildCardTy wc) exp_kind
794 = do { wc_ty <- tcWildCardOcc wc exp_kind
795 ; return (mkNakedCastTy wc_ty (mkTcNomReflCo exp_kind))
796 -- Take care here! Even though the coercion is Refl,
797 -- we still need it to establish Note [The tcType invariant]
798 }
799
800 -- disposed of by renamer
801 tc_hs_type _ ty@(HsAppsTy {}) _
802 = pprPanic "tc_hs_tyep HsAppsTy" (ppr ty)
803
804 tcWildCardOcc :: HsWildCardInfo -> Kind -> TcM TcType
805 tcWildCardOcc wc_info exp_kind
806 = do { wc_tv <- tcLookupTyVar (wildCardName wc_info)
807 -- The wildcard's kind should be an un-filled-in meta tyvar
808 ; checkExpectedKind (HsWildCardTy wc_info) (mkTyVarTy wc_tv)
809 (tyVarKind wc_tv) exp_kind }
810
811 ---------------------------
812 -- | Call 'tc_infer_hs_type' and check its result against an expected kind.
813 tc_infer_hs_type_ek :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
814 tc_infer_hs_type_ek mode hs_ty ek
815 = do { (ty, k) <- tc_infer_hs_type mode hs_ty
816 ; checkExpectedKind hs_ty ty k ek }
817
818 ---------------------------
819 tupKindSort_maybe :: TcKind -> Maybe TupleSort
820 tupKindSort_maybe k
821 | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
822 | Just k' <- tcView k = tupKindSort_maybe k'
823 | isConstraintKind k = Just ConstraintTuple
824 | isLiftedTypeKind k = Just BoxedTuple
825 | otherwise = Nothing
826
827 tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
828 tc_tuple rn_ty mode tup_sort tys exp_kind
829 = do { arg_kinds <- case tup_sort of
830 BoxedTuple -> return (nOfThem arity liftedTypeKind)
831 UnboxedTuple -> mapM (\_ -> newOpenTypeKind) tys
832 ConstraintTuple -> return (nOfThem arity constraintKind)
833 ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
834 ; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
835 where
836 arity = length tys
837
838 finish_tuple :: HsType GhcRn
839 -> TupleSort
840 -> [TcType] -- ^ argument types
841 -> [TcKind] -- ^ of these kinds
842 -> TcKind -- ^ expected kind of the whole tuple
843 -> TcM TcType
844 finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
845 = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
846 ; let arg_tys = case tup_sort of
847 -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
848 UnboxedTuple -> tau_reps ++ tau_tys
849 BoxedTuple -> tau_tys
850 ConstraintTuple -> tau_tys
851 ; tycon <- case tup_sort of
852 ConstraintTuple
853 | arity > mAX_CTUPLE_SIZE
854 -> failWith (bigConstraintTuple arity)
855 | otherwise -> tcLookupTyCon (cTupleTyConName arity)
856 BoxedTuple -> do { let tc = tupleTyCon Boxed arity
857 ; checkWiredInTyCon tc
858 ; return tc }
859 UnboxedTuple -> return (tupleTyCon Unboxed arity)
860 ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind }
861 where
862 arity = length tau_tys
863 tau_reps = map getRuntimeRepFromKind tau_kinds
864 res_kind = case tup_sort of
865 UnboxedTuple -> unboxedTupleKind tau_reps
866 BoxedTuple -> liftedTypeKind
867 ConstraintTuple -> constraintKind
868
869 bigConstraintTuple :: Arity -> MsgDoc
870 bigConstraintTuple arity
871 = hang (text "Constraint tuple arity too large:" <+> int arity
872 <+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
873 2 (text "Instead, use a nested tuple")
874
875 ---------------------------
876 -- | Apply a type of a given kind to a list of arguments. This instantiates
877 -- invisible parameters as necessary. Always consumes all the arguments,
878 -- using matchExpectedFunKind as necessary.
879 -- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.
880 -- These kinds should be used to instantiate invisible kind variables;
881 -- they come from an enclosing class for an associated type/data family.
882 tcInferApps :: TcTyMode
883 -> Maybe (VarEnv Kind) -- ^ Possibly, kind info (see above)
884 -> LHsType GhcRn -- ^ Function (for printing only)
885 -> TcType -- ^ Function (could be knot-tied)
886 -> TcKind -- ^ Function kind (zonked)
887 -> [LHsType GhcRn] -- ^ Args
888 -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
889 -- Precondition: typeKind fun_ty = fun_ki
890 -- Reason: we will return a type application like (fun_ty arg1 ... argn),
891 -- and that type must be well-kinded
892 -- See Note [The tcType invariant]
893 tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
894 = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki)
895 ; stuff <- go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
896 ; traceTc "tcInferApps }" empty
897 ; return stuff }
898 where
899 empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
900 tyCoVarsOfType fun_ki
901 (orig_ki_binders, orig_inner_ki) = tcSplitPiTys fun_ki
902
903 go :: Int -- the # of the next argument
904 -> [TcType] -- already type-checked args, in reverse order
905 -> TCvSubst -- instantiating substitution
906 -> TcType -- function applied to some args, could be knot-tied
907 -> [TyBinder] -- binders in function kind (both vis. and invis.)
908 -> TcKind -- function kind body (not a Pi-type)
909 -> [LHsType GhcRn] -- un-type-checked args
910 -> TcM (TcType, [TcType], TcKind) -- same as overall return type
911
912 -- no user-written args left. We're done!
913 go _ acc_args subst fun ki_binders inner_ki []
914 = return (fun, reverse acc_args, substTy subst $ mkPiTys ki_binders inner_ki)
915
916 -- The function's kind has a binder. Is it visible or invisible?
917 go n acc_args subst fun (ki_binder:ki_binders) inner_ki
918 all_args@(arg:args)
919 | isInvisibleBinder ki_binder
920 -- It's invisible. Instantiate.
921 = do { traceTc "tcInferApps (invis)" (ppr ki_binder $$ ppr subst)
922 ; (subst', arg') <- tcInstBinder mb_kind_info subst ki_binder
923 ; go n (arg' : acc_args) subst' (mkNakedAppTy fun arg')
924 ki_binders inner_ki all_args }
925
926 | otherwise
927 -- It's visible. Check the next user-written argument
928 = do { traceTc "tcInferApps (vis)" (vcat [ ppr ki_binder, ppr arg
929 , ppr (tyBinderType ki_binder)
930 , ppr subst ])
931 ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
932 tc_lhs_type mode arg (substTy subst $ tyBinderType ki_binder)
933 ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
934 ; go (n+1) (arg' : acc_args) subst'
935 (mkNakedAppTy fun arg')
936 ki_binders inner_ki args }
937
938 -- We've run out of known binders in the functions's kind.
939 go n acc_args subst fun [] inner_ki all_args
940 | not (null new_ki_binders)
941 -- But, after substituting, we have more binders.
942 = go n acc_args zapped_subst fun new_ki_binders new_inner_ki all_args
943
944 | otherwise
945 -- Even after substituting, still no binders. Use matchExpectedFunKind
946 = do { traceTc "tcInferApps (no binder)" (ppr new_inner_ki $$ ppr zapped_subst)
947 ; (co, arg_k, res_k) <- matchExpectedFunKind hs_ty substed_inner_ki
948 ; let new_in_scope = tyCoVarsOfTypes [arg_k, res_k]
949 subst' = zapped_subst `extendTCvInScopeSet` new_in_scope
950 ; go n acc_args subst'
951 (fun `mkNakedCastTy` co)
952 [mkAnonBinder arg_k]
953 res_k all_args }
954 where
955 substed_inner_ki = substTy subst inner_ki
956 (new_ki_binders, new_inner_ki) = tcSplitPiTys substed_inner_ki
957 zapped_subst = zapTCvSubst subst
958 hs_ty = mkHsAppTys orig_hs_ty (take (n-1) orig_hs_args)
959
960
961 -- | Applies a type to a list of arguments.
962 -- Always consumes all the arguments, using 'matchExpectedFunKind' as
963 -- necessary. If you wish to apply a type to a list of HsTypes, this is
964 -- your function.
965 -- Used for type-checking types only.
966 tcTyApps :: TcTyMode
967 -> LHsType GhcRn -- ^ Function (for printing only)
968 -> TcType -- ^ Function (could be knot-tied)
969 -> TcKind -- ^ Function kind (zonked)
970 -> [LHsType GhcRn] -- ^ Args
971 -> TcM (TcType, TcKind) -- ^ (f args, result kind)
972 -- Precondition: see precondition for tcInferApps
973 tcTyApps mode orig_hs_ty fun_ty fun_ki args
974 = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty fun_ty fun_ki args
975 ; return (ty', ki') }
976
977 --------------------------
978 -- Like checkExpectedKindX, but returns only the final type; convenient wrapper
979 -- Obeys Note [The tcType invariant]
980 checkExpectedKind :: HsType GhcRn -- type we're checking (for printing)
981 -> TcType -- type we're checking (might be knot-tied)
982 -> TcKind -- the known kind of that type
983 -> TcKind -- the expected kind
984 -> TcM TcType
985 checkExpectedKind hs_ty ty act exp
986 = fstOf3 <$> checkExpectedKindX Nothing (ppr hs_ty) ty act exp
987
988 checkExpectedKindX :: Maybe (VarEnv Kind) -- Possibly, instantiations for kind vars
989 -> SDoc -- HsType whose kind we're checking
990 -> TcType -- the type whose kind we're checking
991 -> TcKind -- the known kind of that type, k
992 -> TcKind -- the expected kind, exp_kind
993 -> TcM (TcType, [TcType], TcCoercionN)
994 -- (the new args, the coercion)
995 -- Instantiate a kind (if necessary) and then call unifyType
996 -- (checkExpectedKind ty act_kind exp_kind)
997 -- checks that the actual kind act_kind is compatible
998 -- with the expected kind exp_kind
999 checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
1000 = do { -- We need to make sure that both kinds have the same number of implicit
1001 -- foralls out front. If the actual kind has more, instantiate accordingly.
1002 -- Otherwise, just pass the type & kind through: the errors are caught
1003 -- in unifyType.
1004 let (exp_bndrs, _) = splitPiTysInvisible exp_kind
1005 n_exp = length exp_bndrs
1006 ; (new_args, act_kind') <- instantiateTyUntilN mb_kind_env n_exp act_kind
1007
1008 ; let origin = TypeEqOrigin { uo_actual = act_kind'
1009 , uo_expected = exp_kind
1010 , uo_thing = Just pp_hs_ty
1011 , uo_visible = True } -- the hs_ty is visible
1012 ty' = mkNakedAppTys ty new_args
1013
1014 ; traceTc "checkExpectedKind" $
1015 vcat [ pp_hs_ty
1016 , text "act_kind:" <+> ppr act_kind
1017 , text "act_kind':" <+> ppr act_kind'
1018 , text "exp_kind:" <+> ppr exp_kind ]
1019
1020 ; if act_kind' `tcEqType` exp_kind
1021 then return (ty', new_args, mkTcNomReflCo exp_kind) -- This is very common
1022 else do { co_k <- uType KindLevel origin act_kind' exp_kind
1023 ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
1024 , ppr exp_kind
1025 , ppr co_k ])
1026 ; let result_ty = ty' `mkNakedCastTy` co_k
1027 -- See Note [The tcType invariant]
1028 ; return (result_ty, new_args, co_k) } }
1029
1030 -- | Instantiate @n@ invisible arguments to a type. If @n <= 0@, no instantiation
1031 -- occurs. If @n@ is too big, then all available invisible arguments are instantiated.
1032 -- (In other words, this function is very forgiving about bad values of @n@.)
1033 instantiateTyN :: Maybe (VarEnv Kind) -- ^ Predetermined instantiations
1034 -- (for assoc. type patterns)
1035 -> Int -- ^ @n@
1036 -> [TyBinder] -> TcKind -- ^ its kind
1037 -> TcM ([TcType], TcKind) -- ^ The inst'ed type, new args, kind
1038 instantiateTyN mb_kind_env n bndrs inner_ki
1039 | n <= 0
1040 = return ([], ki)
1041
1042 | otherwise
1043 = do { (subst, inst_args) <- tcInstBinders empty_subst mb_kind_env inst_bndrs
1044 ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
1045 ki' = substTy subst rebuilt_ki
1046 ; traceTc "instantiateTyN" (vcat [ ppr ki
1047 , ppr n
1048 , ppr subst
1049 , ppr rebuilt_ki
1050 , ppr ki' ])
1051 ; return (inst_args, ki') }
1052 where
1053 -- NB: splitAt is forgiving with invalid numbers
1054 (inst_bndrs, leftover_bndrs) = splitAt n bndrs
1055 ki = mkPiTys bndrs inner_ki
1056 empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ki))
1057
1058 -- | Instantiate a type to have at most @n@ invisible arguments.
1059 instantiateTyUntilN :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
1060 -> Int -- ^ @n@
1061 -> TcKind -- ^ its kind
1062 -> TcM ([TcType], TcKind) -- ^ The new args, final kind
1063 instantiateTyUntilN mb_kind_env n ki
1064 = let (bndrs, inner_ki) = splitPiTysInvisible ki
1065 num_to_inst = length bndrs - n
1066 in
1067 instantiateTyN mb_kind_env num_to_inst bndrs inner_ki
1068
1069 ---------------------------
1070 tcHsMbContext :: Maybe (LHsContext GhcRn) -> TcM [PredType]
1071 tcHsMbContext Nothing = return []
1072 tcHsMbContext (Just cxt) = tcHsContext cxt
1073
1074 tcHsContext :: LHsContext GhcRn -> TcM [PredType]
1075 tcHsContext = tc_hs_context typeLevelMode
1076
1077 tcLHsPredType :: LHsType GhcRn -> TcM PredType
1078 tcLHsPredType = tc_lhs_pred typeLevelMode
1079
1080 tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
1081 tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)
1082
1083 tc_lhs_pred :: TcTyMode -> LHsType GhcRn -> TcM PredType
1084 tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
1085
1086 ---------------------------
1087 tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
1088 -- See Note [Type checking recursive type and class declarations]
1089 -- in TcTyClsDecls
1090 tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
1091 = do { traceTc "lk1" (ppr name)
1092 ; thing <- tcLookup name
1093 ; case thing of
1094 ATyVar _ tv -> -- Important: zonk before returning
1095 -- We may have the application ((a::kappa) b)
1096 -- where kappa is already unified to (k1 -> k2)
1097 -- Then we want to see that arrow. Best done
1098 -- here because we are also maintaining
1099 -- Note [The tcType invariant], so we don't just
1100 -- want to zonk the kind, leaving the TyVar
1101 -- un-zonked (Trac #114873)
1102 do { ty <- zonkTcTyVar tv
1103 ; return (ty, typeKind ty) }
1104
1105 ATcTyCon tc_tc -> do { -- See Note [GADT kind self-reference]
1106 unless
1107 (isTypeLevel (mode_level mode))
1108 (promotionErr name TyConPE)
1109 ; check_tc tc_tc
1110 ; tc <- get_loopy_tc name tc_tc
1111 ; handle_tyfams tc tc_tc }
1112 -- mkNakedTyConApp: see Note [Type-checking inside the knot]
1113 -- NB: we really should check if we're at the kind level
1114 -- and if the tycon is promotable if -XNoTypeInType is set.
1115 -- But this is a terribly large amount of work! Not worth it.
1116
1117 AGlobal (ATyCon tc)
1118 -> do { check_tc tc
1119 ; handle_tyfams tc tc }
1120
1121 AGlobal (AConLike (RealDataCon dc))
1122 -> do { data_kinds <- xoptM LangExt.DataKinds
1123 ; unless (data_kinds || specialPromotedDc dc) $
1124 promotionErr name NoDataKindsDC
1125 ; type_in_type <- xoptM LangExt.TypeInType
1126 ; unless ( type_in_type ||
1127 ( isTypeLevel (mode_level mode) &&
1128 isLegacyPromotableDataCon dc ) ||
1129 ( isKindLevel (mode_level mode) &&
1130 specialPromotedDc dc ) ) $
1131 promotionErr name NoTypeInTypeDC
1132 ; let tc = promoteDataCon dc
1133 ; return (mkNakedTyConApp tc [], tyConKind tc) }
1134
1135 APromotionErr err -> promotionErr name err
1136
1137 _ -> wrongThingErr "type" thing name }
1138 where
1139 check_tc :: TyCon -> TcM ()
1140 check_tc tc = do { type_in_type <- xoptM LangExt.TypeInType
1141 ; data_kinds <- xoptM LangExt.DataKinds
1142 ; unless (isTypeLevel (mode_level mode) ||
1143 data_kinds ||
1144 isKindTyCon tc) $
1145 promotionErr name NoDataKindsTC
1146 ; unless (isTypeLevel (mode_level mode) ||
1147 type_in_type ||
1148 isLegacyPromotableTyCon tc) $
1149 promotionErr name NoTypeInTypeTC }
1150
1151 -- if we are type-checking a type family tycon, we must instantiate
1152 -- any invisible arguments right away. Otherwise, we get #11246
1153 handle_tyfams :: TyCon -- the tycon to instantiate (might be loopy)
1154 -> TcTyCon -- a non-loopy version of the tycon
1155 -> TcM (TcType, TcKind)
1156 handle_tyfams tc tc_tc
1157 | mightBeUnsaturatedTyCon tc_tc || mode_unsat mode
1158 -- This is where mode_unsat is used
1159 = do { traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind)
1160 ; return (mkNakedTyConApp tc [], tc_kind) }
1161
1162 | otherwise
1163 = do { (tc_args, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc))
1164 tc_kind_bndrs tc_inner_ki
1165 ; let tc_ty = mkNakedTyConApp tc tc_args
1166 -- tc and tc_ty must not be traced here, because that would
1167 -- force the evaluation of a potentially knot-tied variable (tc),
1168 -- and the typechecker would hang, as per #11708
1169 ; traceTc "tcTyVar2b" (vcat [ ppr tc_tc <+> dcolon <+> ppr tc_kind
1170 , ppr kind ])
1171 ; return (tc_ty, kind) }
1172 where
1173 tc_kind = tyConKind tc_tc
1174 (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
1175
1176 get_loopy_tc :: Name -> TyCon -> TcM TyCon
1177 -- Return the knot-tied global TyCon if there is one
1178 -- Otherwise the local TcTyCon; we must be doing kind checking
1179 -- but we still want to return a TyCon of some sort to use in
1180 -- error messages
1181 get_loopy_tc name tc_tc
1182 = do { env <- getGblEnv
1183 ; case lookupNameEnv (tcg_type_env env) name of
1184 Just (ATyCon tc) -> return tc
1185 _ -> do { traceTc "lk1 (loopy)" (ppr name)
1186 ; return tc_tc } }
1187
1188 tcClass :: Name -> TcM (Class, TcKind)
1189 tcClass cls -- Must be a class
1190 = do { thing <- tcLookup cls
1191 ; case thing of
1192 ATcTyCon tc -> return (aThingErr "tcClass" cls, tyConKind tc)
1193 AGlobal (ATyCon tc)
1194 | Just cls <- tyConClass_maybe tc
1195 -> return (cls, tyConKind tc)
1196 _ -> wrongThingErr "class" thing cls }
1197
1198
1199 aThingErr :: String -> Name -> b
1200 -- The type checker for types is sometimes called simply to
1201 -- do *kind* checking; and in that case it ignores the type
1202 -- returned. Which is a good thing since it may not be available yet!
1203 aThingErr str x = pprPanic "AThing evaluated unexpectedly" (text str <+> ppr x)
1204
1205 {-
1206 Note [Type-checking inside the knot]
1207 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1208 Suppose we are checking the argument types of a data constructor. We
1209 must zonk the types before making the DataCon, because once built we
1210 can't change it. So we must traverse the type.
1211
1212 BUT the parent TyCon is knot-tied, so we can't look at it yet.
1213
1214 So we must be careful not to use "smart constructors" for types that
1215 look at the TyCon or Class involved.
1216
1217 * Hence the use of mkNakedXXX functions. These do *not* enforce
1218 the invariants (for example that we use (FunTy s t) rather
1219 than (TyConApp (->) [s,t])).
1220
1221 * The zonking functions establish invariants (even zonkTcType, a change from
1222 previous behaviour). So we must never inspect the result of a
1223 zonk that might mention a knot-tied TyCon. This is generally OK
1224 because we zonk *kinds* while kind-checking types. And the TyCons
1225 in kinds shouldn't be knot-tied, because they come from a previous
1226 mutually recursive group.
1227
1228 * TcHsSyn.zonkTcTypeToType also can safely check/establish
1229 invariants.
1230
1231 This is horribly delicate. I hate it. A good example of how
1232 delicate it is can be seen in Trac #7903.
1233
1234 Note [GADT kind self-reference]
1235 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1236
1237 A promoted type cannot be used in the body of that type's declaration.
1238 Trac #11554 shows this example, which made GHC loop:
1239
1240 import Data.Kind
1241 data P (x :: k) = Q
1242 data A :: Type where
1243 B :: forall (a :: A). P a -> A
1244
1245 In order to check the constructor B, we need to have the promoted type A, but in
1246 order to get that promoted type, B must first be checked. To prevent looping, a
1247 TyConPE promotion error is given when tcTyVar checks an ATcTyCon in kind mode.
1248 Any ATcTyCon is a TyCon being defined in the current recursive group (see data
1249 type decl for TcTyThing), and all such TyCons are illegal in kinds.
1250
1251 Trac #11962 proposes checking the head of a data declaration separately from
1252 its constructors. This would allow the example above to pass.
1253
1254 Note [Body kind of a HsForAllTy]
1255 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1256 The body of a forall is usually a type, but in principle
1257 there's no reason to prohibit *unlifted* types.
1258 In fact, GHC can itself construct a function with an
1259 unboxed tuple inside a for-all (via CPR analysis; see
1260 typecheck/should_compile/tc170).
1261
1262 Moreover in instance heads we get forall-types with
1263 kind Constraint.
1264
1265 It's tempting to check that the body kind is either * or #. But this is
1266 wrong. For example:
1267
1268 class C a b
1269 newtype N = Mk Foo deriving (C a)
1270
1271 We're doing newtype-deriving for C. But notice how `a` isn't in scope in
1272 the predicate `C a`. So we quantify, yielding `forall a. C a` even though
1273 `C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
1274 convenient. Bottom line: don't check for * or # here.
1275
1276 Note [Body kind of a HsQualTy]
1277 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1278 If ctxt is non-empty, the HsQualTy really is a /function/, so the
1279 kind of the result really is '*', and in that case the kind of the
1280 body-type can be lifted or unlifted.
1281
1282 However, consider
1283 instance Eq a => Eq [a] where ...
1284 or
1285 f :: (Eq a => Eq [a]) => blah
1286 Here both body-kind of the HsQualTy is Constraint rather than *.
1287 Rather crudely we tell the difference by looking at exp_kind. It's
1288 very convenient to typecheck instance types like any other HsSigType.
1289
1290 Admittedly the '(Eq a => Eq [a]) => blah' case is erroneous, but it's
1291 better to reject in checkValidType. If we say that the body kind
1292 should be '*' we risk getting TWO error messages, one saying that Eq
1293 [a] doens't have kind '*', and one saying that we need a Constraint to
1294 the left of the outer (=>).
1295
1296 How do we figure out the right body kind? Well, it's a bit of a
1297 kludge: I just look at the expected kind. If it's Constraint, we
1298 must be in this instance situation context. It's a kludge because it
1299 wouldn't work if any unification was involved to compute that result
1300 kind -- but it isn't. (The true way might be to use the 'mode'
1301 parameter, but that seemed like a sledgehammer to crack a nut.)
1302
1303 Note [Inferring tuple kinds]
1304 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1305 Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
1306 we try to figure out whether it's a tuple of kind * or Constraint.
1307 Step 1: look at the expected kind
1308 Step 2: infer argument kinds
1309
1310 If after Step 2 it's not clear from the arguments that it's
1311 Constraint, then it must be *. Once having decided that we re-check
1312 the Check the arguments again to give good error messages
1313 in eg. `(Maybe, Maybe)`
1314
1315 Note that we will still fail to infer the correct kind in this case:
1316
1317 type T a = ((a,a), D a)
1318 type family D :: Constraint -> Constraint
1319
1320 While kind checking T, we do not yet know the kind of D, so we will default the
1321 kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
1322
1323 Note [Desugaring types]
1324 ~~~~~~~~~~~~~~~~~~~~~~~
1325 The type desugarer is phase 2 of dealing with HsTypes. Specifically:
1326
1327 * It transforms from HsType to Type
1328
1329 * It zonks any kinds. The returned type should have no mutable kind
1330 or type variables (hence returning Type not TcType):
1331 - any unconstrained kind variables are defaulted to (Any *) just
1332 as in TcHsSyn.
1333 - there are no mutable type variables because we are
1334 kind-checking a type
1335 Reason: the returned type may be put in a TyCon or DataCon where
1336 it will never subsequently be zonked.
1337
1338 You might worry about nested scopes:
1339 ..a:kappa in scope..
1340 let f :: forall b. T '[a,b] -> Int
1341 In this case, f's type could have a mutable kind variable kappa in it;
1342 and we might then default it to (Any *) when dealing with f's type
1343 signature. But we don't expect this to happen because we can't get a
1344 lexically scoped type variable with a mutable kind variable in it. A
1345 delicate point, this. If it becomes an issue we might need to
1346 distinguish top-level from nested uses.
1347
1348 Moreover
1349 * it cannot fail,
1350 * it does no unifications
1351 * it does no validity checking, except for structural matters, such as
1352 (a) spurious ! annotations.
1353 (b) a class used as a type
1354
1355 Note [Kind of a type splice]
1356 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1357 Consider these terms, each with TH type splice inside:
1358 [| e1 :: Maybe $(..blah..) |]
1359 [| e2 :: $(..blah..) |]
1360 When kind-checking the type signature, we'll kind-check the splice
1361 $(..blah..); we want to give it a kind that can fit in any context,
1362 as if $(..blah..) :: forall k. k.
1363
1364 In the e1 example, the context of the splice fixes kappa to *. But
1365 in the e2 example, we'll desugar the type, zonking the kind unification
1366 variables as we go. When we encounter the unconstrained kappa, we
1367 want to default it to '*', not to (Any *).
1368
1369
1370 Help functions for type applications
1371 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1372 -}
1373
1374 addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
1375 -- Wrap a context around only if we want to show that contexts.
1376 -- Omit invisible ones and ones user's won't grok
1377 addTypeCtxt (L _ ty) thing
1378 = addErrCtxt doc thing
1379 where
1380 doc = text "In the type" <+> quotes (ppr ty)
1381
1382 {-
1383 ************************************************************************
1384 * *
1385 Type-variable binders
1386 %* *
1387 %************************************************************************
1388
1389 Note [Dependent LHsQTyVars]
1390 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1391 We track (in the renamer) which explicitly bound variables in a
1392 LHsQTyVars are manifestly dependent; only precisely these variables
1393 may be used within the LHsQTyVars. We must do this so that kcLHsQTyVars
1394 can produce the right TyConBinders, and tell Anon vs. Required.
1395
1396 Example data T k1 (a:k1) (b:k2) c
1397 = MkT (Proxy a) (Proxy b) (Proxy c)
1398
1399 Here
1400 (a:k1),(b:k2),(c:k3)
1401 are Anon (explicitly specified as a binder, not used
1402 in the kind of any other binder
1403 k1 is Required (explicitly specifed as a binder, but used
1404 in the kind of another binder i.e. dependently)
1405 k2 is Specified (not explicitly bound, but used in the kind
1406 of another binder)
1407 k3 in Inferred (not lexically in scope at all, but inferred
1408 by kind inference)
1409 and
1410 T :: forall {k3} k1. forall k3 -> k1 -> k2 -> k3 -> *
1411
1412 See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility]
1413 in TyCoRep.
1414
1415 kcLHsQTyVars uses the hsq_dependent field to decide whether
1416 k1, a, b, c should be Required or Anon.
1417
1418 Earlier, thought it would work simply to do a free-variable check
1419 during kcLHsQTyVars, but this is bogus, because there may be
1420 unsolved equalities about. And we don't want to eagerly solve the
1421 equalities, because we may get further information after
1422 kcLHsQTyVars is called. (Recall that kcLHsQTyVars is called
1423 only from getInitialKind.)
1424 This is what implements the rule that all variables intended to be
1425 dependent must be manifestly so.
1426
1427 Sidenote: It's quite possible that later, we'll consider (t -> s)
1428 as a degenerate case of some (pi (x :: t) -> s) and then this will
1429 all get more permissive.
1430
1431 Note [Kind generalisation and SigTvs]
1432 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1433 Consider
1434 data T (a :: k1) x = MkT (S a ())
1435 data S (b :: k2) y = MkS (T b ())
1436
1437 While we are doing kind inference for the mutually-recursive S,T,
1438 we will end up unifying k1 and k2 together. So they can't be skolems.
1439 We therefore make them SigTvs, which can unify with type variables,
1440 but not with general types. All this is very similar at the level
1441 of terms: see Note [Quantified variables in partial type signatures]
1442 in TcBinds.
1443
1444 There are some wrinkles
1445
1446 * We always want to kind-generalise over SigTvs, and /not/ default
1447 them to Type. Another way to say this is: a SigTV should /never/
1448 stand for a type, even via defaulting. Hence the check in
1449 TcSimplify.defaultTyVarTcS, and TcMType.defaultTyVar. Here's
1450 another example (Trac #14555):
1451 data Exp :: [TYPE rep] -> TYPE rep -> Type where
1452 Lam :: Exp (a:xs) b -> Exp xs (a -> b)
1453 We want to kind-generalise over the 'rep' variable.
1454 Trac #14563 is another example.
1455
1456 * Consider Trac #11203
1457 data SameKind :: k -> k -> *
1458 data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
1459 Here we will unify k1 with k2, but this time doing so is an error,
1460 because k1 and k2 are bound in the same delcaration.
1461
1462 We sort this out using findDupSigTvs, in TcTyClTyVars; very much
1463 as we do with partial type signatures in mk_psig_qtvs in
1464 TcBinds.chooseInferredQuantifiers
1465
1466 Note [Keeping scoped variables in order: Explicit]
1467 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1468 When the user writes `forall a b c. blah`, we bring a, b, and c into
1469 scope and then check blah. In the process of checking blah, we might
1470 learn the kinds of a, b, and c, and these kinds might indicate that
1471 b depends on c, and thus that we should reject the user-written type.
1472
1473 One approach to doing this would be to bring each of a, b, and c into
1474 scope, one at a time, creating an implication constraint and
1475 bumping the TcLevel for each one. This would work, because the kind
1476 of, say, b would be untouchable when c is in scope (and the constraint
1477 couldn't float out because c blocks it). However, it leads to terrible
1478 error messages, complaining about skolem escape. While it is indeed
1479 a problem of skolem escape, we can do better.
1480
1481 Instead, our approach is to bring the block of variables into scope
1482 all at once, creating one implication constraint for the lot. The
1483 user-written variables are skolems in the implication constraint. In
1484 TcSimplify.setImplicationStatus, we check to make sure that the ordering
1485 is correct, choosing ImplicationStatus IC_BadTelescope if they aren't.
1486 Then, in TcErrors, we report if there is a bad telescope. This way,
1487 we can report a suggested ordering to the user if there is a problem.
1488
1489 Note [Keeping scoped variables in order: Implicit]
1490 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1491 When the user implicitly quantifies over variables (say, in a type
1492 signature), we need to come up with some ordering on these variables.
1493 This is done by bumping the TcLevel, bringing the tyvars into scope,
1494 and then type-checking the thing_inside. The constraints are all
1495 wrapped in an implication, which is then solved. Finally, we can
1496 zonk all the binders and then order them with toposortTyVars.
1497
1498 It's critical to solve before zonking and ordering in order to uncover
1499 any unifications. You might worry that this eager solving could cause
1500 trouble elsewhere. I don't think it will. Because it will solve only
1501 in an increased TcLevel, it can't unify anything that was mentioned
1502 elsewhere. Additionally, we require that the order of implicitly
1503 quantified variables is manifest by the scope of these variables, so
1504 we're not going to learn more information later that will help order
1505 these variables.
1506
1507 Note [Recipe for checking a signature]
1508 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1509 Checking a user-written signature requires several steps:
1510
1511 1. Generate constraints.
1512 2. Solve constraints.
1513 3. Zonk and promote tyvars.
1514 4. (Optional) Kind-generalize.
1515 5. Check validity.
1516
1517 There may be some surprises in here:
1518
1519 Step 2 is necessary for two reasons: most signatures also bring
1520 implicitly quantified variables into scope, and solving is necessary
1521 to get these in the right order (see Note [Keeping scoped variables in
1522 order: Implicit]). Additionally, solving is necessary in order to
1523 kind-generalize correctly.
1524
1525 Step 3 requires *promoting* type variables. If there are any foralls
1526 in a type, the TcLevel will be bumped within the forall. This might
1527 lead to the generation of matavars with a high level. If we don't promote,
1528 we violate MetaTvInv of Note [TcLevel and untouchable type variables]
1529 in TcType.
1530
1531 -}
1532
1533 tcWildCardBinders :: SkolemInfo
1534 -> [Name]
1535 -> ([(Name, TcTyVar)] -> TcM a)
1536 -> TcM a
1537 tcWildCardBinders info = tcWildCardBindersX new_tv (Just info)
1538 where
1539 new_tv name = do { kind <- newMetaKindVar
1540 ; newSkolemTyVar name kind }
1541
1542 tcWildCardBindersX :: (Name -> TcM TcTyVar)
1543 -> Maybe SkolemInfo -- Just <=> we're bringing fresh vars
1544 -- into scope; use scopeTyVars
1545 -> [Name]
1546 -> ([(Name, TcTyVar)] -> TcM a)
1547 -> TcM a
1548 tcWildCardBindersX new_wc maybe_skol_info wc_names thing_inside
1549 = do { wcs <- mapM new_wc wc_names
1550 ; let wc_prs = wc_names `zip` wcs
1551 ; scope_tvs wc_prs $
1552 thing_inside wc_prs }
1553 where
1554 scope_tvs
1555 | Just info <- maybe_skol_info = scopeTyVars2 info
1556 | otherwise = tcExtendTyVarEnv2
1557
1558 -- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
1559 -- user-supplied kind signature (CUSK), generalise the result.
1560 -- Used in 'getInitialKind' (for tycon kinds and other kinds)
1561 -- and in kind-checking (but not for tycon kinds, which are checked with
1562 -- tcTyClDecls). See also Note [Complete user-supplied kind signatures] in
1563 -- HsDecls.
1564 --
1565 -- This function does not do telescope checking.
1566 kcLHsQTyVars :: Name -- ^ of the thing being checked
1567 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
1568 -> Bool -- ^ True <=> the decl being checked has a CUSK
1569 -> LHsQTyVars GhcRn
1570 -> TcM (Kind, r) -- ^ The result kind, possibly with other info
1571 -> TcM (TcTyCon, r) -- ^ A suitably-kinded TcTyCon
1572 kcLHsQTyVars name flav cusk
1573 user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
1574 , hsq_dependent = dep_names }
1575 , hsq_explicit = hs_tvs }) thing_inside
1576 | cusk
1577 = do { typeintype <- xoptM LangExt.TypeInType
1578 ; let m_kind
1579 | typeintype = Nothing
1580 | otherwise = Just liftedTypeKind
1581 -- without -XTypeInType, default all kind variables to have kind *
1582
1583 ; (scoped_kvs, (tc_tvs, (res_kind, stuff)))
1584 <- solveEqualities $
1585 tcImplicitTKBndrsX newSkolemTyVar m_kind skol_info kv_ns $
1586 kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
1587
1588 -- Now, because we're in a CUSK, quantify over the mentioned
1589 -- kind vars, in dependency order.
1590 ; tc_tvs <- mapM zonkTcTyVarToTyVar tc_tvs
1591 ; res_kind <- zonkTcType res_kind
1592 ; let tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
1593 qkvs = tyCoVarsOfTypeWellScoped (mkTyConKind tc_binders res_kind)
1594 -- the visibility of tvs doesn't matter here; we just
1595 -- want the free variables not to include the tvs
1596
1597 -- If there are any meta-tvs left, the user has
1598 -- lied about having a CUSK. Error.
1599 ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
1600 -- skip this check for associated types. Why?
1601 -- Any variables mentioned in the definition will get defaulted,
1602 -- except those that appear in the class head. Defaulted vars do
1603 -- not concern us here (they are fully determined). Variables from
1604 -- the class head will be fully determined whenever the class has
1605 -- a CUSK, and an associated family has a CUSK only when the enclosing
1606 -- class has one. So skipping is safe. But why is it necessary?
1607 -- It's possible that a class variable has too low a TcLevel to have
1608 -- fully settled down by this point, and so this check will get
1609 -- a false positive.
1610 ; when (not_associated && not (null meta_tvs)) $
1611 report_non_cusk_tvs (qkvs ++ tc_tvs)
1612
1613 -- If any of the scoped_kvs aren't actually mentioned in a binder's
1614 -- kind (or the return kind), then we're in the CUSK case from
1615 -- Note [Free-floating kind vars]
1616 ; let all_tc_tvs = good_tvs ++ tc_tvs
1617 all_mentioned_tvs = mapUnionVarSet (tyCoVarsOfType . tyVarKind)
1618 all_tc_tvs
1619 `unionVarSet` tyCoVarsOfType res_kind
1620 unmentioned_kvs = filterOut (`elemVarSet` all_mentioned_tvs)
1621 scoped_kvs
1622 ; reportFloatingKvs name flav all_tc_tvs unmentioned_kvs
1623
1624 ; let final_binders = map (mkNamedTyConBinder Specified) good_tvs
1625 ++ tc_binders
1626 tycon = mkTcTyCon name (ppr user_tyvars) final_binders res_kind
1627 (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
1628 flav
1629 -- the tvs contain the binders already
1630 -- in scope from an enclosing class, but
1631 -- re-adding tvs to the env't doesn't cause
1632 -- harm
1633
1634 ; traceTc "kcLHsQTyVars: cusk" $
1635 vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
1636 , ppr tc_tvs, ppr (mkTyConKind final_binders res_kind)
1637 , ppr qkvs, ppr meta_tvs, ppr good_tvs, ppr final_binders ]
1638
1639 ; return (tycon, stuff) }
1640
1641 | otherwise
1642 = do { typeintype <- xoptM LangExt.TypeInType
1643
1644 -- if -XNoTypeInType and we know all the implicits are kind vars,
1645 -- just give the kind *. This prevents test
1646 -- dependent/should_fail/KindLevelsB from compiling, as it should
1647 ; let default_kind
1648 | typeintype = Nothing
1649 | otherwise = Just liftedTypeKind
1650 -- Why newSigTyVar? See Note [Kind generalisation and sigTvs]
1651 ; (scoped_kvs, (tc_tvs, (res_kind, stuff)))
1652 <- kcImplicitTKBndrs kv_ns default_kind $
1653 kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
1654
1655 ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they
1656 -- must remain lined up with the binders
1657 tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
1658 tycon = mkTcTyCon name (ppr user_tyvars) tc_binders res_kind
1659 (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
1660 flav
1661
1662 ; traceTc "kcLHsQTyVars: not-cusk" $
1663 vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
1664 , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ]
1665 ; return (tycon, stuff) }
1666 where
1667 open_fam = tcFlavourIsOpen flav
1668 not_associated = case flav of
1669 DataFamilyFlavour assoc -> not assoc
1670 OpenTypeFamilyFlavour assoc -> not assoc
1671 _ -> True
1672
1673 skol_info = TyConSkol flav name
1674
1675 mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder
1676 -- See Note [Dependent LHsQTyVars]
1677 mk_tc_binder hs_tv tv
1678 | hsLTyVarName hs_tv `elemNameSet` dep_names
1679 = mkNamedTyConBinder Required tv
1680 | otherwise
1681 = mkAnonTyConBinder tv
1682
1683 report_non_cusk_tvs all_tvs
1684 = do { all_tvs <- mapM zonkTyCoVarKind all_tvs
1685 ; let (_, tidy_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
1686 (meta_tvs, other_tvs) = partition isMetaTyVar tidy_tvs
1687
1688 ; addErr $
1689 vcat [ text "You have written a *complete user-suppled kind signature*,"
1690 , hang (text "but the following variable" <> plural meta_tvs <+>
1691 isOrAre meta_tvs <+> text "undetermined:")
1692 2 (vcat (map pp_tv meta_tvs))
1693 , text "Perhaps add a kind signature."
1694 , hang (text "Inferred kinds of user-written variables:")
1695 2 (vcat (map pp_tv other_tvs)) ] }
1696 where
1697 pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
1698 kcLHsQTyVars _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
1699
1700 kcLHsTyVarBndrs :: Bool -- True <=> bump the TcLevel when bringing vars into scope
1701 -> Bool -- True <=> Default un-annotated tyvar
1702 -- binders to kind *
1703 -> SkolemInfo
1704 -> [LHsTyVarBndr GhcRn]
1705 -> TcM r
1706 -> TcM ([TyVar], r)
1707 -- There may be dependency between the explicit "ty" vars.
1708 -- So, we have to handle them one at a time.
1709 kcLHsTyVarBndrs _ _ _ [] thing
1710 = do { stuff <- thing; return ([], stuff) }
1711
1712 kcLHsTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing
1713 = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
1714 -- NB: Bring all tvs into scope, even non-dependent ones,
1715 -- as they're needed in type synonyms, data constructors, etc.
1716
1717 ; (tvs, stuff) <- bind_unless_scoped tv_pair $
1718 kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs $
1719 thing
1720
1721 ; return ( tv : tvs, stuff ) }
1722 where
1723 -- | Bind the tyvar in the env't unless the bool is True
1724 bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a
1725 bind_unless_scoped (_, True) thing_inside = thing_inside
1726 bind_unless_scoped (tv, False) thing_inside
1727 | cusk = scopeTyVars skol_info [tv] thing_inside
1728 | otherwise = tcExtendTyVarEnv [tv] thing_inside
1729 -- These variables haven't settled down yet, so we don't want to bump
1730 -- the TcLevel. If we do, then we'll have metavars of too high a level
1731 -- floating about. Changing this causes many, many failures in the
1732 -- `dependent` testsuite directory.
1733
1734 kc_hs_tv :: HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
1735 kc_hs_tv (UserTyVar _ lname@(L _ name))
1736 = do { tv_pair@(tv, in_scope) <- tcHsTyVarName newSkolemTyVar Nothing name
1737
1738 -- Open type/data families default their variables to kind *.
1739 -- But don't default in-scope class tyvars, of course
1740 ; when (open_fam && not in_scope) $
1741 discardResult $ unifyKind (Just (HsTyVar noExt NotPromoted lname))
1742 liftedTypeKind (tyVarKind tv)
1743
1744 ; return tv_pair }
1745
1746 kc_hs_tv (KindedTyVar _ (L _ name) lhs_kind)
1747 = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt name) lhs_kind
1748 ; tcHsTyVarName newSkolemTyVar (Just kind) name }
1749
1750 kc_hs_tv (XTyVarBndr{}) = panic "kc_hs_tv"
1751
1752 tcImplicitTKBndrs :: SkolemInfo
1753 -> [Name]
1754 -> TcM a
1755 -> TcM ([TcTyVar], a)
1756 tcImplicitTKBndrs = tcImplicitTKBndrsX newSkolemTyVar Nothing
1757
1758 -- | Like 'tcImplicitTKBndrs', but uses 'newSigTyVar' to create tyvars
1759 tcImplicitTKBndrsSig :: SkolemInfo
1760 -> [Name]
1761 -> TcM a
1762 -> TcM ([TcTyVar], a)
1763 tcImplicitTKBndrsSig = tcImplicitTKBndrsX newSigTyVar Nothing
1764
1765 tcImplicitTKBndrsX :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
1766 -> Maybe Kind -- Just k <=> assign all names this kind
1767 -> SkolemInfo
1768 -> [Name]
1769 -> TcM a
1770 -> TcM ([TcTyVar], a) -- these tyvars are dependency-ordered
1771 -- * Guarantees to call solveLocalEqualities to unify
1772 -- all constraints from thing_inside.
1773 --
1774 -- * Returned TcTyVars have the supplied HsTyVarBndrs,
1775 -- but may be in different order to the original [Name]
1776 -- (because of sorting to respect dependency)
1777 --
1778 -- * Returned TcTyVars have zonked kinds
1779 -- See Note [Keeping scoped variables in order: Implicit]
1780 tcImplicitTKBndrsX new_tv m_kind skol_info tv_names thing_inside
1781 | null tv_names -- Short cut for the common case where there
1782 -- are no implicit type variables to bind
1783 = do { result <- solveLocalEqualities thing_inside
1784 ; return ([], result) }
1785
1786 | otherwise
1787 = do { (skol_tvs, result)
1788 <- solveLocalEqualities $
1789 checkTvConstraints skol_info Nothing $
1790 do { tv_pairs <- mapM (tcHsTyVarName new_tv m_kind) tv_names
1791 ; let must_scope_tvs = [ tv | (tv, False) <- tv_pairs ]
1792 ; result <- tcExtendTyVarEnv must_scope_tvs $
1793 thing_inside
1794 ; return (map fst tv_pairs, result) }
1795
1796
1797 ; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs
1798 -- use zonkTcTyCoVarBndr because a skol_tv might be a SigTv
1799
1800 ; let final_tvs = toposortTyVars skol_tvs
1801 ; traceTc "tcImplicitTKBndrs" (ppr tv_names $$ ppr final_tvs)
1802 ; return (final_tvs, result) }
1803
1804 -- | Bring implicitly quantified type/kind variables into scope during
1805 -- kind checking. Uses SigTvs, as per Note [Use SigTvs in kind-checking pass]
1806 -- in TcTyClsDecls.
1807 kcImplicitTKBndrs :: [Name] -- of the vars
1808 -> Maybe Kind -- Just k <=> use k as the kind for all vars
1809 -- Nothing <=> use a meta-tyvar
1810 -> TcM a
1811 -> TcM ([TcTyVar], a) -- returns the tyvars created
1812 -- these are *not* dependency ordered
1813 kcImplicitTKBndrs var_ns m_kind thing_inside
1814 = do { tkvs_pairs <- mapM (tcHsTyVarName newSigTyVar m_kind) var_ns
1815 ; let must_scope_tkvs = [ tkv | (tkv, False) <- tkvs_pairs ]
1816 ; result <- tcExtendTyVarEnv must_scope_tkvs $
1817 thing_inside
1818 ; return (map fst tkvs_pairs, result) }
1819
1820 tcExplicitTKBndrs :: SkolemInfo
1821 -> [LHsTyVarBndr GhcRn]
1822 -> TcM a
1823 -> TcM ([TcTyVar], a)
1824 -- See also Note [Associated type tyvar names] in Class
1825 tcExplicitTKBndrs skol_info hs_tvs thing_inside
1826 -- This function brings into scope a telescope of binders as written by
1827 -- the user. At first blush, it would then seem that we should bring
1828 -- them into scope one at a time, bumping the TcLevel each time.
1829 -- (Recall that we bump the level to prevent skolem escape from happening.)
1830 -- However, this leads to terrible error messages, because we end up
1831 -- failing to unify with some `k0`. Better would be to allow type inference
1832 -- to work, potentially creating a skolem-escape problem, and then to
1833 -- notice that the telescope is out of order. That's what we do here,
1834 -- following the logic of tcImplicitTKBndrsX.
1835 -- See also Note [Keeping scoped variables in order: Explicit]
1836 --
1837 -- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
1838 | null hs_tvs -- Short cut that avoids creating an implication
1839 -- constraint in the common case where none is needed
1840 = do { result <- thing_inside
1841 ; return ([], result) }
1842
1843 | otherwise
1844 = do { (skol_tvs, result) <- checkTvConstraints skol_info (Just doc) $
1845 bind_tvbs hs_tvs
1846
1847 ; traceTc "tcExplicitTKBndrs" $
1848 vcat [ text "Hs vars:" <+> ppr hs_tvs
1849 , text "tvs:" <+> pprTyVars skol_tvs ]
1850
1851 ; return (skol_tvs, result) }
1852
1853 where
1854 bind_tvbs [] = do { result <- thing_inside
1855 ; return ([], result) }
1856 bind_tvbs (L _ tvb : tvbs)
1857 = do { (tv, in_scope) <- tcHsTyVarBndr newSkolemTyVar tvb
1858 ; (if in_scope then id else tcExtendTyVarEnv [tv]) $
1859 do { (tvs, result) <- bind_tvbs tvbs
1860 ; return (tv : tvs, result) }}
1861
1862 doc = sep (map ppr hs_tvs)
1863
1864 -- | Used during the "kind-checking" pass in TcTyClsDecls only.
1865 -- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
1866 kcExplicitTKBndrs :: [LHsTyVarBndr GhcRn]
1867 -> TcM a
1868 -> TcM a
1869 kcExplicitTKBndrs [] thing_inside = thing_inside
1870 kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside
1871 = do { (tv, _) <- tcHsTyVarBndr newSigTyVar hs_tv
1872 ; tcExtendTyVarEnv [tv] $
1873 kcExplicitTKBndrs hs_tvs thing_inside }
1874
1875 tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
1876 -> HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
1877 -- Return a TcTyVar, built using the provided function
1878 -- Typically the Kind inside the HsTyVarBndr will be a tyvar
1879 -- with a mutable kind in it.
1880 --
1881 -- These variables might be in scope already (with associated types, for example).
1882 -- This function then checks that the kind annotation (if any) matches the
1883 -- kind of the in-scope type variable.
1884 --
1885 -- Returned TcTyVar has the same name; no cloning
1886 --
1887 -- See also Note [Associated type tyvar names] in Class
1888 --
1889 -- Returns True iff the tyvar was already in scope
1890 tcHsTyVarBndr new_tv (UserTyVar _ (L _ tv_nm))
1891 = tcHsTyVarName new_tv Nothing tv_nm
1892 tcHsTyVarBndr new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
1893 = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
1894 ; tcHsTyVarName new_tv (Just kind) tv_nm }
1895 tcHsTyVarBndr _ (XTyVarBndr _) = panic "tcHsTyVarBndr"
1896
1897 newWildTyVar :: Name -> TcM TcTyVar
1898 -- ^ New unification variable for a wildcard
1899 newWildTyVar _name
1900 = do { kind <- newMetaKindVar
1901 ; uniq <- newUnique
1902 ; details <- newMetaDetails TauTv
1903 ; let name = mkSysTvName uniq (fsLit "w")
1904 tyvar = (mkTcTyVar name kind details)
1905 ; traceTc "newWildTyVar" (ppr tyvar)
1906 ; return tyvar }
1907
1908 -- | Produce a tyvar of the given name (with the kind provided, or
1909 -- otherwise a meta-var kind). If
1910 -- the name is already in scope, return the scoped variable, checking
1911 -- to make sure the known kind matches any kind provided. The
1912 -- second return value says whether the variable is in scope (True)
1913 -- or not (False). (Use this for associated types, for example.)
1914 tcHsTyVarName :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
1915 -> Maybe Kind -- Just k <=> use k as the variable's kind
1916 -- Nothing <=> use a meta-tyvar
1917 -> Name -> TcM (TcTyVar, Bool)
1918 tcHsTyVarName new_tv m_kind name
1919 = do { mb_tv <- tcLookupLcl_maybe name
1920 ; case mb_tv of
1921 Just (ATyVar _ tv)
1922 -> do { whenIsJust m_kind $ \ kind ->
1923 discardResult $
1924 unifyKind (Just (HsTyVar noExt NotPromoted (noLoc name)))
1925 kind (tyVarKind tv)
1926 ; return (tv, True) }
1927 _ -> do { kind <- case m_kind of
1928 Just kind -> return kind
1929 Nothing -> newMetaKindVar
1930 ; tv <- new_tv name kind
1931 ; return (tv, False) }}
1932
1933 --------------------------
1934 -- Bringing tyvars into scope
1935 --------------------------
1936
1937 -- | Bring tyvars into scope, wrapping the thing_inside in an implication
1938 -- constraint. The implication constraint is necessary to provide SkolemInfo
1939 -- for the tyvars and to ensure that no unification variables made outside
1940 -- the scope of these tyvars (i.e. lower TcLevel) unify with the locally-scoped
1941 -- tyvars (i.e. higher TcLevel).
1942 --
1943 -- INVARIANT: The thing_inside must check only types, never terms.
1944 --
1945 -- Use this (not tcExtendTyVarEnv) wherever you expect a Λ or ∀ in Core.
1946 -- Use tcExtendTyVarEnv otherwise.
1947 scopeTyVars :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a
1948 scopeTyVars skol_info tvs = scopeTyVars2 skol_info [(tyVarName tv, tv) | tv <- tvs]
1949
1950 -- | Like 'scopeTyVars', but allows you to specify different scoped names
1951 -- than the Names stored within the tyvars.
1952 scopeTyVars2 :: SkolemInfo -> [(Name, TcTyVar)] -> TcM a -> TcM a
1953 scopeTyVars2 skol_info prs thing_inside
1954 = fmap snd $ -- discard the TcEvBinds, which will always be empty
1955 checkConstraints skol_info (map snd prs) [{- no EvVars -}] $
1956 tcExtendTyVarEnv2 prs $
1957 thing_inside
1958
1959 ------------------
1960 kindGeneralize :: TcType -> TcM [KindVar]
1961 -- Quantify the free kind variables of a kind or type
1962 -- In the latter case the type is closed, so it has no free
1963 -- type variables. So in both cases, all the free vars are kind vars
1964 -- Input must be zonked.
1965 -- NB: You must call solveEqualities or solveLocalEqualities before
1966 -- kind generalization
1967 kindGeneralize kind_or_type
1968 = do { let kvs = tyCoVarsOfTypeDSet kind_or_type
1969 dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet }
1970 ; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
1971 ; quantifyTyVars gbl_tvs dvs }
1972
1973 {-
1974 Note [Kind generalisation]
1975 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1976 We do kind generalisation only at the outer level of a type signature.
1977 For example, consider
1978 T :: forall k. k -> *
1979 f :: (forall a. T a -> Int) -> Int
1980 When kind-checking f's type signature we generalise the kind at
1981 the outermost level, thus:
1982 f1 :: forall k. (forall (a:k). T k a -> Int) -> Int -- YES!
1983 and *not* at the inner forall:
1984 f2 :: (forall k. forall (a:k). T k a -> Int) -> Int -- NO!
1985 Reason: same as for HM inference on value level declarations,
1986 we want to infer the most general type. The f2 type signature
1987 would be *less applicable* than f1, because it requires a more
1988 polymorphic argument.
1989
1990 NB: There are no explicit kind variables written in f's signature.
1991 When there are, the renamer adds these kind variables to the list of
1992 variables bound by the forall, so you can indeed have a type that's
1993 higher-rank in its kind. But only by explicit request.
1994
1995 Note [Kinds of quantified type variables]
1996 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1997 tcTyVarBndrsGen quantifies over a specified list of type variables,
1998 *and* over the kind variables mentioned in the kinds of those tyvars.
1999
2000 Note that we must zonk those kinds (obviously) but less obviously, we
2001 must return type variables whose kinds are zonked too. Example
2002 (a :: k7) where k7 := k9 -> k9
2003 We must return
2004 [k9, a:k9->k9]
2005 and NOT
2006 [k9, a:k7]
2007 Reason: we're going to turn this into a for-all type,
2008 forall k9. forall (a:k7). blah
2009 which the type checker will then instantiate, and instantiate does not
2010 look through unification variables!
2011
2012 Hence using zonked_kinds when forming tvs'.
2013
2014 Note [Free-floating kind vars]
2015 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2016 Consider
2017
2018 data T = MkT (forall (a :: k). Proxy a)
2019 -- from test ghci/scripts/T7873
2020
2021 This is not an existential datatype, but a higher-rank one (the forall
2022 to the right of MkT). Also consider
2023
2024 data S a = MkS (Proxy (a :: k))
2025
2026 According to the rules around implicitly-bound kind variables, in both
2027 cases those k's scope over the whole declaration. The renamer grabs
2028 it and adds it to the hsq_implicits field of the HsQTyVars of the
2029 tycon. So it must be in scope during type-checking, but we want to
2030 reject T while accepting S.
2031
2032 Why reject T? Because the kind variable isn't fixed by anything. For
2033 a variable like k to be implicit, it needs to be mentioned in the kind
2034 of a tycon tyvar. But it isn't.
2035
2036 Why accept S? Because kind inference tells us that a has kind k, so it's
2037 all OK.
2038
2039 Our approach depends on whether or not the datatype has a CUSK.
2040
2041 Non-CUSK: In the first pass (kcTyClTyVars) we just bring
2042 k into scope. In the second pass (tcTyClTyVars),
2043 we check to make sure that k has been unified with some other variable
2044 (or generalized over, making k into a skolem). If it hasn't been, then
2045 it must be a free-floating kind var. Error.
2046
2047 CUSK: When we determine the tycon's final, never-to-be-changed kind
2048 in kcLHsQTyVars, we check to make sure all implicitly-bound kind
2049 vars are indeed mentioned in a kind somewhere. If not, error.
2050
2051 We also perform free-floating kind var analysis for type family instances
2052 (see #13985). Here is an interesting example:
2053
2054 type family T :: k
2055 type instance T = (Nothing :: Maybe a)
2056
2057 Upon a cursory glance, it may appear that the kind variable `a` is
2058 free-floating above, since there are no (visible) LHS patterns in `T`. However,
2059 there is an *invisible* pattern due to the return kind, so inside of GHC, the
2060 instance looks closer to this:
2061
2062 type family T @k :: k
2063 type instance T @(Maybe a) = (Nothing :: Maybe a)
2064
2065 Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in
2066 fact not free-floating. Contrast that with this example:
2067
2068 type instance T = Proxy (Nothing :: Maybe a)
2069
2070 This would looks like this inside of GHC:
2071
2072 type instance T @(*) = Proxy (Nothing :: Maybe a)
2073
2074 So this time, `a` is neither bound by a visible nor invisible type pattern on
2075 the LHS, so it would be reported as free-floating.
2076
2077 Finally, here's one more brain-teaser (from #9574). In the example below:
2078
2079 class Funct f where
2080 type Codomain f :: *
2081 instance Funct ('KProxy :: KProxy o) where
2082 type Codomain 'KProxy = NatTr (Proxy :: o -> *)
2083
2084 As it turns out, `o` is not free-floating in this example. That is because `o`
2085 bound by the kind signature of the LHS type pattern 'KProxy. To make this more
2086 obvious, one can also write the instance like so:
2087
2088 instance Funct ('KProxy :: KProxy o) where
2089 type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *)
2090
2091 -}
2092
2093 --------------------
2094 -- getInitialKind has made a suitably-shaped kind for the type or class
2095 -- Look it up in the local environment. This is used only for tycons
2096 -- that we're currently type-checking, so we're sure to find a TcTyCon.
2097 kcLookupTcTyCon :: Name -> TcM TcTyCon
2098 kcLookupTcTyCon nm
2099 = do { tc_ty_thing <- tcLookup nm
2100 ; return $ case tc_ty_thing of
2101 ATcTyCon tc -> tc
2102 _ -> pprPanic "kcLookupTcTyCon" (ppr tc_ty_thing) }
2103
2104 -----------------------
2105 -- | Bring tycon tyvars into scope. This is used during the "kind-checking"
2106 -- pass in TcTyClsDecls. (Never in getInitialKind, never in the
2107 -- "type-checking"/desugaring pass.)
2108 -- Never emits constraints, though the thing_inside might.
2109 kcTyClTyVars :: Name -> TcM a -> TcM a
2110 kcTyClTyVars tycon_name thing_inside
2111 -- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
2112 = do { tycon <- kcLookupTcTyCon tycon_name
2113 ; tcExtendTyVarEnv2 (tcTyConScopedTyVars tycon) $ thing_inside }
2114
2115 tcTyClTyVars :: Name
2116 -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
2117 -- ^ Used for the type variables of a type or class decl
2118 -- on the second full pass (type-checking/desugaring) in TcTyClDecls.
2119 -- This is *not* used in the initial-kind run, nor in the "kind-checking" pass.
2120 -- Accordingly, everything passed to the continuation is fully zonked.
2121 --
2122 -- (tcTyClTyVars T [a,b] thing_inside)
2123 -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
2124 -- calls thing_inside with arguments
2125 -- [k1,k2,a,b] [k1:*, k2:*, Anon (k1 -> *), Anon k1] (k2 -> *)
2126 -- having also extended the type environment with bindings
2127 -- for k1,k2,a,b
2128 --
2129 -- Never emits constraints.
2130 --
2131 -- The LHsTyVarBndrs is always user-written, and the full, generalised
2132 -- kind of the tycon is available in the local env.
2133 tcTyClTyVars tycon_name thing_inside
2134 = do { tycon <- kcLookupTcTyCon tycon_name
2135
2136 -- Do checks on scoped tyvars
2137 -- See Note [Free-floating kind vars]
2138 ; let flav = tyConFlavour tycon
2139 scoped_prs = tcTyConScopedTyVars tycon
2140 scoped_tvs = map snd scoped_prs
2141 still_sig_tvs = filter isSigTyVar scoped_tvs
2142
2143 ; mapM_ report_sig_tv_err (findDupSigTvs scoped_prs)
2144
2145 ; checkNoErrs $ reportFloatingKvs tycon_name flav
2146 scoped_tvs still_sig_tvs
2147
2148 ; let res_kind = tyConResKind tycon
2149 binders = correct_binders (tyConBinders tycon) res_kind
2150 ; traceTc "tcTyClTyVars" (ppr tycon_name <+> ppr binders)
2151 ; scopeTyVars2 (TyConSkol flav tycon_name) scoped_prs $
2152 thing_inside binders res_kind }
2153 where
2154 report_sig_tv_err (n1, n2)
2155 = setSrcSpan (getSrcSpan n2) $
2156 addErrTc (text "Couldn't match" <+> quotes (ppr n1)
2157 <+> text "with" <+> quotes (ppr n2))
2158
2159 -- Given some TyConBinders and a TyCon's result kind, make sure that the
2160 -- correct any wrong Named/Anon choices. For example, consider
2161 -- type Syn k = forall (a :: k). Proxy a
2162 -- At first, it looks like k should be named -- after all, it appears on the RHS.
2163 -- However, the correct kind for Syn is (* -> *).
2164 -- (Why? Because k is the kind of a type, so k's kind is *. And the RHS also has
2165 -- kind *.) See also #13963.
2166 correct_binders :: [TyConBinder] -> Kind -> [TyConBinder]
2167 correct_binders binders kind
2168 = binders'
2169 where
2170 (_, binders') = mapAccumR go (tyCoVarsOfType kind) binders
2171
2172 go :: TyCoVarSet -> TyConBinder -> (TyCoVarSet, TyConBinder)
2173 go fvs binder
2174 | isNamedTyConBinder binder
2175 , not (tv `elemVarSet` fvs)
2176 = (new_fvs, mkAnonTyConBinder tv)
2177
2178 | not (isNamedTyConBinder binder)
2179 , tv `elemVarSet` fvs
2180 = (new_fvs, mkNamedTyConBinder Required tv)
2181 -- always Required, because it was anonymous (i.e. visible) previously
2182
2183 | otherwise
2184 = (new_fvs, binder)
2185
2186 where
2187 tv = binderVar binder
2188 new_fvs = fvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv)
2189
2190 -----------------------------------
2191 tcDataKindSig :: [TyConBinder]
2192 -> Kind
2193 -> TcM ([TyConBinder], Kind)
2194 -- GADT decls can have a (perhaps partial) kind signature
2195 -- e.g. data T a :: * -> * -> * where ...
2196 -- This function makes up suitable (kinded) TyConBinders for the
2197 -- argument kinds. E.g. in this case it might return
2198 -- ([b::*, c::*], *)
2199 -- Never emits constraints.
2200 -- It's a little trickier than you might think: see
2201 -- Note [TyConBinders for the result kind signature of a data type]
2202 tcDataKindSig tc_bndrs kind
2203 = do { loc <- getSrcSpanM
2204 ; uniqs <- newUniqueSupply
2205 ; rdr_env <- getLocalRdrEnv
2206 ; let new_occs = [ occ
2207 | str <- allNameStrings
2208 , let occ = mkOccName tvName str
2209 , isNothing (lookupLocalRdrOcc rdr_env occ)
2210 -- Note [Avoid name clashes for associated data types]
2211 , not (occ `elem` lhs_occs) ]
2212 new_uniqs = uniqsFromSupply uniqs
2213 subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet lhs_tvs))
2214 ; return (go loc new_occs new_uniqs subst [] kind) }
2215 where
2216 lhs_tvs = map binderVar tc_bndrs
2217 lhs_occs = map getOccName lhs_tvs
2218
2219 go loc occs uniqs subst acc kind
2220 = case splitPiTy_maybe kind of
2221 Nothing -> (reverse acc, substTy subst kind)
2222
2223 Just (Anon arg, kind')
2224 -> go loc occs' uniqs' subst' (tcb : acc) kind'
2225 where
2226 arg' = substTy subst arg
2227 tv = mkTyVar (mkInternalName uniq occ loc) arg'
2228 subst' = extendTCvInScope subst tv
2229 tcb = TvBndr tv AnonTCB
2230 (uniq:uniqs') = uniqs
2231 (occ:occs') = occs
2232
2233 Just (Named (TvBndr tv vis), kind')
2234 -> go loc occs uniqs subst' (tcb : acc) kind'
2235 where
2236 (subst', tv') = substTyVarBndr subst tv
2237 tcb = TvBndr tv' (NamedTCB vis)
2238
2239 badKindSig :: Bool -> Kind -> SDoc
2240 badKindSig check_for_type kind
2241 = hang (sep [ text "Kind signature on data type declaration has non-*"
2242 , (if check_for_type then empty else text "and non-variable") <+>
2243 text "return kind" ])
2244 2 (ppr kind)
2245
2246 {- Note [TyConBinders for the result kind signature of a data type]
2247 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2248 Given
2249 data T (a::*) :: * -> forall k. k -> *
2250 we want to generate the extra TyConBinders for T, so we finally get
2251 (a::*) (b::*) (k::*) (c::k)
2252 The function tcDataKindSig generates these extra TyConBinders from
2253 the result kind signature.
2254
2255 We need to take care to give the TyConBinders
2256 (a) OccNames that are fresh (because the TyConBinders of a TyCon
2257 must have distinct OccNames
2258
2259 (b) Uniques that are fresh (obviously)
2260
2261 For (a) we need to avoid clashes with the tyvars declared by
2262 the user before the "::"; in the above example that is 'a'.
2263 And also see Note [Avoid name clashes for associated data types].
2264
2265 For (b) suppose we have
2266 data T :: forall k. k -> forall k. k -> *
2267 where the two k's are identical even up to their uniques. Surprisingly,
2268 this can happen: see Trac #14515.
2269
2270 It's reasonably easy to solve all this; just run down the list with a
2271 substitution; hence the recursive 'go' function. But it has to be
2272 done.
2273
2274 Note [Avoid name clashes for associated data types]
2275 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2276 Consider class C a b where
2277 data D b :: * -> *
2278 When typechecking the decl for D, we'll invent an extra type variable
2279 for D, to fill out its kind. Ideally we don't want this type variable
2280 to be 'a', because when pretty printing we'll get
2281 class C a b where
2282 data D b a0
2283 (NB: the tidying happens in the conversion to IfaceSyn, which happens
2284 as part of pretty-printing a TyThing.)
2285
2286 That's why we look in the LocalRdrEnv to see what's in scope. This is
2287 important only to get nice-looking output when doing ":info C" in GHCi.
2288 It isn't essential for correctness.
2289
2290
2291 ************************************************************************
2292 * *
2293 Partial signatures
2294 * *
2295 ************************************************************************
2296
2297 -}
2298
2299 tcHsPartialSigType
2300 :: UserTypeCtxt
2301 -> LHsSigWcType GhcRn -- The type signature
2302 -> TcM ( [(Name, TcTyVar)] -- Wildcards
2303 , Maybe TcType -- Extra-constraints wildcard
2304 , [Name] -- Original tyvar names, in correspondence with ...
2305 , [TcTyVar] -- ... Implicitly and explicitly bound type variables
2306 , TcThetaType -- Theta part
2307 , TcType ) -- Tau part
2308 -- See Note [Recipe for checking a signature]
2309 tcHsPartialSigType ctxt sig_ty
2310 | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
2311 , HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_hs_tvs }
2312 , hsib_body = hs_ty } <- ib_ty
2313 , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
2314 = addSigCtxt ctxt hs_ty $
2315 do { (implicit_tvs, (explicit_tvs, (wcs, wcx, theta, tau)))
2316 <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ wcs ->
2317 tcImplicitTKBndrsSig skol_info implicit_hs_tvs $
2318 tcExplicitTKBndrs skol_info explicit_hs_tvs $
2319 do { -- Instantiate the type-class context; but if there
2320 -- is an extra-constraints wildcard, just discard it here
2321 (theta, wcx) <- tcPartialContext hs_ctxt
2322
2323 ; tau <- tcHsOpenType hs_tau
2324
2325 ; return (wcs, wcx, theta, tau) }
2326
2327 -- We must return these separately, because all the zonking below
2328 -- might change the name of a SigTv. This, in turn, causes trouble
2329 -- in partial type signatures that bind scoped type variables, as
2330 -- we bring the wrong name into scope in the function body.
2331 -- Test case: partial-sigs/should_compile/LocalDefinitionBug
2332 ; let tv_names = map tyVarName (implicit_tvs ++ explicit_tvs)
2333
2334 -- Spit out the wildcards (including the extra-constraints one)
2335 -- as "hole" constraints, so that they'll be reported if necessary
2336 -- See Note [Extra-constraint holes in partial type signatures]
2337 ; emitWildCardHoleConstraints wcs
2338
2339 -- The SigTvs created above will sometimes have too high a TcLevel
2340 -- (note that they are generated *after* bumping the level in
2341 -- the tc{Im,Ex}plicitTKBndrsSig functions. Bumping the level
2342 -- is still important here, because the kinds of these variables
2343 -- do indeed need to have the higher level, so they can unify
2344 -- with other local type variables. But, now that we've type-checked
2345 -- everything (and solved equalities in the tcImplicit call)
2346 -- we need to promote the SigTvs so we don't violate the TcLevel
2347 -- invariant
2348 ; all_tvs <- mapM zonkPromoteTyCoVarBndr (implicit_tvs ++ explicit_tvs)
2349 -- zonkPromoteTyCoVarBndr deals well with SigTvs
2350
2351 ; theta <- mapM zonkPromoteType theta
2352 ; tau <- zonkPromoteType tau
2353
2354 ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
2355
2356 ; traceTc "tcHsPartialSigType" (ppr all_tvs)
2357 ; return (wcs, wcx, tv_names, all_tvs, theta, tau) }
2358 where
2359 skol_info = SigTypeSkol ctxt
2360 tcHsPartialSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPartialSigType"
2361 tcHsPartialSigType _ (XHsWildCardBndrs _) = panic "tcHsPartialSigType"
2362
2363 tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcType)
2364 tcPartialContext hs_theta
2365 | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
2366 , L _ (HsWildCardTy wc) <- ignoreParens hs_ctxt_last
2367 = do { wc_tv_ty <- tcWildCardOcc wc constraintKind
2368 ; theta <- mapM tcLHsPredType hs_theta1
2369 ; return (theta, Just wc_tv_ty) }
2370 | otherwise
2371 = do { theta <- mapM tcLHsPredType hs_theta
2372 ; return (theta, Nothing) }
2373
2374 {- Note [Extra-constraint holes in partial type signatures]
2375 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2376 Consider
2377 f :: (_) => a -> a
2378 f x = ...
2379
2380 * The renamer makes a wildcard name for the "_", and puts it in
2381 the hswc_wcs field.
2382
2383 * Then, in tcHsPartialSigType, we make a new hole TcTyVar, in
2384 tcWildCardBindersX.
2385
2386 * TcBinds.chooseInferredQuantifiers fills in that hole TcTyVar
2387 with the inferred constraints, e.g. (Eq a, Show a)
2388
2389 * TcErrors.mkHoleError finally reports the error.
2390
2391 An annoying difficulty happens if there are more than 62 inferred
2392 constraints. Then we need to fill in the TcTyVar with (say) a 70-tuple.
2393 Where do we find the TyCon? For good reasons we only have constraint
2394 tuples up to 62 (see Note [How tuples work] in TysWiredIn). So how
2395 can we make a 70-tuple? This was the root cause of Trac #14217.
2396
2397 It's incredibly tiresome, because we only need this type to fill
2398 in the hole, to communicate to the error reporting machinery. Nothing
2399 more. So I use a HACK:
2400
2401 * I make an /ordinary/ tuple of the constraints, in
2402 TcBinds.chooseInferredQuantifiers. This is ill-kinded because
2403 ordinary tuples can't contain constraints, but it works fine. And for
2404 ordinary tuples we don't have the same limit as for constraint
2405 tuples (which need selectors and an assocated class).
2406
2407 * Because it is ill-kinded, it trips an assert in writeMetaTyVar,
2408 so now I disable the assertion if we are writing a type of
2409 kind Constraint. (That seldom/never normally happens so we aren't
2410 losing much.)
2411
2412 Result works fine, but it may eventually bite us.
2413
2414
2415 ************************************************************************
2416 * *
2417 Pattern signatures (i.e signatures that occur in patterns)
2418 * *
2419 ********************************************************************* -}
2420
2421 tcHsPatSigType :: UserTypeCtxt
2422 -> LHsSigWcType GhcRn -- The type signature
2423 -> TcM ( [(Name, TcTyVar)] -- Wildcards
2424 , [(Name, TcTyVar)] -- The new bit of type environment, binding
2425 -- the scoped type variables
2426 , TcType) -- The type
2427 -- Used for type-checking type signatures in
2428 -- (a) patterns e.g f (x::Int) = e
2429 -- (b) RULE forall bndrs e.g. forall (x::Int). f x = x
2430 --
2431 -- This may emit constraints
2432 -- See Note [Recipe for checking a signature]
2433 tcHsPatSigType ctxt sig_ty
2434 | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
2435 , HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars}
2436 , hsib_body = hs_ty } <- ib_ty
2437 = addSigCtxt ctxt hs_ty $
2438 do { sig_tkvs <- mapM new_implicit_tv sig_vars
2439 ; (wcs, sig_ty)
2440 <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ wcs ->
2441 tcExtendTyVarEnv sig_tkvs $
2442 do { sig_ty <- tcHsOpenType hs_ty
2443 ; return (wcs, sig_ty) }
2444
2445 ; emitWildCardHoleConstraints wcs
2446
2447 -- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
2448 -- contains a forall). Promote these.
2449 ; sig_ty <- zonkPromoteType sig_ty
2450 ; checkValidType ctxt sig_ty
2451
2452 ; tv_pairs <- mapM mk_tv_pair sig_tkvs
2453
2454 ; traceTc "tcHsPatSigType" (ppr sig_vars)
2455 ; return (wcs, tv_pairs, sig_ty) }
2456 where
2457 new_implicit_tv name = do { kind <- newMetaKindVar
2458 ; new_tv name kind }
2459
2460 new_tv = case ctxt of
2461 RuleSigCtxt {} -> newSkolemTyVar
2462 _ -> newSigTyVar
2463 -- See Note [Pattern signature binders]
2464 -- See Note [Unifying SigTvs]
2465
2466 mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv
2467 ; return (tyVarName tv, tv') }
2468 -- The Name is one of sig_vars, the lexically scoped name
2469 -- But if it's a SigTyVar, it might have been unified
2470 -- with an existing in-scope skolem, so we must zonk
2471 -- here. See Note [Pattern signature binders]
2472 tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPatSigType"
2473 tcHsPatSigType _ (XHsWildCardBndrs _) = panic "tcHsPatSigType"
2474
2475 tcPatSig :: Bool -- True <=> pattern binding
2476 -> LHsSigWcType GhcRn
2477 -> ExpSigmaType
2478 -> TcM (TcType, -- The type to use for "inside" the signature
2479 [(Name,TcTyVar)], -- The new bit of type environment, binding
2480 -- the scoped type variables
2481 [(Name,TcTyVar)], -- The wildcards
2482 HsWrapper) -- Coercion due to unification with actual ty
2483 -- Of shape: res_ty ~ sig_ty
2484 tcPatSig in_pat_bind sig res_ty
2485 = do { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
2486 -- sig_tvs are the type variables free in 'sig',
2487 -- and not already in scope. These are the ones
2488 -- that should be brought into scope
2489
2490 ; if null sig_tvs then do {
2491 -- Just do the subsumption check and return
2492 wrap <- addErrCtxtM (mk_msg sig_ty) $
2493 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
2494 ; return (sig_ty, [], sig_wcs, wrap)
2495 } else do
2496 -- Type signature binds at least one scoped type variable
2497
2498 -- A pattern binding cannot bind scoped type variables
2499 -- It is more convenient to make the test here
2500 -- than in the renamer
2501 { when in_pat_bind (addErr (patBindSigErr sig_tvs))
2502
2503 -- Check that all newly-in-scope tyvars are in fact
2504 -- constrained by the pattern. This catches tiresome
2505 -- cases like
2506 -- type T a = Int
2507 -- f :: Int -> Int
2508 -- f (x :: T a) = ...
2509 -- Here 'a' doesn't get a binding. Sigh
2510 ; let bad_tvs = [ tv | (_,tv) <- sig_tvs
2511 , not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ]
2512 ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
2513
2514 -- Now do a subsumption check of the pattern signature against res_ty
2515 ; wrap <- addErrCtxtM (mk_msg sig_ty) $
2516 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
2517
2518 -- Phew!
2519 ; return (sig_ty, sig_tvs, sig_wcs, wrap)
2520 } }
2521 where
2522 mk_msg sig_ty tidy_env
2523 = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
2524 ; res_ty <- readExpType res_ty -- should be filled in by now
2525 ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
2526 ; let msg = vcat [ hang (text "When checking that the pattern signature:")
2527 4 (ppr sig_ty)
2528 , nest 2 (hang (text "fits the type of its context:")
2529 2 (ppr res_ty)) ]
2530 ; return (tidy_env, msg) }
2531
2532 patBindSigErr :: [(Name,TcTyVar)] -> SDoc
2533 patBindSigErr sig_tvs
2534 = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
2535 <+> pprQuotedList (map fst sig_tvs))
2536 2 (text "in a pattern binding signature")
2537
2538 {- Note [Pattern signature binders]
2539 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2540 Consider
2541 data T = forall a. T a (a->Int)
2542 f (T x (f :: b->Int)) = blah
2543
2544 Here
2545 * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk',
2546 It must be a skolem so that that it retains its identity, and
2547 TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
2548
2549 * The type signature pattern (f :: b->Int) makes a fresh meta-tyvar b_sig
2550 (a SigTv), and binds "b" :-> b_sig in the envt
2551
2552 * Then unification makes b_sig := a_sk
2553 That's why we must make b_sig a MetaTv (albeit a SigTv),
2554 not a SkolemTv, so that it can unify to a_sk.
2555
2556 * Finally, in 'blah' we must have the envt "b" :-> a_sk. The pair
2557 ("b" :-> a_sk) is returned by tcHsPatSigType, constructed by
2558 mk_tv_pair in that function.
2559
2560 Another example (Trac #13881):
2561 fl :: forall (l :: [a]). Sing l -> Sing l
2562 fl (SNil :: Sing (l :: [y])) = SNil
2563 When we reach the pattern signature, 'l' is in scope from the
2564 outer 'forall':
2565 "a" :-> a_sk :: *
2566 "l" :-> l_sk :: [a_sk]
2567 We make up a fresh meta-SigTv, y_sig, for 'y', and kind-check
2568 the pattern signature
2569 Sing (l :: [y])
2570 That unifies y_sig := a_sk. We return from tcHsPatSigType with
2571 the pair ("y" :-> a_sk).
2572
2573 For RULE binders, though, things are a bit different (yuk).
2574 RULE "foo" forall (x::a) (y::[a]). f x y = ...
2575 Here this really is the binding site of the type variable so we'd like
2576 to use a skolem, so that we get a complaint if we unify two of them
2577 together.
2578
2579 Note [Unifying SigTvs]
2580 ~~~~~~~~~~~~~~~~~~~~~~
2581 ALAS we have no decent way of avoiding two SigTvs getting unified.
2582 Consider
2583 f (x::(a,b)) (y::c)) = [fst x, y]
2584 Here we'd really like to complain that 'a' and 'c' are unified. But
2585 for the reasons above we can't make a,b,c into skolems, so they
2586 are just SigTvs that can unify. And indeed, this would be ok,
2587 f x (y::c) = case x of
2588 (x1 :: a1, True) -> [x,y]
2589 (x1 :: a2, False) -> [x,y,y]
2590 Here the type of x's first component is called 'a1' in one branch and
2591 'a2' in the other. We could try insisting on the same OccName, but
2592 they definitely won't have the sane lexical Name.
2593
2594 I think we could solve this by recording in a SigTv a list of all the
2595 in-scope variables that it should not unify with, but it's fiddly.
2596
2597
2598 ************************************************************************
2599 * *
2600 Checking kinds
2601 * *
2602 ************************************************************************
2603
2604 -}
2605
2606 unifyKinds :: [LHsType GhcRn] -> [(TcType, TcKind)] -> TcM ([TcType], TcKind)
2607 unifyKinds rn_tys act_kinds
2608 = do { kind <- newMetaKindVar
2609 ; let check rn_ty (ty, act_kind) = checkExpectedKind (unLoc rn_ty) ty act_kind kind
2610 ; tys' <- zipWithM check rn_tys act_kinds
2611 ; return (tys', kind) }
2612
2613 {-
2614 ************************************************************************
2615 * *
2616 Promotion
2617 * *
2618 ************************************************************************
2619 -}
2620
2621 -- | Whenever a type is about to be added to the environment, it's necessary
2622 -- to make sure that any free meta-tyvars in the type are promoted to the
2623 -- current TcLevel. (They might be at a higher level due to the level-bumping
2624 -- in tcExplicitTKBndrs, for example.) This function both zonks *and*
2625 -- promotes.
2626 zonkPromoteType :: TcType -> TcM TcType
2627 zonkPromoteType = mapType zonkPromoteMapper ()
2628
2629 -- cf. TcMType.zonkTcTypeMapper
2630 zonkPromoteMapper :: TyCoMapper () TcM
2631 zonkPromoteMapper = TyCoMapper { tcm_smart = True
2632 , tcm_tyvar = const zonkPromoteTcTyVar
2633 , tcm_covar = const covar
2634 , tcm_hole = const hole
2635 , tcm_tybinder = const tybinder }
2636 where
2637 covar cv
2638 = mkCoVarCo <$> zonkPromoteTyCoVarKind cv
2639
2640 hole :: CoercionHole -> TcM Coercion
2641 hole h
2642 = do { contents <- unpackCoercionHole_maybe h
2643 ; case contents of
2644 Just co -> do { co <- zonkPromoteCoercion co
2645 ; checkCoercionHole cv co }
2646 Nothing -> do { cv' <- zonkPromoteTyCoVarKind cv
2647 ; return $ mkHoleCo (setCoHoleCoVar h cv') } }
2648 where
2649 cv = coHoleCoVar h
2650
2651 tybinder :: TyVar -> ArgFlag -> TcM ((), TyVar)
2652 tybinder tv _flag = ((), ) <$> zonkPromoteTyCoVarKind tv
2653
2654 zonkPromoteTcTyVar :: TyCoVar -> TcM TcType
2655 zonkPromoteTcTyVar tv
2656 | isMetaTyVar tv
2657 = do { let ref = metaTyVarRef tv
2658 ; contents <- readTcRef ref
2659 ; case contents of
2660 Flexi -> do { promoted <- promoteTyVar tv
2661 ; if promoted
2662 then zonkPromoteTcTyVar tv -- read it again
2663 else mkTyVarTy <$> zonkPromoteTyCoVarKind tv }
2664 Indirect ty -> zonkPromoteType ty }
2665
2666 | isTcTyVar tv && isSkolemTyVar tv -- NB: isSkolemTyVar says "True" to pure TyVars
2667 = do { tc_lvl <- getTcLevel
2668 ; mkTyVarTy <$> zonkPromoteTyCoVarKind (promoteSkolem tc_lvl tv) }
2669
2670 | otherwise
2671 = mkTyVarTy <$> zonkPromoteTyCoVarKind tv
2672
2673 zonkPromoteTyCoVarKind :: TyCoVar -> TcM TyCoVar
2674 zonkPromoteTyCoVarKind = updateTyVarKindM zonkPromoteType
2675
2676 zonkPromoteTyCoVarBndr :: TyCoVar -> TcM TyCoVar
2677 zonkPromoteTyCoVarBndr tv
2678 | isSigTyVar tv
2679 = tcGetTyVar "zonkPromoteTyCoVarBndr SigTv" <$> zonkPromoteTcTyVar tv
2680
2681 | isTcTyVar tv && isSkolemTyVar tv
2682 = do { tc_lvl <- getTcLevel
2683 ; zonkPromoteTyCoVarKind (promoteSkolem tc_lvl tv) }
2684
2685 | otherwise
2686 = zonkPromoteTyCoVarKind tv
2687
2688 zonkPromoteCoercion :: Coercion -> TcM Coercion
2689 zonkPromoteCoercion = mapCoercion zonkPromoteMapper ()
2690
2691 zonkPromoteTypeInKnot :: TcType -> TcM TcType
2692 zonkPromoteTypeInKnot = mapType (zonkPromoteMapper { tcm_smart = False }) ()
2693 -- NB: Just changing smart to False will still use the smart zonker (not suitable
2694 -- for in-the-knot) for kinds. But that's OK, because kinds aren't knot-tied.
2695
2696 {-
2697 ************************************************************************
2698 * *
2699 Sort checking kinds
2700 * *
2701 ************************************************************************
2702
2703 tcLHsKindSig converts a user-written kind to an internal, sort-checked kind.
2704 It does sort checking and desugaring at the same time, in one single pass.
2705 -}
2706
2707 tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
2708 tcLHsKindSig ctxt hs_kind
2709 -- See Note [Recipe for checking a signature] in TcHsType
2710 = do { kind <- solveLocalEqualities $
2711 tc_lhs_kind kindLevelMode hs_kind
2712 ; kind <- zonkPromoteType kind
2713 -- This zonk is very important in the case of higher rank kinds
2714 -- E.g. Trac #13879 f :: forall (p :: forall z (y::z). <blah>).
2715 -- <more blah>
2716 -- When instantiating p's kind at occurrences of p in <more blah>
2717 -- it's crucial that the kind we instantiate is fully zonked,
2718 -- else we may fail to substitute properly
2719
2720 ; checkValidType ctxt kind
2721 ; return kind }
2722
2723 tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind
2724 tc_lhs_kind mode k
2725 = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $
2726 tc_lhs_type (kindLevel mode) k liftedTypeKind
2727
2728 promotionErr :: Name -> PromotionErr -> TcM a
2729 promotionErr name err
2730 = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here")
2731 2 (parens reason))
2732 where
2733 reason = case err of
2734 FamDataConPE -> text "it comes from a data family instance"
2735 NoDataKindsTC -> text "perhaps you intended to use DataKinds"
2736 NoDataKindsDC -> text "perhaps you intended to use DataKinds"
2737 NoTypeInTypeTC -> text "perhaps you intended to use TypeInType"
2738 NoTypeInTypeDC -> text "perhaps you intended to use TypeInType"
2739 PatSynPE -> text "pattern synonyms cannot be promoted"
2740 PatSynExPE -> sep [ text "the existential variables of a pattern synonym"
2741 , text "signature do not scope over the pattern" ]
2742 _ -> text "it is defined and used in the same recursive group"
2743
2744 {-
2745 ************************************************************************
2746 * *
2747 Scoped type variables
2748 * *
2749 ************************************************************************
2750 -}
2751
2752 badPatSigTvs :: TcType -> [TyVar] -> SDoc
2753 badPatSigTvs sig_ty bad_tvs
2754 = vcat [ fsep [text "The type variable" <> plural bad_tvs,
2755 quotes (pprWithCommas ppr bad_tvs),
2756 text "should be bound by the pattern signature" <+> quotes (ppr sig_ty),
2757 text "but are actually discarded by a type synonym" ]
2758 , text "To fix this, expand the type synonym"
2759 , text "[Note: I hope to lift this restriction in due course]" ]
2760
2761 {-
2762 ************************************************************************
2763 * *
2764 Error messages and such
2765 * *
2766 ************************************************************************
2767 -}
2768
2769 -- | Make an appropriate message for an error in a function argument.
2770 -- Used for both expressions and types.
2771 funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
2772 funAppCtxt fun arg arg_no
2773 = hang (hsep [ text "In the", speakNth arg_no, ptext (sLit "argument of"),
2774 quotes (ppr fun) <> text ", namely"])
2775 2 (quotes (ppr arg))
2776
2777 -- See Note [Free-floating kind vars]
2778 reportFloatingKvs :: Name -- of the tycon
2779 -> TyConFlavour -- What sort of TyCon it is
2780 -> [TcTyVar] -- all tyvars, not necessarily zonked
2781 -> [TcTyVar] -- floating tyvars
2782 -> TcM ()
2783 reportFloatingKvs tycon_name flav all_tvs bad_tvs
2784 = unless (null bad_tvs) $ -- don't bother zonking if there's no error
2785 do { all_tvs <- mapM zonkTcTyVarToTyVar all_tvs
2786 ; bad_tvs <- mapM zonkTcTyVarToTyVar bad_tvs
2787 ; let (tidy_env, tidy_all_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
2788 tidy_bad_tvs = map (tidyTyVarOcc tidy_env) bad_tvs
2789 ; typeintype <- xoptM LangExt.TypeInType
2790 ; mapM_ (report typeintype tidy_all_tvs) tidy_bad_tvs }
2791 where
2792 report typeintype tidy_all_tvs tidy_bad_tv
2793 = addErr $
2794 vcat [ text "Kind variable" <+> quotes (ppr tidy_bad_tv) <+>
2795 text "is implicitly bound in" <+> ppr flav
2796 , quotes (ppr tycon_name) <> comma <+>
2797 text "but does not appear as the kind of any"
2798 , text "of its type variables. Perhaps you meant"
2799 , text "to bind it" <+> ppWhen (not typeintype)
2800 (text "(with TypeInType)") <+>
2801 text "explicitly somewhere?"
2802 , ppWhen (not (null tidy_all_tvs)) $
2803 hang (text "Type variables with inferred kinds:")
2804 2 (ppr_tv_bndrs tidy_all_tvs) ]
2805
2806 ppr_tv_bndrs tvs = sep (map pp_tv tvs)
2807 pp_tv tv = parens (ppr tv <+> dcolon <+> ppr (tyVarKind tv))