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