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