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