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