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