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