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