Rename SigTv to TyVarTv (#15480)
[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 >>= zonkTcType
211
212 ; checkValidType ctxt ty
213 ; traceTc "end tcHsSigType }" (ppr ty)
214 ; return ty }
215 where
216 skol_info = SigTypeSkol ctxt
217
218 tc_hs_sig_type_and_gen :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
219 -- Kind-checks/desugars an 'LHsSigType',
220 -- solve equalities,
221 -- and then kind-generalizes.
222 -- This will never emit constraints, as it uses solveEqualities interally.
223 -- No validity checking or zonking
224 tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext = sig_vars
225 , hsib_body = hs_ty }) kind
226 = do { ((tkvs, ty), wanted) <- captureConstraints $
227 tcImplicitTKBndrs skol_info sig_vars $
228 tc_lhs_type typeLevelMode hs_ty kind
229 -- Any remaining variables (unsolved in the solveLocalEqualities in the
230 -- tcImplicitTKBndrs)
231 -- should be in the global tyvars, and therefore won't be quantified
232 -- 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 emptyZonkEnv cls_kind
257 ; ty <- zonkTcTypeToType emptyZonkEnv 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 emptyZonkEnv 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 emptyZonkEnv 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 every 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 (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. zonkPromoteType and friends zonk and promote at the same time.
1487 Accordingly, the function does setps 3-5 all at once, preventing
1488 the need for multiple traversals.
1489
1490 2. kindGeneralize does not require a zonked type -- it zonks as it
1491 gathers free variables. So this way effectively sidesteps step 3.
1492
1493 -}
1494
1495 tcWildCardBinders :: [Name]
1496 -> ([(Name, TcTyVar)] -> TcM a)
1497 -> TcM a
1498 tcWildCardBinders wc_names thing_inside
1499 = do { wcs <- mapM newWildTyVar wc_names
1500 ; let wc_prs = wc_names `zip` wcs
1501 ; tcExtendNameTyVarEnv wc_prs $
1502 thing_inside wc_prs }
1503
1504 -- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
1505 -- user-supplied kind signature (CUSK), generalise the result.
1506 -- Used in 'getInitialKind' (for tycon kinds and other kinds)
1507 -- and in kind-checking (but not for tycon kinds, which are checked with
1508 -- tcTyClDecls). See Note [CUSKs: complete user-supplied kind signatures]
1509 -- in HsDecls.
1510 --
1511 -- This function does not do telescope checking.
1512 kcLHsQTyVars :: Name -- ^ of the thing being checked
1513 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
1514 -> Bool -- ^ True <=> the decl being checked has a CUSK
1515 -> LHsQTyVars GhcRn
1516 -> TcM Kind -- ^ The result kind
1517 -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon
1518 kcLHsQTyVars name flav cusk
1519 user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
1520 , hsq_dependent = dep_names }
1521 , hsq_explicit = hs_tvs }) thing_inside
1522 | cusk
1523 = do { (scoped_kvs, (tc_tvs, res_kind))
1524 <- solveEqualities $
1525 tcImplicitQTKBndrs skol_info kv_ns $
1526 kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
1527
1528 -- Now, because we're in a CUSK, quantify over the mentioned
1529 -- kind vars, in dependency order.
1530 ; let tc_binders_unzonked = zipWith mk_tc_binder hs_tvs tc_tvs
1531 ; dvs <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys scoped_kvs $
1532 mkTyConKind tc_binders_unzonked res_kind)
1533 ; qkvs <- quantifyTyVars emptyVarSet dvs
1534 -- don't call tcGetGlobalTyCoVars. For associated types, it gets the
1535 -- tyvars from the enclosing class -- but that's wrong. We *do* want
1536 -- to quantify over those tyvars.
1537
1538 ; scoped_kvs <- mapM zonkTcTyVarToTyVar scoped_kvs
1539 ; tc_tvs <- mapM zonkTcTyVarToTyVar tc_tvs
1540 ; res_kind <- zonkTcType res_kind
1541 ; let tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
1542
1543 -- If any of the scoped_kvs aren't actually mentioned in a binder's
1544 -- kind (or the return kind), then we're in the CUSK case from
1545 -- Note [Free-floating kind vars]
1546 ; let all_tc_tvs = scoped_kvs ++ tc_tvs
1547 all_mentioned_tvs = mapUnionVarSet (tyCoVarsOfType . tyVarKind)
1548 all_tc_tvs
1549 `unionVarSet` tyCoVarsOfType res_kind
1550 unmentioned_kvs = filterOut (`elemVarSet` all_mentioned_tvs)
1551 scoped_kvs
1552 ; reportFloatingKvs name flav all_tc_tvs unmentioned_kvs
1553
1554 ; let final_binders = map (mkNamedTyConBinder Inferred) qkvs
1555 ++ map (mkNamedTyConBinder Specified) scoped_kvs
1556 ++ tc_binders
1557 tycon = mkTcTyCon name (ppr user_tyvars) final_binders res_kind
1558 (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
1559 flav
1560 -- the tvs contain the binders already
1561 -- in scope from an enclosing class, but
1562 -- re-adding tvs to the env't doesn't cause
1563 -- harm
1564
1565 ; traceTc "kcLHsQTyVars: cusk" $
1566 vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
1567 , ppr tc_tvs, ppr (mkTyConKind final_binders res_kind)
1568 , ppr qkvs, ppr final_binders ]
1569
1570 ; return tycon }
1571
1572 | otherwise
1573 = do { (scoped_kvs, (tc_tvs, res_kind))
1574 -- Why kcImplicitTKBndrs which uses newTyVarTyVar?
1575 -- See Note [Kind generalisation and TyVarTvs]
1576 <- kcImplicitTKBndrs kv_ns $
1577 kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
1578
1579 ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they
1580 -- must remain lined up with the binders
1581 tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
1582 tycon = mkTcTyCon name (ppr user_tyvars) tc_binders res_kind
1583 (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
1584 flav
1585
1586 ; traceTc "kcLHsQTyVars: not-cusk" $
1587 vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
1588 , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ]
1589 ; return tycon }
1590 where
1591 open_fam = tcFlavourIsOpen flav
1592 skol_info = TyConSkol flav name
1593
1594 mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder
1595 -- See Note [Dependent LHsQTyVars]
1596 mk_tc_binder hs_tv tv
1597 | hsLTyVarName hs_tv `elemNameSet` dep_names
1598 = mkNamedTyConBinder Required tv
1599 | otherwise
1600 = mkAnonTyConBinder tv
1601
1602 kcLHsQTyVars _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
1603
1604 kcLHsQTyVarBndrs :: Bool -- True <=> bump the TcLevel when bringing vars into scope
1605 -> Bool -- True <=> Default un-annotated tyvar
1606 -- binders to kind *
1607 -> SkolemInfo
1608 -> [LHsTyVarBndr GhcRn]
1609 -> TcM r
1610 -> TcM ([TyVar], r)
1611 -- There may be dependency between the explicit "ty" vars.
1612 -- So, we have to handle them one at a time.
1613 kcLHsQTyVarBndrs _ _ _ [] thing
1614 = do { stuff <- thing; return ([], stuff) }
1615
1616 kcLHsQTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing
1617 = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
1618 -- NB: Bring all tvs into scope, even non-dependent ones,
1619 -- as they're needed in type synonyms, data constructors, etc.
1620
1621 ; (tvs, stuff) <- bind_unless_scoped tv_pair $
1622 kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs $
1623 thing
1624
1625 ; return ( tv : tvs, stuff ) }
1626 where
1627 -- | Bind the tyvar in the env't unless the bool is True
1628 bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a
1629 bind_unless_scoped (_, True) thing_inside = thing_inside
1630 bind_unless_scoped (tv, False) thing_inside
1631 | cusk = scopeTyVars skol_info [tv] thing_inside
1632 | otherwise = tcExtendTyVarEnv [tv] thing_inside
1633 -- These variables haven't settled down yet, so we don't want to bump
1634 -- the TcLevel. If we do, then we'll have metavars of too high a level
1635 -- floating about. Changing this causes many, many failures in the
1636 -- `dependent` testsuite directory.
1637
1638 kc_hs_tv :: HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
1639 -- Special handling for the case where the binder is already in scope
1640 -- See Note [Associated type tyvar names] in Class and
1641 -- Note [TyVar binders for associated decls] in HsDecls
1642 kc_hs_tv (UserTyVar _ (L _ name))
1643 = do { mb_tv <- tcLookupLcl_maybe name
1644 ; case mb_tv of -- See Note [TyVar binders for associated decls]
1645 Just (ATyVar _ tv) -> return (tv, True)
1646 _ -> do { kind <- if open_fam
1647 then return liftedTypeKind
1648 else newMetaKindVar
1649 -- Open type/data families default their variables
1650 -- variables to kind *. But don't default in-scope
1651 -- class tyvars, of course
1652 ; tv <- newSkolemTyVar name kind
1653 ; return (tv, False) } }
1654
1655 kc_hs_tv (KindedTyVar _ lname@(L _ name) lhs_kind)
1656 = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt name) lhs_kind
1657 ; mb_tv <- tcLookupLcl_maybe name
1658 ; case mb_tv of
1659 Just (ATyVar _ tv)
1660 -> do { discardResult $
1661 unifyKind (Just (HsTyVar noExt NotPromoted lname))
1662 kind (tyVarKind tv)
1663 ; return (tv, True) }
1664 _ -> do { tv <- newSkolemTyVar name kind
1665 ; return (tv, False) } }
1666
1667 kc_hs_tv (XTyVarBndr{}) = panic "kc_hs_tv"
1668
1669 {- Note [Kind-checking tyvar binders for associated types]
1670 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1671 When kind-checking the type-variable binders for associated
1672 data/newtype decls
1673 family decls
1674 we behave specially for type variables that are already in scope;
1675 that is, bound by the enclosing class decl. This is done in
1676 kcLHsQTyVarBndrs:
1677 * The use of tcImplicitQTKBndrs
1678 * The tcLookupLocal_maybe code in kc_hs_tv
1679
1680 See Note [Associated type tyvar names] in Class and
1681 Note [TyVar binders for associated decls] in HsDecls
1682
1683 We must do the same for family instance decls, where the in-scope
1684 variables may be bound by the enclosing class instance decl.
1685 Hence the use of tcImplicitQTKBndrs in tcFamTyPats.
1686 -}
1687
1688
1689 --------------------------------------
1690 -- Implicit binders
1691 --------------------------------------
1692
1693 -- | Bring implicitly quantified type/kind variables into scope during
1694 -- kind checking. Uses TyVarTvs, as per Note [Use TyVarTvs in kind-checking pass]
1695 -- in TcTyClsDecls.
1696 kcImplicitTKBndrs :: [Name] -- of the vars
1697 -> TcM a
1698 -> TcM ([TcTyVar], a) -- returns the tyvars created
1699 -- these are *not* dependency ordered
1700 kcImplicitTKBndrs var_ns thing_inside
1701 = do { tkvs <- mapM newFlexiKindedTyVarTyVar var_ns
1702 ; result <- tcExtendTyVarEnv tkvs thing_inside
1703 ; return (tkvs, result) }
1704
1705
1706 tcImplicitTKBndrs, tcImplicitTKBndrsSig, tcImplicitQTKBndrs
1707 :: SkolemInfo
1708 -> [Name]
1709 -> TcM a
1710 -> TcM ([TcTyVar], a)
1711 tcImplicitTKBndrs = tcImplicitTKBndrsX newFlexiKindedSkolemTyVar
1712 tcImplicitTKBndrsSig = tcImplicitTKBndrsX newFlexiKindedTyVarTyVar
1713 tcImplicitQTKBndrs = tcImplicitTKBndrsX newFlexiKindedQTyVar
1714
1715 tcImplicitTKBndrsX :: (Name -> TcM TcTyVar) -- new_tv function
1716 -> SkolemInfo
1717 -> [Name]
1718 -> TcM a
1719 -> TcM ([TcTyVar], a) -- these tyvars are dependency-ordered
1720 -- * Guarantees to call solveLocalEqualities to unify
1721 -- all constraints from thing_inside.
1722 --
1723 -- * Returned TcTyVars have the supplied HsTyVarBndrs,
1724 -- but may be in different order to the original [Name]
1725 -- (because of sorting to respect dependency)
1726 --
1727 -- * Returned TcTyVars have zonked kinds
1728 -- See Note [Keeping scoped variables in order: Implicit]
1729 tcImplicitTKBndrsX new_tv skol_info tv_names thing_inside
1730 | null tv_names -- Short cut for the common case where there
1731 -- are no implicit type variables to bind
1732 = do { result <- solveLocalEqualities thing_inside
1733 ; return ([], result) }
1734
1735 | otherwise
1736 = do { (skol_tvs, result)
1737 <- solveLocalEqualities $
1738 checkTvConstraints skol_info Nothing $
1739 do { tkvs <- mapM new_tv tv_names
1740 ; result <- tcExtendTyVarEnv tkvs thing_inside
1741 ; return (tkvs, result) }
1742
1743 ; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs
1744 -- use zonkTcTyCoVarBndr because a skol_tv might be a TyVarTv
1745
1746 -- do a stable topological sort, following
1747 -- Note [Ordering of implicit variables] in HsTypes
1748 ; let final_tvs = toposortTyVars skol_tvs
1749 ; traceTc "tcImplicitTKBndrs" (ppr tv_names $$ ppr final_tvs)
1750 ; return (final_tvs, result) }
1751
1752 newFlexiKindedQTyVar :: Name -> TcM TcTyVar
1753 -- Make a new skolem for an implicit binder in a type/class/type
1754 -- instance declaration, with a flexi-kind
1755 -- But check for in-scope-ness, and if so return that instead
1756 newFlexiKindedQTyVar name
1757 = do { mb_tv <- tcLookupLcl_maybe name
1758 ; case mb_tv of
1759 Just (ATyVar _ tv) -> return tv
1760 _ -> newFlexiKindedSkolemTyVar name }
1761
1762 newFlexiKindedTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM TyVar
1763 newFlexiKindedTyVar new_tv name
1764 = do { kind <- newMetaKindVar
1765 ; new_tv name kind }
1766
1767 newFlexiKindedSkolemTyVar :: Name -> TcM TyVar
1768 newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar
1769
1770 newFlexiKindedTyVarTyVar :: Name -> TcM TyVar
1771 newFlexiKindedTyVarTyVar = newFlexiKindedTyVar newTyVarTyVar
1772
1773 --------------------------------------
1774 -- Explicit binders
1775 --------------------------------------
1776
1777 -- | Used during the "kind-checking" pass in TcTyClsDecls only,
1778 -- and even then only for data-con declarations.
1779 -- See Note [Use TyVarTvs in kind-checking pass] in TcTyClsDecls
1780 kcExplicitTKBndrs :: [LHsTyVarBndr GhcRn]
1781 -> TcM a
1782 -> TcM a
1783 kcExplicitTKBndrs [] thing_inside = thing_inside
1784 kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside
1785 = do { tv <- tcHsTyVarBndr newTyVarTyVar hs_tv
1786 ; tcExtendTyVarEnv [tv] $
1787 kcExplicitTKBndrs hs_tvs thing_inside }
1788
1789 tcExplicitTKBndrs :: SkolemInfo
1790 -> [LHsTyVarBndr GhcRn]
1791 -> TcM a
1792 -> TcM ([TcTyVar], a)
1793 tcExplicitTKBndrs skol_info hs_tvs thing_inside
1794 -- Used for the forall'd binders in type signatures of various kinds:
1795 -- - function signatures
1796 -- - data con signatures in GADT-style decls
1797 -- - pattern synonym signatures
1798 -- - expression type signatures
1799 --
1800 -- Specifically NOT used for the binders of a data type
1801 -- or type family decl. So the forall'd variables always /shadow/
1802 -- anything already in scope, and the complications of
1803 -- tcHsQTyVarName to not apply.
1804 --
1805 -- This function brings into scope a telescope of binders as written by
1806 -- the user. At first blush, it would then seem that we should bring
1807 -- them into scope one at a time, bumping the TcLevel each time.
1808 -- (Recall that we bump the level to prevent skolem escape from happening.)
1809 -- However, this leads to terrible error messages, because we end up
1810 -- failing to unify with some `k0`. Better would be to allow type inference
1811 -- to work, potentially creating a skolem-escape problem, and then to
1812 -- notice that the telescope is out of order. That's what we do here,
1813 -- following the logic of tcImplicitTKBndrsX.
1814 -- See also Note [Keeping scoped variables in order: Explicit]
1815 --
1816 -- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
1817 | null hs_tvs -- Short cut that avoids creating an implication
1818 -- constraint in the common case where none is needed
1819 = do { result <- thing_inside
1820 ; return ([], result) }
1821
1822 | otherwise
1823 = do { (skol_tvs, result) <- checkTvConstraints skol_info (Just doc) $
1824 bind_tvbs hs_tvs
1825
1826 ; traceTc "tcExplicitTKBndrs" $
1827 vcat [ text "Hs vars:" <+> ppr hs_tvs
1828 , text "tvs:" <+> pprTyVars skol_tvs ]
1829
1830 ; return (skol_tvs, result) }
1831
1832 where
1833 bind_tvbs [] = do { result <- thing_inside
1834 ; return ([], result) }
1835 bind_tvbs (L _ tvb : tvbs)
1836 = do { tv <- tcHsTyVarBndr newSkolemTyVar tvb
1837 ; tcExtendTyVarEnv [tv] $
1838 do { (tvs, result) <- bind_tvbs tvbs
1839 ; return (tv : tvs, result) }}
1840
1841 doc = sep (map ppr hs_tvs)
1842
1843 -----------------
1844 tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
1845 -> HsTyVarBndr GhcRn -> TcM TcTyVar
1846 -- Return a TcTyVar, built using the provided function
1847 -- Typically the Kind inside the HsTyVarBndr will be a tyvar
1848 -- with a mutable kind in it.
1849 --
1850 -- Returned TcTyVar has the same name; no cloning
1851 tcHsTyVarBndr new_tv (UserTyVar _ (L _ tv_nm))
1852 = newFlexiKindedTyVar new_tv tv_nm
1853 tcHsTyVarBndr new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
1854 = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
1855 ; new_tv tv_nm kind }
1856 tcHsTyVarBndr _ (XTyVarBndr _) = panic "tcHsTyVarBndr"
1857
1858 -----------------
1859 newWildTyVar :: Name -> TcM TcTyVar
1860 -- ^ New unification variable for a wildcard
1861 newWildTyVar _name
1862 = do { kind <- newMetaKindVar
1863 ; uniq <- newUnique
1864 ; details <- newMetaDetails TauTv
1865 ; let name = mkSysTvName uniq (fsLit "w")
1866 tyvar = (mkTcTyVar name kind details)
1867 ; traceTc "newWildTyVar" (ppr tyvar)
1868 ; return tyvar }
1869
1870 --------------------------
1871 -- Bringing tyvars into scope
1872 --------------------------
1873
1874 -- | Bring tyvars into scope, wrapping the thing_inside in an implication
1875 -- constraint. The implication constraint is necessary to provide SkolemInfo
1876 -- for the tyvars and to ensure that no unification variables made outside
1877 -- the scope of these tyvars (i.e. lower TcLevel) unify with the locally-scoped
1878 -- tyvars (i.e. higher TcLevel).
1879 --
1880 -- INVARIANT: The thing_inside must check only types, never terms.
1881 --
1882 -- Use this (not tcExtendTyVarEnv) wherever you expect a Λ or ∀ in Core.
1883 -- Use tcExtendTyVarEnv otherwise.
1884 scopeTyVars :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a
1885 scopeTyVars skol_info tvs = scopeTyVars2 skol_info [(tyVarName tv, tv) | tv <- tvs]
1886
1887 -- | Like 'scopeTyVars', but allows you to specify different scoped names
1888 -- than the Names stored within the tyvars.
1889 scopeTyVars2 :: SkolemInfo -> [(Name, TcTyVar)] -> TcM a -> TcM a
1890 scopeTyVars2 skol_info prs thing_inside
1891 = fmap snd $ -- discard the TcEvBinds, which will always be empty
1892 checkConstraints skol_info (map snd prs) [{- no EvVars -}] $
1893 tcExtendNameTyVarEnv prs $
1894 thing_inside
1895
1896 ------------------
1897 kindGeneralize :: TcType -> TcM [KindVar]
1898 -- Quantify the free kind variables of a kind or type
1899 -- In the latter case the type is closed, so it has no free
1900 -- type variables. So in both cases, all the free vars are kind vars
1901 -- Input needn't be zonked.
1902 -- NB: You must call solveEqualities or solveLocalEqualities before
1903 -- kind generalization
1904 kindGeneralize = kindGeneralizeLocal emptyWC
1905
1906 -- | This variant of 'kindGeneralize' refuses to generalize over any
1907 -- variables free in the given WantedConstraints. Instead, it promotes
1908 -- these variables into an outer TcLevel. See also
1909 -- Note [Promoting unification variables] in TcSimplify
1910 kindGeneralizeLocal :: WantedConstraints -> TcType -> TcM [KindVar]
1911 kindGeneralizeLocal wanted kind_or_type
1912 = do {
1913 -- This bit is very much like decideMonoTyVars in TcSimplify,
1914 -- but constraints are so much simpler in kinds, it is much
1915 -- easier here. (In particular, we never quantify over a
1916 -- constraint in a type.)
1917 ; constrained <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted)
1918 ; (_, constrained) <- promoteTyVarSet constrained
1919
1920 -- NB: zonk here, after promotion
1921 ; kvs <- zonkTcTypeAndFV kind_or_type
1922 ; let dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet }
1923
1924 ; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
1925 ; traceTc "kindGeneralizeLocal" (vcat [ ppr wanted
1926 , ppr kind_or_type
1927 , ppr constrained
1928 , ppr dvs ])
1929
1930 ; quantifyTyVars (gbl_tvs `unionVarSet` constrained) dvs }
1931
1932 {-
1933 Note [Kind generalisation]
1934 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1935 We do kind generalisation only at the outer level of a type signature.
1936 For example, consider
1937 T :: forall k. k -> *
1938 f :: (forall a. T a -> Int) -> Int
1939 When kind-checking f's type signature we generalise the kind at
1940 the outermost level, thus:
1941 f1 :: forall k. (forall (a:k). T k a -> Int) -> Int -- YES!
1942 and *not* at the inner forall:
1943 f2 :: (forall k. forall (a:k). T k a -> Int) -> Int -- NO!
1944 Reason: same as for HM inference on value level declarations,
1945 we want to infer the most general type. The f2 type signature
1946 would be *less applicable* than f1, because it requires a more
1947 polymorphic argument.
1948
1949 NB: There are no explicit kind variables written in f's signature.
1950 When there are, the renamer adds these kind variables to the list of
1951 variables bound by the forall, so you can indeed have a type that's
1952 higher-rank in its kind. But only by explicit request.
1953
1954 Note [Kinds of quantified type variables]
1955 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1956 tcTyVarBndrsGen quantifies over a specified list of type variables,
1957 *and* over the kind variables mentioned in the kinds of those tyvars.
1958
1959 Note that we must zonk those kinds (obviously) but less obviously, we
1960 must return type variables whose kinds are zonked too. Example
1961 (a :: k7) where k7 := k9 -> k9
1962 We must return
1963 [k9, a:k9->k9]
1964 and NOT
1965 [k9, a:k7]
1966 Reason: we're going to turn this into a for-all type,
1967 forall k9. forall (a:k7). blah
1968 which the type checker will then instantiate, and instantiate does not
1969 look through unification variables!
1970
1971 Hence using zonked_kinds when forming tvs'.
1972
1973 Note [Free-floating kind vars]
1974 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1975 Consider
1976
1977 data T = MkT (forall (a :: k). Proxy a)
1978 -- from test ghci/scripts/T7873
1979
1980 This is not an existential datatype, but a higher-rank one (the forall
1981 to the right of MkT). Also consider
1982
1983 data S a = MkS (Proxy (a :: k))
1984
1985 According to the rules around implicitly-bound kind variables, in both
1986 cases those k's scope over the whole declaration. The renamer grabs
1987 it and adds it to the hsq_implicits field of the HsQTyVars of the
1988 tycon. So it must be in scope during type-checking, but we want to
1989 reject T while accepting S.
1990
1991 Why reject T? Because the kind variable isn't fixed by anything. For
1992 a variable like k to be implicit, it needs to be mentioned in the kind
1993 of a tycon tyvar. But it isn't.
1994
1995 Why accept S? Because kind inference tells us that a has kind k, so it's
1996 all OK.
1997
1998 Our approach depends on whether or not the datatype has a CUSK.
1999
2000 Non-CUSK: In the first pass (kcTyClTyVars) we just bring
2001 k into scope. In the second pass (tcTyClTyVars),
2002 we check to make sure that k has been unified with some other variable
2003 (or generalized over, making k into a skolem). If it hasn't been, then
2004 it must be a free-floating kind var. Error.
2005
2006 CUSK: When we determine the tycon's final, never-to-be-changed kind
2007 in kcLHsQTyVars, we check to make sure all implicitly-bound kind
2008 vars are indeed mentioned in a kind somewhere. If not, error.
2009
2010 We also perform free-floating kind var analysis for type family instances
2011 (see #13985). Here is an interesting example:
2012
2013 type family T :: k
2014 type instance T = (Nothing :: Maybe a)
2015
2016 Upon a cursory glance, it may appear that the kind variable `a` is
2017 free-floating above, since there are no (visible) LHS patterns in `T`. However,
2018 there is an *invisible* pattern due to the return kind, so inside of GHC, the
2019 instance looks closer to this:
2020
2021 type family T @k :: k
2022 type instance T @(Maybe a) = (Nothing :: Maybe a)
2023
2024 Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in
2025 fact not free-floating. Contrast that with this example:
2026
2027 type instance T = Proxy (Nothing :: Maybe a)
2028
2029 This would looks like this inside of GHC:
2030
2031 type instance T @(*) = Proxy (Nothing :: Maybe a)
2032
2033 So this time, `a` is neither bound by a visible nor invisible type pattern on
2034 the LHS, so it would be reported as free-floating.
2035
2036 Finally, here's one more brain-teaser (from #9574). In the example below:
2037
2038 class Funct f where
2039 type Codomain f :: *
2040 instance Funct ('KProxy :: KProxy o) where
2041 type Codomain 'KProxy = NatTr (Proxy :: o -> *)
2042
2043 As it turns out, `o` is not free-floating in this example. That is because `o`
2044 bound by the kind signature of the LHS type pattern 'KProxy. To make this more
2045 obvious, one can also write the instance like so:
2046
2047 instance Funct ('KProxy :: KProxy o) where
2048 type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *)
2049
2050 -}
2051
2052 --------------------
2053 -- getInitialKind has made a suitably-shaped kind for the type or class
2054 -- Look it up in the local environment. This is used only for tycons
2055 -- that we're currently type-checking, so we're sure to find a TcTyCon.
2056 kcLookupTcTyCon :: Name -> TcM TcTyCon
2057 kcLookupTcTyCon nm
2058 = do { tc_ty_thing <- tcLookup nm
2059 ; return $ case tc_ty_thing of
2060 ATcTyCon tc -> tc
2061 _ -> pprPanic "kcLookupTcTyCon" (ppr tc_ty_thing) }
2062
2063 -----------------------
2064 -- | Bring tycon tyvars into scope. This is used during the "kind-checking"
2065 -- pass in TcTyClsDecls. (Never in getInitialKind, never in the
2066 -- "type-checking"/desugaring pass.)
2067 -- Never emits constraints, though the thing_inside might.
2068 kcTyClTyVars :: Name -> TcM a -> TcM a
2069 kcTyClTyVars tycon_name thing_inside
2070 -- See Note [Use TyVarTvs in kind-checking pass] in TcTyClsDecls
2071 = do { tycon <- kcLookupTcTyCon tycon_name
2072 ; tcExtendNameTyVarEnv (tcTyConScopedTyVars tycon) $ thing_inside }
2073
2074 tcTyClTyVars :: Name
2075 -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
2076 -- ^ Used for the type variables of a type or class decl
2077 -- on the second full pass (type-checking/desugaring) in TcTyClDecls.
2078 -- This is *not* used in the initial-kind run, nor in the "kind-checking" pass.
2079 -- Accordingly, everything passed to the continuation is fully zonked.
2080 --
2081 -- (tcTyClTyVars T [a,b] thing_inside)
2082 -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
2083 -- calls thing_inside with arguments
2084 -- [k1,k2,a,b] [k1:*, k2:*, Anon (k1 -> *), Anon k1] (k2 -> *)
2085 -- having also extended the type environment with bindings
2086 -- for k1,k2,a,b
2087 --
2088 -- Never emits constraints.
2089 --
2090 -- The LHsTyVarBndrs is always user-written, and the full, generalised
2091 -- kind of the tycon is available in the local env.
2092 tcTyClTyVars tycon_name thing_inside
2093 = do { tycon <- kcLookupTcTyCon tycon_name
2094
2095 -- Do checks on scoped tyvars
2096 -- See Note [Free-floating kind vars]
2097 ; let flav = tyConFlavour tycon
2098 scoped_prs = tcTyConScopedTyVars tycon
2099 scoped_tvs = map snd scoped_prs
2100 still_sig_tvs = filter isTyVarTyVar scoped_tvs
2101
2102 ; mapM_ report_sig_tv_err (findDupTyVarTvs scoped_prs)
2103
2104 ; checkNoErrs $ reportFloatingKvs tycon_name flav
2105 scoped_tvs still_sig_tvs
2106
2107 ; let res_kind = tyConResKind tycon
2108 binders = correct_binders (tyConBinders tycon) res_kind
2109 ; traceTc "tcTyClTyVars" (ppr tycon_name <+> ppr binders)
2110 ; scopeTyVars2 (TyConSkol flav tycon_name) scoped_prs $
2111 thing_inside binders res_kind }
2112 where
2113 report_sig_tv_err (n1, n2)
2114 = setSrcSpan (getSrcSpan n2) $
2115 addErrTc (text "Couldn't match" <+> quotes (ppr n1)
2116 <+> text "with" <+> quotes (ppr n2))
2117
2118 -- Given some TyConBinders and a TyCon's result kind, make sure that the
2119 -- correct any wrong Named/Anon choices. For example, consider
2120 -- type Syn k = forall (a :: k). Proxy a
2121 -- At first, it looks like k should be named -- after all, it appears on the RHS.
2122 -- However, the correct kind for Syn is (* -> *).
2123 -- (Why? Because k is the kind of a type, so k's kind is *. And the RHS also has
2124 -- kind *.) See also #13963.
2125 correct_binders :: [TyConBinder] -> Kind -> [TyConBinder]
2126 correct_binders binders kind
2127 = binders'
2128 where
2129 (_, binders') = mapAccumR go (tyCoVarsOfType kind) binders
2130
2131 go :: TyCoVarSet -> TyConBinder -> (TyCoVarSet, TyConBinder)
2132 go fvs binder
2133 | isNamedTyConBinder binder
2134 , not (tv `elemVarSet` fvs)
2135 = (new_fvs, mkAnonTyConBinder tv)
2136
2137 | not (isNamedTyConBinder binder)
2138 , tv `elemVarSet` fvs
2139 = (new_fvs, mkNamedTyConBinder Required tv)
2140 -- always Required, because it was anonymous (i.e. visible) previously
2141
2142 | otherwise
2143 = (new_fvs, binder)
2144
2145 where
2146 tv = binderVar binder
2147 new_fvs = fvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv)
2148
2149 -----------------------------------
2150 tcDataKindSig :: [TyConBinder]
2151 -> Kind
2152 -> TcM ([TyConBinder], Kind)
2153 -- GADT decls can have a (perhaps partial) kind signature
2154 -- e.g. data T a :: * -> * -> * where ...
2155 -- This function makes up suitable (kinded) TyConBinders for the
2156 -- argument kinds. E.g. in this case it might return
2157 -- ([b::*, c::*], *)
2158 -- Never emits constraints.
2159 -- It's a little trickier than you might think: see
2160 -- Note [TyConBinders for the result kind signature of a data type]
2161 tcDataKindSig tc_bndrs kind
2162 = do { loc <- getSrcSpanM
2163 ; uniqs <- newUniqueSupply
2164 ; rdr_env <- getLocalRdrEnv
2165 ; let new_occs = [ occ
2166 | str <- allNameStrings
2167 , let occ = mkOccName tvName str
2168 , isNothing (lookupLocalRdrOcc rdr_env occ)
2169 -- Note [Avoid name clashes for associated data types]
2170 , not (occ `elem` lhs_occs) ]
2171 new_uniqs = uniqsFromSupply uniqs
2172 subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet lhs_tvs))
2173 ; return (go loc new_occs new_uniqs subst [] kind) }
2174 where
2175 lhs_tvs = map binderVar tc_bndrs
2176 lhs_occs = map getOccName lhs_tvs
2177
2178 go loc occs uniqs subst acc kind
2179 = case splitPiTy_maybe kind of
2180 Nothing -> (reverse acc, substTy subst kind)
2181
2182 Just (Anon arg, kind')
2183 -> go loc occs' uniqs' subst' (tcb : acc) kind'
2184 where
2185 arg' = substTy subst arg
2186 tv = mkTyVar (mkInternalName uniq occ loc) arg'
2187 subst' = extendTCvInScope subst tv
2188 tcb = TvBndr tv AnonTCB
2189 (uniq:uniqs') = uniqs
2190 (occ:occs') = occs
2191
2192 Just (Named (TvBndr tv vis), kind')
2193 -> go loc occs uniqs subst' (tcb : acc) kind'
2194 where
2195 (subst', tv') = substTyVarBndr subst tv
2196 tcb = TvBndr tv' (NamedTCB vis)
2197
2198 badKindSig :: Bool -> Kind -> SDoc
2199 badKindSig check_for_type kind
2200 = hang (sep [ text "Kind signature on data type declaration has non-*"
2201 , (if check_for_type then empty else text "and non-variable") <+>
2202 text "return kind" ])
2203 2 (ppr kind)
2204
2205 {- Note [TyConBinders for the result kind signature of a data type]
2206 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2207 Given
2208 data T (a::*) :: * -> forall k. k -> *
2209 we want to generate the extra TyConBinders for T, so we finally get
2210 (a::*) (b::*) (k::*) (c::k)
2211 The function tcDataKindSig generates these extra TyConBinders from
2212 the result kind signature.
2213
2214 We need to take care to give the TyConBinders
2215 (a) OccNames that are fresh (because the TyConBinders of a TyCon
2216 must have distinct OccNames
2217
2218 (b) Uniques that are fresh (obviously)
2219
2220 For (a) we need to avoid clashes with the tyvars declared by
2221 the user before the "::"; in the above example that is 'a'.
2222 And also see Note [Avoid name clashes for associated data types].
2223
2224 For (b) suppose we have
2225 data T :: forall k. k -> forall k. k -> *
2226 where the two k's are identical even up to their uniques. Surprisingly,
2227 this can happen: see Trac #14515.
2228
2229 It's reasonably easy to solve all this; just run down the list with a
2230 substitution; hence the recursive 'go' function. But it has to be
2231 done.
2232
2233 Note [Avoid name clashes for associated data types]
2234 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2235 Consider class C a b where
2236 data D b :: * -> *
2237 When typechecking the decl for D, we'll invent an extra type variable
2238 for D, to fill out its kind. Ideally we don't want this type variable
2239 to be 'a', because when pretty printing we'll get
2240 class C a b where
2241 data D b a0
2242 (NB: the tidying happens in the conversion to IfaceSyn, which happens
2243 as part of pretty-printing a TyThing.)
2244
2245 That's why we look in the LocalRdrEnv to see what's in scope. This is
2246 important only to get nice-looking output when doing ":info C" in GHCi.
2247 It isn't essential for correctness.
2248
2249
2250 ************************************************************************
2251 * *
2252 Partial signatures
2253 * *
2254 ************************************************************************
2255
2256 -}
2257
2258 tcHsPartialSigType
2259 :: UserTypeCtxt
2260 -> LHsSigWcType GhcRn -- The type signature
2261 -> TcM ( [(Name, TcTyVar)] -- Wildcards
2262 , Maybe TcType -- Extra-constraints wildcard
2263 , [Name] -- Original tyvar names, in correspondence with ...
2264 , [TcTyVar] -- ... Implicitly and explicitly bound type variables
2265 , TcThetaType -- Theta part
2266 , TcType ) -- Tau part
2267 -- See Note [Recipe for checking a signature]
2268 tcHsPartialSigType ctxt sig_ty
2269 | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
2270 , HsIB { hsib_ext = implicit_hs_tvs
2271 , hsib_body = hs_ty } <- ib_ty
2272 , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
2273 = addSigCtxt ctxt hs_ty $
2274 do { (implicit_tvs, (explicit_tvs, (wcs, wcx, theta, tau)))
2275 <- tcWildCardBinders sig_wcs $ \ wcs ->
2276 tcImplicitTKBndrsSig skol_info implicit_hs_tvs $
2277 tcExplicitTKBndrs skol_info explicit_hs_tvs $
2278 do { -- Instantiate the type-class context; but if there
2279 -- is an extra-constraints wildcard, just discard it here
2280 (theta, wcx) <- tcPartialContext hs_ctxt
2281
2282 ; tau <- tcHsOpenType hs_tau
2283
2284 ; return (wcs, wcx, theta, tau) }
2285
2286 -- We must return these separately, because all the zonking below
2287 -- might change the name of a TyVarTv. This, in turn, causes trouble
2288 -- in partial type signatures that bind scoped type variables, as
2289 -- we bring the wrong name into scope in the function body.
2290 -- Test case: partial-sigs/should_compile/LocalDefinitionBug
2291 ; let tv_names = map tyVarName (implicit_tvs ++ explicit_tvs)
2292
2293 -- Spit out the wildcards (including the extra-constraints one)
2294 -- as "hole" constraints, so that they'll be reported if necessary
2295 -- See Note [Extra-constraint holes in partial type signatures]
2296 ; emitWildCardHoleConstraints wcs
2297
2298 -- The TyVarTvs created above will sometimes have too high a TcLevel
2299 -- (note that they are generated *after* bumping the level in
2300 -- the tc{Im,Ex}plicitTKBndrsSig functions. Bumping the level
2301 -- is still important here, because the kinds of these variables
2302 -- do indeed need to have the higher level, so they can unify
2303 -- with other local type variables. But, now that we've type-checked
2304 -- everything (and solved equalities in the tcImplicit call)
2305 -- we need to promote the TyVarTvs so we don't violate the TcLevel
2306 -- invariant
2307 ; all_tvs <- mapM zonkPromoteTyCoVarBndr (implicit_tvs ++ explicit_tvs)
2308 -- zonkPromoteTyCoVarBndr deals well with TyVarTvs
2309
2310 ; theta <- mapM zonkPromoteType theta
2311 ; tau <- zonkPromoteType tau
2312
2313 ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
2314
2315 ; traceTc "tcHsPartialSigType" (ppr all_tvs)
2316 ; return (wcs, wcx, tv_names, all_tvs, theta, tau) }
2317 where
2318 skol_info = SigTypeSkol ctxt
2319 tcHsPartialSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPartialSigType"
2320 tcHsPartialSigType _ (XHsWildCardBndrs _) = panic "tcHsPartialSigType"
2321
2322 tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcType)
2323 tcPartialContext hs_theta
2324 | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
2325 , L _ (HsWildCardTy wc) <- ignoreParens hs_ctxt_last
2326 = do { wc_tv_ty <- tcWildCardOcc wc constraintKind
2327 ; theta <- mapM tcLHsPredType hs_theta1
2328 ; return (theta, Just wc_tv_ty) }
2329 | otherwise
2330 = do { theta <- mapM tcLHsPredType hs_theta
2331 ; return (theta, Nothing) }
2332
2333 {- Note [Extra-constraint holes in partial type signatures]
2334 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2335 Consider
2336 f :: (_) => a -> a
2337 f x = ...
2338
2339 * The renamer makes a wildcard name for the "_", and puts it in
2340 the hswc_wcs field.
2341
2342 * Then, in tcHsPartialSigType, we make a new hole TcTyVar, in
2343 tcWildCardBinders.
2344
2345 * TcBinds.chooseInferredQuantifiers fills in that hole TcTyVar
2346 with the inferred constraints, e.g. (Eq a, Show a)
2347
2348 * TcErrors.mkHoleError finally reports the error.
2349
2350 An annoying difficulty happens if there are more than 62 inferred
2351 constraints. Then we need to fill in the TcTyVar with (say) a 70-tuple.
2352 Where do we find the TyCon? For good reasons we only have constraint
2353 tuples up to 62 (see Note [How tuples work] in TysWiredIn). So how
2354 can we make a 70-tuple? This was the root cause of Trac #14217.
2355
2356 It's incredibly tiresome, because we only need this type to fill
2357 in the hole, to communicate to the error reporting machinery. Nothing
2358 more. So I use a HACK:
2359
2360 * I make an /ordinary/ tuple of the constraints, in
2361 TcBinds.chooseInferredQuantifiers. This is ill-kinded because
2362 ordinary tuples can't contain constraints, but it works fine. And for
2363 ordinary tuples we don't have the same limit as for constraint
2364 tuples (which need selectors and an assocated class).
2365
2366 * Because it is ill-kinded, it trips an assert in writeMetaTyVar,
2367 so now I disable the assertion if we are writing a type of
2368 kind Constraint. (That seldom/never normally happens so we aren't
2369 losing much.)
2370
2371 Result works fine, but it may eventually bite us.
2372
2373
2374 ************************************************************************
2375 * *
2376 Pattern signatures (i.e signatures that occur in patterns)
2377 * *
2378 ********************************************************************* -}
2379
2380 tcHsPatSigType :: UserTypeCtxt
2381 -> LHsSigWcType GhcRn -- The type signature
2382 -> TcM ( [(Name, TcTyVar)] -- Wildcards
2383 , [(Name, TcTyVar)] -- The new bit of type environment, binding
2384 -- the scoped type variables
2385 , TcType) -- The type
2386 -- Used for type-checking type signatures in
2387 -- (a) patterns e.g f (x::Int) = e
2388 -- (b) RULE forall bndrs e.g. forall (x::Int). f x = x
2389 --
2390 -- This may emit constraints
2391 -- See Note [Recipe for checking a signature]
2392 tcHsPatSigType ctxt sig_ty
2393 | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
2394 , HsIB { hsib_ext = sig_vars
2395 , hsib_body = hs_ty } <- ib_ty
2396 = addSigCtxt ctxt hs_ty $
2397 do { sig_tkvs <- mapM new_implicit_tv sig_vars
2398 ; (wcs, sig_ty)
2399 <- tcWildCardBinders sig_wcs $ \ wcs ->
2400 tcExtendTyVarEnv sig_tkvs $
2401 do { sig_ty <- tcHsOpenType hs_ty
2402 ; return (wcs, sig_ty) }
2403
2404 ; emitWildCardHoleConstraints wcs
2405
2406 -- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
2407 -- contains a forall). Promote these.
2408 -- Ex: f (x :: forall a. Proxy a -> ()) = ... x ...
2409 -- When we instantiate x, we have to compare the kind of the argument
2410 -- to a's kind, which will be a metavariable.
2411 ; sig_ty <- zonkPromoteType sig_ty
2412 ; checkValidType ctxt sig_ty
2413
2414 ; tv_pairs <- mapM mk_tv_pair sig_tkvs
2415
2416 ; traceTc "tcHsPatSigType" (ppr sig_vars)
2417 ; return (wcs, tv_pairs, sig_ty) }
2418 where
2419 new_implicit_tv name = do { kind <- newMetaKindVar
2420 ; new_tv name kind }
2421
2422 new_tv = case ctxt of
2423 RuleSigCtxt {} -> newSkolemTyVar
2424 _ -> newTauTyVar
2425 -- See Note [Pattern signature binders]
2426
2427 mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv
2428 ; return (tyVarName tv, tv') }
2429 -- The Name is one of sig_vars, the lexically scoped name
2430 -- But if it's a TyVarTv, it might have been unified
2431 -- with an existing in-scope skolem, so we must zonk
2432 -- here. See Note [Pattern signature binders]
2433 tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPatSigType"
2434 tcHsPatSigType _ (XHsWildCardBndrs _) = panic "tcHsPatSigType"
2435
2436 tcPatSig :: Bool -- True <=> pattern binding
2437 -> LHsSigWcType GhcRn
2438 -> ExpSigmaType
2439 -> TcM (TcType, -- The type to use for "inside" the signature
2440 [(Name,TcTyVar)], -- The new bit of type environment, binding
2441 -- the scoped type variables
2442 [(Name,TcTyVar)], -- The wildcards
2443 HsWrapper) -- Coercion due to unification with actual ty
2444 -- Of shape: res_ty ~ sig_ty
2445 tcPatSig in_pat_bind sig res_ty
2446 = do { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
2447 -- sig_tvs are the type variables free in 'sig',
2448 -- and not already in scope. These are the ones
2449 -- that should be brought into scope
2450
2451 ; if null sig_tvs then do {
2452 -- Just do the subsumption check and return
2453 wrap <- addErrCtxtM (mk_msg sig_ty) $
2454 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
2455 ; return (sig_ty, [], sig_wcs, wrap)
2456 } else do
2457 -- Type signature binds at least one scoped type variable
2458
2459 -- A pattern binding cannot bind scoped type variables
2460 -- It is more convenient to make the test here
2461 -- than in the renamer
2462 { when in_pat_bind (addErr (patBindSigErr sig_tvs))
2463
2464 -- Check that all newly-in-scope tyvars are in fact
2465 -- constrained by the pattern. This catches tiresome
2466 -- cases like
2467 -- type T a = Int
2468 -- f :: Int -> Int
2469 -- f (x :: T a) = ...
2470 -- Here 'a' doesn't get a binding. Sigh
2471 ; let bad_tvs = [ tv | (_,tv) <- sig_tvs
2472 , not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ]
2473 ; checkTc (null bad_tvs) (badPatTyVarTvs sig_ty bad_tvs)
2474
2475 -- Now do a subsumption check of the pattern signature against res_ty
2476 ; wrap <- addErrCtxtM (mk_msg sig_ty) $
2477 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
2478
2479 -- Phew!
2480 ; return (sig_ty, sig_tvs, sig_wcs, wrap)
2481 } }
2482 where
2483 mk_msg sig_ty tidy_env
2484 = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
2485 ; res_ty <- readExpType res_ty -- should be filled in by now
2486 ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
2487 ; let msg = vcat [ hang (text "When checking that the pattern signature:")
2488 4 (ppr sig_ty)
2489 , nest 2 (hang (text "fits the type of its context:")
2490 2 (ppr res_ty)) ]
2491 ; return (tidy_env, msg) }
2492
2493 patBindSigErr :: [(Name,TcTyVar)] -> SDoc
2494 patBindSigErr sig_tvs
2495 = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
2496 <+> pprQuotedList (map fst sig_tvs))
2497 2 (text "in a pattern binding signature")
2498
2499 {- Note [Pattern signature binders]
2500 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2501 Consider
2502
2503 data T where
2504 MkT :: forall a. a -> (a -> Int) -> T
2505
2506 f :: T -> ...
2507 f (MkT x (f :: b -> c)) = ...
2508
2509 Here
2510 * The pattern (MkT p1 p2) creates a *skolem* type variable 'a_sk',
2511 It must be a skolem so that that it retains its identity, and
2512 TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
2513
2514 * The type signature pattern (f :: b -> c) makes freshs meta-tyvars
2515 beta and gamma (TauTvs), and binds "b" :-> beta, "c" :-> gamma in the
2516 environment
2517
2518 * Then unification makes beta := a_sk, gamma := Int
2519 That's why we must make beta and gamma a MetaTv,
2520 not a SkolemTv, so that it can unify to a_sk rsp. Int.
2521 Note that gamma unifies with a type, not just a type variable
2522 (see https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0029-scoped-type-variables-types.rst)
2523
2524 * Finally, in 'blah' we must have the envt "b" :-> a_sk, "c" :-> Int.
2525 The pairs ("b" :-> a_sk, "c" :-> Int) are returned by tcHsPatSigType,
2526 constructed by mk_tv_pair in that function.
2527
2528 Another example (Trac #13881):
2529 fl :: forall (l :: [a]). Sing l -> Sing l
2530 fl (SNil :: Sing (l :: [y])) = SNil
2531 When we reach the pattern signature, 'l' is in scope from the
2532 outer 'forall':
2533 "a" :-> a_sk :: *
2534 "l" :-> l_sk :: [a_sk]
2535 We make up a fresh meta-TauTv, y_sig, for 'y', and kind-check
2536 the pattern signature
2537 Sing (l :: [y])
2538 That unifies y_sig := a_sk. We return from tcHsPatSigType with
2539 the pair ("y" :-> a_sk).
2540
2541 For RULE binders, though, things are a bit different (yuk).
2542 RULE "foo" forall (x::a) (y::[a]). f x y = ...
2543 Here this really is the binding site of the type variable so we'd like
2544 to use a skolem, so that we get a complaint if we unify two of them
2545 together.
2546
2547
2548
2549 ************************************************************************
2550 * *
2551 Checking kinds
2552 * *
2553 ************************************************************************
2554
2555 -}
2556
2557 unifyKinds :: [LHsType GhcRn] -> [(TcType, TcKind)] -> TcM ([TcType], TcKind)
2558 unifyKinds rn_tys act_kinds
2559 = do { kind <- newMetaKindVar
2560 ; let check rn_ty (ty, act_kind) = checkExpectedKind (unLoc rn_ty) ty act_kind kind
2561 ; tys' <- zipWithM check rn_tys act_kinds
2562 ; return (tys', kind) }
2563
2564 {-
2565 ************************************************************************
2566 * *
2567 Promotion
2568 * *
2569 ************************************************************************
2570 -}
2571
2572 -- | Whenever a type is about to be added to the environment, it's necessary
2573 -- to make sure that any free meta-tyvars in the type are promoted to the
2574 -- current TcLevel. (They might be at a higher level due to the level-bumping
2575 -- in tcExplicitTKBndrs, for example.) This function both zonks *and*
2576 -- promotes. Why at the same time? See Note [Recipe for checking a signature]
2577 zonkPromoteType :: TcType -> TcM TcType
2578 zonkPromoteType = mapType zonkPromoteMapper ()
2579
2580 -- cf. TcMType.zonkTcTypeMapper
2581 zonkPromoteMapper :: TyCoMapper () TcM
2582 zonkPromoteMapper = TyCoMapper { tcm_smart = True
2583 , tcm_tyvar = const zonkPromoteTcTyVar
2584 , tcm_covar = const covar
2585 , tcm_hole = const hole
2586 , tcm_tybinder = const tybinder
2587 , tcm_tycon = return }
2588 where
2589 covar cv
2590 = mkCoVarCo <$> zonkPromoteTyCoVarKind cv
2591
2592 hole :: CoercionHole -> TcM Coercion
2593 hole h
2594 = do { contents <- unpackCoercionHole_maybe h
2595 ; case contents of
2596 Just co -> do { co <- zonkPromoteCoercion co
2597 ; checkCoercionHole cv co }
2598 Nothing -> do { cv' <- zonkPromoteTyCoVarKind cv
2599 ; return $ mkHoleCo (setCoHoleCoVar h cv') } }
2600 where
2601 cv = coHoleCoVar h
2602
2603 tybinder :: TyVar -> ArgFlag -> TcM ((), TyVar)
2604 tybinder tv _flag = ((), ) <$> zonkPromoteTyCoVarKind tv
2605
2606 zonkPromoteTcTyVar :: TyCoVar -> TcM TcType
2607 zonkPromoteTcTyVar tv
2608 | isMetaTyVar tv
2609 = do { let ref = metaTyVarRef tv
2610 ; contents <- readTcRef ref
2611 ; case contents of
2612 Flexi -> do { (_, promoted_tv) <- promoteTyVar tv
2613 ; mkTyVarTy <$> zonkPromoteTyCoVarKind promoted_tv }
2614 Indirect ty -> zonkPromoteType ty }
2615
2616 | isTcTyVar tv && isSkolemTyVar tv -- NB: isSkolemTyVar says "True" to pure TyVars
2617 = do { tc_lvl <- getTcLevel
2618 ; mkTyVarTy <$> zonkPromoteTyCoVarKind (promoteSkolem tc_lvl tv) }
2619
2620 | otherwise
2621 = mkTyVarTy <$> zonkPromoteTyCoVarKind tv
2622
2623 zonkPromoteTyCoVarKind :: TyCoVar -> TcM TyCoVar
2624 zonkPromoteTyCoVarKind = updateTyVarKindM zonkPromoteType
2625
2626 zonkPromoteTyCoVarBndr :: TyCoVar -> TcM TyCoVar
2627 zonkPromoteTyCoVarBndr tv
2628 | isTyVarTyVar tv
2629 = tcGetTyVar "zonkPromoteTyCoVarBndr TyVarTv" <$> zonkPromoteTcTyVar tv
2630
2631 | isTcTyVar tv && isSkolemTyVar tv
2632 = do { tc_lvl <- getTcLevel
2633 ; zonkPromoteTyCoVarKind (promoteSkolem tc_lvl tv) }
2634
2635 | otherwise
2636 = zonkPromoteTyCoVarKind tv
2637
2638 zonkPromoteCoercion :: Coercion -> TcM Coercion
2639 zonkPromoteCoercion = mapCoercion zonkPromoteMapper ()
2640
2641 {-
2642 ************************************************************************
2643 * *
2644 Sort checking kinds
2645 * *
2646 ************************************************************************
2647
2648 tcLHsKindSig converts a user-written kind to an internal, sort-checked kind.
2649 It does sort checking and desugaring at the same time, in one single pass.
2650 -}
2651
2652 tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
2653 tcLHsKindSig ctxt hs_kind
2654 -- See Note [Recipe for checking a signature] in TcHsType
2655 -- Result is zonked
2656 = do { kind <- solveLocalEqualities $
2657 tc_lhs_kind kindLevelMode hs_kind
2658 ; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind)
2659 -- No generalization, so we must promote
2660 ; kind <- zonkPromoteType kind
2661 -- This zonk is very important in the case of higher rank kinds
2662 -- E.g. Trac #13879 f :: forall (p :: forall z (y::z). <blah>).
2663 -- <more blah>
2664 -- When instantiating p's kind at occurrences of p in <more blah>
2665 -- it's crucial that the kind we instantiate is fully zonked,
2666 -- else we may fail to substitute properly
2667
2668 ; checkValidType ctxt kind
2669 ; traceTc "tcLHsKindSig2" (ppr kind)
2670 ; return kind }
2671
2672 tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind
2673 tc_lhs_kind mode k
2674 = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $
2675 tc_lhs_type (kindLevel mode) k liftedTypeKind
2676
2677 promotionErr :: Name -> PromotionErr -> TcM a
2678 promotionErr name err
2679 = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here")
2680 2 (parens reason))
2681 where
2682 reason = case err of
2683 ConstrainedDataConPE pred
2684 -> text "it has an unpromotable context"
2685 <+> quotes (ppr pred)
2686 FamDataConPE -> text "it comes from a data family instance"
2687 NoDataKindsTC -> text "perhaps you intended to use DataKinds"
2688 NoDataKindsDC -> text "perhaps you intended to use DataKinds"
2689 PatSynPE -> text "pattern synonyms cannot be promoted"
2690 PatSynExPE -> sep [ text "the existential variables of a pattern synonym"
2691 , text "signature do not scope over the pattern" ]
2692 _ -> text "it is defined and used in the same recursive group"
2693
2694 {-
2695 ************************************************************************
2696 * *
2697 Scoped type variables
2698 * *
2699 ************************************************************************
2700 -}
2701
2702 badPatTyVarTvs :: TcType -> [TyVar] -> SDoc
2703 badPatTyVarTvs sig_ty bad_tvs
2704 = vcat [ fsep [text "The type variable" <> plural bad_tvs,
2705 quotes (pprWithCommas ppr bad_tvs),
2706 text "should be bound by the pattern signature" <+> quotes (ppr sig_ty),
2707 text "but are actually discarded by a type synonym" ]
2708 , text "To fix this, expand the type synonym"
2709 , text "[Note: I hope to lift this restriction in due course]" ]
2710
2711 {-
2712 ************************************************************************
2713 * *
2714 Error messages and such
2715 * *
2716 ************************************************************************
2717 -}
2718
2719 -- | Make an appropriate message for an error in a function argument.
2720 -- Used for both expressions and types.
2721 funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
2722 funAppCtxt fun arg arg_no
2723 = hang (hsep [ text "In the", speakNth arg_no, ptext (sLit "argument of"),
2724 quotes (ppr fun) <> text ", namely"])
2725 2 (quotes (ppr arg))
2726
2727 -- See Note [Free-floating kind vars]
2728 reportFloatingKvs :: Name -- of the tycon
2729 -> TyConFlavour -- What sort of TyCon it is
2730 -> [TcTyVar] -- all tyvars, not necessarily zonked
2731 -> [TcTyVar] -- floating tyvars
2732 -> TcM ()
2733 reportFloatingKvs tycon_name flav all_tvs bad_tvs
2734 = unless (null bad_tvs) $ -- don't bother zonking if there's no error
2735 do { all_tvs <- mapM zonkTcTyVarToTyVar all_tvs
2736 ; bad_tvs <- mapM zonkTcTyVarToTyVar bad_tvs
2737 ; let (tidy_env, tidy_all_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
2738 tidy_bad_tvs = map (tidyTyVarOcc tidy_env) bad_tvs
2739 ; mapM_ (report tidy_all_tvs) tidy_bad_tvs }
2740 where
2741 report tidy_all_tvs tidy_bad_tv
2742 = addErr $
2743 vcat [ text "Kind variable" <+> quotes (ppr tidy_bad_tv) <+>
2744 text "is implicitly bound in" <+> ppr flav
2745 , quotes (ppr tycon_name) <> comma <+>
2746 text "but does not appear as the kind of any"
2747 , text "of its type variables. Perhaps you meant"
2748 , text "to bind it explicitly somewhere?"
2749 , ppWhen (not (null tidy_all_tvs)) $
2750 hang (text "Type variables with inferred kinds:")
2751 2 (ppr_tv_bndrs tidy_all_tvs) ]
2752
2753 ppr_tv_bndrs tvs = sep (map pp_tv tvs)
2754 pp_tv tv = parens (ppr tv <+> dcolon <+> ppr (tyVarKind tv))
2755
2756 -- | If the inner action emits constraints, reports them as errors and fails;
2757 -- otherwise, propagates the return value. Useful as a wrapper around
2758 -- 'tcImplicitTKBndrs', which uses solveLocalEqualities, when there won't be
2759 -- another chance to solve constraints
2760 failIfEmitsConstraints :: TcM a -> TcM a
2761 failIfEmitsConstraints thing_inside
2762 = do { (res, lie) <- captureConstraints thing_inside
2763 ; reportAllUnsolved lie
2764 ; return res
2765 }