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