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