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