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