ci: push perf test metrics even when the testsuite doesn't pass
[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 TypeApplications #-}
11 {-# LANGUAGE TypeFamilies #-}
12 {-# LANGUAGE ViewPatterns #-}
13
14 module TcHsType (
15 -- Type signatures
16 kcClassSigType, tcClassSigType,
17 tcHsSigType, tcHsSigWcType,
18 tcHsPartialSigType,
19 tcStandaloneKindSig,
20 funsSigCtxt, addSigCtxt, pprSigCtxt,
21
22 tcHsClsInstType,
23 tcHsDeriv, tcDerivStrategy,
24 tcHsTypeApp,
25 UserTypeCtxt(..),
26 bindImplicitTKBndrs_Tv, bindImplicitTKBndrs_Skol,
27 bindImplicitTKBndrs_Q_Tv, bindImplicitTKBndrs_Q_Skol,
28 bindExplicitTKBndrs_Tv, bindExplicitTKBndrs_Skol,
29 bindExplicitTKBndrs_Q_Tv, bindExplicitTKBndrs_Q_Skol,
30 ContextKind(..),
31
32 -- Type checking type and class decls
33 kcLookupTcTyCon, bindTyClTyVars,
34 etaExpandAlgTyCon, tcbVisibilities,
35
36 -- tyvars
37 zonkAndScopedSort,
38
39 -- Kind-checking types
40 -- No kind generalisation, no checkValidType
41 InitialKindStrategy(..),
42 SAKS_or_CUSK(..),
43 kcDeclHeader,
44 tcNamedWildCardBinders,
45 tcHsLiftedType, tcHsOpenType,
46 tcHsLiftedTypeNC, tcHsOpenTypeNC,
47 tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
48 tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps,
49 failIfEmitsConstraints,
50 solveEqualities, -- useful re-export
51
52 typeLevelMode, kindLevelMode,
53
54 kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone,
55 checkExpectedKind_pp,
56
57 -- Sort-checking kinds
58 tcLHsKindSig, checkDataKindSig, DataSort(..),
59 checkClassKindSig,
60
61 -- Pattern type signatures
62 tcHsPatSigType, tcPatSig,
63
64 -- Error messages
65 funAppCtxt, addTyConFlavCtxt
66 ) where
67
68 #include "HsVersions.h"
69
70 import GhcPrelude
71
72 import GHC.Hs
73 import TcRnMonad
74 import TcOrigin
75 import Predicate
76 import Constraint
77 import TcEvidence
78 import TcEnv
79 import TcMType
80 import TcValidity
81 import TcUnify
82 import TcIface
83 import TcSimplify
84 import TcHsSyn
85 import TyCoRep
86 import TcErrors ( reportAllUnsolved )
87 import TcType
88 import Inst ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
89 import Type
90 import TysPrim
91 import RdrName( lookupLocalRdrOcc )
92 import Var
93 import VarSet
94 import TyCon
95 import ConLike
96 import DataCon
97 import Class
98 import Name
99 -- import NameSet
100 import VarEnv
101 import TysWiredIn
102 import BasicTypes
103 import SrcLoc
104 import Constants ( mAX_CTUPLE_SIZE )
105 import ErrUtils( MsgDoc )
106 import Unique
107 import UniqSet
108 import Util
109 import UniqSupply
110 import Outputable
111 import FastString
112 import PrelNames hiding ( wildCardName )
113 import DynFlags
114 import qualified GHC.LanguageExtensions as LangExt
115
116 import Maybes
117 import Data.List ( find )
118 import Control.Monad
119
120 {-
121 ----------------------------
122 General notes
123 ----------------------------
124
125 Unlike with expressions, type-checking types both does some checking and
126 desugars at the same time. This is necessary because we often want to perform
127 equality checks on the types right away, and it would be incredibly painful
128 to do this on un-desugared types. Luckily, desugared types are close enough
129 to HsTypes to make the error messages sane.
130
131 During type-checking, we perform as little validity checking as possible.
132 Generally, after type-checking, you will want to do validity checking, say
133 with TcValidity.checkValidType.
134
135 Validity checking
136 ~~~~~~~~~~~~~~~~~
137 Some of the validity check could in principle be done by the kind checker,
138 but not all:
139
140 - During desugaring, we normalise by expanding type synonyms. Only
141 after this step can we check things like type-synonym saturation
142 e.g. type T k = k Int
143 type S a = a
144 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
145 and then S is saturated. This is a GHC extension.
146
147 - Similarly, also a GHC extension, we look through synonyms before complaining
148 about the form of a class or instance declaration
149
150 - Ambiguity checks involve functional dependencies
151
152 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
153 finished building the loop. So to keep things simple, we postpone most validity
154 checking until step (3).
155
156 %************************************************************************
157 %* *
158 Check types AND do validity checking
159 * *
160 ************************************************************************
161 -}
162
163 funsSigCtxt :: [Located Name] -> UserTypeCtxt
164 -- Returns FunSigCtxt, with no redundant-context-reporting,
165 -- form a list of located names
166 funsSigCtxt (L _ name1 : _) = FunSigCtxt name1 False
167 funsSigCtxt [] = panic "funSigCtxt"
168
169 addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
170 addSigCtxt ctxt hs_ty thing_inside
171 = setSrcSpan (getLoc hs_ty) $
172 addErrCtxt (pprSigCtxt ctxt hs_ty) $
173 thing_inside
174
175 pprSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> SDoc
176 -- (pprSigCtxt ctxt <extra> <type>)
177 -- prints In the type signature for 'f':
178 -- f :: <type>
179 -- The <extra> is either empty or "the ambiguity check for"
180 pprSigCtxt ctxt hs_ty
181 | Just n <- isSigMaybe ctxt
182 = hang (text "In the type signature:")
183 2 (pprPrefixOcc n <+> dcolon <+> ppr hs_ty)
184
185 | otherwise
186 = hang (text "In" <+> pprUserTypeCtxt ctxt <> colon)
187 2 (ppr hs_ty)
188
189 tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
190 -- This one is used when we have a LHsSigWcType, but in
191 -- a place where wildcards aren't allowed. The renamer has
192 -- already checked this, so we can simply ignore it.
193 tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
194
195 kcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
196 kcClassSigType skol_info names sig_ty
197 = discardResult $
198 tcClassSigType skol_info names sig_ty
199 -- tcClassSigType does a fair amount of extra work that we don't need,
200 -- such as ordering quantified variables. But we absolutely do need
201 -- to push the level when checking method types and solve local equalities,
202 -- and so it seems easier just to call tcClassSigType than selectively
203 -- extract the lines of code from tc_hs_sig_type that we really need.
204 -- If we don't push the level, we get #16517, where GHC accepts
205 -- class C a where
206 -- meth :: forall k. Proxy (a :: k) -> ()
207 -- Note that k is local to meth -- this is hogwash.
208
209 tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
210 -- Does not do validity checking
211 tcClassSigType skol_info names sig_ty
212 = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
213 snd <$> tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
214 -- Do not zonk-to-Type, nor perform a validity check
215 -- We are in a knot with the class and associated types
216 -- Zonking and validity checking is done by tcClassDecl
217 -- No need to fail here if the type has an error:
218 -- If we're in the kind-checking phase, the solveEqualities
219 -- in kcTyClGroup catches the error
220 -- If we're in the type-checking phase, the solveEqualities
221 -- in tcClassDecl1 gets it
222 -- Failing fast here degrades the error message in, e.g., tcfail135:
223 -- class Foo f where
224 -- baa :: f a -> f
225 -- If we fail fast, we're told that f has kind `k1` when we wanted `*`.
226 -- It should be that f has kind `k2 -> *`, but we never get a chance
227 -- to run the solver where the kind of f is touchable. This is
228 -- painfully delicate.
229
230 tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
231 -- Does validity checking
232 -- See Note [Recipe for checking a signature]
233 tcHsSigType ctxt sig_ty
234 = addSigCtxt ctxt (hsSigType sig_ty) $
235 do { traceTc "tcHsSigType {" (ppr sig_ty)
236
237 -- Generalise here: see Note [Kind generalisation]
238 ; (insol, ty) <- tc_hs_sig_type skol_info sig_ty
239 (expectedKindInCtxt ctxt)
240 ; ty <- zonkTcType ty
241
242 ; when insol failM
243 -- See Note [Fail fast if there are insoluble kind equalities] in TcSimplify
244
245 ; checkValidType ctxt ty
246 ; traceTc "end tcHsSigType }" (ppr ty)
247 ; return ty }
248 where
249 skol_info = SigTypeSkol ctxt
250
251 -- Does validity checking and zonking.
252 tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind)
253 tcStandaloneKindSig (L _ kisig) = case kisig of
254 StandaloneKindSig _ (L _ name) ksig ->
255 let ctxt = StandaloneKindSigCtxt name in
256 addSigCtxt ctxt (hsSigType ksig) $
257 do { kind <- tcTopLHsType kindLevelMode ksig (expectedKindInCtxt ctxt)
258 ; checkValidType ctxt kind
259 ; return (name, kind) }
260 XStandaloneKindSig nec -> noExtCon nec
261
262 tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
263 -> ContextKind -> TcM (Bool, TcType)
264 -- Kind-checks/desugars an 'LHsSigType',
265 -- solve equalities,
266 -- and then kind-generalizes.
267 -- This will never emit constraints, as it uses solveEqualities interally.
268 -- No validity checking or zonking
269 -- Returns also a Bool indicating whether the type induced an insoluble constraint;
270 -- True <=> constraint is insoluble
271 tc_hs_sig_type skol_info hs_sig_type ctxt_kind
272 | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
273 = do { (tc_lvl, (wanted, (spec_tkvs, ty)))
274 <- pushTcLevelM $
275 solveLocalEqualitiesX "tc_hs_sig_type" $
276 bindImplicitTKBndrs_Skol sig_vars $
277 do { kind <- newExpectedKind ctxt_kind
278 ; tc_lhs_type typeLevelMode hs_ty kind }
279 -- Any remaining variables (unsolved in the solveLocalEqualities)
280 -- should be in the global tyvars, and therefore won't be quantified
281
282 ; spec_tkvs <- zonkAndScopedSort spec_tkvs
283 ; let ty1 = mkSpecForAllTys spec_tkvs ty
284
285 -- This bit is very much like decideMonoTyVars in TcSimplify,
286 -- but constraints are so much simpler in kinds, it is much
287 -- easier here. (In particular, we never quantify over a
288 -- constraint in a type.)
289 ; constrained <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted)
290 ; let should_gen = not . (`elemVarSet` constrained)
291
292 ; kvs <- kindGeneralizeSome should_gen ty1
293 ; emitResidualTvConstraint skol_info Nothing (kvs ++ spec_tkvs)
294 tc_lvl wanted
295
296 ; return (insolubleWC wanted, mkInvForAllTys kvs ty1) }
297
298 tc_hs_sig_type _ (XHsImplicitBndrs nec) _ = noExtCon nec
299
300 tcTopLHsType :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
301 -- tcTopLHsType is used for kind-checking top-level HsType where
302 -- we want to fully solve /all/ equalities, and report errors
303 -- Does zonking, but not validity checking because it's used
304 -- for things (like deriving and instances) that aren't
305 -- ordinary types
306 tcTopLHsType mode hs_sig_type ctxt_kind
307 | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
308 = do { traceTc "tcTopLHsType {" (ppr hs_ty)
309 ; (spec_tkvs, ty)
310 <- pushTcLevelM_ $
311 solveEqualities $
312 bindImplicitTKBndrs_Skol sig_vars $
313 do { kind <- newExpectedKind ctxt_kind
314 ; tc_lhs_type mode hs_ty kind }
315
316 ; spec_tkvs <- zonkAndScopedSort spec_tkvs
317 ; let ty1 = mkSpecForAllTys spec_tkvs ty
318 ; kvs <- kindGeneralizeAll ty1 -- "All" because it's a top-level type
319 ; final_ty <- zonkTcTypeToType (mkInvForAllTys kvs ty1)
320 ; traceTc "End tcTopLHsType }" (vcat [ppr hs_ty, ppr final_ty])
321 ; return final_ty}
322
323 tcTopLHsType _ (XHsImplicitBndrs nec) _ = noExtCon nec
324
325 -----------------
326 tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
327 -- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
328 -- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
329 -- E.g. class C (a::*) (b::k->k)
330 -- data T a b = ... deriving( C Int )
331 -- returns ([k], C, [k, Int], [k->k])
332 -- Return values are fully zonked
333 tcHsDeriv hs_ty
334 = do { ty <- checkNoErrs $ -- Avoid redundant error report
335 -- with "illegal deriving", below
336 tcTopLHsType typeLevelMode hs_ty AnyKind
337 ; let (tvs, pred) = splitForAllTys ty
338 (kind_args, _) = splitFunTys (tcTypeKind pred)
339 ; case getClassPredTys_maybe pred of
340 Just (cls, tys) -> return (tvs, cls, tys, kind_args)
341 Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
342
343 -- | Typecheck a deriving strategy. For most deriving strategies, this is a
344 -- no-op, but for the @via@ strategy, this requires typechecking the @via@ type.
345 tcDerivStrategy ::
346 Maybe (LDerivStrategy GhcRn)
347 -- ^ The deriving strategy
348 -> TcM (Maybe (LDerivStrategy GhcTc), [TyVar])
349 -- ^ The typechecked deriving strategy and the tyvars that it binds
350 -- (if using 'ViaStrategy').
351 tcDerivStrategy mb_lds
352 = case mb_lds of
353 Nothing -> boring_case Nothing
354 Just (dL->L loc ds) ->
355 setSrcSpan loc $ do
356 (ds', tvs) <- tc_deriv_strategy ds
357 pure (Just (cL loc ds'), tvs)
358 where
359 tc_deriv_strategy :: DerivStrategy GhcRn
360 -> TcM (DerivStrategy GhcTc, [TyVar])
361 tc_deriv_strategy StockStrategy = boring_case StockStrategy
362 tc_deriv_strategy AnyclassStrategy = boring_case AnyclassStrategy
363 tc_deriv_strategy NewtypeStrategy = boring_case NewtypeStrategy
364 tc_deriv_strategy (ViaStrategy ty) = do
365 ty' <- checkNoErrs $ tcTopLHsType typeLevelMode ty AnyKind
366 let (via_tvs, via_pred) = splitForAllTys ty'
367 pure (ViaStrategy via_pred, via_tvs)
368
369 boring_case :: ds -> TcM (ds, [TyVar])
370 boring_case ds = pure (ds, [])
371
372 tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt
373 -> LHsSigType GhcRn
374 -> TcM Type
375 -- Like tcHsSigType, but for a class instance declaration
376 tcHsClsInstType user_ctxt hs_inst_ty
377 = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
378 do { -- Fail eagerly if tcTopLHsType fails. We are at top level so
379 -- these constraints will never be solved later. And failing
380 -- eagerly avoids follow-on errors when checkValidInstance
381 -- sees an unsolved coercion hole
382 inst_ty <- checkNoErrs $
383 tcTopLHsType typeLevelMode hs_inst_ty (TheKind constraintKind)
384 ; checkValidInstance user_ctxt hs_inst_ty inst_ty
385 ; return inst_ty }
386
387 ----------------------------------------------
388 -- | Type-check a visible type application
389 tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
390 -- See Note [Recipe for checking a signature] in TcHsType
391 tcHsTypeApp wc_ty kind
392 | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
393 = do { ty <- solveLocalEqualities "tcHsTypeApp" $
394 -- We are looking at a user-written type, very like a
395 -- signature so we want to solve its equalities right now
396 unsetWOptM Opt_WarnPartialTypeSignatures $
397 setXOptM LangExt.PartialTypeSignatures $
398 -- See Note [Wildcards in visible type application]
399 tcNamedWildCardBinders sig_wcs $ \ _ ->
400 tcCheckLHsType hs_ty kind
401 -- We do not kind-generalize type applications: we just
402 -- instantiate with exactly what the user says.
403 -- See Note [No generalization in type application]
404 -- We still must call kindGeneralizeNone, though, according
405 -- to Note [Recipe for checking a signature]
406 ; kindGeneralizeNone ty
407 ; ty <- zonkTcType ty
408 ; checkValidType TypeAppCtxt ty
409 ; return ty }
410 tcHsTypeApp (XHsWildCardBndrs nec) _ = noExtCon nec
411
412 {- Note [Wildcards in visible type application]
413 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
414 A HsWildCardBndrs's hswc_ext now only includes /named/ wildcards, so
415 any unnamed wildcards stay unchanged in hswc_body. When called in
416 tcHsTypeApp, tcCheckLHsType will call emitAnonWildCardHoleConstraint
417 on these anonymous wildcards. However, this would trigger
418 error/warning when an anonymous wildcard is passed in as a visible type
419 argument, which we do not want because users should be able to write
420 @_ to skip a instantiating a type variable variable without fuss. The
421 solution is to switch the PartialTypeSignatures flags here to let the
422 typechecker know that it's checking a '@_' and do not emit hole
423 constraints on it. See related Note [Wildcards in visible kind
424 application] and Note [The wildcard story for types] in GHC.Hs.Types
425
426 Ugh!
427
428 Note [No generalization in type application]
429 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
430 We do not kind-generalize type applications. Imagine
431
432 id @(Proxy Nothing)
433
434 If we kind-generalized, we would get
435
436 id @(forall {k}. Proxy @(Maybe k) (Nothing @k))
437
438 which is very sneakily impredicative instantiation.
439
440 There is also the possibility of mentioning a wildcard
441 (`id @(Proxy _)`), which definitely should not be kind-generalized.
442
443 -}
444
445 {-
446 ************************************************************************
447 * *
448 The main kind checker: no validity checks here
449 * *
450 ************************************************************************
451 -}
452
453 ---------------------------
454 tcHsOpenType, tcHsLiftedType,
455 tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
456 -- Used for type signatures
457 -- Do not do validity checking
458 tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty
459 tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty
460
461 tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind
462 ; tc_lhs_type typeLevelMode ty ek }
463 tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
464
465 -- Like tcHsType, but takes an expected kind
466 tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
467 tcCheckLHsType hs_ty exp_kind
468 = addTypeCtxt hs_ty $
469 tc_lhs_type typeLevelMode hs_ty exp_kind
470
471 tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
472 -- Called from outside: set the context
473 tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
474
475 -- Like tcLHsType, but use it in a context where type synonyms and type families
476 -- do not need to be saturated, like in a GHCi :kind call
477 tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
478 tcLHsTypeUnsaturated hs_ty
479 | Just (hs_fun_ty, hs_args) <- splitHsAppTys (unLoc hs_ty)
480 = addTypeCtxt hs_ty $
481 do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty
482 ; tcInferApps_nosat mode hs_fun_ty fun_ty hs_args }
483 -- Notice the 'nosat'; do not instantiate trailing
484 -- invisible arguments of a type family.
485 -- See Note [Dealing with :kind]
486
487 | otherwise
488 = addTypeCtxt hs_ty $
489 tc_infer_lhs_type mode hs_ty
490
491 where
492 mode = typeLevelMode
493
494 {- Note [Dealing with :kind]
495 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
496 Consider this GHCi command
497 ghci> type family F :: Either j k
498 ghci> :kind F
499 F :: forall {j,k}. Either j k
500
501 We will only get the 'forall' if we /refrain/ from saturating those
502 invisible binders. But generally we /do/ saturate those invisible
503 binders (see tcInferApps), and we want to do so for nested application
504 even in GHCi. Consider for example (#16287)
505 ghci> type family F :: k
506 ghci> data T :: (forall k. k) -> Type
507 ghci> :kind T F
508 We want to reject this. It's just at the very top level that we want
509 to switch off saturation.
510
511 So tcLHsTypeUnsaturated does a little special case for top level
512 applications. Actually the common case is a bare variable, as above.
513
514
515 ************************************************************************
516 * *
517 Type-checking modes
518 * *
519 ************************************************************************
520
521 The kind-checker is parameterised by a TcTyMode, which contains some
522 information about where we're checking a type.
523
524 The renamer issues errors about what it can. All errors issued here must
525 concern things that the renamer can't handle.
526
527 -}
528
529 -- | Info about the context in which we're checking a type. Currently,
530 -- differentiates only between types and kinds, but this will likely
531 -- grow, at least to include the distinction between patterns and
532 -- not-patterns.
533 --
534 -- To find out where the mode is used, search for 'mode_level'
535 data TcTyMode = TcTyMode { mode_level :: TypeOrKind }
536
537 typeLevelMode :: TcTyMode
538 typeLevelMode = TcTyMode { mode_level = TypeLevel }
539
540 kindLevelMode :: TcTyMode
541 kindLevelMode = TcTyMode { mode_level = KindLevel }
542
543 -- switch to kind level
544 kindLevel :: TcTyMode -> TcTyMode
545 kindLevel mode = mode { mode_level = KindLevel }
546
547 instance Outputable TcTyMode where
548 ppr = ppr . mode_level
549
550 {-
551 Note [Bidirectional type checking]
552 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
553 In expressions, whenever we see a polymorphic identifier, say `id`, we are
554 free to instantiate it with metavariables, knowing that we can always
555 re-generalize with type-lambdas when necessary. For example:
556
557 rank2 :: (forall a. a -> a) -> ()
558 x = rank2 id
559
560 When checking the body of `x`, we can instantiate `id` with a metavariable.
561 Then, when we're checking the application of `rank2`, we notice that we really
562 need a polymorphic `id`, and then re-generalize over the unconstrained
563 metavariable.
564
565 In types, however, we're not so lucky, because *we cannot re-generalize*!
566 There is no lambda. So, we must be careful only to instantiate at the last
567 possible moment, when we're sure we're never going to want the lost polymorphism
568 again. This is done in calls to tcInstInvisibleTyBinders.
569
570 To implement this behavior, we use bidirectional type checking, where we
571 explicitly think about whether we know the kind of the type we're checking
572 or not. Note that there is a difference between not knowing a kind and
573 knowing a metavariable kind: the metavariables are TauTvs, and cannot become
574 forall-quantified kinds. Previously (before dependent types), there were
575 no higher-rank kinds, and so we could instantiate early and be sure that
576 no types would have polymorphic kinds, and so we could always assume that
577 the kind of a type was a fresh metavariable. Not so anymore, thus the
578 need for two algorithms.
579
580 For HsType forms that can never be kind-polymorphic, we implement only the
581 "down" direction, where we safely assume a metavariable kind. For HsType forms
582 that *can* be kind-polymorphic, we implement just the "up" (functions with
583 "infer" in their name) version, as we gain nothing by also implementing the
584 "down" version.
585
586 Note [Future-proofing the type checker]
587 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
588 As discussed in Note [Bidirectional type checking], each HsType form is
589 handled in *either* tc_infer_hs_type *or* tc_hs_type. These functions
590 are mutually recursive, so that either one can work for any type former.
591 But, we want to make sure that our pattern-matches are complete. So,
592 we have a bunch of repetitive code just so that we get warnings if we're
593 missing any patterns.
594
595 -}
596
597 ------------------------------------------
598 -- | Check and desugar a type, returning the core type and its
599 -- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
600 -- level.
601 tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
602 tc_infer_lhs_type mode (L span ty)
603 = setSrcSpan span $
604 tc_infer_hs_type mode ty
605
606 ---------------------------
607 -- | Call 'tc_infer_hs_type' and check its result against an expected kind.
608 tc_infer_hs_type_ek :: HasDebugCallStack => TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
609 tc_infer_hs_type_ek mode hs_ty ek
610 = do { (ty, k) <- tc_infer_hs_type mode hs_ty
611 ; checkExpectedKind hs_ty ty k ek }
612
613 ---------------------------
614 -- | Infer the kind of a type and desugar. This is the "up" type-checker,
615 -- as described in Note [Bidirectional type checking]
616 tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
617
618 tc_infer_hs_type mode (HsParTy _ t)
619 = tc_infer_lhs_type mode t
620
621 tc_infer_hs_type mode ty
622 | Just (hs_fun_ty, hs_args) <- splitHsAppTys ty
623 = do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty
624 ; tcInferApps mode hs_fun_ty fun_ty hs_args }
625
626 tc_infer_hs_type mode (HsKindSig _ ty sig)
627 = do { sig' <- tcLHsKindSig KindSigCtxt sig
628 -- We must typecheck the kind signature, and solve all
629 -- its equalities etc; from this point on we may do
630 -- things like instantiate its foralls, so it needs
631 -- to be fully determined (#14904)
632 ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
633 ; ty' <- tc_lhs_type mode ty sig'
634 ; return (ty', sig') }
635
636 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
637 -- the splice location to the typechecker. Here we skip over it in order to have
638 -- the same kind inferred for a given expression whether it was produced from
639 -- splices or not.
640 --
641 -- See Note [Delaying modFinalizers in untyped splices].
642 tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
643 = tc_infer_hs_type mode ty
644
645 tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
646 tc_infer_hs_type _ (XHsType (NHsCoreTy ty))
647 = return (ty, tcTypeKind ty)
648
649 tc_infer_hs_type _ (HsExplicitListTy _ _ tys)
650 | null tys -- this is so that we can use visible kind application with '[]
651 -- e.g ... '[] @Bool
652 = return (mkTyConTy promotedNilDataCon,
653 mkSpecForAllTys [alphaTyVar] $ mkListTy alphaTy)
654
655 tc_infer_hs_type mode other_ty
656 = do { kv <- newMetaKindVar
657 ; ty' <- tc_hs_type mode other_ty kv
658 ; return (ty', kv) }
659
660 ------------------------------------------
661 tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
662 tc_lhs_type mode (L span ty) exp_kind
663 = setSrcSpan span $
664 tc_hs_type mode ty exp_kind
665
666 tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
667 -- See Note [Bidirectional type checking]
668
669 tc_hs_type mode (HsParTy _ ty) exp_kind = tc_lhs_type mode ty exp_kind
670 tc_hs_type mode (HsDocTy _ ty _) exp_kind = tc_lhs_type mode ty exp_kind
671 tc_hs_type _ ty@(HsBangTy _ bang _) _
672 -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
673 -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
674 -- bangs are invalid, so fail. (#7210, #14761)
675 = do { let bangError err = failWith $
676 text "Unexpected" <+> text err <+> text "annotation:" <+> ppr ty $$
677 text err <+> text "annotation cannot appear nested inside a type"
678 ; case bang of
679 HsSrcBang _ SrcUnpack _ -> bangError "UNPACK"
680 HsSrcBang _ SrcNoUnpack _ -> bangError "NOUNPACK"
681 HsSrcBang _ NoSrcUnpack SrcLazy -> bangError "laziness"
682 HsSrcBang _ _ _ -> bangError "strictness" }
683 tc_hs_type _ ty@(HsRecTy {}) _
684 -- Record types (which only show up temporarily in constructor
685 -- signatures) should have been removed by now
686 = failWithTc (text "Record syntax is illegal here:" <+> ppr ty)
687
688 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType'.
689 -- Here we get rid of it and add the finalizers to the global environment
690 -- while capturing the local environment.
691 --
692 -- See Note [Delaying modFinalizers in untyped splices].
693 tc_hs_type mode (HsSpliceTy _ (HsSpliced _ mod_finalizers (HsSplicedTy ty)))
694 exp_kind
695 = do addModFinalizersWithLclEnv mod_finalizers
696 tc_hs_type mode ty exp_kind
697
698 -- This should never happen; type splices are expanded by the renamer
699 tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind
700 = failWithTc (text "Unexpected type splice:" <+> ppr ty)
701
702 ---------- Functions and applications
703 tc_hs_type mode (HsFunTy _ ty1 ty2) exp_kind
704 = tc_fun_type mode ty1 ty2 exp_kind
705
706 tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
707 | op `hasKey` funTyConKey
708 = tc_fun_type mode ty1 ty2 exp_kind
709
710 --------- Foralls
711 tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs
712 , hst_body = ty }) exp_kind
713 = do { (tclvl, wanted, (tvs', ty'))
714 <- pushLevelAndCaptureConstraints $
715 bindExplicitTKBndrs_Skol hs_tvs $
716 tc_lhs_type mode ty exp_kind
717 -- Do not kind-generalise here! See Note [Kind generalisation]
718 -- Why exp_kind? See Note [Body kind of HsForAllTy]
719 ; let argf = case fvf of
720 ForallVis -> Required
721 ForallInvis -> Specified
722 bndrs = mkTyVarBinders argf tvs'
723 skol_info = ForAllSkol (ppr forall)
724 m_telescope = Just (sep (map ppr hs_tvs))
725
726 ; emitResidualTvConstraint skol_info m_telescope tvs' tclvl wanted
727
728 ; return (mkForAllTys bndrs ty') }
729
730 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
731 | null (unLoc ctxt)
732 = tc_lhs_type mode rn_ty exp_kind
733
734 -- See Note [Body kind of a HsQualTy]
735 | tcIsConstraintKind exp_kind
736 = do { ctxt' <- tc_hs_context mode ctxt
737 ; ty' <- tc_lhs_type mode rn_ty constraintKind
738 ; return (mkPhiTy ctxt' ty') }
739
740 | otherwise
741 = do { ctxt' <- tc_hs_context mode ctxt
742
743 ; ek <- newOpenTypeKind -- The body kind (result of the function) can
744 -- be TYPE r, for any r, hence newOpenTypeKind
745 ; ty' <- tc_lhs_type mode rn_ty ek
746 ; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
747 liftedTypeKind exp_kind }
748
749 --------- Lists, arrays, and tuples
750 tc_hs_type mode rn_ty@(HsListTy _ elt_ty) exp_kind
751 = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
752 ; checkWiredInTyCon listTyCon
753 ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
754
755 -- See Note [Distinguishing tuple kinds] in GHC.Hs.Types
756 -- See Note [Inferring tuple kinds]
757 tc_hs_type mode rn_ty@(HsTupleTy _ HsBoxedOrConstraintTuple hs_tys) exp_kind
758 -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
759 | Just tup_sort <- tupKindSort_maybe exp_kind
760 = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
761 tc_tuple rn_ty mode tup_sort hs_tys exp_kind
762 | otherwise
763 = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
764 ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
765 ; kinds <- mapM zonkTcType kinds
766 -- Infer each arg type separately, because errors can be
767 -- confusing if we give them a shared kind. Eg #7410
768 -- (Either Int, Int), we do not want to get an error saying
769 -- "the second argument of a tuple should have kind *->*"
770
771 ; let (arg_kind, tup_sort)
772 = case [ (k,s) | k <- kinds
773 , Just s <- [tupKindSort_maybe k] ] of
774 ((k,s) : _) -> (k,s)
775 [] -> (liftedTypeKind, BoxedTuple)
776 -- In the [] case, it's not clear what the kind is, so guess *
777
778 ; tys' <- sequence [ setSrcSpan loc $
779 checkExpectedKind hs_ty ty kind arg_kind
780 | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
781
782 ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
783
784
785 tc_hs_type mode rn_ty@(HsTupleTy _ hs_tup_sort tys) exp_kind
786 = tc_tuple rn_ty mode tup_sort tys exp_kind
787 where
788 tup_sort = case hs_tup_sort of -- Fourth case dealt with above
789 HsUnboxedTuple -> UnboxedTuple
790 HsBoxedTuple -> BoxedTuple
791 HsConstraintTuple -> ConstraintTuple
792 _ -> panic "tc_hs_type HsTupleTy"
793
794 tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
795 = do { let arity = length hs_tys
796 ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
797 ; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
798 ; let arg_reps = map kindRep arg_kinds
799 arg_tys = arg_reps ++ tau_tys
800 sum_ty = mkTyConApp (sumTyCon arity) arg_tys
801 sum_kind = unboxedSumKind arg_reps
802 ; checkExpectedKind rn_ty sum_ty sum_kind exp_kind
803 }
804
805 --------- Promoted lists and tuples
806 tc_hs_type mode rn_ty@(HsExplicitListTy _ _ tys) exp_kind
807 = do { tks <- mapM (tc_infer_lhs_type mode) tys
808 ; (taus', kind) <- unifyKinds tys tks
809 ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
810 ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
811 where
812 mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
813 mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k]
814
815 tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
816 -- using newMetaKindVar means that we force instantiations of any polykinded
817 -- types. At first, I just used tc_infer_lhs_type, but that led to #11255.
818 = do { ks <- replicateM arity newMetaKindVar
819 ; taus <- zipWithM (tc_lhs_type mode) tys ks
820 ; let kind_con = tupleTyCon Boxed arity
821 ty_con = promotedTupleDataCon Boxed arity
822 tup_k = mkTyConApp kind_con ks
823 ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
824 where
825 arity = length tys
826
827 --------- Constraint types
828 tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
829 = do { MASSERT( isTypeLevel (mode_level mode) )
830 ; ty' <- tc_lhs_type mode ty liftedTypeKind
831 ; let n' = mkStrLitTy $ hsIPNameFS n
832 ; ipClass <- tcLookupClass ipClassName
833 ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
834 constraintKind exp_kind }
835
836 tc_hs_type _ rn_ty@(HsStarTy _ _) exp_kind
837 -- Desugaring 'HsStarTy' to 'Data.Kind.Type' here means that we don't have to
838 -- handle it in 'coreView' and 'tcView'.
839 = checkExpectedKind rn_ty liftedTypeKind liftedTypeKind exp_kind
840
841 --------- Literals
842 tc_hs_type _ rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
843 = do { checkWiredInTyCon typeNatKindCon
844 ; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
845
846 tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
847 = do { checkWiredInTyCon typeSymbolKindCon
848 ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
849
850 --------- Potentially kind-polymorphic types: call the "up" checker
851 -- See Note [Future-proofing the type checker]
852 tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
853 tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek
854 tc_hs_type mode ty@(HsAppKindTy{}) ek = tc_infer_hs_type_ek mode ty ek
855 tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
856 tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
857 tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
858 tc_hs_type _ wc@(HsWildCardTy _) ek = tcAnonWildCardOcc wc ek
859
860 ------------------------------------------
861 tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
862 -> TcM TcType
863 tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
864 TypeLevel ->
865 do { arg_k <- newOpenTypeKind
866 ; res_k <- newOpenTypeKind
867 ; ty1' <- tc_lhs_type mode ty1 arg_k
868 ; ty2' <- tc_lhs_type mode ty2 res_k
869 ; checkExpectedKind (HsFunTy noExtField ty1 ty2) (mkVisFunTy ty1' ty2')
870 liftedTypeKind exp_kind }
871 KindLevel -> -- no representation polymorphism in kinds. yet.
872 do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
873 ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
874 ; checkExpectedKind (HsFunTy noExtField ty1 ty2) (mkVisFunTy ty1' ty2')
875 liftedTypeKind exp_kind }
876
877 ---------------------------
878 tcAnonWildCardOcc :: HsType GhcRn -> Kind -> TcM TcType
879 tcAnonWildCardOcc wc exp_kind
880 = do { wc_tv <- newWildTyVar -- The wildcard's kind will be an un-filled-in meta tyvar
881
882 ; part_tysig <- xoptM LangExt.PartialTypeSignatures
883 ; warning <- woptM Opt_WarnPartialTypeSignatures
884
885 ; unless (part_tysig && not warning) $
886 emitAnonWildCardHoleConstraint wc_tv
887 -- Why the 'unless' guard?
888 -- See Note [Wildcards in visible kind application]
889
890 ; checkExpectedKind wc (mkTyVarTy wc_tv)
891 (tyVarKind wc_tv) exp_kind }
892
893 {- Note [Wildcards in visible kind application]
894 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
895 There are cases where users might want to pass in a wildcard as a visible kind
896 argument, for instance:
897
898 data T :: forall k1 k2. k1 → k2 → Type where
899 MkT :: T a b
900 x :: T @_ @Nat False n
901 x = MkT
902
903 So we should allow '@_' without emitting any hole constraints, and
904 regardless of whether PartialTypeSignatures is enabled or not. But how would
905 the typechecker know which '_' is being used in VKA and which is not when it
906 calls emitNamedWildCardHoleConstraints in tcHsPartialSigType on all HsWildCardBndrs?
907 The solution then is to neither rename nor include unnamed wildcards in HsWildCardBndrs,
908 but instead give every anonymous wildcard a fresh wild tyvar in tcAnonWildCardOcc.
909 And whenever we see a '@', we automatically turn on PartialTypeSignatures and
910 turn off hole constraint warnings, and do not call emitAnonWildCardHoleConstraint
911 under these conditions.
912 See related Note [Wildcards in visible type application] here and
913 Note [The wildcard story for types] in GHC.Hs.Types
914
915 -}
916
917 {- *********************************************************************
918 * *
919 Tuples
920 * *
921 ********************************************************************* -}
922
923 ---------------------------
924 tupKindSort_maybe :: TcKind -> Maybe TupleSort
925 tupKindSort_maybe k
926 | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
927 | Just k' <- tcView k = tupKindSort_maybe k'
928 | tcIsConstraintKind k = Just ConstraintTuple
929 | tcIsLiftedTypeKind k = Just BoxedTuple
930 | otherwise = Nothing
931
932 tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
933 tc_tuple rn_ty mode tup_sort tys exp_kind
934 = do { arg_kinds <- case tup_sort of
935 BoxedTuple -> return (replicate arity liftedTypeKind)
936 UnboxedTuple -> replicateM arity newOpenTypeKind
937 ConstraintTuple -> return (replicate arity constraintKind)
938 ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
939 ; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
940 where
941 arity = length tys
942
943 finish_tuple :: HsType GhcRn
944 -> TupleSort
945 -> [TcType] -- ^ argument types
946 -> [TcKind] -- ^ of these kinds
947 -> TcKind -- ^ expected kind of the whole tuple
948 -> TcM TcType
949 finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
950 = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
951 ; let arg_tys = case tup_sort of
952 -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
953 UnboxedTuple -> tau_reps ++ tau_tys
954 BoxedTuple -> tau_tys
955 ConstraintTuple -> tau_tys
956 ; tycon <- case tup_sort of
957 ConstraintTuple
958 | arity > mAX_CTUPLE_SIZE
959 -> failWith (bigConstraintTuple arity)
960 | otherwise -> tcLookupTyCon (cTupleTyConName arity)
961 BoxedTuple -> do { let tc = tupleTyCon Boxed arity
962 ; checkWiredInTyCon tc
963 ; return tc }
964 UnboxedTuple -> return (tupleTyCon Unboxed arity)
965 ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind }
966 where
967 arity = length tau_tys
968 tau_reps = map kindRep tau_kinds
969 res_kind = case tup_sort of
970 UnboxedTuple -> unboxedTupleKind tau_reps
971 BoxedTuple -> liftedTypeKind
972 ConstraintTuple -> constraintKind
973
974 bigConstraintTuple :: Arity -> MsgDoc
975 bigConstraintTuple arity
976 = hang (text "Constraint tuple arity too large:" <+> int arity
977 <+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
978 2 (text "Instead, use a nested tuple")
979
980
981 {- *********************************************************************
982 * *
983 Type applications
984 * *
985 ********************************************************************* -}
986
987 splitHsAppTys :: HsType GhcRn -> Maybe (LHsType GhcRn, [LHsTypeArg GhcRn])
988 splitHsAppTys hs_ty
989 | is_app hs_ty = Just (go (noLoc hs_ty) [])
990 | otherwise = Nothing
991 where
992 is_app :: HsType GhcRn -> Bool
993 is_app (HsAppKindTy {}) = True
994 is_app (HsAppTy {}) = True
995 is_app (HsOpTy _ _ (L _ op) _) = not (op `hasKey` funTyConKey)
996 -- I'm not sure why this funTyConKey test is necessary
997 -- Can it even happen? Perhaps for t1 `(->)` t2
998 -- but then maybe it's ok to treat that like a normal
999 -- application rather than using the special rule for HsFunTy
1000 is_app (HsTyVar {}) = True
1001 is_app (HsParTy _ (L _ ty)) = is_app ty
1002 is_app _ = False
1003
1004 go (L _ (HsAppTy _ f a)) as = go f (HsValArg a : as)
1005 go (L _ (HsAppKindTy l ty k)) as = go ty (HsTypeArg l k : as)
1006 go (L sp (HsParTy _ f)) as = go f (HsArgPar sp : as)
1007 go (L _ (HsOpTy _ l op@(L sp _) r)) as
1008 = ( L sp (HsTyVar noExtField NotPromoted op)
1009 , HsValArg l : HsValArg r : as )
1010 go f as = (f, as)
1011
1012 ---------------------------
1013 tcInferAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
1014 -- Version of tc_infer_lhs_type specialised for the head of an
1015 -- application. In particular, for a HsTyVar (which includes type
1016 -- constructors, it does not zoom off into tcInferApps and family
1017 -- saturation
1018 tcInferAppHead mode (L _ (HsTyVar _ _ (L _ tv)))
1019 = tcTyVar mode tv
1020 tcInferAppHead mode ty
1021 = tc_infer_lhs_type mode ty
1022
1023 ---------------------------
1024 -- | Apply a type of a given kind to a list of arguments. This instantiates
1025 -- invisible parameters as necessary. Always consumes all the arguments,
1026 -- using matchExpectedFunKind as necessary.
1027 -- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.-
1028 -- These kinds should be used to instantiate invisible kind variables;
1029 -- they come from an enclosing class for an associated type/data family.
1030 --
1031 -- tcInferApps also arranges to saturate any trailing invisible arguments
1032 -- of a type-family application, which is usually the right thing to do
1033 -- tcInferApps_nosat does not do this saturation; it is used only
1034 -- by ":kind" in GHCi
1035 tcInferApps, tcInferApps_nosat
1036 :: TcTyMode
1037 -> LHsType GhcRn -- ^ Function (for printing only)
1038 -> TcType -- ^ Function
1039 -> [LHsTypeArg GhcRn] -- ^ Args
1040 -> TcM (TcType, TcKind) -- ^ (f args, args, result kind)
1041 tcInferApps mode hs_ty fun hs_args
1042 = do { (f_args, res_k) <- tcInferApps_nosat mode hs_ty fun hs_args
1043 ; saturateFamApp f_args res_k }
1044
1045 tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
1046 = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args)
1047 ; (f_args, res_k) <- go_init 1 fun orig_hs_args
1048 ; traceTc "tcInferApps }" (ppr f_args <+> dcolon <+> ppr res_k)
1049 ; return (f_args, res_k) }
1050 where
1051
1052 -- go_init just initialises the auxiliary
1053 -- arguments of the 'go' loop
1054 go_init n fun all_args
1055 = go n fun empty_subst fun_ki all_args
1056 where
1057 fun_ki = tcTypeKind fun
1058 -- We do (tcTypeKind fun) here, even though the caller
1059 -- knows the function kind, to absolutely guarantee
1060 -- INVARIANT for 'go'
1061 -- Note that in a typical application (F t1 t2 t3),
1062 -- the 'fun' is just a TyCon, so tcTypeKind is fast
1063
1064 empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
1065 tyCoVarsOfType fun_ki
1066
1067 go :: Int -- The # of the next argument
1068 -> TcType -- Function applied to some args
1069 -> TCvSubst -- Applies to function kind
1070 -> TcKind -- Function kind
1071 -> [LHsTypeArg GhcRn] -- Un-type-checked args
1072 -> TcM (TcType, TcKind) -- Result type and its kind
1073 -- INVARIANT: in any call (go n fun subst fun_ki args)
1074 -- tcTypeKind fun = subst(fun_ki)
1075 -- So the 'subst' and 'fun_ki' arguments are simply
1076 -- there to avoid repeatedly calling tcTypeKind.
1077 --
1078 -- Reason for INVARIANT: to support the Purely Kinded Type Invariant
1079 -- it's important that if fun_ki has a forall, then so does
1080 -- (tcTypeKind fun), because the next thing we are going to do
1081 -- is apply 'fun' to an argument type.
1082
1083 -- Dispatch on all_args first, for performance reasons
1084 go n fun subst fun_ki all_args = case (all_args, tcSplitPiTy_maybe fun_ki) of
1085
1086 ---------------- No user-written args left. We're done!
1087 ([], _) -> return (fun, substTy subst fun_ki)
1088
1089 ---------------- HsArgPar: We don't care about parens here
1090 (HsArgPar _ : args, _) -> go n fun subst fun_ki args
1091
1092 ---------------- HsTypeArg: a kind application (fun @ki)
1093 (HsTypeArg _ hs_ki_arg : hs_args, Just (ki_binder, inner_ki)) ->
1094 case ki_binder of
1095
1096 -- FunTy with PredTy on LHS, or ForAllTy with Inferred
1097 Named (Bndr _ Inferred) -> instantiate ki_binder inner_ki
1098 Anon InvisArg _ -> instantiate ki_binder inner_ki
1099
1100 Named (Bndr _ Specified) -> -- Visible kind application
1101 do { traceTc "tcInferApps (vis kind app)"
1102 (vcat [ ppr ki_binder, ppr hs_ki_arg
1103 , ppr (tyBinderType ki_binder)
1104 , ppr subst ])
1105
1106 ; let exp_kind = substTy subst $ tyBinderType ki_binder
1107
1108 ; ki_arg <- addErrCtxt (funAppCtxt orig_hs_ty hs_ki_arg n) $
1109 unsetWOptM Opt_WarnPartialTypeSignatures $
1110 setXOptM LangExt.PartialTypeSignatures $
1111 -- Urgh! see Note [Wildcards in visible kind application]
1112 -- ToDo: must kill this ridiculous messing with DynFlags
1113 tc_lhs_type (kindLevel mode) hs_ki_arg exp_kind
1114
1115 ; traceTc "tcInferApps (vis kind app)" (ppr exp_kind)
1116 ; (subst', fun') <- mkAppTyM subst fun ki_binder ki_arg
1117 ; go (n+1) fun' subst' inner_ki hs_args }
1118
1119 -- Attempted visible kind application (fun @ki), but fun_ki is
1120 -- forall k -> blah or k1 -> k2
1121 -- So we need a normal application. Error.
1122 _ -> ty_app_err hs_ki_arg $ substTy subst fun_ki
1123
1124 -- No binder; try applying the substitution, or fail if that's not possible
1125 (HsTypeArg _ ki_arg : _, Nothing) -> try_again_after_substing_or $
1126 ty_app_err ki_arg substed_fun_ki
1127
1128 ---------------- HsValArg: a nomal argument (fun ty)
1129 (HsValArg arg : args, Just (ki_binder, inner_ki))
1130 -- next binder is invisible; need to instantiate it
1131 | isInvisibleBinder ki_binder -- FunTy with InvisArg on LHS;
1132 -- or ForAllTy with Inferred or Specified
1133 -> instantiate ki_binder inner_ki
1134
1135 -- "normal" case
1136 | otherwise
1137 -> do { traceTc "tcInferApps (vis normal app)"
1138 (vcat [ ppr ki_binder
1139 , ppr arg
1140 , ppr (tyBinderType ki_binder)
1141 , ppr subst ])
1142 ; let exp_kind = substTy subst $ tyBinderType ki_binder
1143 ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
1144 tc_lhs_type mode arg exp_kind
1145 ; traceTc "tcInferApps (vis normal app) 2" (ppr exp_kind)
1146 ; (subst', fun') <- mkAppTyM subst fun ki_binder arg'
1147 ; go (n+1) fun' subst' inner_ki args }
1148
1149 -- no binder; try applying the substitution, or infer another arrow in fun kind
1150 (HsValArg _ : _, Nothing)
1151 -> try_again_after_substing_or $
1152 do { let arrows_needed = n_initial_val_args all_args
1153 ; co <- matchExpectedFunKind hs_ty arrows_needed substed_fun_ki
1154
1155 ; fun' <- zonkTcType (fun `mkTcCastTy` co)
1156 -- This zonk is essential, to expose the fruits
1157 -- of matchExpectedFunKind to the 'go' loop
1158
1159 ; traceTc "tcInferApps (no binder)" $
1160 vcat [ ppr fun <+> dcolon <+> ppr fun_ki
1161 , ppr arrows_needed
1162 , ppr co
1163 , ppr fun' <+> dcolon <+> ppr (tcTypeKind fun')]
1164 ; go_init n fun' all_args }
1165 -- Use go_init to establish go's INVARIANT
1166 where
1167 instantiate ki_binder inner_ki
1168 = do { traceTc "tcInferApps (need to instantiate)"
1169 (vcat [ ppr ki_binder, ppr subst])
1170 ; (subst', arg') <- tcInstInvisibleTyBinder subst ki_binder
1171 ; go n (mkAppTy fun arg') subst' inner_ki all_args }
1172 -- Because tcInvisibleTyBinder instantiate ki_binder,
1173 -- the kind of arg' will have the same shape as the kind
1174 -- of ki_binder. So we don't need mkAppTyM here.
1175
1176 try_again_after_substing_or fallthrough
1177 | not (isEmptyTCvSubst subst)
1178 = go n fun zapped_subst substed_fun_ki all_args
1179 | otherwise
1180 = fallthrough
1181
1182 zapped_subst = zapTCvSubst subst
1183 substed_fun_ki = substTy subst fun_ki
1184 hs_ty = appTypeToArg orig_hs_ty (take (n-1) orig_hs_args)
1185
1186 n_initial_val_args :: [HsArg tm ty] -> Arity
1187 -- Count how many leading HsValArgs we have
1188 n_initial_val_args (HsValArg {} : args) = 1 + n_initial_val_args args
1189 n_initial_val_args (HsArgPar {} : args) = n_initial_val_args args
1190 n_initial_val_args _ = 0
1191
1192 ty_app_err arg ty
1193 = failWith $ text "Cannot apply function of kind" <+> quotes (ppr ty)
1194 $$ text "to visible kind argument" <+> quotes (ppr arg)
1195
1196
1197 mkAppTyM :: TCvSubst
1198 -> TcType -> TyCoBinder -- fun, plus its top-level binder
1199 -> TcType -- arg
1200 -> TcM (TCvSubst, TcType) -- Extended subst, plus (fun arg)
1201 -- Precondition: the application (fun arg) is well-kinded after zonking
1202 -- That is, the application makes sense
1203 --
1204 -- Precondition: for (mkAppTyM subst fun bndr arg)
1205 -- tcTypeKind fun = Pi bndr. body
1206 -- That is, fun always has a ForAllTy or FunTy at the top
1207 -- and 'bndr' is fun's pi-binder
1208 --
1209 -- Postcondition: if fun and arg satisfy (PKTI), the purely-kinded type
1210 -- invariant, then so does the result type (fun arg)
1211 --
1212 -- We do not require that
1213 -- tcTypeKind arg = tyVarKind (binderVar bndr)
1214 -- This must be true after zonking (precondition 1), but it's not
1215 -- required for the (PKTI).
1216 mkAppTyM subst fun ki_binder arg
1217 | -- See Note [mkAppTyM]: Nasty case 2
1218 TyConApp tc args <- fun
1219 , isTypeSynonymTyCon tc
1220 , args `lengthIs` (tyConArity tc - 1)
1221 , any isTrickyTvBinder (tyConTyVars tc) -- We could cache this in the synonym
1222 = do { arg' <- zonkTcType arg
1223 ; args' <- zonkTcTypes args
1224 ; let subst' = case ki_binder of
1225 Anon {} -> subst
1226 Named (Bndr tv _) -> extendTvSubstAndInScope subst tv arg'
1227 ; return (subst', mkTyConApp tc (args' ++ [arg'])) }
1228
1229
1230 mkAppTyM subst fun (Anon {}) arg
1231 = return (subst, mk_app_ty fun arg)
1232
1233 mkAppTyM subst fun (Named (Bndr tv _)) arg
1234 = do { arg' <- if isTrickyTvBinder tv
1235 then -- See Note [mkAppTyM]: Nasty case 1
1236 zonkTcType arg
1237 else return arg
1238 ; return ( extendTvSubstAndInScope subst tv arg'
1239 , mk_app_ty fun arg' ) }
1240
1241 mk_app_ty :: TcType -> TcType -> TcType
1242 -- This function just adds an ASSERT for mkAppTyM's precondition
1243 mk_app_ty fun arg
1244 = ASSERT2( isPiTy fun_kind
1245 , ppr fun <+> dcolon <+> ppr fun_kind $$ ppr arg )
1246 mkAppTy fun arg
1247 where
1248 fun_kind = tcTypeKind fun
1249
1250 isTrickyTvBinder :: TcTyVar -> Bool
1251 -- NB: isTrickyTvBinder is just an optimisation
1252 -- It would be absolutely sound to return True always
1253 isTrickyTvBinder tv = isPiTy (tyVarKind tv)
1254
1255 {- Note [The Purely Kinded Type Invariant (PKTI)]
1256 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1257 During type inference, we maintain this invariant
1258
1259 (PKTI) It is legal to call 'tcTypeKind' on any Type ty,
1260 on any sub-term of ty, /without/ zonking ty
1261
1262 Moreover, any such returned kind
1263 will itself satisfy (PKTI)
1264
1265 By "legal to call tcTypeKind" we mean "tcTypeKind will not crash".
1266 The way in which tcTypeKind can crash is in applications
1267 (a t1 t2 .. tn)
1268 if 'a' is a type variable whose kind doesn't have enough arrows
1269 or foralls. (The crash is in piResultTys.)
1270
1271 The loop in tcInferApps has to be very careful to maintain the (PKTI).
1272 For example, suppose
1273 kappa is a unification variable
1274 We have already unified kappa := Type
1275 yielding co :: Refl (Type -> Type)
1276 a :: kappa
1277 then consider the type
1278 (a Int)
1279 If we call tcTypeKind on that, we'll crash, because the (un-zonked)
1280 kind of 'a' is just kappa, not an arrow kind. So we must zonk first.
1281
1282 So the type inference engine is very careful when building applications.
1283 This happens in tcInferApps. Suppose we are kind-checking the type (a Int),
1284 where (a :: kappa). Then in tcInferApps we'll run out of binders on
1285 a's kind, so we'll call matchExpectedFunKind, and unify
1286 kappa := kappa1 -> kappa2, with evidence co :: kappa ~ (kappa1 ~ kappa2)
1287 At this point we must zonk the function type to expose the arrrow, so
1288 that (a Int) will satisfy (PKTI).
1289
1290 The absence of this caused #14174 and #14520.
1291
1292 The calls to mkAppTyM is the other place we are very careful.
1293
1294 Note [mkAppTyM]
1295 ~~~~~~~~~~~~~~~
1296 mkAppTyM is trying to guarantee the Purely Kinded Type Invariant
1297 (PKTI) for its result type (fun arg). There are two ways it can go wrong:
1298
1299 * Nasty case 1: forall types (polykinds/T14174a)
1300 T :: forall (p :: *->*). p Int -> p Bool
1301 Now kind-check (T x), where x::kappa.
1302 Well, T and x both satisfy the PKTI, but
1303 T x :: x Int -> x Bool
1304 and (x Int) does /not/ satisfy the PKTI.
1305
1306 * Nasty case 2: type synonyms
1307 type S f a = f a
1308 Even though (S ff aa) would satisfy the (PKTI) if S was a data type
1309 (i.e. nasty case 1 is dealt with), it might still not satisfy (PKTI)
1310 if S is a type synonym, because the /expansion/ of (S ff aa) is
1311 (ff aa), and /that/ does not satisfy (PKTI). E.g. perhaps
1312 (ff :: kappa), where 'kappa' has already been unified with (*->*).
1313
1314 We check for nasty case 2 on the final argument of a type synonym.
1315
1316 Notice that in both cases the trickiness only happens if the
1317 bound variable has a pi-type. Hence isTrickyTvBinder.
1318 -}
1319
1320
1321 saturateFamApp :: TcType -> TcKind -> TcM (TcType, TcKind)
1322 -- Precondition for (saturateFamApp ty kind):
1323 -- tcTypeKind ty = kind
1324 --
1325 -- If 'ty' is an unsaturated family application wtih trailing
1326 -- invisible arguments, instanttiate them.
1327 -- See Note [saturateFamApp]
1328
1329 saturateFamApp ty kind
1330 | Just (tc, args) <- tcSplitTyConApp_maybe ty
1331 , mustBeSaturated tc
1332 , let n_to_inst = tyConArity tc - length args
1333 = do { (extra_args, ki') <- tcInstInvisibleTyBinders n_to_inst kind
1334 ; return (ty `mkTcAppTys` extra_args, ki') }
1335 | otherwise
1336 = return (ty, kind)
1337
1338 {- Note [saturateFamApp]
1339 ~~~~~~~~~~~~~~~~~~~~~~~~
1340 Consider
1341 type family F :: Either j k
1342 type instance F @Type = Right Maybe
1343 type instance F @Type = Right Either```
1344
1345 Then F :: forall {j,k}. Either j k
1346
1347 The two type instances do a visible kind application that instantiates
1348 'j' but not 'k'. But we want to end up with instances that look like
1349 type instance F @Type @(*->*) = Right @Type @(*->*) Maybe
1350
1351 so that F has arity 2. We must instantiate that trailing invisible
1352 binder. In general, Invisible binders precede Specified and Required,
1353 so this is only going to bite for apparently-nullary families.
1354
1355 Note that
1356 type family F2 :: forall k. k -> *
1357 is quite different and really does have arity 0.
1358
1359 It's not just type instances where we need to saturate those
1360 unsaturated arguments: see #11246. Hence doing this in tcInferApps.
1361 -}
1362
1363 appTypeToArg :: LHsType GhcRn -> [LHsTypeArg GhcRn] -> LHsType GhcRn
1364 appTypeToArg f [] = f
1365 appTypeToArg f (HsValArg arg : args) = appTypeToArg (mkHsAppTy f arg) args
1366 appTypeToArg f (HsArgPar _ : args) = appTypeToArg f args
1367 appTypeToArg f (HsTypeArg l arg : args)
1368 = appTypeToArg (mkHsAppKindTy l f arg) args
1369
1370
1371 {- *********************************************************************
1372 * *
1373 checkExpectedKind
1374 * *
1375 ********************************************************************* -}
1376
1377 -- | This instantiates invisible arguments for the type being checked if it must
1378 -- be saturated and is not yet saturated. It then calls and uses the result
1379 -- from checkExpectedKindX to build the final type
1380 checkExpectedKind :: HasDebugCallStack
1381 => HsType GhcRn -- ^ type we're checking (for printing)
1382 -> TcType -- ^ type we're checking
1383 -> TcKind -- ^ the known kind of that type
1384 -> TcKind -- ^ the expected kind
1385 -> TcM TcType
1386 -- Just a convenience wrapper to save calls to 'ppr'
1387 checkExpectedKind hs_ty ty act exp
1388 = checkExpectedKind_pp (ppr hs_ty) ty act exp
1389
1390 checkExpectedKind_pp :: HasDebugCallStack
1391 => SDoc -- ^ The thing we are checking
1392 -> TcType -- ^ type we're checking
1393 -> TcKind -- ^ the known kind of that type
1394 -> TcKind -- ^ the expected kind
1395 -> TcM TcType
1396 checkExpectedKind_pp pp_hs_ty ty act_kind exp_kind
1397 = do { traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind)
1398
1399 ; (new_args, act_kind') <- tcInstInvisibleTyBinders n_to_inst act_kind
1400
1401 ; let origin = TypeEqOrigin { uo_actual = act_kind'
1402 , uo_expected = exp_kind
1403 , uo_thing = Just pp_hs_ty
1404 , uo_visible = True } -- the hs_ty is visible
1405
1406 ; traceTc "checkExpectedKindX" $
1407 vcat [ pp_hs_ty
1408 , text "act_kind':" <+> ppr act_kind'
1409 , text "exp_kind:" <+> ppr exp_kind ]
1410
1411 ; let res_ty = ty `mkTcAppTys` new_args
1412
1413 ; if act_kind' `tcEqType` exp_kind
1414 then return res_ty -- This is very common
1415 else do { co_k <- uType KindLevel origin act_kind' exp_kind
1416 ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
1417 , ppr exp_kind
1418 , ppr co_k ])
1419 ; return (res_ty `mkTcCastTy` co_k) } }
1420 where
1421 -- We need to make sure that both kinds have the same number of implicit
1422 -- foralls out front. If the actual kind has more, instantiate accordingly.
1423 -- Otherwise, just pass the type & kind through: the errors are caught
1424 -- in unifyType.
1425 n_exp_invis_bndrs = invisibleTyBndrCount exp_kind
1426 n_act_invis_bndrs = invisibleTyBndrCount act_kind
1427 n_to_inst = n_act_invis_bndrs - n_exp_invis_bndrs
1428
1429
1430 ---------------------------
1431 tcHsMbContext :: Maybe (LHsContext GhcRn) -> TcM [PredType]
1432 tcHsMbContext Nothing = return []
1433 tcHsMbContext (Just cxt) = tcHsContext cxt
1434
1435 tcHsContext :: LHsContext GhcRn -> TcM [PredType]
1436 tcHsContext = tc_hs_context typeLevelMode
1437
1438 tcLHsPredType :: LHsType GhcRn -> TcM PredType
1439 tcLHsPredType = tc_lhs_pred typeLevelMode
1440
1441 tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
1442 tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)
1443
1444 tc_lhs_pred :: TcTyMode -> LHsType GhcRn -> TcM PredType
1445 tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
1446
1447 ---------------------------
1448 tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
1449 -- See Note [Type checking recursive type and class declarations]
1450 -- in TcTyClsDecls
1451 tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
1452 = do { traceTc "lk1" (ppr name)
1453 ; thing <- tcLookup name
1454 ; case thing of
1455 ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
1456
1457 ATcTyCon tc_tc
1458 -> do { -- See Note [GADT kind self-reference]
1459 unless (isTypeLevel (mode_level mode))
1460 (promotionErr name TyConPE)
1461 ; check_tc tc_tc
1462 ; return (mkTyConTy tc_tc, tyConKind tc_tc) }
1463
1464 AGlobal (ATyCon tc)
1465 -> do { check_tc tc
1466 ; return (mkTyConTy tc, tyConKind tc) }
1467
1468 AGlobal (AConLike (RealDataCon dc))
1469 -> do { data_kinds <- xoptM LangExt.DataKinds
1470 ; unless (data_kinds || specialPromotedDc dc) $
1471 promotionErr name NoDataKindsDC
1472 ; when (isFamInstTyCon (dataConTyCon dc)) $
1473 -- see #15245
1474 promotionErr name FamDataConPE
1475 ; let (_, _, _, theta, _, _) = dataConFullSig dc
1476 ; traceTc "tcTyVar" (ppr dc <+> ppr theta $$ ppr (dc_theta_illegal_constraint theta))
1477 ; case dc_theta_illegal_constraint theta of
1478 Just pred -> promotionErr name $
1479 ConstrainedDataConPE pred
1480 Nothing -> pure ()
1481 ; let tc = promoteDataCon dc
1482 ; return (mkTyConApp tc [], tyConKind tc) }
1483
1484 APromotionErr err -> promotionErr name err
1485
1486 _ -> wrongThingErr "type" thing name }
1487 where
1488 check_tc :: TyCon -> TcM ()
1489 check_tc tc = do { data_kinds <- xoptM LangExt.DataKinds
1490 ; unless (isTypeLevel (mode_level mode) ||
1491 data_kinds ||
1492 isKindTyCon tc) $
1493 promotionErr name NoDataKindsTC }
1494
1495 -- We cannot promote a data constructor with a context that contains
1496 -- constraints other than equalities, so error if we find one.
1497 -- See Note [Constraints in kinds] in TyCoRep
1498 dc_theta_illegal_constraint :: ThetaType -> Maybe PredType
1499 dc_theta_illegal_constraint = find (not . isEqPred)
1500
1501 {-
1502 Note [GADT kind self-reference]
1503 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1504
1505 A promoted type cannot be used in the body of that type's declaration.
1506 #11554 shows this example, which made GHC loop:
1507
1508 import Data.Kind
1509 data P (x :: k) = Q
1510 data A :: Type where
1511 B :: forall (a :: A). P a -> A
1512
1513 In order to check the constructor B, we need to have the promoted type A, but in
1514 order to get that promoted type, B must first be checked. To prevent looping, a
1515 TyConPE promotion error is given when tcTyVar checks an ATcTyCon in kind mode.
1516 Any ATcTyCon is a TyCon being defined in the current recursive group (see data
1517 type decl for TcTyThing), and all such TyCons are illegal in kinds.
1518
1519 #11962 proposes checking the head of a data declaration separately from
1520 its constructors. This would allow the example above to pass.
1521
1522 Note [Body kind of a HsForAllTy]
1523 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1524 The body of a forall is usually a type, but in principle
1525 there's no reason to prohibit *unlifted* types.
1526 In fact, GHC can itself construct a function with an
1527 unboxed tuple inside a for-all (via CPR analysis; see
1528 typecheck/should_compile/tc170).
1529
1530 Moreover in instance heads we get forall-types with
1531 kind Constraint.
1532
1533 It's tempting to check that the body kind is either * or #. But this is
1534 wrong. For example:
1535
1536 class C a b
1537 newtype N = Mk Foo deriving (C a)
1538
1539 We're doing newtype-deriving for C. But notice how `a` isn't in scope in
1540 the predicate `C a`. So we quantify, yielding `forall a. C a` even though
1541 `C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
1542 convenient. Bottom line: don't check for * or # here.
1543
1544 Note [Body kind of a HsQualTy]
1545 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1546 If ctxt is non-empty, the HsQualTy really is a /function/, so the
1547 kind of the result really is '*', and in that case the kind of the
1548 body-type can be lifted or unlifted.
1549
1550 However, consider
1551 instance Eq a => Eq [a] where ...
1552 or
1553 f :: (Eq a => Eq [a]) => blah
1554 Here both body-kind of the HsQualTy is Constraint rather than *.
1555 Rather crudely we tell the difference by looking at exp_kind. It's
1556 very convenient to typecheck instance types like any other HsSigType.
1557
1558 Admittedly the '(Eq a => Eq [a]) => blah' case is erroneous, but it's
1559 better to reject in checkValidType. If we say that the body kind
1560 should be '*' we risk getting TWO error messages, one saying that Eq
1561 [a] doens't have kind '*', and one saying that we need a Constraint to
1562 the left of the outer (=>).
1563
1564 How do we figure out the right body kind? Well, it's a bit of a
1565 kludge: I just look at the expected kind. If it's Constraint, we
1566 must be in this instance situation context. It's a kludge because it
1567 wouldn't work if any unification was involved to compute that result
1568 kind -- but it isn't. (The true way might be to use the 'mode'
1569 parameter, but that seemed like a sledgehammer to crack a nut.)
1570
1571 Note [Inferring tuple kinds]
1572 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1573 Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
1574 we try to figure out whether it's a tuple of kind * or Constraint.
1575 Step 1: look at the expected kind
1576 Step 2: infer argument kinds
1577
1578 If after Step 2 it's not clear from the arguments that it's
1579 Constraint, then it must be *. Once having decided that we re-check
1580 the arguments to give good error messages in
1581 e.g. (Maybe, Maybe)
1582
1583 Note that we will still fail to infer the correct kind in this case:
1584
1585 type T a = ((a,a), D a)
1586 type family D :: Constraint -> Constraint
1587
1588 While kind checking T, we do not yet know the kind of D, so we will default the
1589 kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
1590
1591 Note [Desugaring types]
1592 ~~~~~~~~~~~~~~~~~~~~~~~
1593 The type desugarer is phase 2 of dealing with HsTypes. Specifically:
1594
1595 * It transforms from HsType to Type
1596
1597 * It zonks any kinds. The returned type should have no mutable kind
1598 or type variables (hence returning Type not TcType):
1599 - any unconstrained kind variables are defaulted to (Any *) just
1600 as in TcHsSyn.
1601 - there are no mutable type variables because we are
1602 kind-checking a type
1603 Reason: the returned type may be put in a TyCon or DataCon where
1604 it will never subsequently be zonked.
1605
1606 You might worry about nested scopes:
1607 ..a:kappa in scope..
1608 let f :: forall b. T '[a,b] -> Int
1609 In this case, f's type could have a mutable kind variable kappa in it;
1610 and we might then default it to (Any *) when dealing with f's type
1611 signature. But we don't expect this to happen because we can't get a
1612 lexically scoped type variable with a mutable kind variable in it. A
1613 delicate point, this. If it becomes an issue we might need to
1614 distinguish top-level from nested uses.
1615
1616 Moreover
1617 * it cannot fail,
1618 * it does no unifications
1619 * it does no validity checking, except for structural matters, such as
1620 (a) spurious ! annotations.
1621 (b) a class used as a type
1622
1623 Note [Kind of a type splice]
1624 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1625 Consider these terms, each with TH type splice inside:
1626 [| e1 :: Maybe $(..blah..) |]
1627 [| e2 :: $(..blah..) |]
1628 When kind-checking the type signature, we'll kind-check the splice
1629 $(..blah..); we want to give it a kind that can fit in any context,
1630 as if $(..blah..) :: forall k. k.
1631
1632 In the e1 example, the context of the splice fixes kappa to *. But
1633 in the e2 example, we'll desugar the type, zonking the kind unification
1634 variables as we go. When we encounter the unconstrained kappa, we
1635 want to default it to '*', not to (Any *).
1636
1637 Help functions for type applications
1638 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1639 -}
1640
1641 addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
1642 -- Wrap a context around only if we want to show that contexts.
1643 -- Omit invisible ones and ones user's won't grok
1644 addTypeCtxt (L _ (HsWildCardTy _)) thing = thing -- "In the type '_'" just isn't helpful.
1645 addTypeCtxt (L _ ty) thing
1646 = addErrCtxt doc thing
1647 where
1648 doc = text "In the type" <+> quotes (ppr ty)
1649
1650 {-
1651 ************************************************************************
1652 * *
1653 Type-variable binders
1654 %* *
1655 %************************************************************************
1656
1657 Note [Keeping scoped variables in order: Explicit]
1658 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1659 When the user writes `forall a b c. blah`, we bring a, b, and c into
1660 scope and then check blah. In the process of checking blah, we might
1661 learn the kinds of a, b, and c, and these kinds might indicate that
1662 b depends on c, and thus that we should reject the user-written type.
1663
1664 One approach to doing this would be to bring each of a, b, and c into
1665 scope, one at a time, creating an implication constraint and
1666 bumping the TcLevel for each one. This would work, because the kind
1667 of, say, b would be untouchable when c is in scope (and the constraint
1668 couldn't float out because c blocks it). However, it leads to terrible
1669 error messages, complaining about skolem escape. While it is indeed
1670 a problem of skolem escape, we can do better.
1671
1672 Instead, our approach is to bring the block of variables into scope
1673 all at once, creating one implication constraint for the lot. The
1674 user-written variables are skolems in the implication constraint. In
1675 TcSimplify.setImplicationStatus, we check to make sure that the ordering
1676 is correct, choosing ImplicationStatus IC_BadTelescope if they aren't.
1677 Then, in TcErrors, we report if there is a bad telescope. This way,
1678 we can report a suggested ordering to the user if there is a problem.
1679
1680 See also Note [Checking telescopes] in Constraint
1681
1682 Note [Keeping scoped variables in order: Implicit]
1683 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1684 When the user implicitly quantifies over variables (say, in a type
1685 signature), we need to come up with some ordering on these variables.
1686 This is done by bumping the TcLevel, bringing the tyvars into scope,
1687 and then type-checking the thing_inside. The constraints are all
1688 wrapped in an implication, which is then solved. Finally, we can
1689 zonk all the binders and then order them with scopedSort.
1690
1691 It's critical to solve before zonking and ordering in order to uncover
1692 any unifications. You might worry that this eager solving could cause
1693 trouble elsewhere. I don't think it will. Because it will solve only
1694 in an increased TcLevel, it can't unify anything that was mentioned
1695 elsewhere. Additionally, we require that the order of implicitly
1696 quantified variables is manifest by the scope of these variables, so
1697 we're not going to learn more information later that will help order
1698 these variables.
1699
1700 Note [Recipe for checking a signature]
1701 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1702 Checking a user-written signature requires several steps:
1703
1704 1. Generate constraints.
1705 2. Solve constraints.
1706 3. Promote tyvars and/or kind-generalize.
1707 4. Zonk.
1708 5. Check validity.
1709
1710 There may be some surprises in here:
1711
1712 Step 2 is necessary for two reasons: most signatures also bring
1713 implicitly quantified variables into scope, and solving is necessary
1714 to get these in the right order (see Note [Keeping scoped variables in
1715 order: Implicit]). Additionally, solving is necessary in order to
1716 kind-generalize correctly: otherwise, we do not know which metavariables
1717 are left unsolved.
1718
1719 Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to
1720 kindGeneralize{All,Some,None}. Here, we have to deal with the fact that
1721 metatyvars generated in the type may have a bumped TcLevel, because explicit
1722 foralls raise the TcLevel. To avoid these variables from ever being visible in
1723 the surrounding context, we must obey the following dictum:
1724
1725 Every metavariable in a type must either be
1726 (A) generalized, or
1727 (B) promoted, or See Note [Promotion in signatures]
1728 (C) zapped to Any See Note [Naughty quantification candidates] in TcMType
1729
1730 The kindGeneralize functions do not require pre-zonking; they zonk as they
1731 go.
1732
1733 If you are actually doing kind-generalization, you need to bump the level
1734 before generating constraints, as we will only generalize variables with
1735 a TcLevel higher than the ambient one.
1736
1737 After promoting/generalizing, we need to zonk again because both
1738 promoting and generalizing fill in metavariables.
1739
1740 Note [Promotion in signatures]
1741 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1742 If an unsolved metavariable in a signature is not generalized
1743 (because we're not generalizing the construct -- e.g., pattern
1744 sig -- or because the metavars are constrained -- see kindGeneralizeSome)
1745 we need to promote to maintain (MetaTvInv) of Note [TcLevel and untouchable type variables]
1746 in TcType. Note that promotion is identical in effect to generalizing
1747 and the reinstantiating with a fresh metavariable at the current level.
1748 So in some sense, we generalize *all* variables, but then re-instantiate
1749 some of them.
1750
1751 Here is an example of why we must promote:
1752 foo (x :: forall a. a -> Proxy b) = ...
1753
1754 In the pattern signature, `b` is unbound, and will thus be brought into
1755 scope. We do not know its kind: it will be assigned kappa[2]. Note that
1756 kappa is at TcLevel 2, because it is invented under a forall. (A priori,
1757 the kind kappa might depend on `a`, so kappa rightly has a higher TcLevel
1758 than the surrounding context.) This kappa cannot be solved for while checking
1759 the pattern signature (which is not kind-generalized). When we are checking
1760 the *body* of foo, though, we need to unify the type of x with the argument
1761 type of bar. At this point, the ambient TcLevel is 1, and spotting a
1762 matavariable with level 2 would violate the (MetaTvInv) invariant of
1763 Note [TcLevel and untouchable type variables]. So, instead of kind-generalizing,
1764 we promote the metavariable to level 1. This is all done in kindGeneralizeNone.
1765
1766 -}
1767
1768 tcNamedWildCardBinders :: [Name]
1769 -> ([(Name, TcTyVar)] -> TcM a)
1770 -> TcM a
1771 -- Bring into scope the /named/ wildcard binders. Remember that
1772 -- plain wildcards _ are anonymous and dealt with by HsWildCardTy
1773 -- Soe Note [The wildcard story for types] in GHC.Hs.Types
1774 tcNamedWildCardBinders wc_names thing_inside
1775 = do { wcs <- mapM (const newWildTyVar) wc_names
1776 ; let wc_prs = wc_names `zip` wcs
1777 ; tcExtendNameTyVarEnv wc_prs $
1778 thing_inside wc_prs }
1779
1780 newWildTyVar :: TcM TcTyVar
1781 -- ^ New unification variable '_' for a wildcard
1782 newWildTyVar
1783 = do { kind <- newMetaKindVar
1784 ; uniq <- newUnique
1785 ; details <- newMetaDetails TauTv
1786 ; let name = mkSysTvName uniq (fsLit "_")
1787 tyvar = mkTcTyVar name kind details
1788 ; traceTc "newWildTyVar" (ppr tyvar)
1789 ; return tyvar }
1790
1791 {- *********************************************************************
1792 * *
1793 Kind inference for type declarations
1794 * *
1795 ********************************************************************* -}
1796
1797 -- See Note [kcCheckDeclHeader vs kcInferDeclHeader]
1798 data InitialKindStrategy
1799 = InitialKindCheck SAKS_or_CUSK
1800 | InitialKindInfer
1801
1802 -- Does the declaration have a standalone kind signature (SAKS) or a complete
1803 -- user-specified kind (CUSK)?
1804 data SAKS_or_CUSK
1805 = SAKS Kind -- Standalone kind signature, fully zonked! (zonkTcTypeToType)
1806 | CUSK -- Complete user-specified kind (CUSK)
1807
1808 instance Outputable SAKS_or_CUSK where
1809 ppr (SAKS k) = text "SAKS" <+> ppr k
1810 ppr CUSK = text "CUSK"
1811
1812 -- See Note [kcCheckDeclHeader vs kcInferDeclHeader]
1813 kcDeclHeader
1814 :: InitialKindStrategy
1815 -> Name -- ^ of the thing being checked
1816 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
1817 -> LHsQTyVars GhcRn -- ^ Binders in the header
1818 -> TcM ContextKind -- ^ The result kind
1819 -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon
1820 kcDeclHeader (InitialKindCheck msig) = kcCheckDeclHeader msig
1821 kcDeclHeader InitialKindInfer = kcInferDeclHeader
1822
1823 {- Note [kcCheckDeclHeader vs kcInferDeclHeader]
1824 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1825 kcCheckDeclHeader and kcInferDeclHeader are responsible for getting the initial kind
1826 of a type constructor.
1827
1828 * kcCheckDeclHeader: the TyCon has a standalone kind signature or a CUSK. In that
1829 case, find the full, final, poly-kinded kind of the TyCon. It's very like a
1830 term-level binding where we have a complete type signature for the function.
1831
1832 * kcInferDeclHeader: the TyCon has neither a standalone kind signature nor a
1833 CUSK. Find a monomorphic kind, with unification variables in it; they will be
1834 generalised later. It's very like a term-level binding where we do not have a
1835 type signature (or, more accurately, where we have a partial type signature),
1836 so we infer the type and generalise.
1837 -}
1838
1839 ------------------------------
1840 kcCheckDeclHeader
1841 :: SAKS_or_CUSK
1842 -> Name -- ^ of the thing being checked
1843 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
1844 -> LHsQTyVars GhcRn -- ^ Binders in the header
1845 -> TcM ContextKind -- ^ The result kind. AnyKind == no result signature
1846 -> TcM TcTyCon -- ^ A suitably-kinded generalized TcTyCon
1847 kcCheckDeclHeader (SAKS sig) = kcCheckDeclHeader_sig sig
1848 kcCheckDeclHeader CUSK = kcCheckDeclHeader_cusk
1849
1850 kcCheckDeclHeader_cusk
1851 :: Name -- ^ of the thing being checked
1852 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
1853 -> LHsQTyVars GhcRn -- ^ Binders in the header
1854 -> TcM ContextKind -- ^ The result kind
1855 -> TcM TcTyCon -- ^ A suitably-kinded generalized TcTyCon
1856 kcCheckDeclHeader_cusk name flav
1857 (HsQTvs { hsq_ext = kv_ns
1858 , hsq_explicit = hs_tvs }) kc_res_ki
1859 -- CUSK case
1860 -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
1861 = addTyConFlavCtxt name flav $
1862 do { (scoped_kvs, (tc_tvs, res_kind))
1863 <- pushTcLevelM_ $
1864 solveEqualities $
1865 bindImplicitTKBndrs_Q_Skol kv_ns $
1866 bindExplicitTKBndrs_Q_Skol ctxt_kind hs_tvs $
1867 newExpectedKind =<< kc_res_ki
1868
1869 -- Now, because we're in a CUSK,
1870 -- we quantify over the mentioned kind vars
1871 ; let spec_req_tkvs = scoped_kvs ++ tc_tvs
1872 all_kinds = res_kind : map tyVarKind spec_req_tkvs
1873
1874 ; candidates' <- candidateQTyVarsOfKinds all_kinds
1875 -- 'candidates' are all the variables that we are going to
1876 -- skolemise and then quantify over. We do not include spec_req_tvs
1877 -- because they are /already/ skolems
1878
1879 ; let non_tc_candidates = filter (not . isTcTyVar) (nonDetEltsUniqSet (tyCoVarsOfTypes all_kinds))
1880 candidates = candidates' { dv_kvs = dv_kvs candidates' `extendDVarSetList` non_tc_candidates }
1881 inf_candidates = candidates `delCandidates` spec_req_tkvs
1882
1883 ; inferred <- quantifyTyVars inf_candidates
1884 -- NB: 'inferred' comes back sorted in dependency order
1885
1886 ; scoped_kvs <- mapM zonkTyCoVarKind scoped_kvs
1887 ; tc_tvs <- mapM zonkTyCoVarKind tc_tvs
1888 ; res_kind <- zonkTcType res_kind
1889
1890 ; let mentioned_kv_set = candidateKindVars candidates
1891 specified = scopedSort scoped_kvs
1892 -- NB: maintain the L-R order of scoped_kvs
1893
1894 final_tc_binders = mkNamedTyConBinders Inferred inferred
1895 ++ mkNamedTyConBinders Specified specified
1896 ++ map (mkRequiredTyConBinder mentioned_kv_set) tc_tvs
1897
1898 all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
1899 tycon = mkTcTyCon name final_tc_binders res_kind all_tv_prs
1900 True -- it is generalised
1901 flav
1902 -- If the ordering from
1903 -- Note [Required, Specified, and Inferred for types] in TcTyClsDecls
1904 -- doesn't work, we catch it here, before an error cascade
1905 ; checkTyConTelescope tycon
1906
1907 ; traceTc "kcCheckDeclHeader_cusk " $
1908 vcat [ text "name" <+> ppr name
1909 , text "kv_ns" <+> ppr kv_ns
1910 , text "hs_tvs" <+> ppr hs_tvs
1911 , text "scoped_kvs" <+> ppr scoped_kvs
1912 , text "tc_tvs" <+> ppr tc_tvs
1913 , text "res_kind" <+> ppr res_kind
1914 , text "candidates" <+> ppr candidates
1915 , text "inferred" <+> ppr inferred
1916 , text "specified" <+> ppr specified
1917 , text "final_tc_binders" <+> ppr final_tc_binders
1918 , text "mkTyConKind final_tc_bndrs res_kind"
1919 <+> ppr (mkTyConKind final_tc_binders res_kind)
1920 , text "all_tv_prs" <+> ppr all_tv_prs ]
1921
1922 ; return tycon }
1923 where
1924 ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
1925 | otherwise = AnyKind
1926 kcCheckDeclHeader_cusk _ _ (XLHsQTyVars nec) _ = noExtCon nec
1927
1928 -- | Kind-check a 'LHsQTyVars'. Used in 'inferInitialKind' (for tycon kinds and
1929 -- other kinds).
1930 --
1931 -- This function does not do telescope checking.
1932 kcInferDeclHeader
1933 :: Name -- ^ of the thing being checked
1934 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
1935 -> LHsQTyVars GhcRn
1936 -> TcM ContextKind -- ^ The result kind
1937 -> TcM TcTyCon -- ^ A suitably-kinded non-generalized TcTyCon
1938 kcInferDeclHeader name flav
1939 (HsQTvs { hsq_ext = kv_ns
1940 , hsq_explicit = hs_tvs }) kc_res_ki
1941 -- No standalane kind signature and no CUSK.
1942 -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
1943 = do { (scoped_kvs, (tc_tvs, res_kind))
1944 -- Why bindImplicitTKBndrs_Q_Tv which uses newTyVarTyVar?
1945 -- See Note [Inferring kinds for type declarations] in TcTyClsDecls
1946 <- bindImplicitTKBndrs_Q_Tv kv_ns $
1947 bindExplicitTKBndrs_Q_Tv ctxt_kind hs_tvs $
1948 newExpectedKind =<< kc_res_ki
1949 -- Why "_Tv" not "_Skol"? See third wrinkle in
1950 -- Note [Inferring kinds for type declarations] in TcTyClsDecls,
1951
1952 ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they
1953 -- might unify with kind vars in other types in a mutually
1954 -- recursive group.
1955 -- See Note [Inferring kinds for type declarations] in TcTyClsDecls
1956
1957 tc_binders = mkAnonTyConBinders VisArg tc_tvs
1958 -- Also, note that tc_binders has the tyvars from only the
1959 -- user-written tyvarbinders. See S1 in Note [How TcTyCons work]
1960 -- in TcTyClsDecls
1961 --
1962 -- mkAnonTyConBinder: see Note [No polymorphic recursion]
1963
1964 all_tv_prs = (kv_ns `zip` scoped_kvs) ++
1965 (hsLTyVarNames hs_tvs `zip` tc_tvs)
1966 -- NB: bindIplicitTKBndrs_Q_Tv makes /freshly-named/ unification
1967 -- variables, hence the need to zip here. Ditto bindExplicit..
1968 -- See TcMType Note [Unification variables need fresh Names]
1969
1970 tycon = mkTcTyCon name tc_binders res_kind all_tv_prs
1971 False -- not yet generalised
1972 flav
1973
1974 ; traceTc "kcInferDeclHeader: not-cusk" $
1975 vcat [ ppr name, ppr kv_ns, ppr hs_tvs
1976 , ppr scoped_kvs
1977 , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ]
1978 ; return tycon }
1979 where
1980 ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
1981 | otherwise = AnyKind
1982
1983 kcInferDeclHeader _ _ (XLHsQTyVars nec) _ = noExtCon nec
1984
1985 -- | Kind-check a declaration header against a standalone kind signature.
1986 -- See Note [Arity inference in kcCheckDeclHeader_sig]
1987 kcCheckDeclHeader_sig
1988 :: Kind -- ^ Standalone kind signature, fully zonked! (zonkTcTypeToType)
1989 -> Name -- ^ of the thing being checked
1990 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
1991 -> LHsQTyVars GhcRn -- ^ Binders in the header
1992 -> TcM ContextKind -- ^ The result kind. AnyKind == no result signature
1993 -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon
1994 kcCheckDeclHeader_sig kisig name flav ktvs kc_res_ki =
1995 addTyConFlavCtxt name flav $
1996 pushTcLevelM_ $
1997 solveEqualities $ -- #16687
1998 bind_implicit (hsq_ext ktvs) $ \implicit_tcv_prs -> do
1999
2000 -- Step 1: zip user-written binders with quantifiers from the kind signature.
2001 -- For example:
2002 --
2003 -- type F :: forall k -> k -> forall j. j -> Type
2004 -- data F i a b = ...
2005 --
2006 -- Results in the following 'zipped_binders':
2007 --
2008 -- TyBinder LHsTyVarBndr
2009 -- ---------------------------------------
2010 -- ZippedBinder forall k -> i
2011 -- ZippedBinder k -> a
2012 -- ZippedBinder forall j.
2013 -- ZippedBinder j -> b
2014 --
2015 let (zipped_binders, excess_bndrs, kisig') = zipBinders kisig (hsq_explicit ktvs)
2016
2017 -- Report binders that don't have a corresponding quantifier.
2018 -- For example:
2019 --
2020 -- type T :: Type -> Type
2021 -- data T b1 b2 b3 = ...
2022 --
2023 -- Here, b1 is zipped with Type->, while b2 and b3 are excess binders.
2024 --
2025 unless (null excess_bndrs) $ failWithTc (tooManyBindersErr kisig' excess_bndrs)
2026
2027 -- Convert each ZippedBinder to TyConBinder for tyConBinders
2028 -- and to [(Name, TcTyVar)] for tcTyConScopedTyVars
2029 (vis_tcbs, concat -> explicit_tv_prs) <- mapAndUnzipM zipped_to_tcb zipped_binders
2030
2031 tcExtendNameTyVarEnv explicit_tv_prs $ do
2032
2033 -- Check that inline kind annotations on binders are valid.
2034 -- For example:
2035 --
2036 -- type T :: Maybe k -> Type
2037 -- data T (a :: Maybe j) = ...
2038 --
2039 -- Here we unify Maybe k ~ Maybe j
2040 mapM_ check_zipped_binder zipped_binders
2041
2042 -- Kind-check the result kind annotation, if present:
2043 --
2044 -- data T a b :: res_ki where
2045 -- ^^^^^^^^^
2046 -- We do it here because at this point the environment has been
2047 -- extended with both 'implicit_tcv_prs' and 'explicit_tv_prs'.
2048 m_res_ki <- kc_res_ki >>= \ctx_k ->
2049 case ctx_k of
2050 AnyKind -> return Nothing
2051 _ -> Just <$> newExpectedKind ctx_k
2052
2053 -- Step 2: split off invisible binders.
2054 -- For example:
2055 --
2056 -- type F :: forall k1 k2. (k1, k2) -> Type
2057 -- type family F
2058 --
2059 -- Does 'forall k1 k2' become a part of 'tyConBinders' or 'tyConResKind'?
2060 -- See Note [Arity inference in kcCheckDeclHeader_sig]
2061 let (invis_binders, r_ki) = split_invis kisig' m_res_ki
2062
2063 -- Convert each invisible TyCoBinder to TyConBinder for tyConBinders.
2064 invis_tcbs <- mapM invis_to_tcb invis_binders
2065
2066 -- Check that the inline result kind annotation is valid.
2067 -- For example:
2068 --
2069 -- type T :: Type -> Maybe k
2070 -- type family T a :: Maybe j where
2071 --
2072 -- Here we unify Maybe k ~ Maybe j
2073 whenIsJust m_res_ki $ \res_ki ->
2074 discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
2075 unifyKind Nothing r_ki res_ki
2076
2077 -- Zonk the implicitly quantified variables.
2078 implicit_tv_prs <- mapSndM zonkTcTyVarToTyVar implicit_tcv_prs
2079
2080 -- Build the final, generalized TcTyCon
2081 let tcbs = vis_tcbs ++ invis_tcbs
2082 all_tv_prs = implicit_tv_prs ++ explicit_tv_prs
2083 tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav
2084
2085 traceTc "kcCheckDeclHeader_sig done:" $ vcat
2086 [ text "tyConName = " <+> ppr (tyConName tc)
2087 , text "kisig =" <+> debugPprType kisig
2088 , text "tyConKind =" <+> debugPprType (tyConKind tc)
2089 , text "tyConBinders = " <+> ppr (tyConBinders tc)
2090 , text "tcTyConScopedTyVars" <+> ppr (tcTyConScopedTyVars tc)
2091 , text "tyConResKind" <+> debugPprType (tyConResKind tc)
2092 ]
2093 return tc
2094 where
2095 -- Consider this declaration:
2096 --
2097 -- type T :: forall a. forall b -> (a~b) => Proxy a -> Type
2098 -- data T x p = MkT
2099 --
2100 -- Here, we have every possible variant of ZippedBinder:
2101 --
2102 -- TyBinder LHsTyVarBndr
2103 -- ----------------------------------------------
2104 -- ZippedBinder forall {k}.
2105 -- ZippedBinder forall (a::k).
2106 -- ZippedBinder forall (b::k) -> x
2107 -- ZippedBinder (a~b) =>
2108 -- ZippedBinder Proxy a -> p
2109 --
2110 -- Given a ZippedBinder zipped_to_tcb produces:
2111 --
2112 -- * TyConBinder for tyConBinders
2113 -- * (Name, TcTyVar) for tcTyConScopedTyVars, if there's a user-written LHsTyVarBndr
2114 --
2115 zipped_to_tcb :: ZippedBinder -> TcM (TyConBinder, [(Name, TcTyVar)])
2116 zipped_to_tcb zb = case zb of
2117
2118 -- Inferred variable, no user-written binder.
2119 -- Example: forall {k}.
2120 ZippedBinder (Named (Bndr v Specified)) Nothing ->
2121 return (mkNamedTyConBinder Specified v, [])
2122
2123 -- Specified variable, no user-written binder.
2124 -- Example: forall (a::k).
2125 ZippedBinder (Named (Bndr v Inferred)) Nothing ->
2126 return (mkNamedTyConBinder Inferred v, [])
2127
2128 -- Constraint, no user-written binder.
2129 -- Example: (a~b) =>
2130 ZippedBinder (Anon InvisArg bndr_ki) Nothing -> do
2131 name <- newSysName (mkTyVarOccFS (fsLit "ev"))
2132 let tv = mkTyVar name bndr_ki
2133 return (mkAnonTyConBinder InvisArg tv, [])
2134
2135 -- Non-dependent visible argument with a user-written binder.
2136 -- Example: Proxy a ->
2137 ZippedBinder (Anon VisArg bndr_ki) (Just b) ->
2138 return $
2139 let v_name = getName b
2140 tv = mkTyVar v_name bndr_ki
2141 tcb = mkAnonTyConBinder VisArg tv
2142 in (tcb, [(v_name, tv)])
2143
2144 -- Dependent visible argument with a user-written binder.
2145 -- Example: forall (b::k) ->
2146 ZippedBinder (Named (Bndr v Required)) (Just b) ->
2147 return $
2148 let v_name = getName b
2149 tcb = mkNamedTyConBinder Required v
2150 in (tcb, [(v_name, v)])
2151
2152 -- 'zipBinders' does not produce any other variants of ZippedBinder.
2153 _ -> panic "goVis: invalid ZippedBinder"
2154
2155 -- Given an invisible binder that comes from 'split_invis',
2156 -- convert it to TyConBinder.
2157 invis_to_tcb :: TyCoBinder -> TcM TyConBinder
2158 invis_to_tcb tb = do
2159 (tcb, stv) <- zipped_to_tcb (ZippedBinder tb Nothing)
2160 MASSERT(null stv)
2161 return tcb
2162
2163 -- similar to: bindImplicitTKBndrs_Tv
2164 bind_implicit :: [Name] -> ([(Name,TcTyVar)] -> TcM a) -> TcM a
2165 bind_implicit tv_names thing_inside =
2166 do { let new_tv name = do { tcv <- newFlexiKindedTyVarTyVar name
2167 ; return (name, tcv) }
2168 ; tcvs <- mapM new_tv tv_names
2169 ; tcExtendNameTyVarEnv tcvs (thing_inside tcvs) }
2170
2171 -- Check that the inline kind annotation on a binder is valid
2172 -- by unifying it with the kind of the quantifier.
2173 check_zipped_binder :: ZippedBinder -> TcM ()
2174 check_zipped_binder (ZippedBinder _ Nothing) = return ()
2175 check_zipped_binder (ZippedBinder tb (Just b)) =
2176 case unLoc b of
2177 UserTyVar _ _ -> return ()
2178 KindedTyVar _ v v_hs_ki -> do
2179 v_ki <- tcLHsKindSig (TyVarBndrKindCtxt (unLoc v)) v_hs_ki
2180 discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
2181 unifyKind (Just (HsTyVar noExtField NotPromoted v))
2182 (tyBinderType tb)
2183 v_ki
2184 XTyVarBndr nec -> noExtCon nec
2185
2186 -- Split the invisible binders that should become a part of 'tyConBinders'
2187 -- rather than 'tyConResKind'.
2188 -- See Note [Arity inference in kcCheckDeclHeader_sig]
2189 split_invis :: Kind -> Maybe Kind -> ([TyCoBinder], Kind)
2190 split_invis sig_ki Nothing =
2191 -- instantiate all invisible binders
2192 splitPiTysInvisible sig_ki
2193 split_invis sig_ki (Just res_ki) =
2194 -- subtraction a la checkExpectedKind
2195 let n_res_invis_bndrs = invisibleTyBndrCount res_ki
2196 n_sig_invis_bndrs = invisibleTyBndrCount sig_ki
2197 n_inst = n_sig_invis_bndrs - n_res_invis_bndrs
2198 in splitPiTysInvisibleN n_inst sig_ki
2199
2200 -- A quantifier from a kind signature zipped with a user-written binder for it.
2201 data ZippedBinder =
2202 ZippedBinder TyBinder (Maybe (LHsTyVarBndr GhcRn))
2203
2204 -- See Note [Arity inference in kcCheckDeclHeader_sig]
2205 zipBinders
2206 :: Kind -- kind signature
2207 -> [LHsTyVarBndr GhcRn] -- user-written binders
2208 -> ([ZippedBinder], -- zipped binders
2209 [LHsTyVarBndr GhcRn], -- remaining user-written binders
2210 Kind) -- remainder of the kind signature
2211 zipBinders = zip_binders []
2212 where
2213 zip_binders acc ki [] = (reverse acc, [], ki)
2214 zip_binders acc ki (b:bs) =
2215 case tcSplitPiTy_maybe ki of
2216 Nothing -> (reverse acc, b:bs, ki)
2217 Just (tb, ki') ->
2218 let
2219 (zb, bs') | zippable = (ZippedBinder tb (Just b), bs)
2220 | otherwise = (ZippedBinder tb Nothing, b:bs)
2221 zippable =
2222 case tb of
2223 Named (Bndr _ Specified) -> False
2224 Named (Bndr _ Inferred) -> False
2225 Named (Bndr _ Required) -> True
2226 Anon InvisArg _ -> False
2227 Anon VisArg _ -> True
2228 in
2229 zip_binders (zb:acc) ki' bs'
2230
2231 tooManyBindersErr :: Kind -> [LHsTyVarBndr GhcRn] -> SDoc
2232 tooManyBindersErr ki bndrs =
2233 hang (text "Not a function kind:")
2234 4 (ppr ki) $$
2235 hang (text "but extra binders found:")
2236 4 (fsep (map ppr bndrs))
2237
2238 {- Note [Arity inference in kcCheckDeclHeader_sig]
2239 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2240 Given a kind signature 'kisig' and a declaration header, kcCheckDeclHeader_sig
2241 verifies that the declaration conforms to the signature. The end result is a
2242 TcTyCon 'tc' such that:
2243
2244 tyConKind tc == kisig
2245
2246 This TcTyCon would be rather easy to produce if we didn't have to worry about
2247 arity. Consider these declarations:
2248
2249 type family S1 :: forall k. k -> Type
2250 type family S2 (a :: k) :: Type
2251
2252 Both S1 and S2 can be given the same standalone kind signature:
2253
2254 type S2 :: forall k. k -> Type
2255
2256 And, indeed, tyConKind S1 == tyConKind S2. However, tyConKind is built from
2257 tyConBinders and tyConResKind, such that
2258
2259 tyConKind tc == mkTyConKind (tyConBinders tc) (tyConResKind tc)
2260
2261 For S1 and S2, tyConBinders and tyConResKind are different:
2262
2263 tyConBinders S1 == []
2264 tyConResKind S1 == forall k. k -> Type
2265 tyConKind S1 == forall k. k -> Type
2266
2267 tyConBinders S2 == [spec k, anon-vis (a :: k)]
2268 tyConResKind S2 == Type
2269 tyConKind S1 == forall k. k -> Type
2270
2271 This difference determines the arity:
2272
2273 tyConArity tc == length (tyConBinders tc)
2274
2275 That is, the arity of S1 is 0, while the arity of S2 is 2.
2276
2277 'kcCheckDeclHeader_sig' needs to infer the desired arity to split the standalone
2278 kind signature into binders and the result kind. It does so in two rounds:
2279
2280 1. zip user-written binders (vis_tcbs)
2281 2. split off invisible binders (invis_tcbs)
2282
2283 Consider the following declarations:
2284
2285 type F :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
2286 type family F a b
2287
2288 type G :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
2289 type family G a b :: forall r2. (r1, r2) -> Type
2290
2291 In step 1 (zip user-written binders), we zip the quantifiers in the signature
2292 with the binders in the header using 'zipBinders'. In both F and G, this results in
2293 the following zipped binders:
2294
2295 TyBinder LHsTyVarBndr
2296 ---------------------------------------
2297 ZippedBinder Type -> a
2298 ZippedBinder forall j.
2299 ZippedBinder j -> b
2300
2301
2302 At this point, we have accumulated three zipped binders which correspond to a
2303 prefix of the standalone kind signature:
2304
2305 Type -> forall j. j -> ...
2306
2307 In step 2 (split off invisible binders), we have to decide how much remaining
2308 invisible binders of the standalone kind signature to split off:
2309
2310 forall k1 k2. (k1, k2) -> Type
2311 ^^^^^^^^^^^^^
2312 split off or not?
2313
2314 This decision is made in 'split_invis':
2315
2316 * If a user-written result kind signature is not provided, as in F,
2317 then split off all invisible binders. This is why we need special treatment
2318 for AnyKind.
2319 * If a user-written result kind signature is provided, as in G,
2320 then do as checkExpectedKind does and split off (n_sig - n_res) binders.
2321 That is, split off such an amount of binders that the remainder of the
2322 standalone kind signature and the user-written result kind signature have the
2323 same amount of invisible quantifiers.
2324
2325 For F, split_invis splits away all invisible binders, and we have 2:
2326
2327 forall k1 k2. (k1, k2) -> Type
2328 ^^^^^^^^^^^^^
2329 split away both binders
2330
2331 The resulting arity of F is 3+2=5. (length vis_tcbs = 3,
2332 length invis_tcbs = 2,
2333 length tcbs = 5)
2334
2335 For G, split_invis decides to split off 1 invisible binder, so that we have the
2336 same amount of invisible quantifiers left:
2337
2338 res_ki = forall r2. (r1, r2) -> Type
2339 kisig = forall k1 k2. (k1, k2) -> Type
2340 ^^^
2341 split off this one.
2342
2343 The resulting arity of G is 3+1=4. (length vis_tcbs = 3,
2344 length invis_tcbs = 1,
2345 length tcbs = 4)
2346
2347 -}
2348
2349 {- Note [discardResult in kcCheckDeclHeader_sig]
2350 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2351 We use 'unifyKind' to check inline kind annotations in declaration headers
2352 against the signature.
2353
2354 type T :: [i] -> Maybe j -> Type
2355 data T (a :: [k1]) (b :: Maybe k2) :: Type where ...
2356
2357 Here, we will unify:
2358
2359 [k1] ~ [i]
2360 Maybe k2 ~ Maybe j
2361 Type ~ Type
2362
2363 The end result is that we fill in unification variables k1, k2:
2364
2365 k1 := i
2366 k2 := j
2367
2368 We also validate that the user isn't confused:
2369
2370 type T :: Type -> Type
2371 data T (a :: Bool) = ...
2372
2373 This will report that (Type ~ Bool) failed to unify.
2374
2375 Now, consider the following example:
2376
2377 type family Id a where Id x = x
2378 type T :: Bool -> Type
2379 type T (a :: Id Bool) = ...
2380
2381 We will unify (Bool ~ Id Bool), and this will produce a non-reflexive coercion.
2382 However, we are free to discard it, as the kind of 'T' is determined by the
2383 signature, not by the inline kind annotation:
2384
2385 we have T :: Bool -> Type
2386 rather than T :: Id Bool -> Type
2387
2388 This (Id Bool) will not show up anywhere after we're done validating it, so we
2389 have no use for the produced coercion.
2390 -}
2391
2392 {- Note [No polymorphic recursion]
2393 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2394 Should this kind-check?
2395 data T ka (a::ka) b = MkT (T Type Int Bool)
2396 (T (Type -> Type) Maybe Bool)
2397
2398 Notice that T is used at two different kinds in its RHS. No!
2399 This should not kind-check. Polymorphic recursion is known to
2400 be a tough nut.
2401
2402 Previously, we laboriously (with help from the renamer)
2403 tried to give T the polymoprhic kind
2404 T :: forall ka -> ka -> kappa -> Type
2405 where kappa is a unification variable, even in the inferInitialKinds
2406 phase (which is what kcInferDeclHeader is all about). But
2407 that is dangerously fragile (see the ticket).
2408
2409 Solution: make kcInferDeclHeader give T a straightforward
2410 monomorphic kind, with no quantification whatsoever. That's why
2411 we use mkAnonTyConBinder for all arguments when figuring out
2412 tc_binders.
2413
2414 But notice that (#16322 comment:3)
2415
2416 * The algorithm successfully kind-checks this declaration:
2417 data T2 ka (a::ka) = MkT2 (T2 Type a)
2418
2419 Starting with (inferInitialKinds)
2420 T2 :: (kappa1 :: kappa2 :: *) -> (kappa3 :: kappa4 :: *) -> *
2421 we get
2422 kappa4 := kappa1 -- from the (a:ka) kind signature
2423 kappa1 := Type -- From application T2 Type
2424
2425 These constraints are soluble so generaliseTcTyCon gives
2426 T2 :: forall (k::Type) -> k -> *
2427
2428 But now the /typechecking/ (aka desugaring, tcTyClDecl) phase
2429 fails, because the call (T2 Type a) in the RHS is ill-kinded.
2430
2431 We'd really prefer all errors to show up in the kind checking
2432 phase.
2433
2434 * This algorithm still accepts (in all phases)
2435 data T3 ka (a::ka) = forall b. MkT3 (T3 Type b)
2436 although T3 is really polymorphic-recursive too.
2437 Perhaps we should somehow reject that.
2438
2439 Note [Kind-checking tyvar binders for associated types]
2440 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2441 When kind-checking the type-variable binders for associated
2442 data/newtype decls
2443 family decls
2444 we behave specially for type variables that are already in scope;
2445 that is, bound by the enclosing class decl. This is done in
2446 kcLHsQTyVarBndrs:
2447 * The use of tcImplicitQTKBndrs
2448 * The tcLookupLocal_maybe code in kc_hs_tv
2449
2450 See Note [Associated type tyvar names] in Class and
2451 Note [TyVar binders for associated decls] in GHC.Hs.Decls
2452
2453 We must do the same for family instance decls, where the in-scope
2454 variables may be bound by the enclosing class instance decl.
2455 Hence the use of tcImplicitQTKBndrs in tcFamTyPatsAndGen.
2456
2457 Note [Kind variable ordering for associated types]
2458 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2459 What should be the kind of `T` in the following example? (#15591)
2460
2461 class C (a :: Type) where
2462 type T (x :: f a)
2463
2464 As per Note [Ordering of implicit variables] in RnTypes, we want to quantify
2465 the kind variables in left-to-right order of first occurrence in order to
2466 support visible kind application. But we cannot perform this analysis on just
2467 T alone, since its variable `a` actually occurs /before/ `f` if you consider
2468 the fact that `a` was previously bound by the parent class `C`. That is to say,
2469 the kind of `T` should end up being:
2470
2471 T :: forall a f. f a -> Type
2472
2473 (It wouldn't necessarily be /wrong/ if the kind ended up being, say,
2474 forall f a. f a -> Type, but that would not be as predictable for users of
2475 visible kind application.)
2476
2477 In contrast, if `T` were redefined to be a top-level type family, like `T2`
2478 below:
2479
2480 type family T2 (x :: f (a :: Type))
2481
2482 Then `a` first appears /after/ `f`, so the kind of `T2` should be:
2483
2484 T2 :: forall f a. f a -> Type
2485
2486 In order to make this distinction, we need to know (in kcCheckDeclHeader) which
2487 type variables have been bound by the parent class (if there is one). With
2488 the class-bound variables in hand, we can ensure that we always quantify
2489 these first.
2490 -}
2491
2492
2493 {- *********************************************************************
2494 * *
2495 Expected kinds
2496 * *
2497 ********************************************************************* -}
2498
2499 -- | Describes the kind expected in a certain context.
2500 data ContextKind = TheKind Kind -- ^ a specific kind
2501 | AnyKind -- ^ any kind will do
2502 | OpenKind -- ^ something of the form @TYPE _@
2503
2504 -----------------------
2505 newExpectedKind :: ContextKind -> TcM Kind
2506 newExpectedKind (TheKind k) = return k
2507 newExpectedKind AnyKind = newMetaKindVar
2508 newExpectedKind OpenKind = newOpenTypeKind
2509
2510 -----------------------
2511 expectedKindInCtxt :: UserTypeCtxt -> ContextKind
2512 -- Depending on the context, we might accept any kind (for instance, in a TH
2513 -- splice), or only certain kinds (like in type signatures).
2514 expectedKindInCtxt (TySynCtxt _) = AnyKind
2515 expectedKindInCtxt ThBrackCtxt = AnyKind
2516 expectedKindInCtxt (GhciCtxt {}) = AnyKind
2517 -- The types in a 'default' decl can have varying kinds
2518 -- See Note [Extended defaults]" in TcEnv
2519 expectedKindInCtxt DefaultDeclCtxt = AnyKind
2520 expectedKindInCtxt TypeAppCtxt = AnyKind
2521 expectedKindInCtxt (ForSigCtxt _) = TheKind liftedTypeKind
2522 expectedKindInCtxt (InstDeclCtxt {}) = TheKind constraintKind
2523 expectedKindInCtxt SpecInstCtxt = TheKind constraintKind
2524 expectedKindInCtxt _ = OpenKind
2525
2526
2527 {- *********************************************************************
2528 * *
2529 Bringing type variables into scope
2530 * *
2531 ********************************************************************* -}
2532
2533 --------------------------------------
2534 -- Implicit binders
2535 --------------------------------------
2536
2537 bindImplicitTKBndrs_Skol, bindImplicitTKBndrs_Tv,
2538 bindImplicitTKBndrs_Q_Skol, bindImplicitTKBndrs_Q_Tv
2539 :: [Name] -> TcM a -> TcM ([TcTyVar], a)
2540 bindImplicitTKBndrs_Skol = bindImplicitTKBndrsX newFlexiKindedSkolemTyVar
2541 bindImplicitTKBndrs_Tv = bindImplicitTKBndrsX newFlexiKindedTyVarTyVar
2542 bindImplicitTKBndrs_Q_Skol = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedSkolemTyVar)
2543 bindImplicitTKBndrs_Q_Tv = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedTyVarTyVar)
2544
2545 bindImplicitTKBndrsX
2546 :: (Name -> TcM TcTyVar) -- new_tv function
2547 -> [Name]
2548 -> TcM a
2549 -> TcM ([TcTyVar], a) -- Returned [TcTyVar] are in 1-1 correspondence
2550 -- with the passed in [Name]
2551 bindImplicitTKBndrsX new_tv tv_names thing_inside
2552 = do { tkvs <- mapM new_tv tv_names
2553 ; traceTc "bindImplicitTKBndrs" (ppr tv_names $$ ppr tkvs)
2554 ; res <- tcExtendNameTyVarEnv (tv_names `zip` tkvs)
2555 thing_inside
2556 ; return (tkvs, res) }
2557
2558 newImplicitTyVarQ :: (Name -> TcM TcTyVar) -> Name -> TcM TcTyVar
2559 -- Behave like new_tv, except that if the tyvar is in scope, use it
2560 newImplicitTyVarQ new_tv name
2561 = do { mb_tv <- tcLookupLcl_maybe name
2562 ; case mb_tv of
2563 Just (ATyVar _ tv) -> return tv
2564 _ -> new_tv name }
2565
2566 newFlexiKindedTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM TyVar
2567 newFlexiKindedTyVar new_tv name
2568 = do { kind <- newMetaKindVar
2569 ; new_tv name kind }
2570
2571 newFlexiKindedSkolemTyVar :: Name -> TcM TyVar
2572 newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar
2573
2574 newFlexiKindedTyVarTyVar :: Name -> TcM TyVar
2575 newFlexiKindedTyVarTyVar = newFlexiKindedTyVar newTyVarTyVar
2576 -- See Note [Unification variables need fresh Names] in TcMType
2577
2578 --------------------------------------
2579 -- Explicit binders
2580 --------------------------------------
2581
2582 bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv
2583 :: [LHsTyVarBndr GhcRn]
2584 -> TcM a
2585 -> TcM ([TcTyVar], a)
2586
2587 bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr newSkolemTyVar)
2588 bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr newTyVarTyVar)
2589
2590 bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Q_Tv
2591 :: ContextKind
2592 -> [LHsTyVarBndr GhcRn]
2593 -> TcM a
2594 -> TcM ([TcTyVar], a)
2595
2596 bindExplicitTKBndrs_Q_Skol ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newSkolemTyVar)
2597 bindExplicitTKBndrs_Q_Tv ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newTyVarTyVar)
2598
2599 bindExplicitTKBndrsX
2600 :: (HsTyVarBndr GhcRn -> TcM TcTyVar)
2601 -> [LHsTyVarBndr GhcRn]
2602 -> TcM a
2603 -> TcM ([TcTyVar], a) -- Returned [TcTyVar] are in 1-1 correspondence
2604 -- with the passed-in [LHsTyVarBndr]
2605 bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
2606 = do { traceTc "bindExplicTKBndrs" (ppr hs_tvs)
2607 ; go hs_tvs }
2608 where
2609 go [] = do { res <- thing_inside
2610 ; return ([], res) }
2611 go (L _ hs_tv : hs_tvs)
2612 = do { tv <- tc_tv hs_tv
2613 -- Extend the environment as we go, in case a binder
2614 -- is mentioned in the kind of a later binder
2615 -- e.g. forall k (a::k). blah
2616 -- NB: tv's Name may differ from hs_tv's
2617 -- See TcMType Note [Unification variables need fresh Names]
2618 ; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $
2619 go hs_tvs
2620 ; return (tv:tvs, res) }
2621
2622 -----------------
2623 tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
2624 -> HsTyVarBndr GhcRn -> TcM TcTyVar
2625 -- Returned TcTyVar has the same name; no cloning
2626 tcHsTyVarBndr new_tv (UserTyVar _ (L _ tv_nm))
2627 = do { kind <- newMetaKindVar
2628 ; new_tv tv_nm kind }
2629 tcHsTyVarBndr new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
2630 = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
2631 ; new_tv tv_nm kind }
2632 tcHsTyVarBndr _ (XTyVarBndr nec) = noExtCon nec
2633
2634 -----------------
2635 tcHsQTyVarBndr :: ContextKind
2636 -> (Name -> Kind -> TcM TyVar)
2637 -> HsTyVarBndr GhcRn -> TcM TcTyVar
2638 -- Just like tcHsTyVarBndr, but also
2639 -- - uses the in-scope TyVar from class, if it exists
2640 -- - takes a ContextKind to use for the no-sig case
2641 tcHsQTyVarBndr ctxt_kind new_tv (UserTyVar _ (L _ tv_nm))
2642 = do { mb_tv <- tcLookupLcl_maybe tv_nm
2643 ; case mb_tv of
2644 Just (ATyVar _ tv) -> return tv
2645 _ -> do { kind <- newExpectedKind ctxt_kind
2646 ; new_tv tv_nm kind } }
2647
2648 tcHsQTyVarBndr _ new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
2649 = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
2650 ; mb_tv <- tcLookupLcl_maybe tv_nm
2651 ; case mb_tv of
2652 Just (ATyVar _ tv)
2653 -> do { discardResult $ unifyKind (Just hs_tv)
2654 kind (tyVarKind tv)
2655 -- This unify rejects:
2656 -- class C (m :: * -> *) where
2657 -- type F (m :: *) = ...
2658 ; return tv }
2659
2660 _ -> new_tv tv_nm kind }
2661 where
2662 hs_tv = HsTyVar noExtField NotPromoted (noLoc tv_nm)
2663 -- Used for error messages only
2664
2665 tcHsQTyVarBndr _ _ (XTyVarBndr nec) = noExtCon nec
2666
2667 --------------------------------------
2668 -- Binding type/class variables in the
2669 -- kind-checking and typechecking phases
2670 --------------------------------------
2671
2672 bindTyClTyVars :: Name
2673 -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
2674 -- ^ Used for the type variables of a type or class decl
2675 -- in the "kind checking" and "type checking" pass,
2676 -- but not in the initial-kind run.
2677 bindTyClTyVars tycon_name thing_inside
2678 = do { tycon <- kcLookupTcTyCon tycon_name
2679 ; let scoped_prs = tcTyConScopedTyVars tycon
2680 res_kind = tyConResKind tycon
2681 binders = tyConBinders tycon
2682 ; traceTc "bindTyClTyVars" (ppr tycon_name <+> ppr binders $$ ppr scoped_prs)
2683 ; tcExtendNameTyVarEnv scoped_prs $
2684 thing_inside binders res_kind }
2685
2686 -- inferInitialKind has made a suitably-shaped kind for the type or class
2687 -- Look it up in the local environment. This is used only for tycons
2688 -- that we're currently type-checking, so we're sure to find a TcTyCon.
2689 kcLookupTcTyCon :: Name -> TcM TcTyCon
2690 kcLookupTcTyCon nm
2691 = do { tc_ty_thing <- tcLookup nm
2692 ; return $ case tc_ty_thing of
2693 ATcTyCon tc -> tc
2694 _ -> pprPanic "kcLookupTcTyCon" (ppr tc_ty_thing) }
2695
2696
2697 {- *********************************************************************
2698 * *
2699 Kind generalisation
2700 * *
2701 ********************************************************************* -}
2702
2703 zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
2704 zonkAndScopedSort spec_tkvs
2705 = do { spec_tkvs <- mapM zonkAndSkolemise spec_tkvs
2706 -- Use zonkAndSkolemise because a skol_tv might be a TyVarTv
2707
2708 -- Do a stable topological sort, following
2709 -- Note [Ordering of implicit variables] in RnTypes
2710 ; return (scopedSort spec_tkvs) }
2711
2712 -- | Generalize some of the free variables in the given type.
2713 -- All such variables should be *kind* variables; any type variables
2714 -- should be explicitly quantified (with a `forall`) before now.
2715 -- The supplied predicate says which free variables to quantify.
2716 -- But in all cases,
2717 -- generalize only those variables whose TcLevel is strictly greater
2718 -- than the ambient level. This "strictly greater than" means that
2719 -- you likely need to push the level before creating whatever type
2720 -- gets passed here. Any variable whose level is greater than the
2721 -- ambient level but is not selected to be generalized will be
2722 -- promoted. (See [Promoting unification variables] in TcSimplify
2723 -- and Note [Recipe for checking a signature].)
2724 -- The resulting KindVar are the variables to
2725 -- quantify over, in the correct, well-scoped order. They should
2726 -- generally be Inferred, not Specified, but that's really up to
2727 -- the caller of this function.
2728 kindGeneralizeSome :: (TcTyVar -> Bool)
2729 -> TcType -- ^ needn't be zonked
2730 -> TcM [KindVar]
2731 kindGeneralizeSome should_gen kind_or_type
2732 = do { traceTc "kindGeneralizeSome {" (ppr kind_or_type)
2733
2734 -- use the "Kind" variant here, as any types we see
2735 -- here will already have all type variables quantified;
2736 -- thus, every free variable is really a kv, never a tv.
2737 ; dvs <- candidateQTyVarsOfKind kind_or_type
2738
2739 -- So 'dvs' are the variables free in kind_or_type, with a level greater
2740 -- than the ambient level, hence candidates for quantification
2741 -- Next: filter out the ones we don't want to generalize (specified by should_gen)
2742 -- and promote them instead
2743
2744 ; let (to_promote, dvs') = partitionCandidates dvs (not . should_gen)
2745
2746 ; (_, promoted) <- promoteTyVarSet (dVarSetToVarSet to_promote)
2747 ; qkvs <- quantifyTyVars dvs'
2748
2749 ; traceTc "kindGeneralizeSome }" $
2750 vcat [ text "Kind or type:" <+> ppr kind_or_type
2751 , text "dvs:" <+> ppr dvs
2752 , text "dvs':" <+> ppr dvs'
2753 , text "to_promote:" <+> pprTyVars (dVarSetElems to_promote)
2754 , text "promoted:" <+> pprTyVars (nonDetEltsUniqSet promoted)
2755 , text "qkvs:" <+> pprTyVars qkvs ]
2756
2757 ; return qkvs }
2758
2759 -- | Specialized version of 'kindGeneralizeSome', but where all variables
2760 -- can be generalized. Use this variant when you can be sure that no more
2761 -- constraints on the type's metavariables will arise or be solved.
2762 kindGeneralizeAll :: TcType -- needn't be zonked
2763 -> TcM [KindVar]
2764 kindGeneralizeAll ty = do { traceTc "kindGeneralizeAll" empty
2765 ; kindGeneralizeSome (const True) ty }
2766
2767 -- | Specialized version of 'kindGeneralizeSome', but where no variables
2768 -- can be generalized. Use this variant when it is unknowable whether metavariables
2769 -- might later be constrained.
2770 -- See Note [Recipe for checking a signature] for why and where this
2771 -- function is needed.
2772 kindGeneralizeNone :: TcType -- needn't be zonked
2773 -> TcM ()
2774 kindGeneralizeNone ty
2775 = do { traceTc "kindGeneralizeNone" empty
2776 ; kvs <- kindGeneralizeSome (const False) ty
2777 ; MASSERT( null kvs )
2778 }
2779
2780 {- Note [Levels and generalisation]
2781 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2782 Consider
2783 f x = e
2784 with no type signature. We are currently at level i.
2785 We must
2786 * Push the level to level (i+1)
2787 * Allocate a fresh alpha[i+1] for the result type
2788 * Check that e :: alpha[i+1], gathering constraint WC
2789 * Solve WC as far as possible
2790 * Zonking the result type alpha[i+1], say to beta[i-1] -> gamma[i]
2791 * Find the free variables with level > i, in this case gamma[i]
2792 * Skolemise those free variables and quantify over them, giving
2793 f :: forall g. beta[i-1] -> g
2794 * Emit the residiual constraint wrapped in an implication for g,
2795 thus forall g. WC
2796
2797 All of this happens for types too. Consider
2798 f :: Int -> (forall a. Proxy a -> Int)
2799
2800 Note [Kind generalisation]
2801 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2802 We do kind generalisation only at the outer level of a type signature.
2803 For example, consider
2804 T :: forall k. k -> *
2805 f :: (forall a. T a -> Int) -> Int
2806 When kind-checking f's type signature we generalise the kind at
2807 the outermost level, thus:
2808 f1 :: forall k. (forall (a:k). T k a -> Int) -> Int -- YES!
2809 and *not* at the inner forall:
2810 f2 :: (forall k. forall (a:k). T k a -> Int) -> Int -- NO!
2811 Reason: same as for HM inference on value level declarations,
2812 we want to infer the most general type. The f2 type signature
2813 would be *less applicable* than f1, because it requires a more
2814 polymorphic argument.
2815
2816 NB: There are no explicit kind variables written in f's signature.
2817 When there are, the renamer adds these kind variables to the list of
2818 variables bound by the forall, so you can indeed have a type that's
2819 higher-rank in its kind. But only by explicit request.
2820
2821 Note [Kinds of quantified type variables]
2822 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2823 tcTyVarBndrsGen quantifies over a specified list of type variables,
2824 *and* over the kind variables mentioned in the kinds of those tyvars.
2825
2826 Note that we must zonk those kinds (obviously) but less obviously, we
2827 must return type variables whose kinds are zonked too. Example
2828 (a :: k7) where k7 := k9 -> k9
2829 We must return
2830 [k9, a:k9->k9]
2831 and NOT
2832 [k9, a:k7]
2833 Reason: we're going to turn this into a for-all type,
2834 forall k9. forall (a:k7). blah
2835 which the type checker will then instantiate, and instantiate does not
2836 look through unification variables!
2837
2838 Hence using zonked_kinds when forming tvs'.
2839
2840 -}
2841
2842 -----------------------------------
2843 etaExpandAlgTyCon :: [TyConBinder]
2844 -> Kind
2845 -> TcM ([TyConBinder], Kind)
2846 -- GADT decls can have a (perhaps partial) kind signature
2847 -- e.g. data T a :: * -> * -> * where ...
2848 -- This function makes up suitable (kinded) TyConBinders for the
2849 -- argument kinds. E.g. in this case it might return
2850 -- ([b::*, c::*], *)
2851 -- Never emits constraints.
2852 -- It's a little trickier than you might think: see
2853 -- Note [TyConBinders for the result kind signature of a data type]
2854 etaExpandAlgTyCon tc_bndrs kind
2855 = do { loc <- getSrcSpanM
2856 ; uniqs <- newUniqueSupply
2857 ; rdr_env <- getLocalRdrEnv
2858 ; let new_occs = [ occ
2859 | str <- allNameStrings
2860 , let occ = mkOccName tvName str
2861 , isNothing (lookupLocalRdrOcc rdr_env occ)
2862 -- Note [Avoid name clashes for associated data types]
2863 , not (occ `elem` lhs_occs) ]
2864 new_uniqs = uniqsFromSupply uniqs
2865 subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet lhs_tvs))
2866 ; return (go loc new_occs new_uniqs subst [] kind) }
2867 where
2868 lhs_tvs = map binderVar tc_bndrs
2869 lhs_occs = map getOccName lhs_tvs
2870
2871 go loc occs uniqs subst acc kind
2872 = case splitPiTy_maybe kind of
2873 Nothing -> (reverse acc, substTy subst kind)
2874
2875 Just (Anon af arg, kind')
2876 -> go loc occs' uniqs' subst' (tcb : acc) kind'
2877 where
2878 arg' = substTy subst arg
2879 tv = mkTyVar (mkInternalName uniq occ loc) arg'
2880 subst' = extendTCvInScope subst tv
2881 tcb = Bndr tv (AnonTCB af)
2882 (uniq:uniqs') = uniqs
2883 (occ:occs') = occs
2884
2885 Just (Named (Bndr tv vis), kind')
2886 -> go loc occs uniqs subst' (tcb : acc) kind'
2887 where
2888 (subst', tv') = substTyVarBndr subst tv
2889 tcb = Bndr tv' (NamedTCB vis)
2890
2891 -- | A description of whether something is a
2892 --
2893 -- * @data@ or @newtype@ ('DataDeclSort')
2894 --
2895 -- * @data instance@ or @newtype instance@ ('DataInstanceSort')
2896 --
2897 -- * @data family@ ('DataFamilySort')
2898 --
2899 -- At present, this data type is only consumed by 'checkDataKindSig'.
2900 data DataSort
2901 = DataDeclSort NewOrData
2902 | DataInstanceSort NewOrData
2903 | DataFamilySort
2904
2905 -- | Checks that the return kind in a data declaration's kind signature is
2906 -- permissible. There are three cases:
2907 --
2908 -- If dealing with a @data@, @newtype@, @data instance@, or @newtype instance@
2909 -- declaration, check that the return kind is @Type@.
2910 --
2911 -- If the declaration is a @newtype@ or @newtype instance@ and the
2912 -- @UnliftedNewtypes@ extension is enabled, this check is slightly relaxed so
2913 -- that a return kind of the form @TYPE r@ (for some @r@) is permitted.
2914 -- See @Note [Implementation of UnliftedNewtypes]@ in "TcTyClsDecls".
2915 --
2916 -- If dealing with a @data family@ declaration, check that the return kind is
2917 -- either of the form:
2918 --
2919 -- 1. @TYPE r@ (for some @r@), or
2920 --
2921 -- 2. @k@ (where @k@ is a bare kind variable; see #12369)
2922 checkDataKindSig :: DataSort -> Kind -> TcM ()
2923 checkDataKindSig data_sort kind = do
2924 dflags <- getDynFlags
2925 checkTc (is_TYPE_or_Type dflags || is_kind_var) (err_msg dflags)
2926 where
2927 pp_dec :: SDoc
2928 pp_dec = text $
2929 case data_sort of
2930 DataDeclSort DataType -> "data type"
2931 DataDeclSort NewType -> "newtype"
2932 DataInstanceSort DataType -> "data instance"
2933 DataInstanceSort NewType -> "newtype instance"
2934 DataFamilySort -> "data family"
2935
2936 is_newtype :: Bool
2937 is_newtype =
2938 case data_sort of
2939 DataDeclSort new_or_data -> new_or_data == NewType
2940 DataInstanceSort new_or_data -> new_or_data == NewType
2941 DataFamilySort -> False
2942
2943 is_data_family :: Bool
2944 is_data_family =
2945 case data_sort of
2946 DataDeclSort{} -> False
2947 DataInstanceSort{} -> False
2948 DataFamilySort -> True
2949
2950 tYPE_ok :: DynFlags -> Bool
2951 tYPE_ok dflags =
2952 (is_newtype && xopt LangExt.UnliftedNewtypes dflags)
2953 -- With UnliftedNewtypes, we allow kinds other than Type, but they
2954 -- must still be of the form `TYPE r` since we don't want to accept
2955 -- Constraint or Nat.
2956 -- See Note [Implementation of UnliftedNewtypes] in TcTyClsDecls.
2957 || is_data_family
2958 -- If this is a `data family` declaration, we don't need to check if
2959 -- UnliftedNewtypes is enabled, since data family declarations can
2960 -- have return kind `TYPE r` unconditionally (#16827).
2961
2962 is_TYPE :: Bool
2963 is_TYPE = tcIsRuntimeTypeKind kind
2964
2965 is_TYPE_or_Type :: DynFlags -> Bool
2966 is_TYPE_or_Type dflags | tYPE_ok dflags = is_TYPE
2967 | otherwise = tcIsLiftedTypeKind kind
2968
2969 -- In the particular case of a data family, permit a return kind of the
2970 -- form `:: k` (where `k` is a bare kind variable).
2971 is_kind_var :: Bool
2972 is_kind_var | is_data_family = isJust (tcGetCastedTyVar_maybe kind)
2973 | otherwise = False
2974
2975 err_msg :: DynFlags -> SDoc
2976 err_msg dflags =
2977 sep [ (sep [ text "Kind signature on" <+> pp_dec <+>
2978 text "declaration has non-" <>
2979 (if tYPE_ok dflags then text "TYPE" else ppr liftedTypeKind)
2980 , (if is_data_family then text "and non-variable" else empty) <+>
2981 text "return kind" <+> quotes (ppr kind) ])
2982 , if not (tYPE_ok dflags) && is_TYPE && is_newtype &&
2983 not (xopt LangExt.UnliftedNewtypes dflags)
2984 then text "Perhaps you intended to use UnliftedNewtypes"
2985 else empty ]
2986
2987 -- | Checks that the result kind of a class is exactly `Constraint`, rejecting
2988 -- type synonyms and type families that reduce to `Constraint`. See #16826.
2989 checkClassKindSig :: Kind -> TcM ()
2990 checkClassKindSig kind = checkTc (tcIsConstraintKind kind) err_msg
2991 where
2992 err_msg :: SDoc
2993 err_msg =
2994 text "Kind signature on a class must end with" <+> ppr constraintKind $$
2995 text "unobscured by type families"
2996
2997 tcbVisibilities :: TyCon -> [Type] -> [TyConBndrVis]
2998 -- Result is in 1-1 correpondence with orig_args
2999 tcbVisibilities tc orig_args
3000 = go (tyConKind tc) init_subst orig_args
3001 where
3002 init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfTypes orig_args))
3003 go _ _ []
3004 = []
3005
3006 go fun_kind subst all_args@(arg : args)
3007 | Just (tcb, inner_kind) <- splitPiTy_maybe fun_kind
3008 = case tcb of
3009 Anon af _ -> AnonTCB af : go inner_kind subst args
3010 Named (Bndr tv vis) -> NamedTCB vis : go inner_kind subst' args
3011 where
3012 subst' = extendTCvSubst subst tv arg
3013
3014 | not (isEmptyTCvSubst subst)
3015 = go (substTy subst fun_kind) init_subst all_args
3016
3017 | otherwise
3018 = pprPanic "addTcbVisibilities" (ppr tc <+> ppr orig_args)
3019
3020
3021 {- Note [TyConBinders for the result kind signature of a data type]
3022 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3023 Given
3024 data T (a::*) :: * -> forall k. k -> *
3025 we want to generate the extra TyConBinders for T, so we finally get
3026 (a::*) (b::*) (k::*) (c::k)
3027 The function etaExpandAlgTyCon generates these extra TyConBinders from
3028 the result kind signature.
3029
3030 We need to take care to give the TyConBinders
3031 (a) OccNames that are fresh (because the TyConBinders of a TyCon
3032 must have distinct OccNames
3033
3034 (b) Uniques that are fresh (obviously)
3035
3036 For (a) we need to avoid clashes with the tyvars declared by
3037 the user before the "::"; in the above example that is 'a'.
3038 And also see Note [Avoid name clashes for associated data types].
3039
3040 For (b) suppose we have
3041 data T :: forall k. k -> forall k. k -> *
3042 where the two k's are identical even up to their uniques. Surprisingly,
3043 this can happen: see #14515.
3044
3045 It's reasonably easy to solve all this; just run down the list with a
3046 substitution; hence the recursive 'go' function. But it has to be
3047 done.
3048
3049 Note [Avoid name clashes for associated data types]
3050 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3051 Consider class C a b where
3052 data D b :: * -> *
3053 When typechecking the decl for D, we'll invent an extra type variable
3054 for D, to fill out its kind. Ideally we don't want this type variable
3055 to be 'a', because when pretty printing we'll get
3056 class C a b where
3057 data D b a0
3058 (NB: the tidying happens in the conversion to IfaceSyn, which happens
3059 as part of pretty-printing a TyThing.)
3060
3061 That's why we look in the LocalRdrEnv to see what's in scope. This is
3062 important only to get nice-looking output when doing ":info C" in GHCi.
3063 It isn't essential for correctness.
3064
3065
3066 ************************************************************************
3067 * *
3068 Partial signatures
3069 * *
3070 ************************************************************************
3071
3072 -}
3073
3074 tcHsPartialSigType
3075 :: UserTypeCtxt
3076 -> LHsSigWcType GhcRn -- The type signature
3077 -> TcM ( [(Name, TcTyVar)] -- Wildcards
3078 , Maybe TcType -- Extra-constraints wildcard
3079 , [(Name,TcTyVar)] -- Original tyvar names, in correspondence with
3080 -- the implicitly and explicitly bound type variables
3081 , TcThetaType -- Theta part
3082 , TcType ) -- Tau part
3083 -- See Note [Checking partial type signatures]
3084 tcHsPartialSigType ctxt sig_ty
3085 | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
3086 , HsIB { hsib_ext = implicit_hs_tvs
3087 , hsib_body = hs_ty } <- ib_ty
3088 , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
3089 = addSigCtxt ctxt hs_ty $
3090 do { (implicit_tvs, (explicit_tvs, (wcs, wcx, theta, tau)))
3091 <- solveLocalEqualities "tcHsPartialSigType" $
3092 -- This solveLocalEqualiltes fails fast if there are
3093 -- insoluble equalities. See TcSimplify
3094 -- Note [Fail fast if there are insoluble kind equalities]
3095 tcNamedWildCardBinders sig_wcs $ \ wcs ->
3096 bindImplicitTKBndrs_Tv implicit_hs_tvs $
3097 bindExplicitTKBndrs_Tv explicit_hs_tvs $
3098 do { -- Instantiate the type-class context; but if there
3099 -- is an extra-constraints wildcard, just discard it here
3100 (theta, wcx) <- tcPartialContext hs_ctxt
3101
3102 ; tau <- tcHsOpenType hs_tau
3103
3104 ; return (wcs, wcx, theta, tau) }
3105
3106 -- No kind-generalization here:
3107 ; kindGeneralizeNone (mkSpecForAllTys implicit_tvs $
3108 mkSpecForAllTys explicit_tvs $
3109 mkPhiTy theta $
3110 tau)
3111
3112 -- Spit out the wildcards (including the extra-constraints one)
3113 -- as "hole" constraints, so that they'll be reported if necessary
3114 -- See Note [Extra-constraint holes in partial type signatures]
3115 ; emitNamedWildCardHoleConstraints wcs
3116
3117 -- We return a proper (Name,TyVar) environment, to be sure that
3118 -- we bring the right name into scope in the function body.
3119 -- Test case: partial-sigs/should_compile/LocalDefinitionBug
3120 ; let tv_prs = (implicit_hs_tvs `zip` implicit_tvs)
3121 ++ (hsLTyVarNames explicit_hs_tvs `zip` explicit_tvs)
3122
3123 -- NB: checkValidType on the final inferred type will be
3124 -- done later by checkInferredPolyId. We can't do it
3125 -- here because we don't have a complete tuype to check
3126
3127 ; traceTc "tcHsPartialSigType" (ppr tv_prs)
3128 ; return (wcs, wcx, tv_prs, theta, tau) }
3129
3130 tcHsPartialSigType _ (HsWC _ (XHsImplicitBndrs nec)) = noExtCon nec
3131 tcHsPartialSigType _ (XHsWildCardBndrs nec) = noExtCon nec
3132
3133 tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcType)
3134 tcPartialContext hs_theta
3135 | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
3136 , L wc_loc wc@(HsWildCardTy _) <- ignoreParens hs_ctxt_last
3137 = do { wc_tv_ty <- setSrcSpan wc_loc $
3138 tcAnonWildCardOcc wc constraintKind
3139 ; theta <- mapM tcLHsPredType hs_theta1
3140 ; return (theta, Just wc_tv_ty) }
3141 | otherwise
3142 = do { theta <- mapM tcLHsPredType hs_theta
3143 ; return (theta, Nothing) }
3144
3145 {- Note [Checking partial type signatures]
3146 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3147 See also Note [Recipe for checking a signature]
3148
3149 When we have a parital signature like
3150 f,g :: forall a. a -> _
3151 we do the following
3152
3153 * In TcSigs.tcUserSigType we return a PartialSig, which (unlike
3154 the companion CompleteSig) contains the original, as-yet-unchecked
3155 source-code LHsSigWcType
3156
3157 * Then, for f and g /separately/, we call tcInstSig, which in turn
3158 call tchsPartialSig (defined near this Note). It kind-checks the
3159 LHsSigWcType, creating fresh unification variables for each "_"
3160 wildcard. It's important that the wildcards for f and g are distinct
3161 becase they migh get instantiated completely differently. E.g.
3162 f,g :: forall a. a -> _
3163 f x = a
3164 g x = True
3165 It's really as if we'd written two distinct signatures.
3166
3167 * Note that we don't make quantified type (forall a. blah) and then
3168 instantiate it -- it makes no sense to instantiate a type with
3169 wildcards in it. Rather, tcHsPartialSigType just returns the
3170 'a' and the 'blah' separately.
3171
3172 Nor, for the same reason, do we push a level in tcHsPartialSigType.
3173
3174 Note [Extra-constraint holes in partial type signatures]
3175 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3176 Consider
3177 f :: (_) => a -> a
3178 f x = ...
3179
3180 * The renamer leaves '_' untouched.
3181
3182 * Then, in tcHsPartialSigType, we make a new hole TcTyVar, in
3183 tcWildCardBinders.
3184
3185 * TcBinds.chooseInferredQuantifiers fills in that hole TcTyVar
3186 with the inferred constraints, e.g. (Eq a, Show a)
3187
3188 * TcErrors.mkHoleError finally reports the error.
3189
3190 An annoying difficulty happens if there are more than 62 inferred
3191 constraints. Then we need to fill in the TcTyVar with (say) a 70-tuple.
3192 Where do we find the TyCon? For good reasons we only have constraint
3193 tuples up to 62 (see Note [How tuples work] in TysWiredIn). So how
3194 can we make a 70-tuple? This was the root cause of #14217.
3195
3196 It's incredibly tiresome, because we only need this type to fill
3197 in the hole, to communicate to the error reporting machinery. Nothing
3198 more. So I use a HACK:
3199
3200 * I make an /ordinary/ tuple of the constraints, in
3201 TcBinds.chooseInferredQuantifiers. This is ill-kinded because
3202 ordinary tuples can't contain constraints, but it works fine. And for
3203 ordinary tuples we don't have the same limit as for constraint
3204 tuples (which need selectors and an assocated class).
3205
3206 * Because it is ill-kinded, it trips an assert in writeMetaTyVar,
3207 so now I disable the assertion if we are writing a type of
3208 kind Constraint. (That seldom/never normally happens so we aren't
3209 losing much.)
3210
3211 Result works fine, but it may eventually bite us.
3212
3213
3214 ************************************************************************
3215 * *
3216 Pattern signatures (i.e signatures that occur in patterns)
3217 * *
3218 ********************************************************************* -}
3219
3220 tcHsPatSigType :: UserTypeCtxt
3221 -> LHsSigWcType GhcRn -- The type signature
3222 -> TcM ( [(Name, TcTyVar)] -- Wildcards
3223 , [(Name, TcTyVar)] -- The new bit of type environment, binding
3224 -- the scoped type variables
3225 , TcType) -- The type
3226 -- Used for type-checking type signatures in
3227 -- (a) patterns e.g f (x::Int) = e
3228 -- (b) RULE forall bndrs e.g. forall (x::Int). f x = x
3229 --
3230 -- This may emit constraints
3231 -- See Note [Recipe for checking a signature]
3232 tcHsPatSigType ctxt sig_ty
3233 | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
3234 , HsIB { hsib_ext = sig_ns
3235 , hsib_body = hs_ty } <- ib_ty
3236 = addSigCtxt ctxt hs_ty $
3237 do { sig_tkv_prs <- mapM new_implicit_tv sig_ns
3238 ; (wcs, sig_ty)
3239 <- solveLocalEqualities "tcHsPatSigType" $
3240 -- Always solve local equalities if possible,
3241 -- else casts get in the way of deep skolemisation
3242 -- (#16033)
3243 tcNamedWildCardBinders sig_wcs $ \ wcs ->
3244 tcExtendNameTyVarEnv sig_tkv_prs $
3245 do { sig_ty <- tcHsOpenType hs_ty
3246 ; return (wcs, sig_ty) }
3247
3248 ; emitNamedWildCardHoleConstraints wcs
3249
3250 -- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
3251 -- contains a forall). Promote these.
3252 -- Ex: f (x :: forall a. Proxy a -> ()) = ... x ...
3253 -- When we instantiate x, we have to compare the kind of the argument
3254 -- to a's kind, which will be a metavariable.
3255 -- kindGeneralizeNone does this:
3256 ; kindGeneralizeNone sig_ty
3257 ; sig_ty <- zonkTcType sig_ty
3258 ; checkValidType ctxt sig_ty
3259
3260 ; traceTc "tcHsPatSigType" (ppr sig_tkv_prs)
3261 ; return (wcs, sig_tkv_prs, sig_ty) }
3262 where
3263 new_implicit_tv name
3264 = do { kind <- newMetaKindVar
3265 ; tv <- case ctxt of
3266 RuleSigCtxt {} -> newSkolemTyVar name kind
3267 _ -> newPatSigTyVar name kind
3268 -- See Note [Pattern signature binders]
3269 -- NB: tv's Name may be fresh (in the case of newPatSigTyVar)
3270 ; return (name, tv) }
3271
3272 tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs nec)) = noExtCon nec
3273 tcHsPatSigType _ (XHsWildCardBndrs nec) = noExtCon nec
3274
3275 tcPatSig :: Bool -- True <=> pattern binding
3276 -> LHsSigWcType GhcRn
3277 -> ExpSigmaType
3278 -> TcM (TcType, -- The type to use for "inside" the signature
3279 [(Name,TcTyVar)], -- The new bit of type environment, binding
3280 -- the scoped type variables
3281 [(Name,TcTyVar)], -- The wildcards
3282 HsWrapper) -- Coercion due to unification with actual ty
3283 -- Of shape: res_ty ~ sig_ty
3284 tcPatSig in_pat_bind sig res_ty
3285 = do { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
3286 -- sig_tvs are the type variables free in 'sig',
3287 -- and not already in scope. These are the ones
3288 -- that should be brought into scope
3289
3290 ; if null sig_tvs then do {
3291 -- Just do the subsumption check and return
3292 wrap <- addErrCtxtM (mk_msg sig_ty) $
3293 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
3294 ; return (sig_ty, [], sig_wcs, wrap)
3295 } else do
3296 -- Type signature binds at least one scoped type variable
3297
3298 -- A pattern binding cannot bind scoped type variables
3299 -- It is more convenient to make the test here
3300 -- than in the renamer
3301 { when in_pat_bind (addErr (patBindSigErr sig_tvs))
3302
3303 -- Now do a subsumption check of the pattern signature against res_ty
3304 ; wrap <- addErrCtxtM (mk_msg sig_ty) $
3305 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
3306
3307 -- Phew!
3308 ; return (sig_ty, sig_tvs, sig_wcs, wrap)
3309 } }
3310 where
3311 mk_msg sig_ty tidy_env
3312 = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
3313 ; res_ty <- readExpType res_ty -- should be filled in by now
3314 ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
3315 ; let msg = vcat [ hang (text "When checking that the pattern signature:")
3316 4 (ppr sig_ty)
3317 , nest 2 (hang (text "fits the type of its context:")
3318 2 (ppr res_ty)) ]
3319 ; return (tidy_env, msg) }
3320
3321 patBindSigErr :: [(Name,TcTyVar)] -> SDoc
3322 patBindSigErr sig_tvs
3323 = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
3324 <+> pprQuotedList (map fst sig_tvs))
3325 2 (text "in a pattern binding signature")
3326
3327 {- Note [Pattern signature binders]
3328 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3329 See also Note [Type variables in the type environment] in TcRnTypes.
3330 Consider
3331
3332 data T where
3333 MkT :: forall a. a -> (a -> Int) -> T
3334
3335 f :: T -> ...
3336 f (MkT x (f :: b -> c)) = <blah>
3337
3338 Here
3339 * The pattern (MkT p1 p2) creates a *skolem* type variable 'a_sk',
3340 It must be a skolem so that that it retains its identity, and
3341 TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
3342
3343 * The type signature pattern (f :: b -> c) makes freshs meta-tyvars
3344 beta and gamma (TauTvs), and binds "b" :-> beta, "c" :-> gamma in the
3345 environment
3346
3347 * Then unification makes beta := a_sk, gamma := Int
3348 That's why we must make beta and gamma a MetaTv,
3349 not a SkolemTv, so that it can unify to a_sk (or Int, respectively).
3350
3351 * Finally, in '<blah>' we have the envt "b" :-> beta, "c" :-> gamma,
3352 so we return the pairs ("b" :-> beta, "c" :-> gamma) from tcHsPatSigType,
3353
3354 Another example (#13881):
3355 fl :: forall (l :: [a]). Sing l -> Sing l
3356 fl (SNil :: Sing (l :: [y])) = SNil
3357 When we reach the pattern signature, 'l' is in scope from the
3358 outer 'forall':
3359 "a" :-> a_sk :: *
3360 "l" :-> l_sk :: [a_sk]
3361 We make up a fresh meta-TauTv, y_sig, for 'y', and kind-check
3362 the pattern signature
3363 Sing (l :: [y])
3364 That unifies y_sig := a_sk. We return from tcHsPatSigType with
3365 the pair ("y" :-> y_sig).
3366
3367 For RULE binders, though, things are a bit different (yuk).
3368 RULE "foo" forall (x::a) (y::[a]). f x y = ...
3369 Here this really is the binding site of the type variable so we'd like
3370 to use a skolem, so that we get a complaint if we unify two of them
3371 together. Hence the new_tv function in tcHsPatSigType.
3372
3373
3374 ************************************************************************
3375 * *
3376 Checking kinds
3377 * *
3378 ************************************************************************
3379
3380 -}
3381
3382 unifyKinds :: [LHsType GhcRn] -> [(TcType, TcKind)] -> TcM ([TcType], TcKind)
3383 unifyKinds rn_tys act_kinds
3384 = do { kind <- newMetaKindVar
3385 ; let check rn_ty (ty, act_kind)
3386 = checkExpectedKind (unLoc rn_ty) ty act_kind kind
3387 ; tys' <- zipWithM check rn_tys act_kinds
3388 ; return (tys', kind) }
3389
3390 {-
3391 ************************************************************************
3392 * *
3393 Sort checking kinds
3394 * *
3395 ************************************************************************
3396
3397 tcLHsKindSig converts a user-written kind to an internal, sort-checked kind.
3398 It does sort checking and desugaring at the same time, in one single pass.
3399 -}
3400
3401 tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
3402 tcLHsKindSig ctxt hs_kind
3403 -- See Note [Recipe for checking a signature] in TcHsType
3404 -- Result is zonked
3405 = do { kind <- solveLocalEqualities "tcLHsKindSig" $
3406 tc_lhs_kind kindLevelMode hs_kind
3407 ; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind)
3408 -- No generalization:
3409 ; kindGeneralizeNone kind
3410 ; kind <- zonkTcType kind
3411 -- This zonk is very important in the case of higher rank kinds
3412 -- E.g. #13879 f :: forall (p :: forall z (y::z). <blah>).
3413 -- <more blah>
3414 -- When instantiating p's kind at occurrences of p in <more blah>
3415 -- it's crucial that the kind we instantiate is fully zonked,
3416 -- else we may fail to substitute properly
3417
3418 ; checkValidType ctxt kind
3419 ; traceTc "tcLHsKindSig2" (ppr kind)
3420 ; return kind }
3421
3422 tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind
3423 tc_lhs_kind mode k
3424 = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $
3425 tc_lhs_type (kindLevel mode) k liftedTypeKind
3426
3427 promotionErr :: Name -> PromotionErr -> TcM a
3428 promotionErr name err
3429 = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here")
3430 2 (parens reason))
3431 where
3432 reason = case err of
3433 ConstrainedDataConPE pred
3434 -> text "it has an unpromotable context"
3435 <+> quotes (ppr pred)
3436 FamDataConPE -> text "it comes from a data family instance"
3437 NoDataKindsTC -> text "perhaps you intended to use DataKinds"
3438 NoDataKindsDC -> text "perhaps you intended to use DataKinds"
3439 PatSynPE -> text "pattern synonyms cannot be promoted"
3440 _ -> text "it is defined and used in the same recursive group"
3441
3442 {-
3443 ************************************************************************
3444 * *
3445 Error messages and such
3446 * *
3447 ************************************************************************
3448 -}
3449
3450
3451 -- | If the inner action emits constraints, report them as errors and fail;
3452 -- otherwise, propagates the return value. Useful as a wrapper around
3453 -- 'tcImplicitTKBndrs', which uses solveLocalEqualities, when there won't be
3454 -- another chance to solve constraints
3455 failIfEmitsConstraints :: TcM a -> TcM a
3456 failIfEmitsConstraints thing_inside
3457 = checkNoErrs $ -- We say that we fail if there are constraints!
3458 -- c.f same checkNoErrs in solveEqualities
3459 do { (res, lie) <- captureConstraints thing_inside
3460 ; reportAllUnsolved lie
3461 ; return res
3462 }
3463
3464 -- | Make an appropriate message for an error in a function argument.
3465 -- Used for both expressions and types.
3466 funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
3467 funAppCtxt fun arg arg_no
3468 = hang (hsep [ text "In the", speakNth arg_no, ptext (sLit "argument of"),
3469 quotes (ppr fun) <> text ", namely"])
3470 2 (quotes (ppr arg))
3471
3472 -- | Add a "In the data declaration for T" or some such.
3473 addTyConFlavCtxt :: Name -> TyConFlavour -> TcM a -> TcM a
3474 addTyConFlavCtxt name flav
3475 = addErrCtxt $ hsep [ text "In the", ppr flav
3476 , text "declaration for", quotes (ppr name) ]