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