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