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