5f3750f281f9f723faf7125f06b6b16ca56f5b8b
[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(..), TyBinder, 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 -- See Note [Fail fast if there are insoluble kind equalities]
253 -- in TcSimplify
254 ; when (insolubleWC wanted) failM
255
256 ; return (mkInvForAllTys kvs ty1) }
257
258 tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
259
260 tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
261 -- tcTopLHsType is used for kind-checking top-level HsType where
262 -- we want to fully solve /all/ equalities, and report errors
263 -- Does zonking, but not validity checking because it's used
264 -- for things (like deriving and instances) that aren't
265 -- ordinary types
266 tcTopLHsType hs_sig_type ctxt_kind
267 | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
268 = do { traceTc "tcTopLHsType {" (ppr hs_ty)
269 ; (spec_tkvs, ty)
270 <- pushTcLevelM_ $
271 solveEqualities $
272 bindImplicitTKBndrs_Skol sig_vars $
273 do { kind <- newExpectedKind ctxt_kind
274 ; tc_lhs_type typeLevelMode hs_ty kind }
275
276 ; spec_tkvs <- zonkAndScopedSort spec_tkvs
277 ; let ty1 = mkSpecForAllTys spec_tkvs ty
278 ; kvs <- kindGeneralize ty1
279 ; final_ty <- zonkTcTypeToType (mkInvForAllTys kvs ty1)
280 ; traceTc "End tcTopLHsType }" (vcat [ppr hs_ty, ppr final_ty])
281 ; return final_ty}
282
283 tcTopLHsType (XHsImplicitBndrs _) _ = panic "tcTopLHsType"
284
285 -----------------
286 tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], (Class, [Type], [Kind]))
287 -- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
288 -- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
289 -- E.g. class C (a::*) (b::k->k)
290 -- data T a b = ... deriving( C Int )
291 -- returns ([k], C, [k, Int], [k->k])
292 -- Return values are fully zonked
293 tcHsDeriv hs_ty
294 = do { ty <- checkNoErrs $ -- Avoid redundant error report
295 -- with "illegal deriving", below
296 tcTopLHsType hs_ty AnyKind
297 ; let (tvs, pred) = splitForAllTys ty
298 (kind_args, _) = splitFunTys (typeKind pred)
299 ; case getClassPredTys_maybe pred of
300 Just (cls, tys) -> return (tvs, (cls, tys, kind_args))
301 Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
302
303 -- | Typecheck something within the context of a deriving strategy.
304 -- This is of particular importance when the deriving strategy is @via@.
305 -- For instance:
306 --
307 -- @
308 -- deriving via (S a) instance C (T a)
309 -- @
310 --
311 -- We need to typecheck @S a@, and moreover, we need to extend the tyvar
312 -- environment with @a@ before typechecking @C (T a)@, since @S a@ quantified
313 -- the type variable @a@.
314 tcDerivStrategy
315 :: forall a.
316 Maybe (DerivStrategy GhcRn) -- ^ The deriving strategy
317 -> TcM ([TyVar], a) -- ^ The thing to typecheck within the context of the
318 -- deriving strategy, which might quantify some type
319 -- variables of its own.
320 -> TcM (Maybe (DerivStrategy GhcTc), [TyVar], a)
321 -- ^ The typechecked deriving strategy, all quantified tyvars, and
322 -- the payload of the typechecked thing.
323 tcDerivStrategy mds thing_inside
324 = case mds of
325 Nothing -> boring_case Nothing
326 Just ds -> do (ds', tvs, thing) <- tc_deriv_strategy ds
327 pure (Just ds', tvs, thing)
328 where
329 tc_deriv_strategy :: DerivStrategy GhcRn
330 -> TcM (DerivStrategy GhcTc, [TyVar], a)
331 tc_deriv_strategy StockStrategy = boring_case StockStrategy
332 tc_deriv_strategy AnyclassStrategy = boring_case AnyclassStrategy
333 tc_deriv_strategy NewtypeStrategy = boring_case NewtypeStrategy
334 tc_deriv_strategy (ViaStrategy ty) = do
335 ty' <- checkNoErrs $
336 tcTopLHsType ty AnyKind
337 let (via_tvs, via_pred) = splitForAllTys ty'
338 tcExtendTyVarEnv via_tvs $ do
339 (thing_tvs, thing) <- thing_inside
340 pure (ViaStrategy via_pred, via_tvs ++ thing_tvs, thing)
341
342 boring_case :: mds -> TcM (mds, [TyVar], a)
343 boring_case mds = do
344 (thing_tvs, thing) <- thing_inside
345 pure (mds, thing_tvs, thing)
346
347 tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt
348 -> LHsSigType GhcRn
349 -> TcM Type
350 -- Like tcHsSigType, but for a class instance declaration
351 tcHsClsInstType user_ctxt hs_inst_ty
352 = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
353 do { -- Fail eagerly if tcTopLHsType fails. We are at top level so
354 -- these constraints will never be solved later. And failing
355 -- eagerly avoids follow-on errors when checkValidInstance
356 -- sees an unsolved coercion hole
357 inst_ty <- checkNoErrs $
358 tcTopLHsType hs_inst_ty (TheKind constraintKind)
359 ; checkValidInstance user_ctxt hs_inst_ty inst_ty
360 ; return inst_ty }
361
362 ----------------------------------------------
363 -- | Type-check a visible type application
364 tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
365 -- See Note [Recipe for checking a signature] in TcHsType
366 tcHsTypeApp wc_ty kind
367 | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
368 = do { ty <- solveLocalEqualities "tcHsTypeApp" $
369 -- We are looking at a user-written type, very like a
370 -- signature so we want to solve its equalities right now
371 unsetWOptM Opt_WarnPartialTypeSignatures $
372 setXOptM LangExt.PartialTypeSignatures $
373 -- See Note [Wildcards in visible type application]
374 tcWildCardBinders sig_wcs $ \ _ ->
375 tcCheckLHsType hs_ty kind
376 -- We must promote here. Ex:
377 -- f :: forall a. a
378 -- g = f @(forall b. Proxy b -> ()) @Int ...
379 -- After when processing the @Int, we'll have to check its kind
380 -- against the as-yet-unknown kind of b. This check causes an assertion
381 -- failure if we don't promote.
382 ; ty <- zonkPromoteType ty
383 ; checkValidType TypeAppCtxt ty
384 ; return ty }
385 tcHsTypeApp (XHsWildCardBndrs _) _ = panic "tcHsTypeApp"
386
387 {- Note [Wildcards in visible type application]
388 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
389
390 A HsWildCardBndrs's hswc_ext now only includes named wildcards, so any unnamed
391 wildcards stay unchanged in hswc_body and when called in tcHsTypeApp, tcCheckLHsType
392 will call emitWildCardHoleConstraints on them. However, this would trigger
393 error/warning when an unnamed wildcard is passed in as a visible type argument,
394 which we do not want because users should be able to write @_ to skip a instantiating
395 a type variable variable without fuss. The solution is to switch the
396 PartialTypeSignatures flags here to let the typechecker know that it's checking
397 a '@_' and do not emit hole constraints on it.
398 See related Note [Wildcards in visible kind application]
399 and Note [The wildcard story for types] in HsTypes.hs
400
401 -}
402
403 {-
404 ************************************************************************
405 * *
406 The main kind checker: no validity checks here
407 * *
408 ************************************************************************
409
410 First a couple of simple wrappers for kcHsType
411 -}
412
413 ---------------------------
414 tcHsOpenType, tcHsLiftedType,
415 tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
416 -- Used for type signatures
417 -- Do not do validity checking
418 tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty
419 tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty
420
421 tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind
422 ; tc_lhs_type typeLevelMode ty ek }
423 tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
424
425 -- Like tcHsType, but takes an expected kind
426 tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
427 tcCheckLHsType hs_ty exp_kind
428 = addTypeCtxt hs_ty $
429 tc_lhs_type typeLevelMode hs_ty exp_kind
430
431 tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
432 -- Called from outside: set the context
433 tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
434
435 -- Like tcLHsType, but use it in a context where type synonyms and type families
436 -- do not need to be saturated, like in a GHCi :kind call
437 tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
438 tcLHsTypeUnsaturated ty = addTypeCtxt ty (tc_infer_lhs_type mode ty)
439 where
440 mode = allowUnsaturated typeLevelMode
441
442 {-
443 ************************************************************************
444 * *
445 Type-checking modes
446 * *
447 ************************************************************************
448
449 The kind-checker is parameterised by a TcTyMode, which contains some
450 information about where we're checking a type.
451
452 The renamer issues errors about what it can. All errors issued here must
453 concern things that the renamer can't handle.
454
455 -}
456
457 -- | Do we require type families to be saturated?
458 data RequireSaturation
459 = YesSaturation
460 | NoSaturation -- e.g. during a call to GHCi's :kind
461
462 -- | Info about the context in which we're checking a type. Currently,
463 -- differentiates only between types and kinds, but this will likely
464 -- grow, at least to include the distinction between patterns and
465 -- not-patterns.
466 data TcTyMode
467 = TcTyMode { mode_level :: TypeOrKind
468 , mode_sat :: RequireSaturation
469 }
470 -- The mode_unsat field is solely so that type families/synonyms can be unsaturated
471 -- in GHCi :kind calls
472
473 typeLevelMode :: TcTyMode
474 typeLevelMode = TcTyMode { mode_level = TypeLevel, mode_sat = YesSaturation }
475
476 kindLevelMode :: TcTyMode
477 kindLevelMode = TcTyMode { mode_level = KindLevel, mode_sat = YesSaturation }
478
479 allowUnsaturated :: TcTyMode -> TcTyMode
480 allowUnsaturated mode = mode { mode_sat = NoSaturation }
481
482 -- switch to kind level
483 kindLevel :: TcTyMode -> TcTyMode
484 kindLevel mode = mode { mode_level = KindLevel }
485
486 instance Outputable RequireSaturation where
487 ppr YesSaturation = text "YesSaturation"
488 ppr NoSaturation = text "NoSaturation"
489
490 instance Outputable TcTyMode where
491 ppr = ppr . mode_level
492
493 {-
494 Note [Bidirectional type checking]
495 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
496 In expressions, whenever we see a polymorphic identifier, say `id`, we are
497 free to instantiate it with metavariables, knowing that we can always
498 re-generalize with type-lambdas when necessary. For example:
499
500 rank2 :: (forall a. a -> a) -> ()
501 x = rank2 id
502
503 When checking the body of `x`, we can instantiate `id` with a metavariable.
504 Then, when we're checking the application of `rank2`, we notice that we really
505 need a polymorphic `id`, and then re-generalize over the unconstrained
506 metavariable.
507
508 In types, however, we're not so lucky, because *we cannot re-generalize*!
509 There is no lambda. So, we must be careful only to instantiate at the last
510 possible moment, when we're sure we're never going to want the lost polymorphism
511 again. This is done in calls to tcInstTyBinders.
512
513 To implement this behavior, we use bidirectional type checking, where we
514 explicitly think about whether we know the kind of the type we're checking
515 or not. Note that there is a difference between not knowing a kind and
516 knowing a metavariable kind: the metavariables are TauTvs, and cannot become
517 forall-quantified kinds. Previously (before dependent types), there were
518 no higher-rank kinds, and so we could instantiate early and be sure that
519 no types would have polymorphic kinds, and so we could always assume that
520 the kind of a type was a fresh metavariable. Not so anymore, thus the
521 need for two algorithms.
522
523 For HsType forms that can never be kind-polymorphic, we implement only the
524 "down" direction, where we safely assume a metavariable kind. For HsType forms
525 that *can* be kind-polymorphic, we implement just the "up" (functions with
526 "infer" in their name) version, as we gain nothing by also implementing the
527 "down" version.
528
529 Note [Future-proofing the type checker]
530 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
531 As discussed in Note [Bidirectional type checking], each HsType form is
532 handled in *either* tc_infer_hs_type *or* tc_hs_type. These functions
533 are mutually recursive, so that either one can work for any type former.
534 But, we want to make sure that our pattern-matches are complete. So,
535 we have a bunch of repetitive code just so that we get warnings if we're
536 missing any patterns.
537
538 Note [The tcType invariant]
539 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
540 (IT1) If tc_ty = tc_hs_type hs_ty exp_kind
541 then tcTypeKind tc_ty = exp_kind
542 without any zonking needed. The reason for this is that in
543 tcInferApps we see (F ty), and we kind-check 'ty' with an
544 expected-kind coming from F. Then, to make the resulting application
545 well kinded --- see Note [The well-kinded type invariant] in TcType ---
546 we need the kind-checked 'ty' to have exactly the kind that F expects,
547 with no funny zonking nonsense in between.
548
549 The tcType invariant also applies to checkExpectedKind:
550
551 (IT2) if
552 (tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
553 then
554 tcTypeKind tc_ty = exp_ki
555
556 These other invariants are all necessary, too, as these functions
557 are used within tc_hs_type:
558
559 (IT3) If (ty, ki) <- tc_infer_hs_type ..., then tcTypeKind ty == ki.
560
561 (IT4) If (ty, ki) <- tc_infer_hs_type ..., then zonk ki == ki.
562 (In other words, the result kind of tc_infer_hs_type is zonked.)
563
564 (IT5) If (ty, ki) <- tcTyVar ..., then tcTypeKind ty == ki.
565
566 (IT6) If (ty, ki) <- tcTyVar ..., then zonk ki == ki.
567 (In other words, the result kind of tcTyVar is zonked.)
568
569 -}
570
571 ------------------------------------------
572 -- | Check and desugar a type, returning the core type and its
573 -- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
574 -- level.
575 tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
576 tc_infer_lhs_type mode (L span ty)
577 = setSrcSpan span $
578 do { (ty', kind) <- tc_infer_hs_type mode ty
579 ; return (ty', kind) }
580
581 -- | Infer the kind of a type and desugar. This is the "up" type-checker,
582 -- as described in Note [Bidirectional type checking]
583 tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
584 tc_infer_hs_type mode (HsParTy _ t) = tc_infer_lhs_type mode t
585 tc_infer_hs_type mode (HsTyVar _ _ (L _ tv)) = tcTyVar mode tv
586
587 tc_infer_hs_type mode e@(HsAppTy {}) = tcTyApp mode e
588 tc_infer_hs_type mode e@(HsAppKindTy {}) = tcTyApp mode e
589
590 tc_infer_hs_type mode (HsOpTy _ lhs lhs_op@(L _ hs_op) rhs)
591 | not (hs_op `hasKey` funTyConKey)
592 = do { (op, op_kind) <- tcTyVar mode hs_op
593 ; tcTyApps mode (noLoc $ HsTyVar noExt NotPromoted lhs_op) op op_kind
594 [HsValArg lhs, HsValArg rhs] }
595
596 tc_infer_hs_type mode (HsKindSig _ ty sig)
597 = do { sig' <- tcLHsKindSig KindSigCtxt sig
598 -- We must typecheck the kind signature, and solve all
599 -- its equalities etc; from this point on we may do
600 -- things like instantiate its foralls, so it needs
601 -- to be fully determined (Trac #14904)
602 ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
603 ; ty' <- tc_lhs_type mode ty sig'
604 ; return (ty', sig') }
605
606 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
607 -- the splice location to the typechecker. Here we skip over it in order to have
608 -- the same kind inferred for a given expression whether it was produced from
609 -- splices or not.
610 --
611 -- See Note [Delaying modFinalizers in untyped splices].
612 tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
613 = tc_infer_hs_type mode ty
614
615 tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
616 tc_infer_hs_type _ (XHsType (NHsCoreTy ty))
617 = do { ty <- zonkTcType ty -- (IT3) and (IT4) of Note [The tcType invariant]
618 ; return (ty, tcTypeKind ty) }
619
620 tc_infer_hs_type _ (HsExplicitListTy _ _ tys)
621 | null tys -- this is so that we can use visible kind application with '[]
622 -- e.g ... '[] @Bool
623 = return (mkTyConTy promotedNilDataCon,
624 mkSpecForAllTys [alphaTyVar] $ mkListTy alphaTy)
625
626 tc_infer_hs_type mode other_ty
627 = do { kv <- newMetaKindVar
628 ; ty' <- tc_hs_type mode other_ty kv
629 ; return (ty', kv) }
630
631 ------------------------------------------
632 tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
633 tc_lhs_type mode (L span ty) exp_kind
634 = setSrcSpan span $
635 tc_hs_type mode ty exp_kind
636
637 ------------------------------------------
638 tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
639 -> TcM TcType
640 tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
641 TypeLevel ->
642 do { arg_k <- newOpenTypeKind
643 ; res_k <- newOpenTypeKind
644 ; ty1' <- tc_lhs_type mode ty1 arg_k
645 ; ty2' <- tc_lhs_type mode ty2 res_k
646 ; checkExpectedKindMode mode (ppr $ HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
647 liftedTypeKind exp_kind }
648 KindLevel -> -- no representation polymorphism in kinds. yet.
649 do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
650 ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
651 ; checkExpectedKindMode mode (ppr $ HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
652 liftedTypeKind exp_kind }
653
654 ------------------------------------------
655 tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
656 -- See Note [The tcType invariant]
657 -- See Note [Bidirectional type checking]
658
659 tc_hs_type mode (HsParTy _ ty) exp_kind = tc_lhs_type mode ty exp_kind
660 tc_hs_type mode (HsDocTy _ ty _) exp_kind = tc_lhs_type mode ty exp_kind
661 tc_hs_type _ ty@(HsBangTy _ bang _) _
662 -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
663 -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
664 -- bangs are invalid, so fail. (#7210, #14761)
665 = do { let bangError err = failWith $
666 text "Unexpected" <+> text err <+> text "annotation:" <+> ppr ty $$
667 text err <+> text "annotation cannot appear nested inside a type"
668 ; case bang of
669 HsSrcBang _ SrcUnpack _ -> bangError "UNPACK"
670 HsSrcBang _ SrcNoUnpack _ -> bangError "NOUNPACK"
671 HsSrcBang _ NoSrcUnpack SrcLazy -> bangError "laziness"
672 HsSrcBang _ _ _ -> bangError "strictness" }
673 tc_hs_type _ ty@(HsRecTy {}) _
674 -- Record types (which only show up temporarily in constructor
675 -- signatures) should have been removed by now
676 = failWithTc (text "Record syntax is illegal here:" <+> ppr ty)
677
678 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType'.
679 -- Here we get rid of it and add the finalizers to the global environment
680 -- while capturing the local environment.
681 --
682 -- See Note [Delaying modFinalizers in untyped splices].
683 tc_hs_type mode (HsSpliceTy _ (HsSpliced _ mod_finalizers (HsSplicedTy ty)))
684 exp_kind
685 = do addModFinalizersWithLclEnv mod_finalizers
686 tc_hs_type mode ty exp_kind
687
688 -- This should never happen; type splices are expanded by the renamer
689 tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind
690 = failWithTc (text "Unexpected type splice:" <+> ppr ty)
691
692 ---------- Functions and applications
693 tc_hs_type mode (HsFunTy _ ty1 ty2) exp_kind
694 = tc_fun_type mode ty1 ty2 exp_kind
695
696 tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
697 | op `hasKey` funTyConKey
698 = tc_fun_type mode ty1 ty2 exp_kind
699
700 --------- Foralls
701 tc_hs_type mode forall@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
702 = do { (tclvl, wanted, (tvs', ty'))
703 <- pushLevelAndCaptureConstraints $
704 bindExplicitTKBndrs_Skol hs_tvs $
705 tc_lhs_type mode ty exp_kind
706 -- Do not kind-generalise here! See Note [Kind generalisation]
707 -- Why exp_kind? See Note [Body kind of HsForAllTy]
708 ; let bndrs = mkTyVarBinders Specified tvs'
709 skol_info = ForAllSkol (ppr forall)
710 m_telescope = Just (sep (map ppr hs_tvs))
711
712 ; emitResidualTvConstraint skol_info m_telescope tvs' tclvl wanted
713
714 ; return (mkForAllTys bndrs ty') }
715
716 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
717 | null (unLoc ctxt)
718 = tc_lhs_type mode ty exp_kind
719
720 | otherwise
721 = do { ctxt' <- tc_hs_context mode ctxt
722
723 -- See Note [Body kind of a HsQualTy]
724 ; ty' <- if tcIsConstraintKind exp_kind
725 then tc_lhs_type mode ty constraintKind
726 else do { ek <- newOpenTypeKind
727 -- The body kind (result of the function)
728 -- can be TYPE r, for any r, hence newOpenTypeKind
729 ; ty' <- tc_lhs_type mode ty ek
730 ; checkExpectedKindMode mode (ppr ty) ty' liftedTypeKind exp_kind }
731
732 ; return (mkPhiTy ctxt' ty') }
733
734 --------- Lists, arrays, and tuples
735 tc_hs_type mode rn_ty@(HsListTy _ elt_ty) exp_kind
736 = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
737 ; checkWiredInTyCon listTyCon
738 ; checkExpectedKindMode mode (ppr rn_ty) (mkListTy tau_ty) liftedTypeKind exp_kind }
739
740 -- See Note [Distinguishing tuple kinds] in HsTypes
741 -- See Note [Inferring tuple kinds]
742 tc_hs_type mode rn_ty@(HsTupleTy _ HsBoxedOrConstraintTuple hs_tys) exp_kind
743 -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
744 | Just tup_sort <- tupKindSort_maybe exp_kind
745 = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
746 tc_tuple rn_ty mode tup_sort hs_tys exp_kind
747 | otherwise
748 = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
749 ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
750 ; kinds <- mapM zonkTcType kinds
751 -- Infer each arg type separately, because errors can be
752 -- confusing if we give them a shared kind. Eg Trac #7410
753 -- (Either Int, Int), we do not want to get an error saying
754 -- "the second argument of a tuple should have kind *->*"
755
756 ; let (arg_kind, tup_sort)
757 = case [ (k,s) | k <- kinds
758 , Just s <- [tupKindSort_maybe k] ] of
759 ((k,s) : _) -> (k,s)
760 [] -> (liftedTypeKind, BoxedTuple)
761 -- In the [] case, it's not clear what the kind is, so guess *
762
763 ; tys' <- sequence [ setSrcSpan loc $
764 checkExpectedKindMode mode (ppr hs_ty) ty kind arg_kind
765 | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
766
767 ; finish_tuple rn_ty mode tup_sort tys' (map (const arg_kind) tys') exp_kind }
768
769
770 tc_hs_type mode rn_ty@(HsTupleTy _ hs_tup_sort tys) exp_kind
771 = tc_tuple rn_ty mode tup_sort tys exp_kind
772 where
773 tup_sort = case hs_tup_sort of -- Fourth case dealt with above
774 HsUnboxedTuple -> UnboxedTuple
775 HsBoxedTuple -> BoxedTuple
776 HsConstraintTuple -> ConstraintTuple
777 _ -> panic "tc_hs_type HsTupleTy"
778
779 tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
780 = do { let arity = length hs_tys
781 ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
782 ; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
783 ; let arg_reps = map kindRep arg_kinds
784 arg_tys = arg_reps ++ tau_tys
785 ; checkExpectedKindMode mode (ppr rn_ty)
786 (mkTyConApp (sumTyCon arity) arg_tys)
787 (unboxedSumKind arg_reps)
788 exp_kind
789 }
790
791 --------- Promoted lists and tuples
792 tc_hs_type mode rn_ty@(HsExplicitListTy _ _ tys) exp_kind
793 = do { tks <- mapM (tc_infer_lhs_type mode) tys
794 ; (taus', kind) <- unifyKinds tys tks
795 ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
796 ; checkExpectedKindMode mode (ppr rn_ty) ty (mkListTy kind) exp_kind }
797 where
798 mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
799 mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k]
800
801 tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
802 -- using newMetaKindVar means that we force instantiations of any polykinded
803 -- types. At first, I just used tc_infer_lhs_type, but that led to #11255.
804 = do { ks <- replicateM arity newMetaKindVar
805 ; taus <- zipWithM (tc_lhs_type mode) tys ks
806 ; let kind_con = tupleTyCon Boxed arity
807 ty_con = promotedTupleDataCon Boxed arity
808 tup_k = mkTyConApp kind_con ks
809 ; checkExpectedKindMode mode (ppr rn_ty) (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
810 where
811 arity = length tys
812
813 --------- Constraint types
814 tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
815 = do { MASSERT( isTypeLevel (mode_level mode) )
816 ; ty' <- tc_lhs_type mode ty liftedTypeKind
817 ; let n' = mkStrLitTy $ hsIPNameFS n
818 ; ipClass <- tcLookupClass ipClassName
819 ; checkExpectedKindMode mode (ppr rn_ty) (mkClassPred ipClass [n',ty'])
820 constraintKind exp_kind }
821
822 tc_hs_type mode rn_ty@(HsStarTy _ _) exp_kind
823 -- Desugaring 'HsStarTy' to 'Data.Kind.Type' here means that we don't have to
824 -- handle it in 'coreView' and 'tcView'.
825 = checkExpectedKindMode mode (ppr rn_ty) liftedTypeKind liftedTypeKind exp_kind
826
827 --------- Literals
828 tc_hs_type mode rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
829 = do { checkWiredInTyCon typeNatKindCon
830 ; checkExpectedKindMode mode (ppr rn_ty) (mkNumLitTy n) typeNatKind exp_kind }
831
832 tc_hs_type mode rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
833 = do { checkWiredInTyCon typeSymbolKindCon
834 ; checkExpectedKindMode mode (ppr rn_ty) (mkStrLitTy s) typeSymbolKind exp_kind }
835
836 --------- Potentially kind-polymorphic types: call the "up" checker
837 -- See Note [Future-proofing the type checker]
838 tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
839 tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek
840 tc_hs_type mode ty@(HsAppKindTy{}) ek = tc_infer_hs_type_ek mode ty ek
841 tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
842 tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
843 tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
844
845 tc_hs_type mode wc@(HsWildCardTy _) exp_kind
846 = do { wc_ty <- tcWildCardOcc mode wc exp_kind
847 ; return (mkNakedCastTy wc_ty (mkTcNomReflCo exp_kind))
848 -- Take care here! Even though the coercion is Refl,
849 -- we still need it to establish Note [The tcType invariant]
850 }
851
852 tcWildCardOcc :: TcTyMode -> HsType GhcRn -> Kind -> TcM TcType
853 tcWildCardOcc mode wc exp_kind
854 = do { wc_tv <- newWildTyVar
855 -- The wildcard's kind should be an un-filled-in meta tyvar
856 ; loc <- getSrcSpanM
857 ; uniq <- newUnique
858 ; let name = mkInternalName uniq (mkTyVarOcc "_") loc
859 ; part_tysig <- xoptM LangExt.PartialTypeSignatures
860 ; warning <- woptM Opt_WarnPartialTypeSignatures
861 -- See Note [Wildcards in visible kind application]
862 ; unless (part_tysig && not warning)
863 (emitWildCardHoleConstraints [(name,wc_tv)])
864 ; checkExpectedKindMode mode (ppr wc) (mkTyVarTy wc_tv)
865 (tyVarKind wc_tv) exp_kind }
866
867 {- Note [Wildcards in visible kind application]
868 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
869 There are cases where users might want to pass in a wildcard as a visible kind
870 argument, for instance:
871
872 data T :: forall k1 k2. k1 → k2 → Type where
873 MkT :: T a b
874 x :: T @_ @Nat False n
875 x = MkT
876
877 So we should allow '@_' without emitting any hole constraints, and
878 regardless of whether PartialTypeSignatures is enabled or not. But how would
879 the typechecker know which '_' is being used in VKA and which is not when it
880 calls emitWildCardHoleConstraints in tcHsPartialSigType on all HsWildCardBndrs?
881 The solution then is to neither rename nor include unnamed wildcards in HsWildCardBndrs,
882 but instead give every unnamed wildcard a fresh wild tyvar in tcWildCardOcc.
883 And whenever we see a '@', we automatically turn on PartialTypeSignatures and
884 turn off hole constraint warnings, and never call emitWildCardHoleConstraints
885 under these conditions.
886 See related Note [Wildcards in visible type application] here and
887 Note [The wildcard story for types] in HsTypes.hs
888
889 -}
890 ---------------------------
891 -- | Call 'tc_infer_hs_type' and check its result against an expected kind.
892 tc_infer_hs_type_ek :: HasDebugCallStack => TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
893 tc_infer_hs_type_ek mode hs_ty ek
894 = do { (ty, k) <- tc_infer_hs_type mode hs_ty
895 ; checkExpectedKindMode mode (ppr hs_ty) ty k ek }
896
897 ---------------------------
898 tupKindSort_maybe :: TcKind -> Maybe TupleSort
899 tupKindSort_maybe k
900 | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
901 | Just k' <- tcView k = tupKindSort_maybe k'
902 | tcIsConstraintKind k = Just ConstraintTuple
903 | tcIsLiftedTypeKind k = Just BoxedTuple
904 | otherwise = Nothing
905
906 tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
907 tc_tuple rn_ty mode tup_sort tys exp_kind
908 = do { arg_kinds <- case tup_sort of
909 BoxedTuple -> return (nOfThem arity liftedTypeKind)
910 UnboxedTuple -> mapM (\_ -> newOpenTypeKind) tys
911 ConstraintTuple -> return (nOfThem arity constraintKind)
912 ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
913 ; finish_tuple rn_ty mode tup_sort tau_tys arg_kinds exp_kind }
914 where
915 arity = length tys
916
917 finish_tuple :: HsType GhcRn
918 -> TcTyMode
919 -> TupleSort
920 -> [TcType] -- ^ argument types
921 -> [TcKind] -- ^ of these kinds
922 -> TcKind -- ^ expected kind of the whole tuple
923 -> TcM TcType
924 finish_tuple rn_ty mode tup_sort tau_tys tau_kinds exp_kind
925 = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
926 ; let arg_tys = case tup_sort of
927 -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
928 UnboxedTuple -> tau_reps ++ tau_tys
929 BoxedTuple -> tau_tys
930 ConstraintTuple -> tau_tys
931 ; tycon <- case tup_sort of
932 ConstraintTuple
933 | arity > mAX_CTUPLE_SIZE
934 -> failWith (bigConstraintTuple arity)
935 | otherwise -> tcLookupTyCon (cTupleTyConName arity)
936 BoxedTuple -> do { let tc = tupleTyCon Boxed arity
937 ; checkWiredInTyCon tc
938 ; return tc }
939 UnboxedTuple -> return (tupleTyCon Unboxed arity)
940 ; checkExpectedKindMode mode (ppr rn_ty) (mkTyConApp tycon arg_tys) res_kind exp_kind }
941 where
942 arity = length tau_tys
943 tau_reps = map kindRep tau_kinds
944 res_kind = case tup_sort of
945 UnboxedTuple -> unboxedTupleKind tau_reps
946 BoxedTuple -> liftedTypeKind
947 ConstraintTuple -> constraintKind
948
949 bigConstraintTuple :: Arity -> MsgDoc
950 bigConstraintTuple arity
951 = hang (text "Constraint tuple arity too large:" <+> int arity
952 <+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
953 2 (text "Instead, use a nested tuple")
954
955 ---------------------------
956 -- | Apply a type of a given kind to a list of arguments. This instantiates
957 -- invisible parameters as necessary. Always consumes all the arguments,
958 -- using matchExpectedFunKind as necessary.
959 -- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.-
960 -- These kinds should be used to instantiate invisible kind variables;
961 -- they come from an enclosing class for an associated type/data family.
962 tcInferApps :: TcTyMode
963 -> LHsType GhcRn -- ^ Function (for printing only)
964 -> TcType -- ^ Function
965 -> TcKind -- ^ Function kind (zonked)
966 -> [LHsTypeArg GhcRn] -- ^ Args
967 -> TcM (TcType, TcKind) -- ^ (f args, args, result kind)
968 -- Precondition: tcTypeKind fun_ty = fun_ki
969 -- Reason: we will return a type application like (fun_ty arg1 ... argn),
970 -- and that type must be well-kinded
971 -- See Note [The tcType invariant]
972 -- Postcondition: Result kind is zonked.
973 tcInferApps mode orig_hs_ty fun_ty fun_ki orig_hs_args
974 = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki)
975 ; (f_args, res_k) <- go 1 empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
976 ; traceTc "tcInferApps }" empty
977 ; res_k <- zonkTcType res_k -- Uphold (IT4) of Note [The tcType invariant]
978 ; return (f_args, res_k) }
979 where
980 empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
981 tyCoVarsOfType fun_ki
982 (orig_ki_binders, orig_inner_ki) = tcSplitPiTys fun_ki
983
984 go :: Int -- the # of the next argument
985 -> TCvSubst -- instantiating substitution
986 -> TcType -- function applied to some args
987 -> [TyBinder] -- binders in function kind (both vis. and invis.)
988 -> TcKind -- function kind body (not a Pi-type)
989 -> [LHsTypeArg GhcRn] -- un-type-checked args
990 -> TcM (TcType, TcKind) -- same as overall return type
991
992 -- no user-written args left. We're done!
993 go _ subst fun ki_binders inner_ki []
994 = return ( fun
995 , nakedSubstTy subst $ mkPiTys ki_binders inner_ki)
996 -- nakedSubstTy: see Note [The well-kinded type invariant]
997 go n subst fun all_kindbinder inner_ki (HsArgPar _:args)
998 = go n subst fun all_kindbinder inner_ki args
999 -- The function's kind has a binder. Is it visible or invisible?
1000 go n subst fun all_kindbinder@(ki_binder:ki_binders) inner_ki
1001 all_args@(arg:args)
1002 | Specified <- tyCoBinderArgFlag ki_binder
1003 , HsTypeArg _ ki <- arg
1004 -- Invisible and specified binder with visible kind argument
1005 = do { traceTc "tcInferApps (vis kind app)" (vcat [ ppr ki_binder, ppr ki
1006 , ppr (tyBinderType ki_binder)
1007 , ppr subst, ppr (tyCoBinderArgFlag ki_binder) ])
1008 ; let exp_kind = nakedSubstTy subst $ tyBinderType ki_binder
1009 -- nakedSubstTy: see Note [The well-kinded type invariant]
1010 ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty ki n) $
1011 unsetWOptM Opt_WarnPartialTypeSignatures $
1012 setXOptM LangExt.PartialTypeSignatures $
1013 -- see Note [Wildcards in visible kind application]
1014 tc_lhs_type (kindLevel mode) ki exp_kind
1015 ; traceTc "tcInferApps (vis kind app)" (ppr exp_kind)
1016 ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
1017 ; go (n+1) subst'
1018 (mkNakedAppTy fun arg')
1019 ki_binders inner_ki args }
1020
1021 | isInvisibleBinder ki_binder
1022 -- Instantiate if not specified or if there is no kind application
1023 = do { traceTc "tcInferApps (invis normal app)" (ppr ki_binder $$ ppr subst $$ ppr (tyCoBinderArgFlag ki_binder))
1024 ; (subst', arg') <- tcInstTyBinder Nothing subst ki_binder
1025 ; go n subst' (mkNakedAppTy fun arg')
1026 ki_binders inner_ki all_args }
1027
1028 | otherwise -- if binder is visible
1029 = case arg of
1030 HsValArg ty -- check the next argument
1031 -> do { traceTc "tcInferApps (vis normal app)"
1032 (vcat [ ppr ki_binder
1033 , ppr ty
1034 , ppr (tyBinderType ki_binder)
1035 , ppr subst ])
1036 ; let exp_kind = nakedSubstTy subst $ tyBinderType ki_binder
1037 -- nakedSubstTy: see Note [The well-kinded type invariant]
1038 ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty ty n) $
1039 tc_lhs_type mode ty exp_kind
1040 ; traceTc "tcInferApps (vis normal app)" (ppr exp_kind)
1041 ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
1042 ; go (n+1) subst'
1043 (mkNakedAppTy fun arg')
1044 ki_binders inner_ki args }
1045 -- error if the argument is a kind application
1046 HsTypeArg _ ki -> do { traceTc "tcInferApps (error)"
1047 (vcat [ ppr ki_binder
1048 , ppr ki
1049 , ppr (tyBinderType ki_binder)
1050 , ppr subst
1051 , ppr (isInvisibleBinder ki_binder) ])
1052 ; ty_app_err ki $ nakedSubstTy subst $
1053 mkPiTys all_kindbinder inner_ki }
1054
1055 HsArgPar _ -> panic "tcInferApps" -- handled in separate clause of "go"
1056
1057 -- We've run out of known binders in the functions's kind.
1058 go n subst fun [] inner_ki all_args@(arg:args)
1059 | not (null new_ki_binders)
1060 -- But, after substituting, we have more binders.
1061 = go n zapped_subst fun new_ki_binders new_inner_ki all_args
1062
1063 | otherwise
1064 = case arg of
1065 (HsValArg _)
1066 -- Even after substituting, still no binders. Use matchExpectedFunKind
1067 -> do { traceTc "tcInferApps (no binder)" (ppr new_inner_ki $$ ppr zapped_subst)
1068 ; (co, arg_k, res_k) <- matchExpectedFunKind hs_ty substed_inner_ki
1069 ; let new_in_scope = tyCoVarsOfTypes [arg_k, res_k]
1070 subst' = zapped_subst `extendTCvInScopeSet` new_in_scope
1071 ; go n subst'
1072 (fun `mkNakedCastTy` co) -- See Note [The well-kinded type invariant]
1073 [mkAnonBinder arg_k]
1074 res_k all_args }
1075 (HsTypeArg _ ki) -> ty_app_err ki substed_inner_ki
1076 (HsArgPar _) -> go n subst fun [] inner_ki args
1077 where
1078 substed_inner_ki = substTy subst inner_ki
1079 (new_ki_binders, new_inner_ki) = tcSplitPiTys substed_inner_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) ]