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