Debug tracing only
[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
10 module TcHsType (
11 -- Type signatures
12 kcHsSigType, tcClassSigType,
13 tcHsSigType, tcHsSigWcType,
14 tcHsPartialSigType,
15 funsSigCtxt, addSigCtxt, pprSigCtxt,
16
17 tcHsClsInstType,
18 tcHsDeriv, tcHsVectInst,
19 tcHsTypeApp,
20 UserTypeCtxt(..),
21 tcImplicitTKBndrs, tcImplicitTKBndrsX,
22 tcExplicitTKBndrs,
23 kcExplicitTKBndrs, kcImplicitTKBndrs,
24
25 -- Type checking type and class decls
26 kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars,
27 tcDataKindSig,
28
29 -- tyvars
30 scopeTyVars, scopeTyVars2,
31
32 -- Kind-checking types
33 -- No kind generalisation, no checkValidType
34 kcLHsQTyVars, kcLHsTyVarBndrs,
35 tcWildCardBinders,
36 tcHsLiftedType, tcHsOpenType,
37 tcHsLiftedTypeNC, tcHsOpenTypeNC,
38 tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
39 tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps,
40 solveEqualities, -- useful re-export
41
42 typeLevelMode, kindLevelMode,
43
44 kindGeneralize, checkExpectedKindX, instantiateTyUntilN,
45 reportFloatingKvs,
46
47 -- Sort-checking kinds
48 tcLHsKindSig, badKindSig,
49
50 -- Zonking and promoting
51 zonkPromoteType,
52
53 -- Pattern type signatures
54 tcHsPatSigType, tcPatSig, funAppCtxt
55 ) where
56
57 #include "HsVersions.h"
58
59 import GhcPrelude
60
61 import HsSyn
62 import TcRnMonad
63 import TcEvidence
64 import TcEnv
65 import TcMType
66 import TcValidity
67 import TcUnify
68 import TcIface
69 import TcSimplify
70 import TcType
71 import TcHsSyn( zonkSigType )
72 import Inst ( tcInstBinders, tcInstBinder )
73 import TyCoRep( TyBinder(..) ) -- Used in tcDataKindSig
74 import Type
75 import Coercion
76 import Kind
77 import RdrName( lookupLocalRdrOcc )
78 import Var
79 import VarSet
80 import TyCon
81 import ConLike
82 import DataCon
83 import Class
84 import Name
85 import NameEnv
86 import NameSet
87 import VarEnv
88 import TysWiredIn
89 import BasicTypes
90 import SrcLoc
91 import Constants ( mAX_CTUPLE_SIZE )
92 import ErrUtils( MsgDoc )
93 import Unique
94 import Util
95 import UniqSupply
96 import Outputable
97 import FastString
98 import PrelNames hiding ( wildCardName )
99 import qualified GHC.LanguageExtensions as LangExt
100
101 import Maybes
102 import Data.List ( partition, mapAccumR )
103 import Control.Monad
104
105 {-
106 ----------------------------
107 General notes
108 ----------------------------
109
110 Unlike with expressions, type-checking types both does some checking and
111 desugars at the same time. This is necessary because we often want to perform
112 equality checks on the types right away, and it would be incredibly painful
113 to do this on un-desugared types. Luckily, desugared types are close enough
114 to HsTypes to make the error messages sane.
115
116 During type-checking, we perform as little validity checking as possible.
117 This is because some type-checking is done in a mutually-recursive knot, and
118 if we look too closely at the tycons, we'll loop. This is why we always must
119 use mkNakedTyConApp and mkNakedAppTys, etc., which never look at a tycon.
120 The mkNamed... functions don't uphold Type invariants, but zonkTcTypeToType
121 will repair this for us. Note that zonkTcType *is* safe within a knot, and
122 can be done repeatedly with no ill effect: it just squeezes out metavariables.
123
124 Generally, after type-checking, you will want to do validity checking, say
125 with TcValidity.checkValidType.
126
127 Validity checking
128 ~~~~~~~~~~~~~~~~~
129 Some of the validity check could in principle be done by the kind checker,
130 but not all:
131
132 - During desugaring, we normalise by expanding type synonyms. Only
133 after this step can we check things like type-synonym saturation
134 e.g. type T k = k Int
135 type S a = a
136 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
137 and then S is saturated. This is a GHC extension.
138
139 - Similarly, also a GHC extension, we look through synonyms before complaining
140 about the form of a class or instance declaration
141
142 - Ambiguity checks involve functional dependencies, and it's easier to wait
143 until knots have been resolved before poking into them
144
145 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
146 finished building the loop. So to keep things simple, we postpone most validity
147 checking until step (3).
148
149 Knot tying
150 ~~~~~~~~~~
151 During step (1) we might fault in a TyCon defined in another module, and it might
152 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
153 knot around type declarations with ARecThing, so that the fault-in code can get
154 the TyCon being defined.
155
156 %************************************************************************
157 %* *
158 Check types AND do validity checking
159 * *
160 ************************************************************************
161 -}
162
163 funsSigCtxt :: [Located Name] -> UserTypeCtxt
164 -- Returns FunSigCtxt, with no redundant-context-reporting,
165 -- form a list of located names
166 funsSigCtxt (L _ name1 : _) = FunSigCtxt name1 False
167 funsSigCtxt [] = panic "funSigCtxt"
168
169 addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
170 addSigCtxt ctxt hs_ty thing_inside
171 = setSrcSpan (getLoc hs_ty) $
172 addErrCtxt (pprSigCtxt ctxt hs_ty) $
173 thing_inside
174
175 pprSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> SDoc
176 -- (pprSigCtxt ctxt <extra> <type>)
177 -- prints In the type signature for 'f':
178 -- f :: <type>
179 -- The <extra> is either empty or "the ambiguity check for"
180 pprSigCtxt ctxt hs_ty
181 | Just n <- isSigMaybe ctxt
182 = hang (text "In the type signature:")
183 2 (pprPrefixOcc n <+> dcolon <+> ppr hs_ty)
184
185 | otherwise
186 = hang (text "In" <+> pprUserTypeCtxt ctxt <> colon)
187 2 (ppr hs_ty)
188
189 tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
190 -- This one is used when we have a LHsSigWcType, but in
191 -- a place where wildards aren't allowed. The renamer has
192 -- already checked this, so we can simply ignore it.
193 tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
194
195 kcHsSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
196 kcHsSigType skol_info names (HsIB { hsib_body = hs_ty
197 , hsib_ext = HsIBRn { hsib_vars = sig_vars }})
198 = addSigCtxt (funsSigCtxt names) hs_ty $
199 discardResult $
200 tcImplicitTKBndrs skol_info sig_vars $
201 tc_lhs_type typeLevelMode hs_ty liftedTypeKind
202 kcHsSigType _ _ (XHsImplicitBndrs _) = panic "kcHsSigType"
203
204 tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
205 -- Does not do validity checking; this must be done outside
206 -- the recursive class declaration "knot"
207 tcClassSigType skol_info names sig_ty
208 = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
209 tc_hs_sig_type_and_gen skol_info sig_ty liftedTypeKind
210
211 tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
212 -- Does validity checking
213 -- See Note [Recipe for checking a signature]
214 tcHsSigType ctxt sig_ty
215 = addSigCtxt ctxt (hsSigType sig_ty) $
216 do { traceTc "tcHsSigType {" (ppr sig_ty)
217 ; kind <- case expectedKindInCtxt ctxt of
218 AnythingKind -> newMetaKindVar
219 TheKind k -> return k
220 OpenKind -> newOpenTypeKind
221 -- The kind is checked by checkValidType, and isn't necessarily
222 -- of kind * in a Template Haskell quote eg [t| Maybe |]
223
224 -- Generalise here: see Note [Kind generalisation]
225 ; do_kind_gen <- decideKindGeneralisationPlan sig_ty
226 ; ty <- if do_kind_gen
227 then tc_hs_sig_type_and_gen skol_info sig_ty kind
228 else tc_hs_sig_type skol_info sig_ty kind
229
230 ; checkValidType ctxt ty
231 ; traceTc "end tcHsSigType }" (ppr ty)
232 ; return ty }
233 where
234 skol_info = SigTypeSkol ctxt
235
236 tc_hs_sig_type_and_gen :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
237 -- Kind-checks/desugars an 'LHsSigType',
238 -- solve equalities,
239 -- and then kind-generalizes.
240 -- This will never emit constraints, as it uses solveEqualities interally.
241 -- No validity checking, but it does zonk en route to generalization
242 tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext
243 = HsIBRn { hsib_vars = sig_vars }
244 , hsib_body = hs_ty }) kind
245 = do { (tkvs, ty) <- solveEqualities $
246 tcImplicitTKBndrs skol_info sig_vars $
247 tc_lhs_type typeLevelMode hs_ty kind
248 -- NB the call to solveEqualities, which unifies all those
249 -- kind variables floating about, immediately prior to
250 -- kind generalisation
251
252 -- We use the "InKnot" zonker, because this is called
253 -- on class method sigs in the knot
254 ; ty1 <- zonkPromoteTypeInKnot $ mkSpecForAllTys tkvs ty
255 ; kvs <- kindGeneralize ty1
256 ; zonkSigType (mkInvForAllTys kvs ty1) }
257
258 tc_hs_sig_type_and_gen _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
259
260 tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
261 -- Kind-check/desugar a 'LHsSigType', but does not solve
262 -- the equalities that arise from doing so; instead it may
263 -- emit kind-equality constraints into the monad
264 -- Zonking, but no validity checking
265 tc_hs_sig_type skol_info (HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars }
266 , hsib_body = hs_ty }) kind
267 = do { (tkvs, ty) <- tcImplicitTKBndrs skol_info sig_vars $
268 tc_lhs_type typeLevelMode hs_ty kind
269
270 -- need to promote any remaining metavariables; test case:
271 -- dependent/should_fail/T14066e.
272 ; zonkPromoteType (mkSpecForAllTys tkvs ty) }
273
274 tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type"
275
276 -----------------
277 tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
278 -- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
279 -- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
280 -- E.g. class C (a::*) (b::k->k)
281 -- data T a b = ... deriving( C Int )
282 -- returns ([k], C, [k, Int], [k->k])
283 tcHsDeriv hs_ty
284 = do { cls_kind <- newMetaKindVar
285 -- always safe to kind-generalize, because there
286 -- can be no covars in an outer scope
287 ; ty <- checkNoErrs $
288 -- avoid redundant error report with "illegal deriving", below
289 tc_hs_sig_type_and_gen (SigTypeSkol DerivClauseCtxt) hs_ty cls_kind
290 ; cls_kind <- zonkTcType cls_kind
291 ; let (tvs, pred) = splitForAllTys ty
292 ; let (args, _) = splitFunTys cls_kind
293 ; case getClassPredTys_maybe pred of
294 Just (cls, tys) -> return (tvs, cls, tys, args)
295 Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
296
297 tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt
298 -> LHsSigType GhcRn
299 -> TcM ([TyVar], ThetaType, Class, [Type])
300 -- Like tcHsSigType, but for a class instance declaration
301 tcHsClsInstType user_ctxt hs_inst_ty
302 = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
303 do { inst_ty <- tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind
304 ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
305
306 -- Used for 'VECTORISE [SCALAR] instance' declarations
307 tcHsVectInst :: LHsSigType GhcRn -> TcM (Class, [Type])
308 tcHsVectInst ty
309 | let hs_cls_ty = hsSigType ty
310 , Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe hs_cls_ty
311 -- Ignoring the binders looks pretty dodgy to me
312 = do { (cls, cls_kind) <- tcClass cls_name
313 ; (applied_class, _res_kind)
314 <- tcTyApps typeLevelMode hs_cls_ty (mkClassPred cls []) cls_kind tys
315 ; case tcSplitTyConApp_maybe applied_class of
316 Just (_tc, args) -> ASSERT( _tc == classTyCon cls )
317 return (cls, args)
318 _ -> failWithTc (text "Too many arguments passed to" <+> ppr cls_name) }
319 | otherwise
320 = failWithTc $ text "Malformed instance type"
321
322 ----------------------------------------------
323 -- | Type-check a visible type application
324 tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
325 -- See Note [Recipe for checking a signature] in TcHsType
326 tcHsTypeApp wc_ty kind
327 | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
328 = do { ty <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ _ ->
329 tcCheckLHsType hs_ty kind
330 ; ty <- zonkPromoteType ty
331 ; checkValidType TypeAppCtxt ty
332 ; return ty }
333 -- NB: we don't call emitWildcardHoleConstraints here, because
334 -- we want any holes in visible type applications to be used
335 -- without fuss. No errors, warnings, extensions, etc.
336 tcHsTypeApp (XHsWildCardBndrs _) _ = panic "tcHsTypeApp"
337
338 {-
339 ************************************************************************
340 * *
341 The main kind checker: no validity checks here
342 * *
343 ************************************************************************
344
345 First a couple of simple wrappers for kcHsType
346 -}
347
348 ---------------------------
349 tcHsOpenType, tcHsLiftedType,
350 tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
351 -- Used for type signatures
352 -- Do not do validity checking
353 tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty
354 tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty
355
356 tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind
357 ; tc_lhs_type typeLevelMode ty ek }
358 tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
359
360 -- Like tcHsType, but takes an expected kind
361 tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
362 tcCheckLHsType hs_ty exp_kind
363 = addTypeCtxt hs_ty $
364 tc_lhs_type typeLevelMode hs_ty exp_kind
365
366 tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
367 -- Called from outside: set the context
368 tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
369
370 -- Like tcLHsType, but use it in a context where type synonyms and type families
371 -- do not need to be saturated, like in a GHCi :kind call
372 tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
373 tcLHsTypeUnsaturated ty = addTypeCtxt ty (tc_infer_lhs_type mode ty)
374 where
375 mode = allowUnsaturated typeLevelMode
376
377 ---------------------------
378 -- | Should we generalise the kind of this type signature?
379 -- We *should* generalise if the type is closed
380 -- or if NoMonoLocalBinds is set. Otherwise, nope.
381 -- See Note [Kind generalisation plan]
382 decideKindGeneralisationPlan :: LHsSigType GhcRn -> TcM Bool
383 decideKindGeneralisationPlan sig_ty@(HsIB { hsib_ext
384 = HsIBRn { hsib_closed = closed } })
385 = do { mono_locals <- xoptM LangExt.MonoLocalBinds
386 ; let should_gen = not mono_locals || closed
387 ; traceTc "decideKindGeneralisationPlan"
388 (ppr sig_ty $$ text "should gen?" <+> ppr should_gen)
389 ; return should_gen }
390 decideKindGeneralisationPlan(XHsImplicitBndrs _)
391 = panic "decideKindGeneralisationPlan"
392
393 {- Note [Kind generalisation plan]
394 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
395 When should we do kind-generalisation for user-written type signature?
396 Answer: we use the same rule as for value bindings:
397
398 * We always kind-generalise if the type signature is closed
399 * Additionally, we attempt to generalise if we have NoMonoLocalBinds
400
401 Trac #13337 shows the problem if we kind-generalise an open type (i.e.
402 one that mentions in-scope type variable
403 foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
404 => proxy a -> String
405 foo _ = case eqT :: Maybe (k :~: Type) of
406 Nothing -> ...
407 Just Refl -> case eqT :: Maybe (a :~: Int) of ...
408
409 In the expression type sig on the last line, we have (a :: k)
410 but (Int :: Type). Since (:~:) is kind-homogeneous, this requires
411 k ~ *, which is true in the Refl branch of the outer case.
412
413 That equality will be solved if we allow it to float out to the
414 implication constraint for the Refl match, but not not if we aggressively
415 attempt to solve all equalities the moment they occur; that is, when
416 checking (Maybe (a :~: Int)). (NB: solveEqualities fails unless it
417 solves all the kind equalities, which is the right thing at top level.)
418
419 So here the right thing is simply not to do kind generalisation!
420
421 ************************************************************************
422 * *
423 Type-checking modes
424 * *
425 ************************************************************************
426
427 The kind-checker is parameterised by a TcTyMode, which contains some
428 information about where we're checking a type.
429
430 The renamer issues errors about what it can. All errors issued here must
431 concern things that the renamer can't handle.
432
433 -}
434
435 -- | Info about the context in which we're checking a type. Currently,
436 -- differentiates only between types and kinds, but this will likely
437 -- grow, at least to include the distinction between patterns and
438 -- not-patterns.
439 data TcTyMode
440 = TcTyMode { mode_level :: TypeOrKind
441 , mode_unsat :: Bool -- True <=> allow unsaturated type families
442 }
443 -- The mode_unsat field is solely so that type families/synonyms can be unsaturated
444 -- in GHCi :kind calls
445
446 typeLevelMode :: TcTyMode
447 typeLevelMode = TcTyMode { mode_level = TypeLevel, mode_unsat = False }
448
449 kindLevelMode :: TcTyMode
450 kindLevelMode = TcTyMode { mode_level = KindLevel, mode_unsat = False }
451
452 allowUnsaturated :: TcTyMode -> TcTyMode
453 allowUnsaturated mode = mode { mode_unsat = True }
454
455 -- switch to kind level
456 kindLevel :: TcTyMode -> TcTyMode
457 kindLevel mode = mode { mode_level = KindLevel }
458
459 instance Outputable TcTyMode where
460 ppr = ppr . mode_level
461
462 {-
463 Note [Bidirectional type checking]
464 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
465 In expressions, whenever we see a polymorphic identifier, say `id`, we are
466 free to instantiate it with metavariables, knowing that we can always
467 re-generalize with type-lambdas when necessary. For example:
468
469 rank2 :: (forall a. a -> a) -> ()
470 x = rank2 id
471
472 When checking the body of `x`, we can instantiate `id` with a metavariable.
473 Then, when we're checking the application of `rank2`, we notice that we really
474 need a polymorphic `id`, and then re-generalize over the unconstrained
475 metavariable.
476
477 In types, however, we're not so lucky, because *we cannot re-generalize*!
478 There is no lambda. So, we must be careful only to instantiate at the last
479 possible moment, when we're sure we're never going to want the lost polymorphism
480 again. This is done in calls to tcInstBinders.
481
482 To implement this behavior, we use bidirectional type checking, where we
483 explicitly think about whether we know the kind of the type we're checking
484 or not. Note that there is a difference between not knowing a kind and
485 knowing a metavariable kind: the metavariables are TauTvs, and cannot become
486 forall-quantified kinds. Previously (before dependent types), there were
487 no higher-rank kinds, and so we could instantiate early and be sure that
488 no types would have polymorphic kinds, and so we could always assume that
489 the kind of a type was a fresh metavariable. Not so anymore, thus the
490 need for two algorithms.
491
492 For HsType forms that can never be kind-polymorphic, we implement only the
493 "down" direction, where we safely assume a metavariable kind. For HsType forms
494 that *can* be kind-polymorphic, we implement just the "up" (functions with
495 "infer" in their name) version, as we gain nothing by also implementing the
496 "down" version.
497
498 Note [Future-proofing the type checker]
499 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
500 As discussed in Note [Bidirectional type checking], each HsType form is
501 handled in *either* tc_infer_hs_type *or* tc_hs_type. These functions
502 are mutually recursive, so that either one can work for any type former.
503 But, we want to make sure that our pattern-matches are complete. So,
504 we have a bunch of repetitive code just so that we get warnings if we're
505 missing any patterns.
506
507 Note [The tcType invariant]
508 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
509 If tc_ty = tc_hs_type hs_ty exp_kind
510 then
511 typeKind tc_ty = exp_kind
512 without any zonking needed. The reason for this is that in
513 tcInferApps we see (F ty), and we kind-check 'ty' with an
514 expected-kind coming from F. Then, to make the resulting application
515 well kinded --- see Note [Ensure well-kinded types] in TcType --- we
516 need the kind-checked 'ty' to have exactly the kind that F expects,
517 with no funny zonking nonsense in between.
518
519 The tcType invariant also applies to checkExpectedKind: if
520 (tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
521 then
522 typeKind tc_ty = exp_ki
523 -}
524
525 ------------------------------------------
526 -- | Check and desugar a type, returning the core type and its
527 -- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
528 -- level.
529 tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
530 tc_infer_lhs_type mode (L span ty)
531 = setSrcSpan span $
532 do { (ty', kind) <- tc_infer_hs_type mode ty
533 ; return (ty', kind) }
534
535 -- | Infer the kind of a type and desugar. This is the "up" type-checker,
536 -- as described in Note [Bidirectional type checking]
537 tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
538 tc_infer_hs_type mode (HsParTy _ t) = tc_infer_lhs_type mode t
539 tc_infer_hs_type mode (HsTyVar _ _ (L _ tv)) = tcTyVar mode tv
540
541 tc_infer_hs_type mode (HsAppTy _ ty1 ty2)
542 = do { let (hs_fun_ty, hs_arg_tys) = splitHsAppTys ty1 [ty2]
543 ; (fun_ty, fun_kind) <- tc_infer_lhs_type mode hs_fun_ty
544 -- A worry: what if fun_kind needs zoonking?
545 -- We used to zonk it here, but that got fun_ty and fun_kind
546 -- out of sync (see the precondition to tcTyApps), which caused
547 -- Trac #14873. So I'm now zonking in tcTyVar, and not here.
548 -- Is that enough? Seems so, but I can't see how to be certain.
549 ; tcTyApps mode hs_fun_ty fun_ty fun_kind hs_arg_tys }
550
551 tc_infer_hs_type mode (HsOpTy _ lhs lhs_op@(L _ hs_op) rhs)
552 | not (hs_op `hasKey` funTyConKey)
553 = do { (op, op_kind) <- tcTyVar mode hs_op
554 -- See "A worry" in the HsApp case
555 ; tcTyApps mode (noLoc $ HsTyVar noExt NotPromoted lhs_op) op op_kind
556 [lhs, rhs] }
557
558 tc_infer_hs_type mode (HsKindSig _ ty sig)
559 = do { sig' <- tc_lhs_kind (kindLevel mode) sig
560 ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
561 ; ty' <- tc_lhs_type mode ty sig'
562 ; return (ty', sig') }
563
564 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
565 -- the splice location to the typechecker. Here we skip over it in order to have
566 -- the same kind inferred for a given expression whether it was produced from
567 -- splices or not.
568 --
569 -- See Note [Delaying modFinalizers in untyped splices].
570 tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
571 = tc_infer_hs_type mode ty
572
573 tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
574 tc_infer_hs_type _ (XHsType (NHsCoreTy ty)) = return (ty, typeKind ty)
575 tc_infer_hs_type mode other_ty
576 = do { kv <- newMetaKindVar
577 ; ty' <- tc_hs_type mode other_ty kv
578 ; return (ty', kv) }
579
580 ------------------------------------------
581 tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
582 tc_lhs_type mode (L span ty) exp_kind
583 = setSrcSpan span $
584 tc_hs_type mode ty exp_kind
585
586 ------------------------------------------
587 tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
588 -> TcM TcType
589 tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
590 TypeLevel ->
591 do { arg_k <- newOpenTypeKind
592 ; res_k <- newOpenTypeKind
593 ; ty1' <- tc_lhs_type mode ty1 arg_k
594 ; ty2' <- tc_lhs_type mode ty2 res_k
595 ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
596 liftedTypeKind exp_kind }
597 KindLevel -> -- no representation polymorphism in kinds. yet.
598 do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
599 ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
600 ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
601 liftedTypeKind exp_kind }
602
603 ------------------------------------------
604 tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
605 -- See Note [The tcType invariant]
606 -- See Note [Bidirectional type checking]
607
608 tc_hs_type mode (HsParTy _ ty) exp_kind = tc_lhs_type mode ty exp_kind
609 tc_hs_type mode (HsDocTy _ ty _) exp_kind = tc_lhs_type mode ty exp_kind
610 tc_hs_type _ ty@(HsBangTy _ bang _) _
611 -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
612 -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
613 -- bangs are invalid, so fail. (#7210, #14761)
614 = do { let bangError err = failWith $
615 text "Unexpected" <+> text err <+> text "annotation:" <+> ppr ty $$
616 text err <+> text "annotation cannot appear nested inside a type"
617 ; case bang of
618 HsSrcBang _ SrcUnpack _ -> bangError "UNPACK"
619 HsSrcBang _ SrcNoUnpack _ -> bangError "NOUNPACK"
620 HsSrcBang _ NoSrcUnpack SrcLazy -> bangError "laziness"
621 HsSrcBang _ _ _ -> bangError "strictness" }
622 tc_hs_type _ ty@(HsRecTy {}) _
623 -- Record types (which only show up temporarily in constructor
624 -- signatures) should have been removed by now
625 = failWithTc (text "Record syntax is illegal here:" <+> ppr ty)
626
627 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType'.
628 -- Here we get rid of it and add the finalizers to the global environment
629 -- while capturing the local environment.
630 --
631 -- See Note [Delaying modFinalizers in untyped splices].
632 tc_hs_type mode (HsSpliceTy _ (HsSpliced _ mod_finalizers (HsSplicedTy ty)))
633 exp_kind
634 = do addModFinalizersWithLclEnv mod_finalizers
635 tc_hs_type mode ty exp_kind
636
637 -- This should never happen; type splices are expanded by the renamer
638 tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind
639 = failWithTc (text "Unexpected type splice:" <+> ppr ty)
640
641 ---------- Functions and applications
642 tc_hs_type mode (HsFunTy _ ty1 ty2) exp_kind
643 = tc_fun_type mode ty1 ty2 exp_kind
644
645 tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
646 | op `hasKey` funTyConKey
647 = tc_fun_type mode ty1 ty2 exp_kind
648
649 --------- Foralls
650 tc_hs_type mode forall@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
651 = do { (tvs', ty') <- tcExplicitTKBndrs (ForAllSkol (ppr forall)) hs_tvs $
652 tc_lhs_type mode ty exp_kind
653 -- Do not kind-generalise here! See Note [Kind generalisation]
654 -- Why exp_kind? See Note [Body kind of HsForAllTy]
655 ; let bndrs = mkTyVarBinders Specified tvs'
656 ; return (mkForAllTys bndrs ty') }
657
658 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
659 | null (unLoc ctxt)
660 = tc_lhs_type mode ty exp_kind
661
662 | otherwise
663 = do { ctxt' <- tc_hs_context mode ctxt
664
665 -- See Note [Body kind of a HsQualTy]
666 ; ty' <- if isConstraintKind exp_kind
667 then tc_lhs_type mode ty constraintKind
668 else do { ek <- newOpenTypeKind
669 -- The body kind (result of the function)
670 -- can be * or #, hence newOpenTypeKind
671 ; ty' <- tc_lhs_type mode ty ek
672 ; checkExpectedKind (unLoc ty) ty' liftedTypeKind exp_kind }
673
674 ; return (mkPhiTy ctxt' ty') }
675
676 --------- Lists, arrays, and tuples
677 tc_hs_type mode rn_ty@(HsListTy _ elt_ty) exp_kind
678 = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
679 ; checkWiredInTyCon listTyCon
680 ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
681
682 tc_hs_type mode rn_ty@(HsPArrTy _ elt_ty) exp_kind
683 = do { MASSERT( isTypeLevel (mode_level mode) )
684 ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
685 ; checkWiredInTyCon parrTyCon
686 ; checkExpectedKind rn_ty (mkPArrTy tau_ty) liftedTypeKind exp_kind }
687
688 -- See Note [Distinguishing tuple kinds] in HsTypes
689 -- See Note [Inferring tuple kinds]
690 tc_hs_type mode rn_ty@(HsTupleTy _ HsBoxedOrConstraintTuple hs_tys) exp_kind
691 -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
692 | Just tup_sort <- tupKindSort_maybe exp_kind
693 = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
694 tc_tuple rn_ty mode tup_sort hs_tys exp_kind
695 | otherwise
696 = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
697 ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
698 ; kinds <- mapM zonkTcType kinds
699 -- Infer each arg type separately, because errors can be
700 -- confusing if we give them a shared kind. Eg Trac #7410
701 -- (Either Int, Int), we do not want to get an error saying
702 -- "the second argument of a tuple should have kind *->*"
703
704 ; let (arg_kind, tup_sort)
705 = case [ (k,s) | k <- kinds
706 , Just s <- [tupKindSort_maybe k] ] of
707 ((k,s) : _) -> (k,s)
708 [] -> (liftedTypeKind, BoxedTuple)
709 -- In the [] case, it's not clear what the kind is, so guess *
710
711 ; tys' <- sequence [ setSrcSpan loc $
712 checkExpectedKind hs_ty ty kind arg_kind
713 | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
714
715 ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
716
717
718 tc_hs_type mode rn_ty@(HsTupleTy _ hs_tup_sort tys) exp_kind
719 = tc_tuple rn_ty mode tup_sort tys exp_kind
720 where
721 tup_sort = case hs_tup_sort of -- Fourth case dealt with above
722 HsUnboxedTuple -> UnboxedTuple
723 HsBoxedTuple -> BoxedTuple
724 HsConstraintTuple -> ConstraintTuple
725 _ -> panic "tc_hs_type HsTupleTy"
726
727 tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
728 = do { let arity = length hs_tys
729 ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
730 ; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
731 ; let arg_reps = map getRuntimeRepFromKind arg_kinds
732 arg_tys = arg_reps ++ tau_tys
733 ; checkExpectedKind rn_ty
734 (mkTyConApp (sumTyCon arity) arg_tys)
735 (unboxedSumKind arg_reps)
736 exp_kind
737 }
738
739 --------- Promoted lists and tuples
740 tc_hs_type mode rn_ty@(HsExplicitListTy _ _ tys) exp_kind
741 = do { tks <- mapM (tc_infer_lhs_type mode) tys
742 ; (taus', kind) <- unifyKinds tys tks
743 ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
744 ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
745 where
746 mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
747 mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k]
748
749 tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
750 -- using newMetaKindVar means that we force instantiations of any polykinded
751 -- types. At first, I just used tc_infer_lhs_type, but that led to #11255.
752 = do { ks <- replicateM arity newMetaKindVar
753 ; taus <- zipWithM (tc_lhs_type mode) tys ks
754 ; let kind_con = tupleTyCon Boxed arity
755 ty_con = promotedTupleDataCon Boxed arity
756 tup_k = mkTyConApp kind_con ks
757 ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
758 where
759 arity = length tys
760
761 --------- Constraint types
762 tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
763 = do { MASSERT( isTypeLevel (mode_level mode) )
764 ; ty' <- tc_lhs_type mode ty liftedTypeKind
765 ; let n' = mkStrLitTy $ hsIPNameFS n
766 ; ipClass <- tcLookupClass ipClassName
767 ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
768 constraintKind exp_kind }
769
770 tc_hs_type mode rn_ty@(HsEqTy _ ty1 ty2) exp_kind
771 = do { (ty1', kind1) <- tc_infer_lhs_type mode ty1
772 ; (ty2', kind2) <- tc_infer_lhs_type mode ty2
773 ; ty2'' <- checkExpectedKind (unLoc ty2) ty2' kind2 kind1
774 ; eq_tc <- tcLookupTyCon eqTyConName
775 ; let ty' = mkNakedTyConApp eq_tc [kind1, ty1', ty2'']
776 ; checkExpectedKind rn_ty ty' constraintKind exp_kind }
777
778 --------- Literals
779 tc_hs_type _ rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
780 = do { checkWiredInTyCon typeNatKindCon
781 ; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
782
783 tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
784 = do { checkWiredInTyCon typeSymbolKindCon
785 ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
786
787 --------- Potentially kind-polymorphic types: call the "up" checker
788 -- See Note [Future-proofing the type checker]
789 tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
790 tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek
791 tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
792 tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
793 tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
794
795 tc_hs_type _ (HsWildCardTy wc) exp_kind
796 = do { wc_ty <- tcWildCardOcc wc exp_kind
797 ; return (mkNakedCastTy wc_ty (mkTcNomReflCo exp_kind))
798 -- Take care here! Even though the coercion is Refl,
799 -- we still need it to establish Note [The tcType invariant]
800 }
801
802 -- disposed of by renamer
803 tc_hs_type _ ty@(HsAppsTy {}) _
804 = pprPanic "tc_hs_tyep HsAppsTy" (ppr ty)
805
806 tcWildCardOcc :: HsWildCardInfo -> Kind -> TcM TcType
807 tcWildCardOcc wc_info exp_kind
808 = do { wc_tv <- tcLookupTyVar (wildCardName wc_info)
809 -- The wildcard's kind should be an un-filled-in meta tyvar
810 ; checkExpectedKind (HsWildCardTy wc_info) (mkTyVarTy wc_tv)
811 (tyVarKind wc_tv) exp_kind }
812
813 ---------------------------
814 -- | Call 'tc_infer_hs_type' and check its result against an expected kind.
815 tc_infer_hs_type_ek :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
816 tc_infer_hs_type_ek mode hs_ty ek
817 = do { (ty, k) <- tc_infer_hs_type mode hs_ty
818 ; checkExpectedKind hs_ty ty k ek }
819
820 ---------------------------
821 tupKindSort_maybe :: TcKind -> Maybe TupleSort
822 tupKindSort_maybe k
823 | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
824 | Just k' <- tcView k = tupKindSort_maybe k'
825 | isConstraintKind k = Just ConstraintTuple
826 | isLiftedTypeKind k = Just BoxedTuple
827 | otherwise = Nothing
828
829 tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
830 tc_tuple rn_ty mode tup_sort tys exp_kind
831 = do { arg_kinds <- case tup_sort of
832 BoxedTuple -> return (nOfThem arity liftedTypeKind)
833 UnboxedTuple -> mapM (\_ -> newOpenTypeKind) tys
834 ConstraintTuple -> return (nOfThem arity constraintKind)
835 ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
836 ; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
837 where
838 arity = length tys
839
840 finish_tuple :: HsType GhcRn
841 -> TupleSort
842 -> [TcType] -- ^ argument types
843 -> [TcKind] -- ^ of these kinds
844 -> TcKind -- ^ expected kind of the whole tuple
845 -> TcM TcType
846 finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
847 = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
848 ; let arg_tys = case tup_sort of
849 -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
850 UnboxedTuple -> tau_reps ++ tau_tys
851 BoxedTuple -> tau_tys
852 ConstraintTuple -> tau_tys
853 ; tycon <- case tup_sort of
854 ConstraintTuple
855 | arity > mAX_CTUPLE_SIZE
856 -> failWith (bigConstraintTuple arity)
857 | otherwise -> tcLookupTyCon (cTupleTyConName arity)
858 BoxedTuple -> do { let tc = tupleTyCon Boxed arity
859 ; checkWiredInTyCon tc
860 ; return tc }
861 UnboxedTuple -> return (tupleTyCon Unboxed arity)
862 ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind }
863 where
864 arity = length tau_tys
865 tau_reps = map getRuntimeRepFromKind tau_kinds
866 res_kind = case tup_sort of
867 UnboxedTuple -> unboxedTupleKind tau_reps
868 BoxedTuple -> liftedTypeKind
869 ConstraintTuple -> constraintKind
870
871 bigConstraintTuple :: Arity -> MsgDoc
872 bigConstraintTuple arity
873 = hang (text "Constraint tuple arity too large:" <+> int arity
874 <+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
875 2 (text "Instead, use a nested tuple")
876
877 ---------------------------
878 -- | Apply a type of a given kind to a list of arguments. This instantiates
879 -- invisible parameters as necessary. Always consumes all the arguments,
880 -- using matchExpectedFunKind as necessary.
881 -- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.
882 -- These kinds should be used to instantiate invisible kind variables;
883 -- they come from an enclosing class for an associated type/data family.
884 tcInferApps :: TcTyMode
885 -> Maybe (VarEnv Kind) -- ^ Possibly, kind info (see above)
886 -> LHsType GhcRn -- ^ Function (for printing only)
887 -> TcType -- ^ Function (could be knot-tied)
888 -> TcKind -- ^ Function kind (zonked)
889 -> [LHsType GhcRn] -- ^ Args
890 -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
891 -- Precondition: typeKind fun_ty = fun_ki
892 -- Reason: we will return a type application like (fun_ty arg1 ... argn),
893 -- and that type must be well-kinded
894 -- See Note [The tcType invariant]
895 tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
896 = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki)
897 ; stuff <- go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
898 ; traceTc "tcInferApps }" empty
899 ; return stuff }
900 where
901 empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
902 tyCoVarsOfType fun_ki
903 (orig_ki_binders, orig_inner_ki) = tcSplitPiTys fun_ki
904
905 go :: Int -- the # of the next argument
906 -> [TcType] -- already type-checked args, in reverse order
907 -> TCvSubst -- instantiating substitution
908 -> TcType -- function applied to some args, could be knot-tied
909 -> [TyBinder] -- binders in function kind (both vis. and invis.)
910 -> TcKind -- function kind body (not a Pi-type)
911 -> [LHsType GhcRn] -- un-type-checked args
912 -> TcM (TcType, [TcType], TcKind) -- same as overall return type
913
914 -- no user-written args left. We're done!
915 go _ acc_args subst fun ki_binders inner_ki []
916 = return (fun, reverse acc_args, substTy subst $ mkPiTys ki_binders inner_ki)
917
918 -- The function's kind has a binder. Is it visible or invisible?
919 go n acc_args subst fun (ki_binder:ki_binders) inner_ki
920 all_args@(arg:args)
921 | isInvisibleBinder ki_binder
922 -- It's invisible. Instantiate.
923 = do { traceTc "tcInferApps (invis)" (ppr ki_binder $$ ppr subst)
924 ; (subst', arg') <- tcInstBinder mb_kind_info subst ki_binder
925 ; go n (arg' : acc_args) subst' (mkNakedAppTy fun arg')
926 ki_binders inner_ki all_args }
927
928 | otherwise
929 -- It's visible. Check the next user-written argument
930 = do { traceTc "tcInferApps (vis)" (vcat [ ppr ki_binder, ppr arg
931 , ppr (tyBinderType ki_binder)
932 , ppr subst ])
933 ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
934 tc_lhs_type mode arg (substTy subst $ tyBinderType ki_binder)
935 ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
936 ; go (n+1) (arg' : acc_args) subst'
937 (mkNakedAppTy fun arg')
938 ki_binders inner_ki args }
939
940 -- We've run out of known binders in the functions's kind.
941 go n acc_args subst fun [] inner_ki all_args
942 | not (null new_ki_binders)
943 -- But, after substituting, we have more binders.
944 = go n acc_args zapped_subst fun new_ki_binders new_inner_ki all_args
945
946 | otherwise
947 -- Even after substituting, still no binders. Use matchExpectedFunKind
948 = do { traceTc "tcInferApps (no binder)" (ppr new_inner_ki $$ ppr zapped_subst)
949 ; (co, arg_k, res_k) <- matchExpectedFunKind hs_ty substed_inner_ki
950 ; let new_in_scope = tyCoVarsOfTypes [arg_k, res_k]
951 subst' = zapped_subst `extendTCvInScopeSet` new_in_scope
952 ; go n acc_args subst'
953 (fun `mkNakedCastTy` co)
954 [mkAnonBinder arg_k]
955 res_k all_args }
956 where
957 substed_inner_ki = substTy subst inner_ki
958 (new_ki_binders, new_inner_ki) = tcSplitPiTys substed_inner_ki
959 zapped_subst = zapTCvSubst subst
960 hs_ty = mkHsAppTys orig_hs_ty (take (n-1) orig_hs_args)
961
962
963 -- | Applies a type to a list of arguments.
964 -- Always consumes all the arguments, using 'matchExpectedFunKind' as
965 -- necessary. If you wish to apply a type to a list of HsTypes, this is
966 -- your function.
967 -- Used for type-checking types only.
968 tcTyApps :: TcTyMode
969 -> LHsType GhcRn -- ^ Function (for printing only)
970 -> TcType -- ^ Function (could be knot-tied)
971 -> TcKind -- ^ Function kind (zonked)
972 -> [LHsType GhcRn] -- ^ Args
973 -> TcM (TcType, TcKind) -- ^ (f args, result kind)
974 -- Precondition: see precondition for tcInferApps
975 tcTyApps mode orig_hs_ty fun_ty fun_ki args
976 = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty fun_ty fun_ki args
977 ; return (ty', ki') }
978
979 --------------------------
980 -- Like checkExpectedKindX, but returns only the final type; convenient wrapper
981 -- Obeys Note [The tcType invariant]
982 checkExpectedKind :: HsType GhcRn -- type we're checking (for printing)
983 -> TcType -- type we're checking (might be knot-tied)
984 -> TcKind -- the known kind of that type
985 -> TcKind -- the expected kind
986 -> TcM TcType
987 checkExpectedKind hs_ty ty act exp
988 = fstOf3 <$> checkExpectedKindX Nothing (ppr hs_ty) ty act exp
989
990 checkExpectedKindX :: Maybe (VarEnv Kind) -- Possibly, instantiations for kind vars
991 -> SDoc -- HsType whose kind we're checking
992 -> TcType -- the type whose kind we're checking
993 -> TcKind -- the known kind of that type, k
994 -> TcKind -- the expected kind, exp_kind
995 -> TcM (TcType, [TcType], TcCoercionN)
996 -- (the new args, the coercion)
997 -- Instantiate a kind (if necessary) and then call unifyType
998 -- (checkExpectedKind ty act_kind exp_kind)
999 -- checks that the actual kind act_kind is compatible
1000 -- with the expected kind exp_kind
1001 checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
1002 = do { -- We need to make sure that both kinds have the same number of implicit
1003 -- foralls out front. If the actual kind has more, instantiate accordingly.
1004 -- Otherwise, just pass the type & kind through: the errors are caught
1005 -- in unifyType.
1006 let (exp_bndrs, _) = splitPiTysInvisible exp_kind
1007 n_exp = length exp_bndrs
1008 ; (new_args, act_kind') <- instantiateTyUntilN mb_kind_env n_exp act_kind
1009
1010 ; let origin = TypeEqOrigin { uo_actual = act_kind'
1011 , uo_expected = exp_kind
1012 , uo_thing = Just pp_hs_ty
1013 , uo_visible = True } -- the hs_ty is visible
1014 ty' = mkNakedAppTys ty new_args
1015
1016 ; traceTc "checkExpectedKind" $
1017 vcat [ pp_hs_ty
1018 , text "act_kind:" <+> ppr act_kind
1019 , text "act_kind':" <+> ppr act_kind'
1020 , text "exp_kind:" <+> ppr exp_kind ]
1021
1022 ; if act_kind' `tcEqType` exp_kind
1023 then return (ty', new_args, mkTcNomReflCo exp_kind) -- This is very common
1024 else do { co_k <- uType KindLevel origin act_kind' exp_kind
1025 ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
1026 , ppr exp_kind
1027 , ppr co_k ])
1028 ; let result_ty = ty' `mkNakedCastTy` co_k
1029 -- See Note [The tcType invariant]
1030 ; return (result_ty, new_args, co_k) } }
1031
1032 -- | Instantiate @n@ invisible arguments to a type. If @n <= 0@, no instantiation
1033 -- occurs. If @n@ is too big, then all available invisible arguments are instantiated.
1034 -- (In other words, this function is very forgiving about bad values of @n@.)
1035 instantiateTyN :: Maybe (VarEnv Kind) -- ^ Predetermined instantiations
1036 -- (for assoc. type patterns)
1037 -> Int -- ^ @n@
1038 -> [TyBinder] -> TcKind -- ^ its kind
1039 -> TcM ([TcType], TcKind) -- ^ The inst'ed type, new args, kind
1040 instantiateTyN mb_kind_env n bndrs inner_ki
1041 | n <= 0
1042 = return ([], ki)
1043
1044 | otherwise
1045 = do { (subst, inst_args) <- tcInstBinders empty_subst mb_kind_env inst_bndrs
1046 ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
1047 ki' = substTy subst rebuilt_ki
1048 ; traceTc "instantiateTyN" (vcat [ ppr ki
1049 , ppr n
1050 , ppr subst
1051 , ppr rebuilt_ki
1052 , ppr ki' ])
1053 ; return (inst_args, ki') }
1054 where
1055 -- NB: splitAt is forgiving with invalid numbers
1056 (inst_bndrs, leftover_bndrs) = splitAt n bndrs
1057 ki = mkPiTys bndrs inner_ki
1058 empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ki))
1059
1060 -- | Instantiate a type to have at most @n@ invisible arguments.
1061 instantiateTyUntilN :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
1062 -> Int -- ^ @n@
1063 -> TcKind -- ^ its kind
1064 -> TcM ([TcType], TcKind) -- ^ The new args, final kind
1065 instantiateTyUntilN mb_kind_env n ki
1066 = let (bndrs, inner_ki) = splitPiTysInvisible ki
1067 num_to_inst = length bndrs - n
1068 in
1069 instantiateTyN mb_kind_env num_to_inst bndrs inner_ki
1070
1071 ---------------------------
1072 tcHsMbContext :: Maybe (LHsContext GhcRn) -> TcM [PredType]
1073 tcHsMbContext Nothing = return []
1074 tcHsMbContext (Just cxt) = tcHsContext cxt
1075
1076 tcHsContext :: LHsContext GhcRn -> TcM [PredType]
1077 tcHsContext = tc_hs_context typeLevelMode
1078
1079 tcLHsPredType :: LHsType GhcRn -> TcM PredType
1080 tcLHsPredType = tc_lhs_pred typeLevelMode
1081
1082 tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
1083 tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)
1084
1085 tc_lhs_pred :: TcTyMode -> LHsType GhcRn -> TcM PredType
1086 tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
1087
1088 ---------------------------
1089 tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
1090 -- See Note [Type checking recursive type and class declarations]
1091 -- in TcTyClsDecls
1092 tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
1093 = do { traceTc "lk1" (ppr name)
1094 ; thing <- tcLookup name
1095 ; case thing of
1096 ATyVar _ tv -> -- Important: zonk before returning
1097 -- We may have the application ((a::kappa) b)
1098 -- where kappa is already unified to (k1 -> k2)
1099 -- Then we want to see that arrow. Best done
1100 -- here because we are also maintaining
1101 -- Note [The tcType invariant], so we don't just
1102 -- want to zonk the kind, leaving the TyVar
1103 -- un-zonked (Trac #114873)
1104 do { ty <- zonkTcTyVar tv
1105 ; return (ty, typeKind ty) }
1106
1107 ATcTyCon tc_tc -> do { -- See Note [GADT kind self-reference]
1108 unless
1109 (isTypeLevel (mode_level mode))
1110 (promotionErr name TyConPE)
1111 ; check_tc tc_tc
1112 ; tc <- get_loopy_tc name tc_tc
1113 ; handle_tyfams tc tc_tc }
1114 -- mkNakedTyConApp: see Note [Type-checking inside the knot]
1115 -- NB: we really should check if we're at the kind level
1116 -- and if the tycon is promotable if -XNoTypeInType is set.
1117 -- But this is a terribly large amount of work! Not worth it.
1118
1119 AGlobal (ATyCon tc)
1120 -> do { check_tc tc
1121 ; handle_tyfams tc tc }
1122
1123 AGlobal (AConLike (RealDataCon dc))
1124 -> do { data_kinds <- xoptM LangExt.DataKinds
1125 ; unless (data_kinds || specialPromotedDc dc) $
1126 promotionErr name NoDataKindsDC
1127 ; type_in_type <- xoptM LangExt.TypeInType
1128 ; unless ( type_in_type ||
1129 ( isTypeLevel (mode_level mode) &&
1130 isLegacyPromotableDataCon dc ) ||
1131 ( isKindLevel (mode_level mode) &&
1132 specialPromotedDc dc ) ) $
1133 promotionErr name NoTypeInTypeDC
1134 ; let tc = promoteDataCon dc
1135 ; return (mkNakedTyConApp tc [], tyConKind tc) }
1136
1137 APromotionErr err -> promotionErr name err
1138
1139 _ -> wrongThingErr "type" thing name }
1140 where
1141 check_tc :: TyCon -> TcM ()
1142 check_tc tc = do { type_in_type <- xoptM LangExt.TypeInType
1143 ; data_kinds <- xoptM LangExt.DataKinds
1144 ; unless (isTypeLevel (mode_level mode) ||
1145 data_kinds ||
1146 isKindTyCon tc) $
1147 promotionErr name NoDataKindsTC
1148 ; unless (isTypeLevel (mode_level mode) ||
1149 type_in_type ||
1150 isLegacyPromotableTyCon tc) $
1151 promotionErr name NoTypeInTypeTC }
1152
1153 -- if we are type-checking a type family tycon, we must instantiate
1154 -- any invisible arguments right away. Otherwise, we get #11246
1155 handle_tyfams :: TyCon -- the tycon to instantiate (might be loopy)
1156 -> TcTyCon -- a non-loopy version of the tycon
1157 -> TcM (TcType, TcKind)
1158 handle_tyfams tc tc_tc
1159 | mightBeUnsaturatedTyCon tc_tc || mode_unsat mode
1160 -- This is where mode_unsat is used
1161 = do { traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind)
1162 ; return (mkNakedTyConApp tc [], tc_kind) }
1163
1164 | otherwise
1165 = do { (tc_args, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc))
1166 tc_kind_bndrs tc_inner_ki
1167 ; let tc_ty = mkNakedTyConApp tc tc_args
1168 -- tc and tc_ty must not be traced here, because that would
1169 -- force the evaluation of a potentially knot-tied variable (tc),
1170 -- and the typechecker would hang, as per #11708
1171 ; traceTc "tcTyVar2b" (vcat [ ppr tc_tc <+> dcolon <+> ppr tc_kind
1172 , ppr kind ])
1173 ; return (tc_ty, kind) }
1174 where
1175 tc_kind = tyConKind tc_tc
1176 (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
1177
1178 get_loopy_tc :: Name -> TyCon -> TcM TyCon
1179 -- Return the knot-tied global TyCon if there is one
1180 -- Otherwise the local TcTyCon; we must be doing kind checking
1181 -- but we still want to return a TyCon of some sort to use in
1182 -- error messages
1183 get_loopy_tc name tc_tc
1184 = do { env <- getGblEnv
1185 ; case lookupNameEnv (tcg_type_env env) name of
1186 Just (ATyCon tc) -> return tc
1187 _ -> do { traceTc "lk1 (loopy)" (ppr name)
1188 ; return tc_tc } }
1189
1190 tcClass :: Name -> TcM (Class, TcKind)
1191 tcClass cls -- Must be a class
1192 = do { thing <- tcLookup cls
1193 ; case thing of
1194 ATcTyCon tc -> return (aThingErr "tcClass" cls, tyConKind tc)
1195 AGlobal (ATyCon tc)
1196 | Just cls <- tyConClass_maybe tc
1197 -> return (cls, tyConKind tc)
1198 _ -> wrongThingErr "class" thing cls }
1199
1200
1201 aThingErr :: String -> Name -> b
1202 -- The type checker for types is sometimes called simply to
1203 -- do *kind* checking; and in that case it ignores the type
1204 -- returned. Which is a good thing since it may not be available yet!
1205 aThingErr str x = pprPanic "AThing evaluated unexpectedly" (text str <+> ppr x)
1206
1207 {-
1208 Note [Type-checking inside the knot]
1209 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1210 Suppose we are checking the argument types of a data constructor. We
1211 must zonk the types before making the DataCon, because once built we
1212 can't change it. So we must traverse the type.
1213
1214 BUT the parent TyCon is knot-tied, so we can't look at it yet.
1215
1216 So we must be careful not to use "smart constructors" for types that
1217 look at the TyCon or Class involved.
1218
1219 * Hence the use of mkNakedXXX functions. These do *not* enforce
1220 the invariants (for example that we use (FunTy s t) rather
1221 than (TyConApp (->) [s,t])).
1222
1223 * The zonking functions establish invariants (even zonkTcType, a change from
1224 previous behaviour). So we must never inspect the result of a
1225 zonk that might mention a knot-tied TyCon. This is generally OK
1226 because we zonk *kinds* while kind-checking types. And the TyCons
1227 in kinds shouldn't be knot-tied, because they come from a previous
1228 mutually recursive group.
1229
1230 * TcHsSyn.zonkTcTypeToType also can safely check/establish
1231 invariants.
1232
1233 This is horribly delicate. I hate it. A good example of how
1234 delicate it is can be seen in Trac #7903.
1235
1236 Note [GADT kind self-reference]
1237 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1238
1239 A promoted type cannot be used in the body of that type's declaration.
1240 Trac #11554 shows this example, which made GHC loop:
1241
1242 import Data.Kind
1243 data P (x :: k) = Q
1244 data A :: Type where
1245 B :: forall (a :: A). P a -> A
1246
1247 In order to check the constructor B, we need to have the promoted type A, but in
1248 order to get that promoted type, B must first be checked. To prevent looping, a
1249 TyConPE promotion error is given when tcTyVar checks an ATcTyCon in kind mode.
1250 Any ATcTyCon is a TyCon being defined in the current recursive group (see data
1251 type decl for TcTyThing), and all such TyCons are illegal in kinds.
1252
1253 Trac #11962 proposes checking the head of a data declaration separately from
1254 its constructors. This would allow the example above to pass.
1255
1256 Note [Body kind of a HsForAllTy]
1257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1258 The body of a forall is usually a type, but in principle
1259 there's no reason to prohibit *unlifted* types.
1260 In fact, GHC can itself construct a function with an
1261 unboxed tuple inside a for-all (via CPR analysis; see
1262 typecheck/should_compile/tc170).
1263
1264 Moreover in instance heads we get forall-types with
1265 kind Constraint.
1266
1267 It's tempting to check that the body kind is either * or #. But this is
1268 wrong. For example:
1269
1270 class C a b
1271 newtype N = Mk Foo deriving (C a)
1272
1273 We're doing newtype-deriving for C. But notice how `a` isn't in scope in
1274 the predicate `C a`. So we quantify, yielding `forall a. C a` even though
1275 `C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
1276 convenient. Bottom line: don't check for * or # here.
1277
1278 Note [Body kind of a HsQualTy]
1279 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1280 If ctxt is non-empty, the HsQualTy really is a /function/, so the
1281 kind of the result really is '*', and in that case the kind of the
1282 body-type can be lifted or unlifted.
1283
1284 However, consider
1285 instance Eq a => Eq [a] where ...
1286 or
1287 f :: (Eq a => Eq [a]) => blah
1288 Here both body-kind of the HsQualTy is Constraint rather than *.
1289 Rather crudely we tell the difference by looking at exp_kind. It's
1290 very convenient to typecheck instance types like any other HsSigType.
1291
1292 Admittedly the '(Eq a => Eq [a]) => blah' case is erroneous, but it's
1293 better to reject in checkValidType. If we say that the body kind
1294 should be '*' we risk getting TWO error messages, one saying that Eq
1295 [a] doens't have kind '*', and one saying that we need a Constraint to
1296 the left of the outer (=>).
1297
1298 How do we figure out the right body kind? Well, it's a bit of a
1299 kludge: I just look at the expected kind. If it's Constraint, we
1300 must be in this instance situation context. It's a kludge because it
1301 wouldn't work if any unification was involved to compute that result
1302 kind -- but it isn't. (The true way might be to use the 'mode'
1303 parameter, but that seemed like a sledgehammer to crack a nut.)
1304
1305 Note [Inferring tuple kinds]
1306 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1307 Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
1308 we try to figure out whether it's a tuple of kind * or Constraint.
1309 Step 1: look at the expected kind
1310 Step 2: infer argument kinds
1311
1312 If after Step 2 it's not clear from the arguments that it's
1313 Constraint, then it must be *. Once having decided that we re-check
1314 the Check the arguments again to give good error messages
1315 in eg. `(Maybe, Maybe)`
1316
1317 Note that we will still fail to infer the correct kind in this case:
1318
1319 type T a = ((a,a), D a)
1320 type family D :: Constraint -> Constraint
1321
1322 While kind checking T, we do not yet know the kind of D, so we will default the
1323 kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
1324
1325 Note [Desugaring types]
1326 ~~~~~~~~~~~~~~~~~~~~~~~
1327 The type desugarer is phase 2 of dealing with HsTypes. Specifically:
1328
1329 * It transforms from HsType to Type
1330
1331 * It zonks any kinds. The returned type should have no mutable kind
1332 or type variables (hence returning Type not TcType):
1333 - any unconstrained kind variables are defaulted to (Any *) just
1334 as in TcHsSyn.
1335 - there are no mutable type variables because we are
1336 kind-checking a type
1337 Reason: the returned type may be put in a TyCon or DataCon where
1338 it will never subsequently be zonked.
1339
1340 You might worry about nested scopes:
1341 ..a:kappa in scope..
1342 let f :: forall b. T '[a,b] -> Int
1343 In this case, f's type could have a mutable kind variable kappa in it;
1344 and we might then default it to (Any *) when dealing with f's type
1345 signature. But we don't expect this to happen because we can't get a
1346 lexically scoped type variable with a mutable kind variable in it. A
1347 delicate point, this. If it becomes an issue we might need to
1348 distinguish top-level from nested uses.
1349
1350 Moreover
1351 * it cannot fail,
1352 * it does no unifications
1353 * it does no validity checking, except for structural matters, such as
1354 (a) spurious ! annotations.
1355 (b) a class used as a type
1356
1357 Note [Kind of a type splice]
1358 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1359 Consider these terms, each with TH type splice inside:
1360 [| e1 :: Maybe $(..blah..) |]
1361 [| e2 :: $(..blah..) |]
1362 When kind-checking the type signature, we'll kind-check the splice
1363 $(..blah..); we want to give it a kind that can fit in any context,
1364 as if $(..blah..) :: forall k. k.
1365
1366 In the e1 example, the context of the splice fixes kappa to *. But
1367 in the e2 example, we'll desugar the type, zonking the kind unification
1368 variables as we go. When we encounter the unconstrained kappa, we
1369 want to default it to '*', not to (Any *).
1370
1371
1372 Help functions for type applications
1373 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1374 -}
1375
1376 addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
1377 -- Wrap a context around only if we want to show that contexts.
1378 -- Omit invisible ones and ones user's won't grok
1379 addTypeCtxt (L _ ty) thing
1380 = addErrCtxt doc thing
1381 where
1382 doc = text "In the type" <+> quotes (ppr ty)
1383
1384 {-
1385 ************************************************************************
1386 * *
1387 Type-variable binders
1388 %* *
1389 %************************************************************************
1390
1391 Note [Dependent LHsQTyVars]
1392 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1393 We track (in the renamer) which explicitly bound variables in a
1394 LHsQTyVars are manifestly dependent; only precisely these variables
1395 may be used within the LHsQTyVars. We must do this so that kcLHsQTyVars
1396 can produce the right TyConBinders, and tell Anon vs. Required.
1397
1398 Example data T k1 (a:k1) (b:k2) c
1399 = MkT (Proxy a) (Proxy b) (Proxy c)
1400
1401 Here
1402 (a:k1),(b:k2),(c:k3)
1403 are Anon (explicitly specified as a binder, not used
1404 in the kind of any other binder
1405 k1 is Required (explicitly specifed as a binder, but used
1406 in the kind of another binder i.e. dependently)
1407 k2 is Specified (not explicitly bound, but used in the kind
1408 of another binder)
1409 k3 in Inferred (not lexically in scope at all, but inferred
1410 by kind inference)
1411 and
1412 T :: forall {k3} k1. forall k3 -> k1 -> k2 -> k3 -> *
1413
1414 See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility]
1415 in TyCoRep.
1416
1417 kcLHsQTyVars uses the hsq_dependent field to decide whether
1418 k1, a, b, c should be Required or Anon.
1419
1420 Earlier, thought it would work simply to do a free-variable check
1421 during kcLHsQTyVars, but this is bogus, because there may be
1422 unsolved equalities about. And we don't want to eagerly solve the
1423 equalities, because we may get further information after
1424 kcLHsQTyVars is called. (Recall that kcLHsQTyVars is called
1425 only from getInitialKind.)
1426 This is what implements the rule that all variables intended to be
1427 dependent must be manifestly so.
1428
1429 Sidenote: It's quite possible that later, we'll consider (t -> s)
1430 as a degenerate case of some (pi (x :: t) -> s) and then this will
1431 all get more permissive.
1432
1433 Note [Kind generalisation and SigTvs]
1434 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1435 Consider
1436 data T (a :: k1) x = MkT (S a ())
1437 data S (b :: k2) y = MkS (T b ())
1438
1439 While we are doing kind inference for the mutually-recursive S,T,
1440 we will end up unifying k1 and k2 together. So they can't be skolems.
1441 We therefore make them SigTvs, which can unify with type variables,
1442 but not with general types. All this is very similar at the level
1443 of terms: see Note [Quantified variables in partial type signatures]
1444 in TcBinds.
1445
1446 There are some wrinkles
1447
1448 * We always want to kind-generalise over SigTvs, and /not/ default
1449 them to Type. Another way to say this is: a SigTV should /never/
1450 stand for a type, even via defaulting. Hence the check in
1451 TcSimplify.defaultTyVarTcS, and TcMType.defaultTyVar. Here's
1452 another example (Trac #14555):
1453 data Exp :: [TYPE rep] -> TYPE rep -> Type where
1454 Lam :: Exp (a:xs) b -> Exp xs (a -> b)
1455 We want to kind-generalise over the 'rep' variable.
1456 Trac #14563 is another example.
1457
1458 * Consider Trac #11203
1459 data SameKind :: k -> k -> *
1460 data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
1461 Here we will unify k1 with k2, but this time doing so is an error,
1462 because k1 and k2 are bound in the same delcaration.
1463
1464 We sort this out using findDupSigTvs, in TcTyClTyVars; very much
1465 as we do with partial type signatures in mk_psig_qtvs in
1466 TcBinds.chooseInferredQuantifiers
1467
1468 Note [Keeping scoped variables in order: Explicit]
1469 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1470 When the user writes `forall a b c. blah`, we bring a, b, and c into
1471 scope and then check blah. In the process of checking blah, we might
1472 learn the kinds of a, b, and c, and these kinds might indicate that
1473 b depends on c, and thus that we should reject the user-written type.
1474
1475 One approach to doing this would be to bring each of a, b, and c into
1476 scope, one at a time, creating an implication constraint and
1477 bumping the TcLevel for each one. This would work, because the kind
1478 of, say, b would be untouchable when c is in scope (and the constraint
1479 couldn't float out because c blocks it). However, it leads to terrible
1480 error messages, complaining about skolem escape. While it is indeed
1481 a problem of skolem escape, we can do better.
1482
1483 Instead, our approach is to bring the block of variables into scope
1484 all at once, creating one implication constraint for the lot. The
1485 user-written variables are skolems in the implication constraint. In
1486 TcSimplify.setImplicationStatus, we check to make sure that the ordering
1487 is correct, choosing ImplicationStatus IC_BadTelescope if they aren't.
1488 Then, in TcErrors, we report if there is a bad telescope. This way,
1489 we can report a suggested ordering to the user if there is a problem.
1490
1491 Note [Keeping scoped variables in order: Implicit]
1492 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1493 When the user implicitly quantifies over variables (say, in a type
1494 signature), we need to come up with some ordering on these variables.
1495 This is done by bumping the TcLevel, bringing the tyvars into scope,
1496 and then type-checking the thing_inside. The constraints are all
1497 wrapped in an implication, which is then solved. Finally, we can
1498 zonk all the binders and then order them with toposortTyVars.
1499
1500 It's critical to solve before zonking and ordering in order to uncover
1501 any unifications. You might worry that this eager solving could cause
1502 trouble elsewhere. I don't think it will. Because it will solve only
1503 in an increased TcLevel, it can't unify anything that was mentioned
1504 elsewhere. Additionally, we require that the order of implicitly
1505 quantified variables is manifest by the scope of these variables, so
1506 we're not going to learn more information later that will help order
1507 these variables.
1508
1509 Note [Recipe for checking a signature]
1510 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1511 Checking a user-written signature requires several steps:
1512
1513 1. Generate constraints.
1514 2. Solve constraints.
1515 3. Zonk and promote tyvars.
1516 4. (Optional) Kind-generalize.
1517 5. Check validity.
1518
1519 There may be some surprises in here:
1520
1521 Step 2 is necessary for two reasons: most signatures also bring
1522 implicitly quantified variables into scope, and solving is necessary
1523 to get these in the right order (see Note [Keeping scoped variables in
1524 order: Implicit]). Additionally, solving is necessary in order to
1525 kind-generalize correctly.
1526
1527 Step 3 requires *promoting* type variables. If there are any foralls
1528 in a type, the TcLevel will be bumped within the forall. This might
1529 lead to the generation of matavars with a high level. If we don't promote,
1530 we violate MetaTvInv of Note [TcLevel and untouchable type variables]
1531 in TcType.
1532
1533 -}
1534
1535 tcWildCardBinders :: SkolemInfo
1536 -> [Name]
1537 -> ([(Name, TcTyVar)] -> TcM a)
1538 -> TcM a
1539 tcWildCardBinders info = tcWildCardBindersX new_tv (Just info)
1540 where
1541 new_tv name = do { kind <- newMetaKindVar
1542 ; newSkolemTyVar name kind }
1543
1544 tcWildCardBindersX :: (Name -> TcM TcTyVar)
1545 -> Maybe SkolemInfo -- Just <=> we're bringing fresh vars
1546 -- into scope; use scopeTyVars
1547 -> [Name]
1548 -> ([(Name, TcTyVar)] -> TcM a)
1549 -> TcM a
1550 tcWildCardBindersX new_wc maybe_skol_info wc_names thing_inside
1551 = do { wcs <- mapM new_wc wc_names
1552 ; let wc_prs = wc_names `zip` wcs
1553 ; scope_tvs wc_prs $
1554 thing_inside wc_prs }
1555 where
1556 scope_tvs
1557 | Just info <- maybe_skol_info = scopeTyVars2 info
1558 | otherwise = tcExtendTyVarEnv2
1559
1560 -- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
1561 -- user-supplied kind signature (CUSK), generalise the result.
1562 -- Used in 'getInitialKind' (for tycon kinds and other kinds)
1563 -- and in kind-checking (but not for tycon kinds, which are checked with
1564 -- tcTyClDecls). See also Note [Complete user-supplied kind signatures] in
1565 -- HsDecls.
1566 --
1567 -- This function does not do telescope checking.
1568 kcLHsQTyVars :: Name -- ^ of the thing being checked
1569 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
1570 -> Bool -- ^ True <=> the decl being checked has a CUSK
1571 -> LHsQTyVars GhcRn
1572 -> TcM (Kind, r) -- ^ The result kind, possibly with other info
1573 -> TcM (TcTyCon, r) -- ^ A suitably-kinded TcTyCon
1574 kcLHsQTyVars name flav cusk
1575 user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
1576 , hsq_dependent = dep_names }
1577 , hsq_explicit = hs_tvs }) thing_inside
1578 | cusk
1579 = do { typeintype <- xoptM LangExt.TypeInType
1580 ; let m_kind
1581 | typeintype = Nothing
1582 | otherwise = Just liftedTypeKind
1583 -- without -XTypeInType, default all kind variables to have kind *
1584
1585 ; (scoped_kvs, (tc_tvs, (res_kind, stuff)))
1586 <- solveEqualities $
1587 tcImplicitTKBndrsX newSkolemTyVar m_kind skol_info kv_ns $
1588 kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
1589
1590 -- Now, because we're in a CUSK, quantify over the mentioned
1591 -- kind vars, in dependency order.
1592 ; tc_tvs <- mapM zonkTcTyVarToTyVar tc_tvs
1593 ; res_kind <- zonkTcType res_kind
1594 ; let tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
1595 qkvs = tyCoVarsOfTypeWellScoped (mkTyConKind tc_binders res_kind)
1596 -- the visibility of tvs doesn't matter here; we just
1597 -- want the free variables not to include the tvs
1598
1599 -- If there are any meta-tvs left, the user has
1600 -- lied about having a CUSK. Error.
1601 ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
1602 -- skip this check for associated types. Why?
1603 -- Any variables mentioned in the definition will get defaulted,
1604 -- except those that appear in the class head. Defaulted vars do
1605 -- not concern us here (they are fully determined). Variables from
1606 -- the class head will be fully determined whenever the class has
1607 -- a CUSK, and an associated family has a CUSK only when the enclosing
1608 -- class has one. So skipping is safe. But why is it necessary?
1609 -- It's possible that a class variable has too low a TcLevel to have
1610 -- fully settled down by this point, and so this check will get
1611 -- a false positive.
1612 ; when (not_associated && not (null meta_tvs)) $
1613 report_non_cusk_tvs (qkvs ++ tc_tvs)
1614
1615 -- If any of the scoped_kvs aren't actually mentioned in a binder's
1616 -- kind (or the return kind), then we're in the CUSK case from
1617 -- Note [Free-floating kind vars]
1618 ; let all_tc_tvs = good_tvs ++ tc_tvs
1619 all_mentioned_tvs = mapUnionVarSet (tyCoVarsOfType . tyVarKind)
1620 all_tc_tvs
1621 `unionVarSet` tyCoVarsOfType res_kind
1622 unmentioned_kvs = filterOut (`elemVarSet` all_mentioned_tvs)
1623 scoped_kvs
1624 ; reportFloatingKvs name flav all_tc_tvs unmentioned_kvs
1625
1626 ; let final_binders = map (mkNamedTyConBinder Specified) good_tvs
1627 ++ tc_binders
1628 tycon = mkTcTyCon name (ppr user_tyvars) final_binders res_kind
1629 (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
1630 flav
1631 -- the tvs contain the binders already
1632 -- in scope from an enclosing class, but
1633 -- re-adding tvs to the env't doesn't cause
1634 -- harm
1635
1636 ; traceTc "kcLHsQTyVars: cusk" $
1637 vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
1638 , ppr tc_tvs, ppr (mkTyConKind final_binders res_kind)
1639 , ppr qkvs, ppr meta_tvs, ppr good_tvs, ppr final_binders ]
1640
1641 ; return (tycon, stuff) }
1642
1643 | otherwise
1644 = do { typeintype <- xoptM LangExt.TypeInType
1645
1646 -- if -XNoTypeInType and we know all the implicits are kind vars,
1647 -- just give the kind *. This prevents test
1648 -- dependent/should_fail/KindLevelsB from compiling, as it should
1649 ; let default_kind
1650 | typeintype = Nothing
1651 | otherwise = Just liftedTypeKind
1652 -- Why newSigTyVar? See Note [Kind generalisation and sigTvs]
1653 ; (scoped_kvs, (tc_tvs, (res_kind, stuff)))
1654 <- kcImplicitTKBndrs kv_ns default_kind $
1655 kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
1656
1657 ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they
1658 -- must remain lined up with the binders
1659 tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
1660 tycon = mkTcTyCon name (ppr user_tyvars) tc_binders res_kind
1661 (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
1662 flav
1663
1664 ; traceTc "kcLHsQTyVars: not-cusk" $
1665 vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
1666 , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ]
1667 ; return (tycon, stuff) }
1668 where
1669 open_fam = tcFlavourIsOpen flav
1670 not_associated = case flav of
1671 DataFamilyFlavour assoc -> not assoc
1672 OpenTypeFamilyFlavour assoc -> not assoc
1673 _ -> True
1674
1675 skol_info = TyConSkol flav name
1676
1677 mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder
1678 -- See Note [Dependent LHsQTyVars]
1679 mk_tc_binder hs_tv tv
1680 | hsLTyVarName hs_tv `elemNameSet` dep_names
1681 = mkNamedTyConBinder Required tv
1682 | otherwise
1683 = mkAnonTyConBinder tv
1684
1685 report_non_cusk_tvs all_tvs
1686 = do { all_tvs <- mapM zonkTyCoVarKind all_tvs
1687 ; let (_, tidy_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
1688 (meta_tvs, other_tvs) = partition isMetaTyVar tidy_tvs
1689
1690 ; addErr $
1691 vcat [ text "You have written a *complete user-suppled kind signature*,"
1692 , hang (text "but the following variable" <> plural meta_tvs <+>
1693 isOrAre meta_tvs <+> text "undetermined:")
1694 2 (vcat (map pp_tv meta_tvs))
1695 , text "Perhaps add a kind signature."
1696 , hang (text "Inferred kinds of user-written variables:")
1697 2 (vcat (map pp_tv other_tvs)) ] }
1698 where
1699 pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
1700 kcLHsQTyVars _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
1701
1702 kcLHsTyVarBndrs :: Bool -- True <=> bump the TcLevel when bringing vars into scope
1703 -> Bool -- True <=> Default un-annotated tyvar
1704 -- binders to kind *
1705 -> SkolemInfo
1706 -> [LHsTyVarBndr GhcRn]
1707 -> TcM r
1708 -> TcM ([TyVar], r)
1709 -- There may be dependency between the explicit "ty" vars.
1710 -- So, we have to handle them one at a time.
1711 kcLHsTyVarBndrs _ _ _ [] thing
1712 = do { stuff <- thing; return ([], stuff) }
1713
1714 kcLHsTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing
1715 = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
1716 -- NB: Bring all tvs into scope, even non-dependent ones,
1717 -- as they're needed in type synonyms, data constructors, etc.
1718
1719 ; (tvs, stuff) <- bind_unless_scoped tv_pair $
1720 kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs $
1721 thing
1722
1723 ; return ( tv : tvs, stuff ) }
1724 where
1725 -- | Bind the tyvar in the env't unless the bool is True
1726 bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a
1727 bind_unless_scoped (_, True) thing_inside = thing_inside
1728 bind_unless_scoped (tv, False) thing_inside
1729 | cusk = scopeTyVars skol_info [tv] thing_inside
1730 | otherwise = tcExtendTyVarEnv [tv] thing_inside
1731 -- These variables haven't settled down yet, so we don't want to bump
1732 -- the TcLevel. If we do, then we'll have metavars of too high a level
1733 -- floating about. Changing this causes many, many failures in the
1734 -- `dependent` testsuite directory.
1735
1736 kc_hs_tv :: HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
1737 kc_hs_tv (UserTyVar _ lname@(L _ name))
1738 = do { tv_pair@(tv, in_scope) <- tcHsTyVarName newSkolemTyVar Nothing name
1739
1740 -- Open type/data families default their variables to kind *.
1741 -- But don't default in-scope class tyvars, of course
1742 ; when (open_fam && not in_scope) $
1743 discardResult $ unifyKind (Just (HsTyVar noExt NotPromoted lname))
1744 liftedTypeKind (tyVarKind tv)
1745
1746 ; return tv_pair }
1747
1748 kc_hs_tv (KindedTyVar _ (L _ name) lhs_kind)
1749 = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt name) lhs_kind
1750 ; tcHsTyVarName newSkolemTyVar (Just kind) name }
1751
1752 kc_hs_tv (XTyVarBndr{}) = panic "kc_hs_tv"
1753
1754 tcImplicitTKBndrs :: SkolemInfo
1755 -> [Name]
1756 -> TcM a
1757 -> TcM ([TcTyVar], a)
1758 tcImplicitTKBndrs = tcImplicitTKBndrsX newSkolemTyVar Nothing
1759
1760 -- | Like 'tcImplicitTKBndrs', but uses 'newSigTyVar' to create tyvars
1761 tcImplicitTKBndrsSig :: SkolemInfo
1762 -> [Name]
1763 -> TcM a
1764 -> TcM ([TcTyVar], a)
1765 tcImplicitTKBndrsSig = tcImplicitTKBndrsX newSigTyVar Nothing
1766
1767 tcImplicitTKBndrsX :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
1768 -> Maybe Kind -- Just k <=> assign all names this kind
1769 -> SkolemInfo
1770 -> [Name]
1771 -> TcM a
1772 -> TcM ([TcTyVar], a) -- these tyvars are dependency-ordered
1773 -- * Guarantees to call solveLocalEqualities to unify
1774 -- all constraints from thing_inside.
1775 --
1776 -- * Returned TcTyVars have the supplied HsTyVarBndrs,
1777 -- but may be in different order to the original [Name]
1778 -- (because of sorting to respect dependency)
1779 --
1780 -- * Returned TcTyVars have zonked kinds
1781 -- See Note [Keeping scoped variables in order: Implicit]
1782 tcImplicitTKBndrsX new_tv m_kind skol_info tv_names thing_inside
1783 | null tv_names -- Short cut for the common case where there
1784 -- are no implicit type variables to bind
1785 = do { result <- solveLocalEqualities thing_inside
1786 ; return ([], result) }
1787
1788 | otherwise
1789 = do { (skol_tvs, result)
1790 <- solveLocalEqualities $
1791 checkTvConstraints skol_info Nothing $
1792 do { tv_pairs <- mapM (tcHsTyVarName new_tv m_kind) tv_names
1793 ; let must_scope_tvs = [ tv | (tv, False) <- tv_pairs ]
1794 ; result <- tcExtendTyVarEnv must_scope_tvs $
1795 thing_inside
1796 ; return (map fst tv_pairs, result) }
1797
1798
1799 ; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs
1800 -- use zonkTcTyCoVarBndr because a skol_tv might be a SigTv
1801
1802 ; let final_tvs = toposortTyVars skol_tvs
1803 ; traceTc "tcImplicitTKBndrs" (ppr tv_names $$ ppr final_tvs)
1804 ; return (final_tvs, result) }
1805
1806 -- | Bring implicitly quantified type/kind variables into scope during
1807 -- kind checking. Uses SigTvs, as per Note [Use SigTvs in kind-checking pass]
1808 -- in TcTyClsDecls.
1809 kcImplicitTKBndrs :: [Name] -- of the vars
1810 -> Maybe Kind -- Just k <=> use k as the kind for all vars
1811 -- Nothing <=> use a meta-tyvar
1812 -> TcM a
1813 -> TcM ([TcTyVar], a) -- returns the tyvars created
1814 -- these are *not* dependency ordered
1815 kcImplicitTKBndrs var_ns m_kind thing_inside
1816 = do { tkvs_pairs <- mapM (tcHsTyVarName newSigTyVar m_kind) var_ns
1817 ; let must_scope_tkvs = [ tkv | (tkv, False) <- tkvs_pairs ]
1818 ; result <- tcExtendTyVarEnv must_scope_tkvs $
1819 thing_inside
1820 ; return (map fst tkvs_pairs, result) }
1821
1822 tcExplicitTKBndrs :: SkolemInfo
1823 -> [LHsTyVarBndr GhcRn]
1824 -> TcM a
1825 -> TcM ([TcTyVar], a)
1826 -- See also Note [Associated type tyvar names] in Class
1827 tcExplicitTKBndrs skol_info hs_tvs thing_inside
1828 -- This function brings into scope a telescope of binders as written by
1829 -- the user. At first blush, it would then seem that we should bring
1830 -- them into scope one at a time, bumping the TcLevel each time.
1831 -- (Recall that we bump the level to prevent skolem escape from happening.)
1832 -- However, this leads to terrible error messages, because we end up
1833 -- failing to unify with some `k0`. Better would be to allow type inference
1834 -- to work, potentially creating a skolem-escape problem, and then to
1835 -- notice that the telescope is out of order. That's what we do here,
1836 -- following the logic of tcImplicitTKBndrsX.
1837 -- See also Note [Keeping scoped variables in order: Explicit]
1838 --
1839 -- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
1840 | null hs_tvs -- Short cut that avoids creating an implication
1841 -- constraint in the common case where none is needed
1842 = do { result <- thing_inside
1843 ; return ([], result) }
1844
1845 | otherwise
1846 = do { (skol_tvs, result) <- checkTvConstraints skol_info (Just doc) $
1847 bind_tvbs hs_tvs
1848
1849 ; traceTc "tcExplicitTKBndrs" $
1850 vcat [ text "Hs vars:" <+> ppr hs_tvs
1851 , text "tvs:" <+> pprTyVars skol_tvs ]
1852
1853 ; return (skol_tvs, result) }
1854
1855 where
1856 bind_tvbs [] = do { result <- thing_inside
1857 ; return ([], result) }
1858 bind_tvbs (L _ tvb : tvbs)
1859 = do { (tv, in_scope) <- tcHsTyVarBndr newSkolemTyVar tvb
1860 ; (if in_scope then id else tcExtendTyVarEnv [tv]) $
1861 do { (tvs, result) <- bind_tvbs tvbs
1862 ; return (tv : tvs, result) }}
1863
1864 doc = sep (map ppr hs_tvs)
1865
1866 -- | Used during the "kind-checking" pass in TcTyClsDecls only.
1867 -- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
1868 kcExplicitTKBndrs :: [LHsTyVarBndr GhcRn]
1869 -> TcM a
1870 -> TcM a
1871 kcExplicitTKBndrs [] thing_inside = thing_inside
1872 kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside
1873 = do { (tv, _) <- tcHsTyVarBndr newSigTyVar hs_tv
1874 ; tcExtendTyVarEnv [tv] $
1875 kcExplicitTKBndrs hs_tvs thing_inside }
1876
1877 tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
1878 -> HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
1879 -- Return a TcTyVar, built using the provided function
1880 -- Typically the Kind inside the HsTyVarBndr will be a tyvar
1881 -- with a mutable kind in it.
1882 --
1883 -- These variables might be in scope already (with associated types, for example).
1884 -- This function then checks that the kind annotation (if any) matches the
1885 -- kind of the in-scope type variable.
1886 --
1887 -- Returned TcTyVar has the same name; no cloning
1888 --
1889 -- See also Note [Associated type tyvar names] in Class
1890 --
1891 -- Returns True iff the tyvar was already in scope
1892 tcHsTyVarBndr new_tv (UserTyVar _ (L _ tv_nm))
1893 = tcHsTyVarName new_tv Nothing tv_nm
1894 tcHsTyVarBndr new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
1895 = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
1896 ; tcHsTyVarName new_tv (Just kind) tv_nm }
1897 tcHsTyVarBndr _ (XTyVarBndr _) = panic "tcHsTyVarBndr"
1898
1899 newWildTyVar :: Name -> TcM TcTyVar
1900 -- ^ New unification variable for a wildcard
1901 newWildTyVar _name
1902 = do { kind <- newMetaKindVar
1903 ; uniq <- newUnique
1904 ; details <- newMetaDetails TauTv
1905 ; let name = mkSysTvName uniq (fsLit "w")
1906 tyvar = (mkTcTyVar name kind details)
1907 ; traceTc "newWildTyVar" (ppr tyvar)
1908 ; return tyvar }
1909
1910 -- | Produce a tyvar of the given name (with the kind provided, or
1911 -- otherwise a meta-var kind). If
1912 -- the name is already in scope, return the scoped variable, checking
1913 -- to make sure the known kind matches any kind provided. The
1914 -- second return value says whether the variable is in scope (True)
1915 -- or not (False). (Use this for associated types, for example.)
1916 tcHsTyVarName :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
1917 -> Maybe Kind -- Just k <=> use k as the variable's kind
1918 -- Nothing <=> use a meta-tyvar
1919 -> Name -> TcM (TcTyVar, Bool)
1920 tcHsTyVarName new_tv m_kind name
1921 = do { mb_tv <- tcLookupLcl_maybe name
1922 ; case mb_tv of
1923 Just (ATyVar _ tv)
1924 -> do { whenIsJust m_kind $ \ kind ->
1925 discardResult $
1926 unifyKind (Just (HsTyVar noExt NotPromoted (noLoc name)))
1927 kind (tyVarKind tv)
1928 ; return (tv, True) }
1929 _ -> do { kind <- case m_kind of
1930 Just kind -> return kind
1931 Nothing -> newMetaKindVar
1932 ; tv <- new_tv name kind
1933 ; return (tv, False) }}
1934
1935 --------------------------
1936 -- Bringing tyvars into scope
1937 --------------------------
1938
1939 -- | Bring tyvars into scope, wrapping the thing_inside in an implication
1940 -- constraint. The implication constraint is necessary to provide SkolemInfo
1941 -- for the tyvars and to ensure that no unification variables made outside
1942 -- the scope of these tyvars (i.e. lower TcLevel) unify with the locally-scoped
1943 -- tyvars (i.e. higher TcLevel).
1944 --
1945 -- INVARIANT: The thing_inside must check only types, never terms.
1946 --
1947 -- Use this (not tcExtendTyVarEnv) wherever you expect a Λ or ∀ in Core.
1948 -- Use tcExtendTyVarEnv otherwise.
1949 scopeTyVars :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a
1950 scopeTyVars skol_info tvs = scopeTyVars2 skol_info [(tyVarName tv, tv) | tv <- tvs]
1951
1952 -- | Like 'scopeTyVars', but allows you to specify different scoped names
1953 -- than the Names stored within the tyvars.
1954 scopeTyVars2 :: SkolemInfo -> [(Name, TcTyVar)] -> TcM a -> TcM a
1955 scopeTyVars2 skol_info prs thing_inside
1956 = fmap snd $ -- discard the TcEvBinds, which will always be empty
1957 checkConstraints skol_info (map snd prs) [{- no EvVars -}] $
1958 tcExtendTyVarEnv2 prs $
1959 thing_inside
1960
1961 ------------------
1962 kindGeneralize :: TcType -> TcM [KindVar]
1963 -- Quantify the free kind variables of a kind or type
1964 -- In the latter case the type is closed, so it has no free
1965 -- type variables. So in both cases, all the free vars are kind vars
1966 -- Input must be zonked.
1967 -- NB: You must call solveEqualities or solveLocalEqualities before
1968 -- kind generalization
1969 kindGeneralize kind_or_type
1970 = do { let kvs = tyCoVarsOfTypeDSet kind_or_type
1971 dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet }
1972 ; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
1973 ; quantifyTyVars gbl_tvs dvs }
1974
1975 {-
1976 Note [Kind generalisation]
1977 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1978 We do kind generalisation only at the outer level of a type signature.
1979 For example, consider
1980 T :: forall k. k -> *
1981 f :: (forall a. T a -> Int) -> Int
1982 When kind-checking f's type signature we generalise the kind at
1983 the outermost level, thus:
1984 f1 :: forall k. (forall (a:k). T k a -> Int) -> Int -- YES!
1985 and *not* at the inner forall:
1986 f2 :: (forall k. forall (a:k). T k a -> Int) -> Int -- NO!
1987 Reason: same as for HM inference on value level declarations,
1988 we want to infer the most general type. The f2 type signature
1989 would be *less applicable* than f1, because it requires a more
1990 polymorphic argument.
1991
1992 NB: There are no explicit kind variables written in f's signature.
1993 When there are, the renamer adds these kind variables to the list of
1994 variables bound by the forall, so you can indeed have a type that's
1995 higher-rank in its kind. But only by explicit request.
1996
1997 Note [Kinds of quantified type variables]
1998 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1999 tcTyVarBndrsGen quantifies over a specified list of type variables,
2000 *and* over the kind variables mentioned in the kinds of those tyvars.
2001
2002 Note that we must zonk those kinds (obviously) but less obviously, we
2003 must return type variables whose kinds are zonked too. Example
2004 (a :: k7) where k7 := k9 -> k9
2005 We must return
2006 [k9, a:k9->k9]
2007 and NOT
2008 [k9, a:k7]
2009 Reason: we're going to turn this into a for-all type,
2010 forall k9. forall (a:k7). blah
2011 which the type checker will then instantiate, and instantiate does not
2012 look through unification variables!
2013
2014 Hence using zonked_kinds when forming tvs'.
2015
2016 Note [Free-floating kind vars]
2017 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2018 Consider
2019
2020 data T = MkT (forall (a :: k). Proxy a)
2021 -- from test ghci/scripts/T7873
2022
2023 This is not an existential datatype, but a higher-rank one (the forall
2024 to the right of MkT). Also consider
2025
2026 data S a = MkS (Proxy (a :: k))
2027
2028 According to the rules around implicitly-bound kind variables, in both
2029 cases those k's scope over the whole declaration. The renamer grabs
2030 it and adds it to the hsq_implicits field of the HsQTyVars of the
2031 tycon. So it must be in scope during type-checking, but we want to
2032 reject T while accepting S.
2033
2034 Why reject T? Because the kind variable isn't fixed by anything. For
2035 a variable like k to be implicit, it needs to be mentioned in the kind
2036 of a tycon tyvar. But it isn't.
2037
2038 Why accept S? Because kind inference tells us that a has kind k, so it's
2039 all OK.
2040
2041 Our approach depends on whether or not the datatype has a CUSK.
2042
2043 Non-CUSK: In the first pass (kcTyClTyVars) we just bring
2044 k into scope. In the second pass (tcTyClTyVars),
2045 we check to make sure that k has been unified with some other variable
2046 (or generalized over, making k into a skolem). If it hasn't been, then
2047 it must be a free-floating kind var. Error.
2048
2049 CUSK: When we determine the tycon's final, never-to-be-changed kind
2050 in kcLHsQTyVars, we check to make sure all implicitly-bound kind
2051 vars are indeed mentioned in a kind somewhere. If not, error.
2052
2053 We also perform free-floating kind var analysis for type family instances
2054 (see #13985). Here is an interesting example:
2055
2056 type family T :: k
2057 type instance T = (Nothing :: Maybe a)
2058
2059 Upon a cursory glance, it may appear that the kind variable `a` is
2060 free-floating above, since there are no (visible) LHS patterns in `T`. However,
2061 there is an *invisible* pattern due to the return kind, so inside of GHC, the
2062 instance looks closer to this:
2063
2064 type family T @k :: k
2065 type instance T @(Maybe a) = (Nothing :: Maybe a)
2066
2067 Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in
2068 fact not free-floating. Contrast that with this example:
2069
2070 type instance T = Proxy (Nothing :: Maybe a)
2071
2072 This would looks like this inside of GHC:
2073
2074 type instance T @(*) = Proxy (Nothing :: Maybe a)
2075
2076 So this time, `a` is neither bound by a visible nor invisible type pattern on
2077 the LHS, so it would be reported as free-floating.
2078
2079 Finally, here's one more brain-teaser (from #9574). In the example below:
2080
2081 class Funct f where
2082 type Codomain f :: *
2083 instance Funct ('KProxy :: KProxy o) where
2084 type Codomain 'KProxy = NatTr (Proxy :: o -> *)
2085
2086 As it turns out, `o` is not free-floating in this example. That is because `o`
2087 bound by the kind signature of the LHS type pattern 'KProxy. To make this more
2088 obvious, one can also write the instance like so:
2089
2090 instance Funct ('KProxy :: KProxy o) where
2091 type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *)
2092
2093 -}
2094
2095 --------------------
2096 -- getInitialKind has made a suitably-shaped kind for the type or class
2097 -- Look it up in the local environment. This is used only for tycons
2098 -- that we're currently type-checking, so we're sure to find a TcTyCon.
2099 kcLookupTcTyCon :: Name -> TcM TcTyCon
2100 kcLookupTcTyCon nm
2101 = do { tc_ty_thing <- tcLookup nm
2102 ; return $ case tc_ty_thing of
2103 ATcTyCon tc -> tc
2104 _ -> pprPanic "kcLookupTcTyCon" (ppr tc_ty_thing) }
2105
2106 -----------------------
2107 -- | Bring tycon tyvars into scope. This is used during the "kind-checking"
2108 -- pass in TcTyClsDecls. (Never in getInitialKind, never in the
2109 -- "type-checking"/desugaring pass.)
2110 -- Never emits constraints, though the thing_inside might.
2111 kcTyClTyVars :: Name -> TcM a -> TcM a
2112 kcTyClTyVars tycon_name thing_inside
2113 -- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
2114 = do { tycon <- kcLookupTcTyCon tycon_name
2115 ; tcExtendTyVarEnv2 (tcTyConScopedTyVars tycon) $ thing_inside }
2116
2117 tcTyClTyVars :: Name
2118 -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
2119 -- ^ Used for the type variables of a type or class decl
2120 -- on the second full pass (type-checking/desugaring) in TcTyClDecls.
2121 -- This is *not* used in the initial-kind run, nor in the "kind-checking" pass.
2122 -- Accordingly, everything passed to the continuation is fully zonked.
2123 --
2124 -- (tcTyClTyVars T [a,b] thing_inside)
2125 -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
2126 -- calls thing_inside with arguments
2127 -- [k1,k2,a,b] [k1:*, k2:*, Anon (k1 -> *), Anon k1] (k2 -> *)
2128 -- having also extended the type environment with bindings
2129 -- for k1,k2,a,b
2130 --
2131 -- Never emits constraints.
2132 --
2133 -- The LHsTyVarBndrs is always user-written, and the full, generalised
2134 -- kind of the tycon is available in the local env.
2135 tcTyClTyVars tycon_name thing_inside
2136 = do { tycon <- kcLookupTcTyCon tycon_name
2137
2138 -- Do checks on scoped tyvars
2139 -- See Note [Free-floating kind vars]
2140 ; let flav = tyConFlavour tycon
2141 scoped_prs = tcTyConScopedTyVars tycon
2142 scoped_tvs = map snd scoped_prs
2143 still_sig_tvs = filter isSigTyVar scoped_tvs
2144
2145 ; mapM_ report_sig_tv_err (findDupSigTvs scoped_prs)
2146
2147 ; checkNoErrs $ reportFloatingKvs tycon_name flav
2148 scoped_tvs still_sig_tvs
2149
2150 ; let res_kind = tyConResKind tycon
2151 binders = correct_binders (tyConBinders tycon) res_kind
2152 ; traceTc "tcTyClTyVars" (ppr tycon_name <+> ppr binders)
2153 ; scopeTyVars2 (TyConSkol flav tycon_name) scoped_prs $
2154 thing_inside binders res_kind }
2155 where
2156 report_sig_tv_err (n1, n2)
2157 = setSrcSpan (getSrcSpan n2) $
2158 addErrTc (text "Couldn't match" <+> quotes (ppr n1)
2159 <+> text "with" <+> quotes (ppr n2))
2160
2161 -- Given some TyConBinders and a TyCon's result kind, make sure that the
2162 -- correct any wrong Named/Anon choices. For example, consider
2163 -- type Syn k = forall (a :: k). Proxy a
2164 -- At first, it looks like k should be named -- after all, it appears on the RHS.
2165 -- However, the correct kind for Syn is (* -> *).
2166 -- (Why? Because k is the kind of a type, so k's kind is *. And the RHS also has
2167 -- kind *.) See also #13963.
2168 correct_binders :: [TyConBinder] -> Kind -> [TyConBinder]
2169 correct_binders binders kind
2170 = binders'
2171 where
2172 (_, binders') = mapAccumR go (tyCoVarsOfType kind) binders
2173
2174 go :: TyCoVarSet -> TyConBinder -> (TyCoVarSet, TyConBinder)
2175 go fvs binder
2176 | isNamedTyConBinder binder
2177 , not (tv `elemVarSet` fvs)
2178 = (new_fvs, mkAnonTyConBinder tv)
2179
2180 | not (isNamedTyConBinder binder)
2181 , tv `elemVarSet` fvs
2182 = (new_fvs, mkNamedTyConBinder Required tv)
2183 -- always Required, because it was anonymous (i.e. visible) previously
2184
2185 | otherwise
2186 = (new_fvs, binder)
2187
2188 where
2189 tv = binderVar binder
2190 new_fvs = fvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv)
2191
2192 -----------------------------------
2193 tcDataKindSig :: [TyConBinder]
2194 -> Kind
2195 -> TcM ([TyConBinder], Kind)
2196 -- GADT decls can have a (perhaps partial) kind signature
2197 -- e.g. data T a :: * -> * -> * where ...
2198 -- This function makes up suitable (kinded) TyConBinders for the
2199 -- argument kinds. E.g. in this case it might return
2200 -- ([b::*, c::*], *)
2201 -- Never emits constraints.
2202 -- It's a little trickier than you might think: see
2203 -- Note [TyConBinders for the result kind signature of a data type]
2204 tcDataKindSig tc_bndrs kind
2205 = do { loc <- getSrcSpanM
2206 ; uniqs <- newUniqueSupply
2207 ; rdr_env <- getLocalRdrEnv
2208 ; let new_occs = [ occ
2209 | str <- allNameStrings
2210 , let occ = mkOccName tvName str
2211 , isNothing (lookupLocalRdrOcc rdr_env occ)
2212 -- Note [Avoid name clashes for associated data types]
2213 , not (occ `elem` lhs_occs) ]
2214 new_uniqs = uniqsFromSupply uniqs
2215 subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet lhs_tvs))
2216 ; return (go loc new_occs new_uniqs subst [] kind) }
2217 where
2218 lhs_tvs = map binderVar tc_bndrs
2219 lhs_occs = map getOccName lhs_tvs
2220
2221 go loc occs uniqs subst acc kind
2222 = case splitPiTy_maybe kind of
2223 Nothing -> (reverse acc, substTy subst kind)
2224
2225 Just (Anon arg, kind')
2226 -> go loc occs' uniqs' subst' (tcb : acc) kind'
2227 where
2228 arg' = substTy subst arg
2229 tv = mkTyVar (mkInternalName uniq occ loc) arg'
2230 subst' = extendTCvInScope subst tv
2231 tcb = TvBndr tv AnonTCB
2232 (uniq:uniqs') = uniqs
2233 (occ:occs') = occs
2234
2235 Just (Named (TvBndr tv vis), kind')
2236 -> go loc occs uniqs subst' (tcb : acc) kind'
2237 where
2238 (subst', tv') = substTyVarBndr subst tv
2239 tcb = TvBndr tv' (NamedTCB vis)
2240
2241 badKindSig :: Bool -> Kind -> SDoc
2242 badKindSig check_for_type kind
2243 = hang (sep [ text "Kind signature on data type declaration has non-*"
2244 , (if check_for_type then empty else text "and non-variable") <+>
2245 text "return kind" ])
2246 2 (ppr kind)
2247
2248 {- Note [TyConBinders for the result kind signature of a data type]
2249 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2250 Given
2251 data T (a::*) :: * -> forall k. k -> *
2252 we want to generate the extra TyConBinders for T, so we finally get
2253 (a::*) (b::*) (k::*) (c::k)
2254 The function tcDataKindSig generates these extra TyConBinders from
2255 the result kind signature.
2256
2257 We need to take care to give the TyConBinders
2258 (a) OccNames that are fresh (because the TyConBinders of a TyCon
2259 must have distinct OccNames
2260
2261 (b) Uniques that are fresh (obviously)
2262
2263 For (a) we need to avoid clashes with the tyvars declared by
2264 the user before the "::"; in the above example that is 'a'.
2265 And also see Note [Avoid name clashes for associated data types].
2266
2267 For (b) suppose we have
2268 data T :: forall k. k -> forall k. k -> *
2269 where the two k's are identical even up to their uniques. Surprisingly,
2270 this can happen: see Trac #14515.
2271
2272 It's reasonably easy to solve all this; just run down the list with a
2273 substitution; hence the recursive 'go' function. But it has to be
2274 done.
2275
2276 Note [Avoid name clashes for associated data types]
2277 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2278 Consider class C a b where
2279 data D b :: * -> *
2280 When typechecking the decl for D, we'll invent an extra type variable
2281 for D, to fill out its kind. Ideally we don't want this type variable
2282 to be 'a', because when pretty printing we'll get
2283 class C a b where
2284 data D b a0
2285 (NB: the tidying happens in the conversion to IfaceSyn, which happens
2286 as part of pretty-printing a TyThing.)
2287
2288 That's why we look in the LocalRdrEnv to see what's in scope. This is
2289 important only to get nice-looking output when doing ":info C" in GHCi.
2290 It isn't essential for correctness.
2291
2292
2293 ************************************************************************
2294 * *
2295 Partial signatures
2296 * *
2297 ************************************************************************
2298
2299 -}
2300
2301 tcHsPartialSigType
2302 :: UserTypeCtxt
2303 -> LHsSigWcType GhcRn -- The type signature
2304 -> TcM ( [(Name, TcTyVar)] -- Wildcards
2305 , Maybe TcType -- Extra-constraints wildcard
2306 , [Name] -- Original tyvar names, in correspondence with ...
2307 , [TcTyVar] -- ... Implicitly and explicitly bound type variables
2308 , TcThetaType -- Theta part
2309 , TcType ) -- Tau part
2310 -- See Note [Recipe for checking a signature]
2311 tcHsPartialSigType ctxt sig_ty
2312 | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
2313 , HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_hs_tvs }
2314 , hsib_body = hs_ty } <- ib_ty
2315 , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
2316 = addSigCtxt ctxt hs_ty $
2317 do { (implicit_tvs, (explicit_tvs, (wcs, wcx, theta, tau)))
2318 <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ wcs ->
2319 tcImplicitTKBndrsSig skol_info implicit_hs_tvs $
2320 tcExplicitTKBndrs skol_info explicit_hs_tvs $
2321 do { -- Instantiate the type-class context; but if there
2322 -- is an extra-constraints wildcard, just discard it here
2323 (theta, wcx) <- tcPartialContext hs_ctxt
2324
2325 ; tau <- tcHsOpenType hs_tau
2326
2327 ; return (wcs, wcx, theta, tau) }
2328
2329 -- We must return these separately, because all the zonking below
2330 -- might change the name of a SigTv. This, in turn, causes trouble
2331 -- in partial type signatures that bind scoped type variables, as
2332 -- we bring the wrong name into scope in the function body.
2333 -- Test case: partial-sigs/should_compile/LocalDefinitionBug
2334 ; let tv_names = map tyVarName (implicit_tvs ++ explicit_tvs)
2335
2336 -- Spit out the wildcards (including the extra-constraints one)
2337 -- as "hole" constraints, so that they'll be reported if necessary
2338 -- See Note [Extra-constraint holes in partial type signatures]
2339 ; emitWildCardHoleConstraints wcs
2340
2341 -- The SigTvs created above will sometimes have too high a TcLevel
2342 -- (note that they are generated *after* bumping the level in
2343 -- the tc{Im,Ex}plicitTKBndrsSig functions. Bumping the level
2344 -- is still important here, because the kinds of these variables
2345 -- do indeed need to have the higher level, so they can unify
2346 -- with other local type variables. But, now that we've type-checked
2347 -- everything (and solved equalities in the tcImplicit call)
2348 -- we need to promote the SigTvs so we don't violate the TcLevel
2349 -- invariant
2350 ; all_tvs <- mapM zonkPromoteTyCoVarBndr (implicit_tvs ++ explicit_tvs)
2351 -- zonkPromoteTyCoVarBndr deals well with SigTvs
2352
2353 ; theta <- mapM zonkPromoteType theta
2354 ; tau <- zonkPromoteType tau
2355
2356 ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
2357
2358 ; traceTc "tcHsPartialSigType" (ppr all_tvs)
2359 ; return (wcs, wcx, tv_names, all_tvs, theta, tau) }
2360 where
2361 skol_info = SigTypeSkol ctxt
2362 tcHsPartialSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPartialSigType"
2363 tcHsPartialSigType _ (XHsWildCardBndrs _) = panic "tcHsPartialSigType"
2364
2365 tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcType)
2366 tcPartialContext hs_theta
2367 | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
2368 , L _ (HsWildCardTy wc) <- ignoreParens hs_ctxt_last
2369 = do { wc_tv_ty <- tcWildCardOcc wc constraintKind
2370 ; theta <- mapM tcLHsPredType hs_theta1
2371 ; return (theta, Just wc_tv_ty) }
2372 | otherwise
2373 = do { theta <- mapM tcLHsPredType hs_theta
2374 ; return (theta, Nothing) }
2375
2376 {- Note [Extra-constraint holes in partial type signatures]
2377 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2378 Consider
2379 f :: (_) => a -> a
2380 f x = ...
2381
2382 * The renamer makes a wildcard name for the "_", and puts it in
2383 the hswc_wcs field.
2384
2385 * Then, in tcHsPartialSigType, we make a new hole TcTyVar, in
2386 tcWildCardBindersX.
2387
2388 * TcBinds.chooseInferredQuantifiers fills in that hole TcTyVar
2389 with the inferred constraints, e.g. (Eq a, Show a)
2390
2391 * TcErrors.mkHoleError finally reports the error.
2392
2393 An annoying difficulty happens if there are more than 62 inferred
2394 constraints. Then we need to fill in the TcTyVar with (say) a 70-tuple.
2395 Where do we find the TyCon? For good reasons we only have constraint
2396 tuples up to 62 (see Note [How tuples work] in TysWiredIn). So how
2397 can we make a 70-tuple? This was the root cause of Trac #14217.
2398
2399 It's incredibly tiresome, because we only need this type to fill
2400 in the hole, to communicate to the error reporting machinery. Nothing
2401 more. So I use a HACK:
2402
2403 * I make an /ordinary/ tuple of the constraints, in
2404 TcBinds.chooseInferredQuantifiers. This is ill-kinded because
2405 ordinary tuples can't contain constraints, but it works fine. And for
2406 ordinary tuples we don't have the same limit as for constraint
2407 tuples (which need selectors and an assocated class).
2408
2409 * Because it is ill-kinded, it trips an assert in writeMetaTyVar,
2410 so now I disable the assertion if we are writing a type of
2411 kind Constraint. (That seldom/never normally happens so we aren't
2412 losing much.)
2413
2414 Result works fine, but it may eventually bite us.
2415
2416
2417 ************************************************************************
2418 * *
2419 Pattern signatures (i.e signatures that occur in patterns)
2420 * *
2421 ********************************************************************* -}
2422
2423 tcHsPatSigType :: UserTypeCtxt
2424 -> LHsSigWcType GhcRn -- The type signature
2425 -> TcM ( [(Name, TcTyVar)] -- Wildcards
2426 , [(Name, TcTyVar)] -- The new bit of type environment, binding
2427 -- the scoped type variables
2428 , TcType) -- The type
2429 -- Used for type-checking type signatures in
2430 -- (a) patterns e.g f (x::Int) = e
2431 -- (b) RULE forall bndrs e.g. forall (x::Int). f x = x
2432 --
2433 -- This may emit constraints
2434 -- See Note [Recipe for checking a signature]
2435 tcHsPatSigType ctxt sig_ty
2436 | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
2437 , HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars}
2438 , hsib_body = hs_ty } <- ib_ty
2439 = addSigCtxt ctxt hs_ty $
2440 do { sig_tkvs <- mapM new_implicit_tv sig_vars
2441 ; (wcs, sig_ty)
2442 <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ wcs ->
2443 tcExtendTyVarEnv sig_tkvs $
2444 do { sig_ty <- tcHsOpenType hs_ty
2445 ; return (wcs, sig_ty) }
2446
2447 ; emitWildCardHoleConstraints wcs
2448
2449 -- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
2450 -- contains a forall). Promote these.
2451 ; sig_ty <- zonkPromoteType sig_ty
2452 ; checkValidType ctxt sig_ty
2453
2454 ; tv_pairs <- mapM mk_tv_pair sig_tkvs
2455
2456 ; traceTc "tcHsPatSigType" (ppr sig_vars)
2457 ; return (wcs, tv_pairs, sig_ty) }
2458 where
2459 new_implicit_tv name = do { kind <- newMetaKindVar
2460 ; new_tv name kind }
2461
2462 new_tv = case ctxt of
2463 RuleSigCtxt {} -> newSkolemTyVar
2464 _ -> newSigTyVar
2465 -- See Note [Pattern signature binders]
2466 -- See Note [Unifying SigTvs]
2467
2468 mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv
2469 ; return (tyVarName tv, tv') }
2470 -- The Name is one of sig_vars, the lexically scoped name
2471 -- But if it's a SigTyVar, it might have been unified
2472 -- with an existing in-scope skolem, so we must zonk
2473 -- here. See Note [Pattern signature binders]
2474 tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPatSigType"
2475 tcHsPatSigType _ (XHsWildCardBndrs _) = panic "tcHsPatSigType"
2476
2477 tcPatSig :: Bool -- True <=> pattern binding
2478 -> LHsSigWcType GhcRn
2479 -> ExpSigmaType
2480 -> TcM (TcType, -- The type to use for "inside" the signature
2481 [(Name,TcTyVar)], -- The new bit of type environment, binding
2482 -- the scoped type variables
2483 [(Name,TcTyVar)], -- The wildcards
2484 HsWrapper) -- Coercion due to unification with actual ty
2485 -- Of shape: res_ty ~ sig_ty
2486 tcPatSig in_pat_bind sig res_ty
2487 = do { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
2488 -- sig_tvs are the type variables free in 'sig',
2489 -- and not already in scope. These are the ones
2490 -- that should be brought into scope
2491
2492 ; if null sig_tvs then do {
2493 -- Just do the subsumption check and return
2494 wrap <- addErrCtxtM (mk_msg sig_ty) $
2495 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
2496 ; return (sig_ty, [], sig_wcs, wrap)
2497 } else do
2498 -- Type signature binds at least one scoped type variable
2499
2500 -- A pattern binding cannot bind scoped type variables
2501 -- It is more convenient to make the test here
2502 -- than in the renamer
2503 { when in_pat_bind (addErr (patBindSigErr sig_tvs))
2504
2505 -- Check that all newly-in-scope tyvars are in fact
2506 -- constrained by the pattern. This catches tiresome
2507 -- cases like
2508 -- type T a = Int
2509 -- f :: Int -> Int
2510 -- f (x :: T a) = ...
2511 -- Here 'a' doesn't get a binding. Sigh
2512 ; let bad_tvs = [ tv | (_,tv) <- sig_tvs
2513 , not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ]
2514 ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
2515
2516 -- Now do a subsumption check of the pattern signature against res_ty
2517 ; wrap <- addErrCtxtM (mk_msg sig_ty) $
2518 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
2519
2520 -- Phew!
2521 ; return (sig_ty, sig_tvs, sig_wcs, wrap)
2522 } }
2523 where
2524 mk_msg sig_ty tidy_env
2525 = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
2526 ; res_ty <- readExpType res_ty -- should be filled in by now
2527 ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
2528 ; let msg = vcat [ hang (text "When checking that the pattern signature:")
2529 4 (ppr sig_ty)
2530 , nest 2 (hang (text "fits the type of its context:")
2531 2 (ppr res_ty)) ]
2532 ; return (tidy_env, msg) }
2533
2534 patBindSigErr :: [(Name,TcTyVar)] -> SDoc
2535 patBindSigErr sig_tvs
2536 = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
2537 <+> pprQuotedList (map fst sig_tvs))
2538 2 (text "in a pattern binding signature")
2539
2540 {- Note [Pattern signature binders]
2541 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2542 Consider
2543 data T = forall a. T a (a->Int)
2544 f (T x (f :: b->Int)) = blah
2545
2546 Here
2547 * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk',
2548 It must be a skolem so that that it retains its identity, and
2549 TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
2550
2551 * The type signature pattern (f :: b->Int) makes a fresh meta-tyvar b_sig
2552 (a SigTv), and binds "b" :-> b_sig in the envt
2553
2554 * Then unification makes b_sig := a_sk
2555 That's why we must make b_sig a MetaTv (albeit a SigTv),
2556 not a SkolemTv, so that it can unify to a_sk.
2557
2558 * Finally, in 'blah' we must have the envt "b" :-> a_sk. The pair
2559 ("b" :-> a_sk) is returned by tcHsPatSigType, constructed by
2560 mk_tv_pair in that function.
2561
2562 Another example (Trac #13881):
2563 fl :: forall (l :: [a]). Sing l -> Sing l
2564 fl (SNil :: Sing (l :: [y])) = SNil
2565 When we reach the pattern signature, 'l' is in scope from the
2566 outer 'forall':
2567 "a" :-> a_sk :: *
2568 "l" :-> l_sk :: [a_sk]
2569 We make up a fresh meta-SigTv, y_sig, for 'y', and kind-check
2570 the pattern signature
2571 Sing (l :: [y])
2572 That unifies y_sig := a_sk. We return from tcHsPatSigType with
2573 the pair ("y" :-> a_sk).
2574
2575 For RULE binders, though, things are a bit different (yuk).
2576 RULE "foo" forall (x::a) (y::[a]). f x y = ...
2577 Here this really is the binding site of the type variable so we'd like
2578 to use a skolem, so that we get a complaint if we unify two of them
2579 together.
2580
2581 Note [Unifying SigTvs]
2582 ~~~~~~~~~~~~~~~~~~~~~~
2583 ALAS we have no decent way of avoiding two SigTvs getting unified.
2584 Consider
2585 f (x::(a,b)) (y::c)) = [fst x, y]
2586 Here we'd really like to complain that 'a' and 'c' are unified. But
2587 for the reasons above we can't make a,b,c into skolems, so they
2588 are just SigTvs that can unify. And indeed, this would be ok,
2589 f x (y::c) = case x of
2590 (x1 :: a1, True) -> [x,y]
2591 (x1 :: a2, False) -> [x,y,y]
2592 Here the type of x's first component is called 'a1' in one branch and
2593 'a2' in the other. We could try insisting on the same OccName, but
2594 they definitely won't have the sane lexical Name.
2595
2596 I think we could solve this by recording in a SigTv a list of all the
2597 in-scope variables that it should not unify with, but it's fiddly.
2598
2599
2600 ************************************************************************
2601 * *
2602 Checking kinds
2603 * *
2604 ************************************************************************
2605
2606 -}
2607
2608 unifyKinds :: [LHsType GhcRn] -> [(TcType, TcKind)] -> TcM ([TcType], TcKind)
2609 unifyKinds rn_tys act_kinds
2610 = do { kind <- newMetaKindVar
2611 ; let check rn_ty (ty, act_kind) = checkExpectedKind (unLoc rn_ty) ty act_kind kind
2612 ; tys' <- zipWithM check rn_tys act_kinds
2613 ; return (tys', kind) }
2614
2615 {-
2616 ************************************************************************
2617 * *
2618 Promotion
2619 * *
2620 ************************************************************************
2621 -}
2622
2623 -- | Whenever a type is about to be added to the environment, it's necessary
2624 -- to make sure that any free meta-tyvars in the type are promoted to the
2625 -- current TcLevel. (They might be at a higher level due to the level-bumping
2626 -- in tcExplicitTKBndrs, for example.) This function both zonks *and*
2627 -- promotes.
2628 zonkPromoteType :: TcType -> TcM TcType
2629 zonkPromoteType = mapType zonkPromoteMapper ()
2630
2631 -- cf. TcMType.zonkTcTypeMapper
2632 zonkPromoteMapper :: TyCoMapper () TcM
2633 zonkPromoteMapper = TyCoMapper { tcm_smart = True
2634 , tcm_tyvar = const zonkPromoteTcTyVar
2635 , tcm_covar = const covar
2636 , tcm_hole = const hole
2637 , tcm_tybinder = const tybinder }
2638 where
2639 covar cv
2640 = mkCoVarCo <$> zonkPromoteTyCoVarKind cv
2641
2642 hole :: CoercionHole -> TcM Coercion
2643 hole h
2644 = do { contents <- unpackCoercionHole_maybe h
2645 ; case contents of
2646 Just co -> do { co <- zonkPromoteCoercion co
2647 ; checkCoercionHole cv co }
2648 Nothing -> do { cv' <- zonkPromoteTyCoVarKind cv
2649 ; return $ mkHoleCo (setCoHoleCoVar h cv') } }
2650 where
2651 cv = coHoleCoVar h
2652
2653 tybinder :: TyVar -> ArgFlag -> TcM ((), TyVar)
2654 tybinder tv _flag = ((), ) <$> zonkPromoteTyCoVarKind tv
2655
2656 zonkPromoteTcTyVar :: TyCoVar -> TcM TcType
2657 zonkPromoteTcTyVar tv
2658 | isMetaTyVar tv
2659 = do { let ref = metaTyVarRef tv
2660 ; contents <- readTcRef ref
2661 ; case contents of
2662 Flexi -> do { promoted <- promoteTyVar tv
2663 ; if promoted
2664 then zonkPromoteTcTyVar tv -- read it again
2665 else mkTyVarTy <$> zonkPromoteTyCoVarKind tv }
2666 Indirect ty -> zonkPromoteType ty }
2667
2668 | isTcTyVar tv && isSkolemTyVar tv -- NB: isSkolemTyVar says "True" to pure TyVars
2669 = do { tc_lvl <- getTcLevel
2670 ; mkTyVarTy <$> zonkPromoteTyCoVarKind (promoteSkolem tc_lvl tv) }
2671
2672 | otherwise
2673 = mkTyVarTy <$> zonkPromoteTyCoVarKind tv
2674
2675 zonkPromoteTyCoVarKind :: TyCoVar -> TcM TyCoVar
2676 zonkPromoteTyCoVarKind = updateTyVarKindM zonkPromoteType
2677
2678 zonkPromoteTyCoVarBndr :: TyCoVar -> TcM TyCoVar
2679 zonkPromoteTyCoVarBndr tv
2680 | isSigTyVar tv
2681 = tcGetTyVar "zonkPromoteTyCoVarBndr SigTv" <$> zonkPromoteTcTyVar tv
2682
2683 | isTcTyVar tv && isSkolemTyVar tv
2684 = do { tc_lvl <- getTcLevel
2685 ; zonkPromoteTyCoVarKind (promoteSkolem tc_lvl tv) }
2686
2687 | otherwise
2688 = zonkPromoteTyCoVarKind tv
2689
2690 zonkPromoteCoercion :: Coercion -> TcM Coercion
2691 zonkPromoteCoercion = mapCoercion zonkPromoteMapper ()
2692
2693 zonkPromoteTypeInKnot :: TcType -> TcM TcType
2694 zonkPromoteTypeInKnot = mapType (zonkPromoteMapper { tcm_smart = False }) ()
2695 -- NB: Just changing smart to False will still use the smart zonker (not suitable
2696 -- for in-the-knot) for kinds. But that's OK, because kinds aren't knot-tied.
2697
2698 {-
2699 ************************************************************************
2700 * *
2701 Sort checking kinds
2702 * *
2703 ************************************************************************
2704
2705 tcLHsKindSig converts a user-written kind to an internal, sort-checked kind.
2706 It does sort checking and desugaring at the same time, in one single pass.
2707 -}
2708
2709 tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
2710 tcLHsKindSig ctxt hs_kind
2711 -- See Note [Recipe for checking a signature] in TcHsType
2712 = do { kind <- solveLocalEqualities $
2713 tc_lhs_kind kindLevelMode hs_kind
2714 ; kind <- zonkPromoteType kind
2715 -- This zonk is very important in the case of higher rank kinds
2716 -- E.g. Trac #13879 f :: forall (p :: forall z (y::z). <blah>).
2717 -- <more blah>
2718 -- When instantiating p's kind at occurrences of p in <more blah>
2719 -- it's crucial that the kind we instantiate is fully zonked,
2720 -- else we may fail to substitute properly
2721
2722 ; checkValidType ctxt kind
2723 ; return kind }
2724
2725 tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind
2726 tc_lhs_kind mode k
2727 = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $
2728 tc_lhs_type (kindLevel mode) k liftedTypeKind
2729
2730 promotionErr :: Name -> PromotionErr -> TcM a
2731 promotionErr name err
2732 = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here")
2733 2 (parens reason))
2734 where
2735 reason = case err of
2736 FamDataConPE -> text "it comes from a data family instance"
2737 NoDataKindsTC -> text "perhaps you intended to use DataKinds"
2738 NoDataKindsDC -> text "perhaps you intended to use DataKinds"
2739 NoTypeInTypeTC -> text "perhaps you intended to use TypeInType"
2740 NoTypeInTypeDC -> text "perhaps you intended to use TypeInType"
2741 PatSynPE -> text "pattern synonyms cannot be promoted"
2742 PatSynExPE -> sep [ text "the existential variables of a pattern synonym"
2743 , text "signature do not scope over the pattern" ]
2744 _ -> text "it is defined and used in the same recursive group"
2745
2746 {-
2747 ************************************************************************
2748 * *
2749 Scoped type variables
2750 * *
2751 ************************************************************************
2752 -}
2753
2754 badPatSigTvs :: TcType -> [TyVar] -> SDoc
2755 badPatSigTvs sig_ty bad_tvs
2756 = vcat [ fsep [text "The type variable" <> plural bad_tvs,
2757 quotes (pprWithCommas ppr bad_tvs),
2758 text "should be bound by the pattern signature" <+> quotes (ppr sig_ty),
2759 text "but are actually discarded by a type synonym" ]
2760 , text "To fix this, expand the type synonym"
2761 , text "[Note: I hope to lift this restriction in due course]" ]
2762
2763 {-
2764 ************************************************************************
2765 * *
2766 Error messages and such
2767 * *
2768 ************************************************************************
2769 -}
2770
2771 -- | Make an appropriate message for an error in a function argument.
2772 -- Used for both expressions and types.
2773 funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
2774 funAppCtxt fun arg arg_no
2775 = hang (hsep [ text "In the", speakNth arg_no, ptext (sLit "argument of"),
2776 quotes (ppr fun) <> text ", namely"])
2777 2 (quotes (ppr arg))
2778
2779 -- See Note [Free-floating kind vars]
2780 reportFloatingKvs :: Name -- of the tycon
2781 -> TyConFlavour -- What sort of TyCon it is
2782 -> [TcTyVar] -- all tyvars, not necessarily zonked
2783 -> [TcTyVar] -- floating tyvars
2784 -> TcM ()
2785 reportFloatingKvs tycon_name flav all_tvs bad_tvs
2786 = unless (null bad_tvs) $ -- don't bother zonking if there's no error
2787 do { all_tvs <- mapM zonkTcTyVarToTyVar all_tvs
2788 ; bad_tvs <- mapM zonkTcTyVarToTyVar bad_tvs
2789 ; let (tidy_env, tidy_all_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
2790 tidy_bad_tvs = map (tidyTyVarOcc tidy_env) bad_tvs
2791 ; typeintype <- xoptM LangExt.TypeInType
2792 ; mapM_ (report typeintype tidy_all_tvs) tidy_bad_tvs }
2793 where
2794 report typeintype tidy_all_tvs tidy_bad_tv
2795 = addErr $
2796 vcat [ text "Kind variable" <+> quotes (ppr tidy_bad_tv) <+>
2797 text "is implicitly bound in" <+> ppr flav
2798 , quotes (ppr tycon_name) <> comma <+>
2799 text "but does not appear as the kind of any"
2800 , text "of its type variables. Perhaps you meant"
2801 , text "to bind it" <+> ppWhen (not typeintype)
2802 (text "(with TypeInType)") <+>
2803 text "explicitly somewhere?"
2804 , ppWhen (not (null tidy_all_tvs)) $
2805 hang (text "Type variables with inferred kinds:")
2806 2 (ppr_tv_bndrs tidy_all_tvs) ]
2807
2808 ppr_tv_bndrs tvs = sep (map pp_tv tvs)
2809 pp_tv tv = parens (ppr tv <+> dcolon <+> ppr (tyVarKind tv))