A bit more -ddump-tc tracing
[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, tcImplicitTKBndrsType, tcExplicitTKBndrs,
22
23 -- Type checking type and class decls
24 kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars,
25 tcDataKindSig,
26
27 -- Kind-checking types
28 -- No kind generalisation, no checkValidType
29 tcWildCardBinders,
30 kcHsTyVarBndrs,
31 tcHsLiftedType, tcHsOpenType,
32 tcHsLiftedTypeNC, tcHsOpenTypeNC,
33 tcLHsType, tcCheckLHsType,
34 tcHsContext, tcLHsPredType, tcInferApps, tcTyApps,
35 solveEqualities, -- useful re-export
36
37 typeLevelMode, kindLevelMode,
38
39 kindGeneralize, checkExpectedKindX, instantiateTyUntilN,
40
41 -- Sort-checking kinds
42 tcLHsKindSig,
43
44 -- Pattern type signatures
45 tcHsPatSigType, tcPatSig, funAppCtxt
46 ) where
47
48 #include "HsVersions.h"
49
50 import HsSyn
51 import TcRnMonad
52 import TcEvidence
53 import TcEnv
54 import TcMType
55 import TcValidity
56 import TcUnify
57 import TcIface
58 import TcSimplify ( solveEqualities )
59 import TcType
60 import TcHsSyn( zonkSigType )
61 import Inst ( tcInstBinders, tcInstBinder )
62 import Type
63 import Kind
64 import RdrName( lookupLocalRdrOcc )
65 import Var
66 import VarSet
67 import TyCon
68 import ConLike
69 import DataCon
70 import Class
71 import Name
72 import NameEnv
73 import NameSet
74 import VarEnv
75 import TysWiredIn
76 import BasicTypes
77 import SrcLoc
78 import Constants ( mAX_CTUPLE_SIZE )
79 import ErrUtils( MsgDoc )
80 import Unique
81 import Util
82 import UniqSupply
83 import Outputable
84 import FastString
85 import PrelNames hiding ( wildCardName )
86 import qualified GHC.LanguageExtensions as LangExt
87
88 import Maybes
89 import Data.List ( partition, zipWith4 )
90 import Control.Monad
91
92 {-
93 ----------------------------
94 General notes
95 ----------------------------
96
97 Unlike with expressions, type-checking types both does some checking and
98 desugars at the same time. This is necessary because we often want to perform
99 equality checks on the types right away, and it would be incredibly painful
100 to do this on un-desugared types. Luckily, desugared types are close enough
101 to HsTypes to make the error messages sane.
102
103 During type-checking, we perform as little validity checking as possible.
104 This is because some type-checking is done in a mutually-recursive knot, and
105 if we look too closely at the tycons, we'll loop. This is why we always must
106 use mkNakedTyConApp and mkNakedAppTys, etc., which never look at a tycon.
107 The mkNamed... functions don't uphold Type invariants, but zonkTcTypeToType
108 will repair this for us. Note that zonkTcType *is* safe within a knot, and
109 can be done repeatedly with no ill effect: it just squeezes out metavariables.
110
111 Generally, after type-checking, you will want to do validity checking, say
112 with TcValidity.checkValidType.
113
114 Validity checking
115 ~~~~~~~~~~~~~~~~~
116 Some of the validity check could in principle be done by the kind checker,
117 but not all:
118
119 - During desugaring, we normalise by expanding type synonyms. Only
120 after this step can we check things like type-synonym saturation
121 e.g. type T k = k Int
122 type S a = a
123 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
124 and then S is saturated. This is a GHC extension.
125
126 - Similarly, also a GHC extension, we look through synonyms before complaining
127 about the form of a class or instance declaration
128
129 - Ambiguity checks involve functional dependencies, and it's easier to wait
130 until knots have been resolved before poking into them
131
132 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
133 finished building the loop. So to keep things simple, we postpone most validity
134 checking until step (3).
135
136 Knot tying
137 ~~~~~~~~~~
138 During step (1) we might fault in a TyCon defined in another module, and it might
139 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
140 knot around type declarations with ARecThing, so that the fault-in code can get
141 the TyCon being defined.
142
143 %************************************************************************
144 %* *
145 Check types AND do validity checking
146 * *
147 ************************************************************************
148 -}
149
150 funsSigCtxt :: [Located Name] -> UserTypeCtxt
151 -- Returns FunSigCtxt, with no redundant-context-reporting,
152 -- form a list of located names
153 funsSigCtxt (L _ name1 : _) = FunSigCtxt name1 False
154 funsSigCtxt [] = panic "funSigCtxt"
155
156 addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
157 addSigCtxt ctxt hs_ty thing_inside
158 = setSrcSpan (getLoc hs_ty) $
159 addErrCtxt (pprSigCtxt ctxt hs_ty) $
160 thing_inside
161
162 pprSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> SDoc
163 -- (pprSigCtxt ctxt <extra> <type>)
164 -- prints In the type signature for 'f':
165 -- f :: <type>
166 -- The <extra> is either empty or "the ambiguity check for"
167 pprSigCtxt ctxt hs_ty
168 | Just n <- isSigMaybe ctxt
169 = hang (text "In the type signature:")
170 2 (pprPrefixOcc n <+> dcolon <+> ppr hs_ty)
171
172 | otherwise
173 = hang (text "In" <+> pprUserTypeCtxt ctxt <> colon)
174 2 (ppr hs_ty)
175
176 tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
177 -- This one is used when we have a LHsSigWcType, but in
178 -- a place where wildards aren't allowed. The renamer has
179 -- already checked this, so we can simply ignore it.
180 tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
181
182 kcHsSigType :: [Located Name] -> LHsSigType GhcRn -> TcM ()
183 kcHsSigType names (HsIB { hsib_body = hs_ty
184 , hsib_vars = sig_vars })
185 = addSigCtxt (funsSigCtxt names) hs_ty $
186 discardResult $
187 tcImplicitTKBndrsType sig_vars $
188 tc_lhs_type typeLevelMode hs_ty liftedTypeKind
189
190 tcClassSigType :: [Located Name] -> LHsSigType GhcRn -> TcM Type
191 -- Does not do validity checking; this must be done outside
192 -- the recursive class declaration "knot"
193 tcClassSigType names sig_ty
194 = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
195 tc_hs_sig_type_and_gen sig_ty liftedTypeKind
196
197 tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
198 -- Does validity checking
199 tcHsSigType ctxt sig_ty
200 = addSigCtxt ctxt (hsSigType sig_ty) $
201 do { kind <- case expectedKindInCtxt ctxt of
202 AnythingKind -> newMetaKindVar
203 TheKind k -> return k
204 OpenKind -> newOpenTypeKind
205 -- The kind is checked by checkValidType, and isn't necessarily
206 -- of kind * in a Template Haskell quote eg [t| Maybe |]
207
208 -- Generalise here: see Note [Kind generalisation]
209 ; do_kind_gen <- decideKindGeneralisationPlan sig_ty
210 ; ty <- if do_kind_gen
211 then tc_hs_sig_type_and_gen sig_ty kind
212 else tc_hs_sig_type sig_ty kind >>= zonkTcType
213
214 ; checkValidType ctxt ty
215 ; return ty }
216
217 tc_hs_sig_type_and_gen :: LHsSigType GhcRn -> Kind -> TcM Type
218 -- Kind-checks/desugars an 'LHsSigType',
219 -- solve equalities,
220 -- and then kind-generalizes.
221 -- This will never emit constraints, as it uses solveEqualities interally.
222 -- No validity checking, but it does zonk en route to generalization
223 tc_hs_sig_type_and_gen hs_ty kind
224 = do { ty <- solveEqualities $
225 tc_hs_sig_type hs_ty kind
226 -- NB the call to solveEqualities, which unifies all those
227 -- kind variables floating about, immediately prior to
228 -- kind generalisation
229 ; kindGeneralizeType ty }
230
231 tc_hs_sig_type :: LHsSigType GhcRn -> Kind -> TcM Type
232 -- Kind-check/desugar a 'LHsSigType', but does not solve
233 -- the equalities that arise from doing so; instead it may
234 -- emit kind-equality constraints into the monad
235 -- No zonking or validity checking
236 tc_hs_sig_type (HsIB { hsib_vars = sig_vars
237 , hsib_body = hs_ty }) kind
238 = do { (tkvs, ty) <- tcImplicitTKBndrsType sig_vars $
239 tc_lhs_type typeLevelMode hs_ty kind
240 ; return (mkSpecForAllTys tkvs ty) }
241
242 -----------------
243 tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
244 -- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
245 -- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
246 -- E.g. class C (a::*) (b::k->k)
247 -- data T a b = ... deriving( C Int )
248 -- returns ([k], C, [k, Int], [k->k])
249 tcHsDeriv hs_ty
250 = do { cls_kind <- newMetaKindVar
251 -- always safe to kind-generalize, because there
252 -- can be no covars in an outer scope
253 ; ty <- checkNoErrs $
254 -- avoid redundant error report with "illegal deriving", below
255 tc_hs_sig_type_and_gen hs_ty cls_kind
256 ; cls_kind <- zonkTcType cls_kind
257 ; let (tvs, pred) = splitForAllTys ty
258 ; let (args, _) = splitFunTys cls_kind
259 ; case getClassPredTys_maybe pred of
260 Just (cls, tys) -> return (tvs, cls, tys, args)
261 Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
262
263 tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt
264 -> LHsSigType GhcRn
265 -> TcM ([TyVar], ThetaType, Class, [Type])
266 -- Like tcHsSigType, but for a class instance declaration
267 tcHsClsInstType user_ctxt hs_inst_ty
268 = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
269 do { inst_ty <- tc_hs_sig_type_and_gen hs_inst_ty constraintKind
270 ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
271
272 -- Used for 'VECTORISE [SCALAR] instance' declarations
273 tcHsVectInst :: LHsSigType GhcRn -> TcM (Class, [Type])
274 tcHsVectInst ty
275 | let hs_cls_ty = hsSigType ty
276 , Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe hs_cls_ty
277 -- Ignoring the binders looks pretty dodgy to me
278 = do { (cls, cls_kind) <- tcClass cls_name
279 ; (applied_class, _res_kind)
280 <- tcTyApps typeLevelMode hs_cls_ty (mkClassPred cls []) cls_kind tys
281 ; case tcSplitTyConApp_maybe applied_class of
282 Just (_tc, args) -> ASSERT( _tc == classTyCon cls )
283 return (cls, args)
284 _ -> failWithTc (text "Too many arguments passed to" <+> ppr cls_name) }
285 | otherwise
286 = failWithTc $ text "Malformed instance type"
287
288 ----------------------------------------------
289 -- | Type-check a visible type application
290 tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
291 tcHsTypeApp wc_ty kind
292 | HsWC { hswc_wcs = sig_wcs, hswc_body = hs_ty } <- wc_ty
293 = do { ty <- tcWildCardBindersX newWildTyVar sig_wcs $ \ _ ->
294 tcCheckLHsType hs_ty kind
295 ; ty <- zonkTcType ty
296 ; checkValidType TypeAppCtxt ty
297 ; return ty }
298 -- NB: we don't call emitWildcardHoleConstraints here, because
299 -- we want any holes in visible type applications to be used
300 -- without fuss. No errors, warnings, extensions, etc.
301
302 {-
303 ************************************************************************
304 * *
305 The main kind checker: no validity checks here
306 * *
307 ************************************************************************
308
309 First a couple of simple wrappers for kcHsType
310 -}
311
312 ---------------------------
313 tcHsOpenType, tcHsLiftedType,
314 tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
315 -- Used for type signatures
316 -- Do not do validity checking
317 tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty
318 tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty
319
320 tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind
321 ; tc_lhs_type typeLevelMode ty ek }
322 tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
323
324 -- Like tcHsType, but takes an expected kind
325 tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
326 tcCheckLHsType hs_ty exp_kind
327 = addTypeCtxt hs_ty $
328 tc_lhs_type typeLevelMode hs_ty exp_kind
329
330 tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
331 -- Called from outside: set the context
332 tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
333
334 ---------------------------
335 -- | Should we generalise the kind of this type signature?
336 -- We *should* generalise if the type is closed
337 -- or if NoMonoLocalBinds is set. Otherwise, nope.
338 -- See Note [Kind generalisation plan]
339 decideKindGeneralisationPlan :: LHsSigType GhcRn -> TcM Bool
340 decideKindGeneralisationPlan sig_ty@(HsIB { hsib_closed = closed })
341 = do { mono_locals <- xoptM LangExt.MonoLocalBinds
342 ; let should_gen = not mono_locals || closed
343 ; traceTc "decideKindGeneralisationPlan"
344 (ppr sig_ty $$ text "should gen?" <+> ppr should_gen)
345 ; return should_gen }
346
347 {- Note [Kind generalisation plan]
348 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
349 When should we do kind-generalisation for user-written type signature?
350 Answer: we use the same rule as for value bindings:
351
352 * We always kind-generalise if the type signature is closed
353 * Additionally, we attempt to generalise if we have NoMonoLocalBinds
354
355 Trac #13337 shows the problem if we kind-generalise an open type (i.e.
356 one that mentions in-scope tpe variable
357 foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
358 => proxy a -> String
359 foo _ = case eqT :: Maybe (k :~: Type) of
360 Nothing -> ...
361 Just Refl -> case eqT :: Maybe (a :~: Int) of ...
362
363 In the expression type sig on the last line, we have (a :: k)
364 but (Int :: Type). Since (:~:) is kind-homogeneous, this requires
365 k ~ *, which is true in the Refl branch of the outer case.
366
367 That equality will be solved if we allow it to float out to the
368 implication constraint for the Refl match, bnot not if we aggressively
369 attempt to solve all equalities the moment they occur; that is, when
370 checking (Maybe (a :~: Int)). (NB: solveEqualities fails unless it
371 solves all the kind equalities, which is the right thing at top level.)
372
373 So here the right thing is simply not to do kind generalisation!
374
375 ************************************************************************
376 * *
377 Type-checking modes
378 * *
379 ************************************************************************
380
381 The kind-checker is parameterised by a TcTyMode, which contains some
382 information about where we're checking a type.
383
384 The renamer issues errors about what it can. All errors issued here must
385 concern things that the renamer can't handle.
386
387 -}
388
389 -- | Info about the context in which we're checking a type. Currently,
390 -- differentiates only between types and kinds, but this will likely
391 -- grow, at least to include the distinction between patterns and
392 -- not-patterns.
393 newtype TcTyMode
394 = TcTyMode { mode_level :: TypeOrKind -- True <=> type, False <=> kind
395 }
396
397 typeLevelMode :: TcTyMode
398 typeLevelMode = TcTyMode { mode_level = TypeLevel }
399
400 kindLevelMode :: TcTyMode
401 kindLevelMode = TcTyMode { mode_level = KindLevel }
402
403 -- switch to kind level
404 kindLevel :: TcTyMode -> TcTyMode
405 kindLevel mode = mode { mode_level = KindLevel }
406
407 instance Outputable TcTyMode where
408 ppr = ppr . mode_level
409
410 {-
411 Note [Bidirectional type checking]
412 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
413 In expressions, whenever we see a polymorphic identifier, say `id`, we are
414 free to instantiate it with metavariables, knowing that we can always
415 re-generalize with type-lambdas when necessary. For example:
416
417 rank2 :: (forall a. a -> a) -> ()
418 x = rank2 id
419
420 When checking the body of `x`, we can instantiate `id` with a metavariable.
421 Then, when we're checking the application of `rank2`, we notice that we really
422 need a polymorphic `id`, and then re-generalize over the unconstrained
423 metavariable.
424
425 In types, however, we're not so lucky, because *we cannot re-generalize*!
426 There is no lambda. So, we must be careful only to instantiate at the last
427 possible moment, when we're sure we're never going to want the lost polymorphism
428 again. This is done in calls to tcInstBinders.
429
430 To implement this behavior, we use bidirectional type checking, where we
431 explicitly think about whether we know the kind of the type we're checking
432 or not. Note that there is a difference between not knowing a kind and
433 knowing a metavariable kind: the metavariables are TauTvs, and cannot become
434 forall-quantified kinds. Previously (before dependent types), there were
435 no higher-rank kinds, and so we could instantiate early and be sure that
436 no types would have polymorphic kinds, and so we could always assume that
437 the kind of a type was a fresh metavariable. Not so anymore, thus the
438 need for two algorithms.
439
440 For HsType forms that can never be kind-polymorphic, we implement only the
441 "down" direction, where we safely assume a metavariable kind. For HsType forms
442 that *can* be kind-polymorphic, we implement just the "up" (functions with
443 "infer" in their name) version, as we gain nothing by also implementing the
444 "down" version.
445
446 Note [Future-proofing the type checker]
447 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
448 As discussed in Note [Bidirectional type checking], each HsType form is
449 handled in *either* tc_infer_hs_type *or* tc_hs_type. These functions
450 are mutually recursive, so that either one can work for any type former.
451 But, we want to make sure that our pattern-matches are complete. So,
452 we have a bunch of repetitive code just so that we get warnings if we're
453 missing any patterns.
454 -}
455
456 ------------------------------------------
457 -- | Check and desugar a type, returning the core type and its
458 -- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
459 -- level.
460 tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
461 tc_infer_lhs_type mode (L span ty)
462 = setSrcSpan span $
463 do { (ty', kind) <- tc_infer_hs_type mode ty
464 ; return (ty', kind) }
465
466 -- | Infer the kind of a type and desugar. This is the "up" type-checker,
467 -- as described in Note [Bidirectional type checking]
468 tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
469 tc_infer_hs_type mode (HsTyVar _ (L _ tv)) = tcTyVar mode tv
470 tc_infer_hs_type mode (HsAppTy ty1 ty2)
471 = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
472 ; (fun_ty', fun_kind) <- tc_infer_lhs_type mode fun_ty
473 ; fun_kind' <- zonkTcType fun_kind
474 ; tcTyApps mode fun_ty fun_ty' fun_kind' arg_tys }
475 tc_infer_hs_type mode (HsParTy t) = tc_infer_lhs_type mode t
476 tc_infer_hs_type mode (HsOpTy lhs (L loc_op op) rhs)
477 | not (op `hasKey` funTyConKey)
478 = do { (op', op_kind) <- tcTyVar mode op
479 ; op_kind' <- zonkTcType op_kind
480 ; tcTyApps mode (noLoc $ HsTyVar NotPromoted (L loc_op op)) op' op_kind' [lhs, rhs] }
481 tc_infer_hs_type mode (HsKindSig ty sig)
482 = do { sig' <- tc_lhs_kind (kindLevel mode) sig
483 ; ty' <- tc_lhs_type mode ty sig'
484 ; return (ty', sig') }
485 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
486 -- the splice location to the typechecker. Here we skip over it in order to have
487 -- the same kind inferred for a given expression whether it was produced from
488 -- splices or not.
489 --
490 -- See Note [Delaying modFinalizers in untyped splices].
491 tc_infer_hs_type mode (HsSpliceTy (HsSpliced _ (HsSplicedTy ty)) _)
492 = tc_infer_hs_type mode ty
493 tc_infer_hs_type mode (HsDocTy ty _) = tc_infer_lhs_type mode ty
494 tc_infer_hs_type _ (HsCoreTy ty) = return (ty, typeKind ty)
495 tc_infer_hs_type mode other_ty
496 = do { kv <- newMetaKindVar
497 ; ty' <- tc_hs_type mode other_ty kv
498 ; return (ty', kv) }
499
500 ------------------------------------------
501 tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
502 tc_lhs_type mode (L span ty) exp_kind
503 = setSrcSpan span $
504 do { ty' <- tc_hs_type mode ty exp_kind
505 ; return ty' }
506
507 ------------------------------------------
508 tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
509 -> TcM TcType
510 tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
511 TypeLevel ->
512 do { arg_k <- newOpenTypeKind
513 ; res_k <- newOpenTypeKind
514 ; ty1' <- tc_lhs_type mode ty1 arg_k
515 ; ty2' <- tc_lhs_type mode ty2 res_k
516 ; checkExpectedKind (HsFunTy ty1 ty2) (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
517 KindLevel -> -- no representation polymorphism in kinds. yet.
518 do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
519 ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
520 ; checkExpectedKind (HsFunTy ty1 ty2) (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
521
522 ------------------------------------------
523 -- See also Note [Bidirectional type checking]
524 tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
525 tc_hs_type mode (HsParTy ty) exp_kind = tc_lhs_type mode ty exp_kind
526 tc_hs_type mode (HsDocTy ty _) exp_kind = tc_lhs_type mode ty exp_kind
527 tc_hs_type _ ty@(HsBangTy {}) _
528 -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
529 -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
530 -- bangs are invalid, so fail. (#7210)
531 = failWithTc (text "Unexpected strictness annotation:" <+> ppr ty)
532 tc_hs_type _ ty@(HsRecTy _) _
533 -- Record types (which only show up temporarily in constructor
534 -- signatures) should have been removed by now
535 = failWithTc (text "Record syntax is illegal here:" <+> ppr ty)
536
537 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType'.
538 -- Here we get rid of it and add the finalizers to the global environment
539 -- while capturing the local environment.
540 --
541 -- See Note [Delaying modFinalizers in untyped splices].
542 tc_hs_type mode (HsSpliceTy (HsSpliced mod_finalizers (HsSplicedTy ty))
543 _
544 )
545 exp_kind
546 = do addModFinalizersWithLclEnv mod_finalizers
547 tc_hs_type mode ty exp_kind
548
549 -- This should never happen; type splices are expanded by the renamer
550 tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind
551 = failWithTc (text "Unexpected type splice:" <+> ppr ty)
552
553 ---------- Functions and applications
554 tc_hs_type mode (HsFunTy ty1 ty2) exp_kind
555 = tc_fun_type mode ty1 ty2 exp_kind
556
557 tc_hs_type mode (HsOpTy ty1 (L _ op) ty2) exp_kind
558 | op `hasKey` funTyConKey
559 = tc_fun_type mode ty1 ty2 exp_kind
560
561 --------- Foralls
562 tc_hs_type mode (HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
563 = fmap fst $
564 tcExplicitTKBndrs hs_tvs $ \ tvs' ->
565 -- Do not kind-generalise here! See Note [Kind generalisation]
566 -- Why exp_kind? See Note [Body kind of HsForAllTy]
567 do { ty' <- tc_lhs_type mode ty exp_kind
568 ; let bound_vars = allBoundVariables ty'
569 bndrs = mkTyVarBinders Specified tvs'
570 ; return (mkForAllTys bndrs ty', bound_vars) }
571
572 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
573 | null (unLoc ctxt)
574 = tc_lhs_type mode ty exp_kind
575
576 | otherwise
577 = do { ctxt' <- tc_hs_context mode ctxt
578
579 -- See Note [Body kind of a HsQualTy]
580 ; ty' <- if isConstraintKind exp_kind
581 then tc_lhs_type mode ty constraintKind
582 else do { ek <- newOpenTypeKind
583 -- The body kind (result of the function)
584 -- can be * or #, hence newOpenTypeKind
585 ; ty' <- tc_lhs_type mode ty ek
586 ; checkExpectedKind (unLoc ty) ty' liftedTypeKind exp_kind }
587
588 ; return (mkPhiTy ctxt' ty') }
589
590 --------- Lists, arrays, and tuples
591 tc_hs_type mode rn_ty@(HsListTy elt_ty) exp_kind
592 = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
593 ; checkWiredInTyCon listTyCon
594 ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
595
596 tc_hs_type mode rn_ty@(HsPArrTy elt_ty) exp_kind
597 = do { MASSERT( isTypeLevel (mode_level mode) )
598 ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
599 ; checkWiredInTyCon parrTyCon
600 ; checkExpectedKind rn_ty (mkPArrTy tau_ty) liftedTypeKind exp_kind }
601
602 -- See Note [Distinguishing tuple kinds] in HsTypes
603 -- See Note [Inferring tuple kinds]
604 tc_hs_type mode rn_ty@(HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind
605 -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
606 | Just tup_sort <- tupKindSort_maybe exp_kind
607 = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
608 tc_tuple rn_ty mode tup_sort hs_tys exp_kind
609 | otherwise
610 = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
611 ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
612 ; kinds <- mapM zonkTcType kinds
613 -- Infer each arg type separately, because errors can be
614 -- confusing if we give them a shared kind. Eg Trac #7410
615 -- (Either Int, Int), we do not want to get an error saying
616 -- "the second argument of a tuple should have kind *->*"
617
618 ; let (arg_kind, tup_sort)
619 = case [ (k,s) | k <- kinds
620 , Just s <- [tupKindSort_maybe k] ] of
621 ((k,s) : _) -> (k,s)
622 [] -> (liftedTypeKind, BoxedTuple)
623 -- In the [] case, it's not clear what the kind is, so guess *
624
625 ; tys' <- sequence [ setSrcSpan loc $
626 checkExpectedKind hs_ty ty kind arg_kind
627 | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
628
629 ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
630
631
632 tc_hs_type mode rn_ty@(HsTupleTy hs_tup_sort tys) exp_kind
633 = tc_tuple rn_ty mode tup_sort tys exp_kind
634 where
635 tup_sort = case hs_tup_sort of -- Fourth case dealt with above
636 HsUnboxedTuple -> UnboxedTuple
637 HsBoxedTuple -> BoxedTuple
638 HsConstraintTuple -> ConstraintTuple
639 _ -> panic "tc_hs_type HsTupleTy"
640
641 tc_hs_type mode rn_ty@(HsSumTy hs_tys) exp_kind
642 = do { let arity = length hs_tys
643 ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
644 ; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
645 ; let arg_reps = map (getRuntimeRepFromKind "tc_hs_type HsSumTy") arg_kinds
646 arg_tys = arg_reps ++ tau_tys
647 ; checkExpectedKind rn_ty
648 (mkTyConApp (sumTyCon arity) arg_tys)
649 (unboxedSumKind arg_reps)
650 exp_kind
651 }
652
653 --------- Promoted lists and tuples
654 tc_hs_type mode rn_ty@(HsExplicitListTy _ _k tys) exp_kind
655 = do { tks <- mapM (tc_infer_lhs_type mode) tys
656 ; (taus', kind) <- unifyKinds tys tks
657 ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
658 ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
659 where
660 mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
661 mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k]
662
663 tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
664 -- using newMetaKindVar means that we force instantiations of any polykinded
665 -- types. At first, I just used tc_infer_lhs_type, but that led to #11255.
666 = do { ks <- replicateM arity newMetaKindVar
667 ; taus <- zipWithM (tc_lhs_type mode) tys ks
668 ; let kind_con = tupleTyCon Boxed arity
669 ty_con = promotedTupleDataCon Boxed arity
670 tup_k = mkTyConApp kind_con ks
671 ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
672 where
673 arity = length tys
674
675 --------- Constraint types
676 tc_hs_type mode rn_ty@(HsIParamTy (L _ n) ty) exp_kind
677 = do { MASSERT( isTypeLevel (mode_level mode) )
678 ; ty' <- tc_lhs_type mode ty liftedTypeKind
679 ; let n' = mkStrLitTy $ hsIPNameFS n
680 ; ipClass <- tcLookupClass ipClassName
681 ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
682 constraintKind exp_kind }
683
684 tc_hs_type mode rn_ty@(HsEqTy ty1 ty2) exp_kind
685 = do { (ty1', kind1) <- tc_infer_lhs_type mode ty1
686 ; (ty2', kind2) <- tc_infer_lhs_type mode ty2
687 ; ty2'' <- checkExpectedKind (unLoc ty2) ty2' kind2 kind1
688 ; eq_tc <- tcLookupTyCon eqTyConName
689 ; let ty' = mkNakedTyConApp eq_tc [kind1, ty1', ty2'']
690 ; checkExpectedKind rn_ty ty' constraintKind exp_kind }
691
692 --------- Literals
693 tc_hs_type _ rn_ty@(HsTyLit (HsNumTy _ n)) exp_kind
694 = do { checkWiredInTyCon typeNatKindCon
695 ; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
696
697 tc_hs_type _ rn_ty@(HsTyLit (HsStrTy _ s)) exp_kind
698 = do { checkWiredInTyCon typeSymbolKindCon
699 ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
700
701 --------- Potentially kind-polymorphic types: call the "up" checker
702 -- See Note [Future-proofing the type checker]
703 tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
704 tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek
705 tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
706 tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
707 tc_hs_type mode ty@(HsCoreTy {}) ek = tc_infer_hs_type_ek mode ty ek
708
709 tc_hs_type _ (HsWildCardTy wc) exp_kind
710 = do { wc_tv <- tcWildCardOcc wc exp_kind
711 ; return (mkTyVarTy wc_tv) }
712
713 -- disposed of by renamer
714 tc_hs_type _ ty@(HsAppsTy {}) _
715 = pprPanic "tc_hs_tyep HsAppsTy" (ppr ty)
716
717 tcWildCardOcc :: HsWildCardInfo GhcRn -> Kind -> TcM TcTyVar
718 tcWildCardOcc wc_info exp_kind
719 = do { wc_tv <- tcLookupTyVar (wildCardName wc_info)
720 -- The wildcard's kind should be an un-filled-in meta tyvar
721 ; let Just wc_kind_var = tcGetTyVar_maybe (tyVarKind wc_tv)
722 ; writeMetaTyVar wc_kind_var exp_kind
723 ; return wc_tv }
724
725 ---------------------------
726 -- | Call 'tc_infer_hs_type' and check its result against an expected kind.
727 tc_infer_hs_type_ek :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
728 tc_infer_hs_type_ek mode ty ek
729 = do { (ty', k) <- tc_infer_hs_type mode ty
730 ; checkExpectedKind ty ty' k ek }
731
732 ---------------------------
733 tupKindSort_maybe :: TcKind -> Maybe TupleSort
734 tupKindSort_maybe k
735 | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
736 | Just k' <- tcView k = tupKindSort_maybe k'
737 | isConstraintKind k = Just ConstraintTuple
738 | isLiftedTypeKind k = Just BoxedTuple
739 | otherwise = Nothing
740
741 tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
742 tc_tuple rn_ty mode tup_sort tys exp_kind
743 = do { arg_kinds <- case tup_sort of
744 BoxedTuple -> return (nOfThem arity liftedTypeKind)
745 UnboxedTuple -> mapM (\_ -> newOpenTypeKind) tys
746 ConstraintTuple -> return (nOfThem arity constraintKind)
747 ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
748 ; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
749 where
750 arity = length tys
751
752 finish_tuple :: HsType GhcRn
753 -> TupleSort
754 -> [TcType] -- ^ argument types
755 -> [TcKind] -- ^ of these kinds
756 -> TcKind -- ^ expected kind of the whole tuple
757 -> TcM TcType
758 finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
759 = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
760 ; let arg_tys = case tup_sort of
761 -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
762 UnboxedTuple -> tau_reps ++ tau_tys
763 BoxedTuple -> tau_tys
764 ConstraintTuple -> tau_tys
765 ; tycon <- case tup_sort of
766 ConstraintTuple
767 | arity > mAX_CTUPLE_SIZE
768 -> failWith (bigConstraintTuple arity)
769 | otherwise -> tcLookupTyCon (cTupleTyConName arity)
770 BoxedTuple -> do { let tc = tupleTyCon Boxed arity
771 ; checkWiredInTyCon tc
772 ; return tc }
773 UnboxedTuple -> return (tupleTyCon Unboxed arity)
774 ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind }
775 where
776 arity = length tau_tys
777 tau_reps = map (getRuntimeRepFromKind "finish_tuple") tau_kinds
778 res_kind = case tup_sort of
779 UnboxedTuple -> unboxedTupleKind tau_reps
780 BoxedTuple -> liftedTypeKind
781 ConstraintTuple -> constraintKind
782
783 bigConstraintTuple :: Arity -> MsgDoc
784 bigConstraintTuple arity
785 = hang (text "Constraint tuple arity too large:" <+> int arity
786 <+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
787 2 (text "Instead, use a nested tuple")
788
789 ---------------------------
790 -- | Apply a type of a given kind to a list of arguments. This instantiates
791 -- invisible parameters as necessary. Always consumes all the arguments,
792 -- using matchExpectedFunKind as necessary.
793 -- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.
794 -- These kinds should be used to instantiate invisible kind variables;
795 -- they come from an enclosing class for an associated type/data family.
796 tcInferApps :: TcTyMode
797 -> Maybe (VarEnv Kind) -- ^ Possibly, kind info (see above)
798 -> LHsType GhcRn -- ^ Function (for printing only)
799 -> TcType -- ^ Function (could be knot-tied)
800 -> TcKind -- ^ Function kind (zonked)
801 -> [LHsType GhcRn] -- ^ Args
802 -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
803 tcInferApps mode mb_kind_info orig_ty ty ki args
804 = do { traceTc "tcInferApps" (ppr orig_ty $$ ppr args $$ ppr ki)
805 ; go [] [] orig_subst ty orig_ki_binders orig_inner_ki args 1 }
806 where
807 orig_subst = mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfType ki
808 (orig_ki_binders, orig_inner_ki) = tcSplitPiTys ki
809
810 go :: [LHsType GhcRn] -- already type-checked args, in reverse order, for errors
811 -> [TcType] -- already type-checked args, in reverse order
812 -> TCvSubst -- instantiating substitution
813 -> TcType -- function applied to some args, could be knot-tied
814 -> [TyBinder] -- binders in function kind (both vis. and invis.)
815 -> TcKind -- function kind body (not a Pi-type)
816 -> [LHsType GhcRn] -- un-type-checked args
817 -> Int -- the # of the next argument
818 -> TcM (TcType, [TcType], TcKind) -- same as overall return type
819
820 -- no user-written args left. We're done!
821 go _acc_hs_args acc_args subst fun ki_binders inner_ki [] _
822 = return (fun, reverse acc_args, substTy subst $ mkPiTys ki_binders inner_ki)
823
824 -- The function's kind has a binder. Is it visible or invisible?
825 go acc_hs_args acc_args subst fun (ki_binder:ki_binders) inner_ki
826 all_args@(arg:args) n
827 | isInvisibleBinder ki_binder
828 -- It's invisible. Instantiate.
829 = do { traceTc "tcInferApps (invis)" (ppr ki_binder $$ ppr subst)
830 ; (subst', arg') <- tcInstBinder mb_kind_info subst ki_binder
831 ; go acc_hs_args (arg' : acc_args) subst' (mkNakedAppTy fun arg')
832 ki_binders inner_ki all_args n }
833
834 | otherwise
835 -- It's visible. Check the next user-written argument
836 = do { traceTc "tcInferApps (vis)" (ppr ki_binder $$ ppr arg $$ ppr subst)
837 ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
838 tc_lhs_type mode arg (substTy subst $ tyBinderType ki_binder)
839 ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
840 ; go (arg : acc_hs_args) (arg' : acc_args) subst' (mkNakedAppTy fun arg')
841 ki_binders inner_ki args (n+1) }
842
843 -- We've run out of known binders in the functions's kind.
844 go acc_hs_args acc_args subst fun [] inner_ki all_args n
845 | not (null new_ki_binders)
846 -- But, after substituting, we have more binders.
847 = go acc_hs_args acc_args zapped_subst fun new_ki_binders new_inner_ki all_args n
848
849 | otherwise
850 -- Even after substituting, still no binders. Use matchExpectedFunKind
851 = do { traceTc "tcInferApps (no binder)" (ppr new_inner_ki $$ ppr zapped_subst)
852 ; (co, arg_k, res_k)
853 <- matchExpectedFunKind (mkHsAppTys orig_ty (reverse acc_hs_args))
854 substed_inner_ki
855 ; let subst' = zapped_subst `extendTCvInScopeSet` tyCoVarsOfTypes [arg_k, res_k]
856 ; go acc_hs_args acc_args subst' (fun `mkNakedCastTy` co)
857 [mkAnonBinder arg_k] res_k all_args n }
858 where
859 substed_inner_ki = substTy subst inner_ki
860 (new_ki_binders, new_inner_ki) = tcSplitPiTys substed_inner_ki
861 zapped_subst = zapTCvSubst subst
862
863 -- | Applies a type to a list of arguments.
864 -- Always consumes all the arguments, using 'matchExpectedFunKind' as
865 -- necessary. If you wish to apply a type to a list of HsTypes, this is
866 -- your function.
867 -- Used for type-checking types only.
868 tcTyApps :: TcTyMode
869 -> LHsType GhcRn -- ^ Function (for printing only)
870 -> TcType -- ^ Function (could be knot-tied)
871 -> TcKind -- ^ Function kind (zonked)
872 -> [LHsType GhcRn] -- ^ Args
873 -> TcM (TcType, TcKind) -- ^ (f args, result kind)
874 tcTyApps mode orig_ty ty ki args
875 = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_ty ty ki args
876 ; return (ty', ki') }
877
878 --------------------------
879 -- like checkExpectedKindX, but returns only the final type; convenient wrapper
880 checkExpectedKind :: HsType GhcRn
881 -> TcType
882 -> TcKind
883 -> TcKind
884 -> TcM TcType
885 checkExpectedKind hs_ty ty act exp = fstOf3 <$> checkExpectedKindX Nothing (ppr hs_ty) ty act exp
886
887 checkExpectedKindX :: Maybe (VarEnv Kind) -- Possibly, instantiations for kind vars
888 -> SDoc -- HsType whose kind we're checking
889 -> TcType -- the type whose kind we're checking
890 -> TcKind -- the known kind of that type, k
891 -> TcKind -- the expected kind, exp_kind
892 -> TcM (TcType, [TcType], TcCoercionN)
893 -- (an possibly-inst'ed, casted type :: exp_kind, the new args, the coercion)
894 -- Instantiate a kind (if necessary) and then call unifyType
895 -- (checkExpectedKind ty act_kind exp_kind)
896 -- checks that the actual kind act_kind is compatible
897 -- with the expected kind exp_kind
898 checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
899 = do { (ty', new_args, act_kind') <- instantiate ty act_kind exp_kind
900 ; let origin = TypeEqOrigin { uo_actual = act_kind'
901 , uo_expected = exp_kind
902 , uo_thing = Just pp_hs_ty
903 , uo_visible = True } -- the hs_ty is visible
904 ; co_k <- uType KindLevel origin act_kind' exp_kind
905 ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
906 , ppr exp_kind
907 , ppr co_k ])
908 ; let result_ty = ty' `mkNakedCastTy` co_k
909 ; return (result_ty, new_args, co_k) }
910 where
911 -- we need to make sure that both kinds have the same number of implicit
912 -- foralls out front. If the actual kind has more, instantiate accordingly.
913 -- Otherwise, just pass the type & kind through -- the errors are caught
914 -- in unifyType.
915 instantiate :: TcType -- the type
916 -> TcKind -- of this kind
917 -> TcKind -- but expected to be of this one
918 -> TcM ( TcType -- the inst'ed type
919 , [TcType] -- the new args
920 , TcKind ) -- its new kind
921 instantiate ty act_ki exp_ki
922 = let (exp_bndrs, _) = splitPiTysInvisible exp_ki in
923 instantiateTyUntilN mb_kind_env (length exp_bndrs) ty act_ki
924
925 -- | Instantiate @n@ invisible arguments to a type. If @n <= 0@, no instantiation
926 -- occurs. If @n@ is too big, then all available invisible arguments are instantiated.
927 -- (In other words, this function is very forgiving about bad values of @n@.)
928 instantiateTyN :: Maybe (VarEnv Kind) -- ^ Predetermined instantiations
929 -- (for assoc. type patterns)
930 -> Int -- ^ @n@
931 -> TcType -- ^ the type
932 -> [TyBinder] -> TcKind -- ^ its kind
933 -> TcM (TcType, [TcType], TcKind) -- ^ The inst'ed type, new args, kind
934 instantiateTyN mb_kind_env n ty bndrs inner_ki
935 = let -- NB: splitAt is forgiving with invalid numbers
936 (inst_bndrs, leftover_bndrs) = splitAt n bndrs
937 ki = mkPiTys bndrs inner_ki
938 empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ki))
939 in
940 if n <= 0 then return (ty, [], ki) else
941 do { (subst, inst_args) <- tcInstBinders empty_subst mb_kind_env inst_bndrs
942 ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
943 ki' = substTy subst rebuilt_ki
944 ; traceTc "instantiateTyN" (vcat [ ppr ki
945 , ppr n
946 , ppr subst
947 , ppr rebuilt_ki
948 , ppr ki' ])
949 ; return (mkNakedAppTys ty inst_args, inst_args, ki') }
950
951 -- | Instantiate a type to have at most @n@ invisible arguments.
952 instantiateTyUntilN :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
953 -> Int -- ^ @n@
954 -> TcType -- ^ the type
955 -> TcKind -- ^ its kind
956 -> TcM (TcType, [TcType], TcKind) -- ^ The inst'ed type, new args,
957 -- final kind
958 instantiateTyUntilN mb_kind_env n ty ki
959 = let (bndrs, inner_ki) = splitPiTysInvisible ki
960 num_to_inst = length bndrs - n
961 in
962 instantiateTyN mb_kind_env num_to_inst ty bndrs inner_ki
963
964 ---------------------------
965 tcHsContext :: LHsContext GhcRn -> TcM [PredType]
966 tcHsContext = tc_hs_context typeLevelMode
967
968 tcLHsPredType :: LHsType GhcRn -> TcM PredType
969 tcLHsPredType = tc_lhs_pred typeLevelMode
970
971 tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
972 tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)
973
974 tc_lhs_pred :: TcTyMode -> LHsType GhcRn -> TcM PredType
975 tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
976
977 ---------------------------
978 tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
979 -- See Note [Type checking recursive type and class declarations]
980 -- in TcTyClsDecls
981 tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
982 = do { traceTc "lk1" (ppr name)
983 ; thing <- tcLookup name
984 ; case thing of
985 ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
986
987 ATcTyCon tc_tc -> do { -- See Note [GADT kind self-reference]
988 unless
989 (isTypeLevel (mode_level mode))
990 (promotionErr name TyConPE)
991 ; check_tc tc_tc
992 ; tc <- get_loopy_tc name tc_tc
993 ; handle_tyfams tc tc_tc }
994 -- mkNakedTyConApp: see Note [Type-checking inside the knot]
995 -- NB: we really should check if we're at the kind level
996 -- and if the tycon is promotable if -XNoTypeInType is set.
997 -- But this is a terribly large amount of work! Not worth it.
998
999 AGlobal (ATyCon tc)
1000 -> do { check_tc tc
1001 ; handle_tyfams tc tc }
1002
1003 AGlobal (AConLike (RealDataCon dc))
1004 -> do { data_kinds <- xoptM LangExt.DataKinds
1005 ; unless (data_kinds || specialPromotedDc dc) $
1006 promotionErr name NoDataKindsDC
1007 ; type_in_type <- xoptM LangExt.TypeInType
1008 ; unless ( type_in_type ||
1009 ( isTypeLevel (mode_level mode) &&
1010 isLegacyPromotableDataCon dc ) ||
1011 ( isKindLevel (mode_level mode) &&
1012 specialPromotedDc dc ) ) $
1013 promotionErr name NoTypeInTypeDC
1014 ; let tc = promoteDataCon dc
1015 ; return (mkNakedTyConApp tc [], tyConKind tc) }
1016
1017 APromotionErr err -> promotionErr name err
1018
1019 _ -> wrongThingErr "type" thing name }
1020 where
1021 check_tc :: TyCon -> TcM ()
1022 check_tc tc = do { type_in_type <- xoptM LangExt.TypeInType
1023 ; data_kinds <- xoptM LangExt.DataKinds
1024 ; unless (isTypeLevel (mode_level mode) ||
1025 data_kinds ||
1026 isKindTyCon tc) $
1027 promotionErr name NoDataKindsTC
1028 ; unless (isTypeLevel (mode_level mode) ||
1029 type_in_type ||
1030 isLegacyPromotableTyCon tc) $
1031 promotionErr name NoTypeInTypeTC }
1032
1033 -- if we are type-checking a type family tycon, we must instantiate
1034 -- any invisible arguments right away. Otherwise, we get #11246
1035 handle_tyfams :: TyCon -- the tycon to instantiate (might be loopy)
1036 -> TcTyCon -- a non-loopy version of the tycon
1037 -> TcM (TcType, TcKind)
1038 handle_tyfams tc tc_tc
1039 | mightBeUnsaturatedTyCon tc_tc
1040 = do { traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind)
1041 ; return (ty, tc_kind) }
1042
1043 | otherwise
1044 = do { (tc_ty, _, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc))
1045 ty tc_kind_bndrs tc_inner_ki
1046 -- tc and tc_ty must not be traced here, because that would
1047 -- force the evaluation of a potentially knot-tied variable (tc),
1048 -- and the typechecker would hang, as per #11708
1049 ; traceTc "tcTyVar2b" (vcat [ ppr tc_tc <+> dcolon <+> ppr tc_kind
1050 , ppr kind ])
1051 ; return (tc_ty, kind) }
1052 where
1053 ty = mkNakedTyConApp tc []
1054 tc_kind = tyConKind tc_tc
1055 (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
1056
1057 get_loopy_tc :: Name -> TyCon -> TcM TyCon
1058 -- Return the knot-tied global TyCon if there is one
1059 -- Otherwise the local TcTyCon; we must be doing kind checking
1060 -- but we still want to return a TyCon of some sort to use in
1061 -- error messages
1062 get_loopy_tc name tc_tc
1063 = do { env <- getGblEnv
1064 ; case lookupNameEnv (tcg_type_env env) name of
1065 Just (ATyCon tc) -> return tc
1066 _ -> do { traceTc "lk1 (loopy)" (ppr name)
1067 ; return tc_tc } }
1068
1069 tcClass :: Name -> TcM (Class, TcKind)
1070 tcClass cls -- Must be a class
1071 = do { thing <- tcLookup cls
1072 ; case thing of
1073 ATcTyCon tc -> return (aThingErr "tcClass" cls, tyConKind tc)
1074 AGlobal (ATyCon tc)
1075 | Just cls <- tyConClass_maybe tc
1076 -> return (cls, tyConKind tc)
1077 _ -> wrongThingErr "class" thing cls }
1078
1079
1080 aThingErr :: String -> Name -> b
1081 -- The type checker for types is sometimes called simply to
1082 -- do *kind* checking; and in that case it ignores the type
1083 -- returned. Which is a good thing since it may not be available yet!
1084 aThingErr str x = pprPanic "AThing evaluated unexpectedly" (text str <+> ppr x)
1085
1086 {-
1087 Note [Type-checking inside the knot]
1088 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1089 Suppose we are checking the argument types of a data constructor. We
1090 must zonk the types before making the DataCon, because once built we
1091 can't change it. So we must traverse the type.
1092
1093 BUT the parent TyCon is knot-tied, so we can't look at it yet.
1094
1095 So we must be careful not to use "smart constructors" for types that
1096 look at the TyCon or Class involved.
1097
1098 * Hence the use of mkNakedXXX functions. These do *not* enforce
1099 the invariants (for example that we use (FunTy s t) rather
1100 than (TyConApp (->) [s,t])).
1101
1102 * The zonking functions establish invariants (even zonkTcType, a change from
1103 previous behaviour). So we must never inspect the result of a
1104 zonk that might mention a knot-tied TyCon. This is generally OK
1105 because we zonk *kinds* while kind-checking types. And the TyCons
1106 in kinds shouldn't be knot-tied, because they come from a previous
1107 mutually recursive group.
1108
1109 * TcHsSyn.zonkTcTypeToType also can safely check/establish
1110 invariants.
1111
1112 This is horribly delicate. I hate it. A good example of how
1113 delicate it is can be seen in Trac #7903.
1114
1115 Note [GADT kind self-reference]
1116 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1117
1118 A promoted type cannot be used in the body of that type's declaration.
1119 Trac #11554 shows this example, which made GHC loop:
1120
1121 import Data.Kind
1122 data P (x :: k) = Q
1123 data A :: Type where
1124 B :: forall (a :: A). P a -> A
1125
1126 In order to check the constructor B, we need to have the promoted type A, but in
1127 order to get that promoted type, B must first be checked. To prevent looping, a
1128 TyConPE promotion error is given when tcTyVar checks an ATcTyCon in kind mode.
1129 Any ATcTyCon is a TyCon being defined in the current recursive group (see data
1130 type decl for TcTyThing), and all such TyCons are illegal in kinds.
1131
1132 Trac #11962 proposes checking the head of a data declaration separately from
1133 its constructors. This would allow the example above to pass.
1134
1135 Note [Body kind of a HsForAllTy]
1136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1137 The body of a forall is usually a type, but in principle
1138 there's no reason to prohibit *unlifted* types.
1139 In fact, GHC can itself construct a function with an
1140 unboxed tuple inside a for-all (via CPR analysis; see
1141 typecheck/should_compile/tc170).
1142
1143 Moreover in instance heads we get forall-types with
1144 kind Constraint.
1145
1146 It's tempting to check that the body kind is either * or #. But this is
1147 wrong. For example:
1148
1149 class C a b
1150 newtype N = Mk Foo deriving (C a)
1151
1152 We're doing newtype-deriving for C. But notice how `a` isn't in scope in
1153 the predicate `C a`. So we quantify, yielding `forall a. C a` even though
1154 `C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
1155 convenient. Bottom line: don't check for * or # here.
1156
1157 Note [Body kind of a HsQualTy]
1158 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1159 If ctxt is non-empty, the HsQualTy really is a /function/, so the
1160 kind of the result really is '*', and in that case the kind of the
1161 body-type can be lifted or unlifted.
1162
1163 However, consider
1164 instance Eq a => Eq [a] where ...
1165 or
1166 f :: (Eq a => Eq [a]) => blah
1167 Here both body-kind of the HsQualTy is Constraint rather than *.
1168 Rather crudely we tell the difference by looking at exp_kind. It's
1169 very convenient to typecheck instance types like any other HsSigType.
1170
1171 Admittedly the '(Eq a => Eq [a]) => blah' case is erroneous, but it's
1172 better to reject in checkValidType. If we say that the body kind
1173 should be '*' we risk getting TWO error messages, one saying that Eq
1174 [a] doens't have kind '*', and one saying that we need a Constraint to
1175 the left of the outer (=>).
1176
1177 How do we figure out the right body kind? Well, it's a bit of a
1178 kludge: I just look at the expected kind. If it's Constraint, we
1179 must be in this instance situation context. It's a kludge because it
1180 wouldn't work if any unification was involved to compute that result
1181 kind -- but it isn't. (The true way might be to use the 'mode'
1182 parameter, but that seemed like a sledgehammer to crack a nut.)
1183
1184 Note [Inferring tuple kinds]
1185 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1186 Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
1187 we try to figure out whether it's a tuple of kind * or Constraint.
1188 Step 1: look at the expected kind
1189 Step 2: infer argument kinds
1190
1191 If after Step 2 it's not clear from the arguments that it's
1192 Constraint, then it must be *. Once having decided that we re-check
1193 the Check the arguments again to give good error messages
1194 in eg. `(Maybe, Maybe)`
1195
1196 Note that we will still fail to infer the correct kind in this case:
1197
1198 type T a = ((a,a), D a)
1199 type family D :: Constraint -> Constraint
1200
1201 While kind checking T, we do not yet know the kind of D, so we will default the
1202 kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
1203
1204 Note [Desugaring types]
1205 ~~~~~~~~~~~~~~~~~~~~~~~
1206 The type desugarer is phase 2 of dealing with HsTypes. Specifically:
1207
1208 * It transforms from HsType to Type
1209
1210 * It zonks any kinds. The returned type should have no mutable kind
1211 or type variables (hence returning Type not TcType):
1212 - any unconstrained kind variables are defaulted to (Any *) just
1213 as in TcHsSyn.
1214 - there are no mutable type variables because we are
1215 kind-checking a type
1216 Reason: the returned type may be put in a TyCon or DataCon where
1217 it will never subsequently be zonked.
1218
1219 You might worry about nested scopes:
1220 ..a:kappa in scope..
1221 let f :: forall b. T '[a,b] -> Int
1222 In this case, f's type could have a mutable kind variable kappa in it;
1223 and we might then default it to (Any *) when dealing with f's type
1224 signature. But we don't expect this to happen because we can't get a
1225 lexically scoped type variable with a mutable kind variable in it. A
1226 delicate point, this. If it becomes an issue we might need to
1227 distinguish top-level from nested uses.
1228
1229 Moreover
1230 * it cannot fail,
1231 * it does no unifications
1232 * it does no validity checking, except for structural matters, such as
1233 (a) spurious ! annotations.
1234 (b) a class used as a type
1235
1236 Note [Kind of a type splice]
1237 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1238 Consider these terms, each with TH type splice inside:
1239 [| e1 :: Maybe $(..blah..) |]
1240 [| e2 :: $(..blah..) |]
1241 When kind-checking the type signature, we'll kind-check the splice
1242 $(..blah..); we want to give it a kind that can fit in any context,
1243 as if $(..blah..) :: forall k. k.
1244
1245 In the e1 example, the context of the splice fixes kappa to *. But
1246 in the e2 example, we'll desugar the type, zonking the kind unification
1247 variables as we go. When we encounter the unconstrained kappa, we
1248 want to default it to '*', not to (Any *).
1249
1250
1251 Help functions for type applications
1252 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1253 -}
1254
1255 addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
1256 -- Wrap a context around only if we want to show that contexts.
1257 -- Omit invisible ones and ones user's won't grok
1258 addTypeCtxt (L _ ty) thing
1259 = addErrCtxt doc thing
1260 where
1261 doc = text "In the type" <+> quotes (ppr ty)
1262
1263 {-
1264 ************************************************************************
1265 * *
1266 Type-variable binders
1267 %* *
1268 %************************************************************************
1269
1270 Note [Scope-check inferred kinds]
1271 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1272 Consider
1273
1274 data SameKind :: k -> k -> *
1275 foo :: forall a (b :: Proxy a) (c :: Proxy d). SameKind b c
1276
1277 d has no binding site. So it gets bound implicitly, at the top. The
1278 problem is that d's kind mentions `a`. So it's all ill-scoped.
1279
1280 The way we check for this is to gather all variables *bound* in a
1281 type variable's scope. The type variable's kind should not mention
1282 any of these variables. That is, d's kind can't mention a, b, or c.
1283 We can't just check to make sure that d's kind is in scope, because
1284 we might be about to kindGeneralize.
1285
1286 A little messy, but it works.
1287
1288 Note [Dependent LHsQTyVars]
1289 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1290 We track (in the renamer) which explicitly bound variables in a
1291 LHsQTyVars are manifestly dependent; only precisely these variables
1292 may be used within the LHsQTyVars. We must do this so that kcHsTyVarBndrs
1293 can produce the right TyConBinders, and tell Anon vs. Required.
1294
1295 Example data T k1 (a:k1) (b:k2) c
1296 = MkT (Proxy a) (Proxy b) (Proxy c)
1297
1298 Here
1299 (a:k1),(b:k2),(c:k3)
1300 are Anon (explicitly specified as a binder, not used
1301 in the kind of any other binder
1302 k1 is Required (explicitly specifed as a binder, but used
1303 in the kind of another binder i.e. dependently)
1304 k2 is Specified (not explicitly bound, but used in the kind
1305 of another binder)
1306 k3 in Inferred (not lexically in scope at all, but inferred
1307 by kind inference)
1308 and
1309 T :: forall {k3} k1. forall k3 -> k1 -> k2 -> k3 -> *
1310
1311 See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visiblity]
1312 in TyCoRep.
1313
1314 kcHsTyVarBndrs uses the hsq_dependent field to decide whether
1315 k1, a, b, c should be Required or Anon.
1316
1317 Earlier, thought it would work simply to do a free-variable check
1318 during kcHsTyVarBndrs, but this is bogus, because there may be
1319 unsolved equalities about. And we don't want to eagerly solve the
1320 equalities, because we may get further information after
1321 kcHsTyVarBndrs is called. (Recall that kcHsTyVarBndrs is usually
1322 called from getInitialKind. The only other case is in kcConDecl.)
1323 This is what implements the rule that all variables intended to be
1324 dependent must be manifestly so.
1325
1326 Sidenote: It's quite possible that later, we'll consider (t -> s)
1327 as a degenerate case of some (pi (x :: t) -> s) and then this will
1328 all get more permissive.
1329
1330 -}
1331
1332 tcWildCardBinders :: [Name]
1333 -> ([(Name, TcTyVar)] -> TcM a)
1334 -> TcM a
1335 tcWildCardBinders = tcWildCardBindersX new_tv
1336 where
1337 new_tv name = do { kind <- newMetaKindVar
1338 ; newSkolemTyVar name kind }
1339
1340 tcWildCardBindersX :: (Name -> TcM TcTyVar)
1341 -> [Name]
1342 -> ([(Name, TcTyVar)] -> TcM a)
1343 -> TcM a
1344 tcWildCardBindersX new_wc wc_names thing_inside
1345 = do { wcs <- mapM new_wc wc_names
1346 ; let wc_prs = wc_names `zip` wcs
1347 ; tcExtendTyVarEnv2 wc_prs $
1348 thing_inside wc_prs }
1349
1350 -- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
1351 -- user-supplied kind signature (CUSK), generalise the result.
1352 -- Used in 'getInitialKind' (for tycon kinds and other kinds)
1353 -- and in kind-checking (but not for tycon kinds, which are checked with
1354 -- tcTyClDecls). See also Note [Complete user-supplied kind signatures] in
1355 -- HsDecls.
1356 --
1357 -- This function does not do telescope checking.
1358 kcHsTyVarBndrs :: Name -- ^ of the thing being checked
1359 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
1360 -> Bool -- ^ True <=> the decl being checked has a CUSK
1361 -> Bool -- ^ True <=> all the hsq_implicit are *kind* vars
1362 -- (will give these kind * if -XNoTypeInType)
1363 -> LHsQTyVars GhcRn
1364 -> TcM (Kind, r) -- ^ The result kind, possibly with other info
1365 -> TcM (TcTyCon, r) -- ^ A suitably-kinded TcTyCon
1366 kcHsTyVarBndrs name flav cusk all_kind_vars
1367 (HsQTvs { hsq_implicit = kv_ns, hsq_explicit = hs_tvs
1368 , hsq_dependent = dep_names }) thing_inside
1369 | cusk
1370 = do { kv_kinds <- mk_kv_kinds
1371 ; lvl <- getTcLevel
1372 ; let scoped_kvs = zipWith (mk_skolem_tv lvl) kv_ns kv_kinds
1373 ; tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $
1374 do { (tc_binders, res_kind, stuff) <- solveEqualities $
1375 bind_telescope hs_tvs thing_inside
1376
1377 -- Now, because we're in a CUSK, quantify over the mentioned
1378 -- kind vars, in dependency order.
1379 ; tc_binders <- mapM zonkTcTyVarBinder tc_binders
1380 ; res_kind <- zonkTcType res_kind
1381 ; let tc_tvs = binderVars tc_binders
1382 qkvs = tyCoVarsOfTypeWellScoped (mkTyConKind tc_binders res_kind)
1383 -- the visibility of tvs doesn't matter here; we just
1384 -- want the free variables not to include the tvs
1385
1386 -- If there are any meta-tvs left, the user has
1387 -- lied about having a CUSK. Error.
1388 ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
1389 ; when (not (null meta_tvs)) $
1390 report_non_cusk_tvs (qkvs ++ tc_tvs)
1391
1392 -- If any of the scoped_kvs aren't actually mentioned in a binder's
1393 -- kind (or the return kind), then we're in the CUSK case from
1394 -- Note [Free-floating kind vars]
1395 ; let all_tc_tvs = good_tvs ++ tc_tvs
1396 all_mentioned_tvs = mapUnionVarSet (tyCoVarsOfType . tyVarKind)
1397 all_tc_tvs
1398 `unionVarSet` tyCoVarsOfType res_kind
1399 unmentioned_kvs = filterOut (`elemVarSet` all_mentioned_tvs)
1400 scoped_kvs
1401 ; reportFloatingKvs name flav all_tc_tvs unmentioned_kvs
1402
1403 ; let final_binders = map (mkNamedTyConBinder Specified) good_tvs
1404 ++ tc_binders
1405 tycon = mkTcTyCon name final_binders res_kind
1406 (scoped_kvs ++ tc_tvs) flav
1407 -- the tvs contain the binders already
1408 -- in scope from an enclosing class, but
1409 -- re-adding tvs to the env't doesn't cause
1410 -- harm
1411
1412 ; traceTc "kcHsTyVarBndrs: cusk" $
1413 vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
1414 , ppr tc_binders, ppr (mkTyConKind tc_binders res_kind)
1415 , ppr qkvs, ppr meta_tvs, ppr good_tvs, ppr final_binders ]
1416
1417 ; return (tycon, stuff) }}
1418
1419 | otherwise
1420 = do { kv_kinds <- mk_kv_kinds
1421 ; scoped_kvs <- zipWithM newSigTyVar kv_ns kv_kinds
1422 -- the names must line up in splitTelescopeTvs
1423 ; (binders, res_kind, stuff)
1424 <- tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $
1425 bind_telescope hs_tvs thing_inside
1426 ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they
1427 -- must remain lined up with the binders
1428 tycon = mkTcTyCon name binders res_kind
1429 (scoped_kvs ++ binderVars binders) flav
1430
1431 ; traceTc "kcHsTyVarBndrs: not-cusk" (ppr name <+> ppr binders)
1432 ; return (tycon, stuff) }
1433 where
1434 open_fam = tcFlavourIsOpen flav
1435
1436 -- if -XNoTypeInType and we know all the implicits are kind vars,
1437 -- just give the kind *. This prevents test
1438 -- dependent/should_fail/KindLevelsB from compiling, as it should
1439 mk_kv_kinds :: TcM [Kind]
1440 mk_kv_kinds = do { typeintype <- xoptM LangExt.TypeInType
1441 ; if not typeintype && all_kind_vars
1442 then return (map (const liftedTypeKind) kv_ns)
1443 else mapM (const newMetaKindVar) kv_ns }
1444
1445 -- there may be dependency between the explicit "ty" vars. So, we have
1446 -- to handle them one at a time.
1447 bind_telescope :: [LHsTyVarBndr GhcRn]
1448 -> TcM (Kind, r)
1449 -> TcM ([TyConBinder], TcKind, r)
1450 bind_telescope [] thing
1451 = do { (res_kind, stuff) <- thing
1452 ; return ([], res_kind, stuff) }
1453 bind_telescope (L _ hs_tv : hs_tvs) thing
1454 = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
1455 -- NB: Bring all tvs into scope, even non-dependent ones,
1456 -- as they're needed in type synonyms, data constructors, etc.
1457 ; (binders, res_kind, stuff) <- bind_unless_scoped tv_pair $
1458 bind_telescope hs_tvs $
1459 thing
1460 -- See Note [Dependent LHsQTyVars]
1461 ; let new_binder | hsTyVarName hs_tv `elemNameSet` dep_names
1462 = mkNamedTyConBinder Required tv
1463 | otherwise
1464 = mkAnonTyConBinder tv
1465 ; return ( new_binder : binders
1466 , res_kind, stuff ) }
1467
1468 -- | Bind the tyvar in the env't unless the bool is True
1469 bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a
1470 bind_unless_scoped (_, True) thing_inside = thing_inside
1471 bind_unless_scoped (tv, False) thing_inside
1472 = tcExtendTyVarEnv [tv] thing_inside
1473
1474 kc_hs_tv :: HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
1475 kc_hs_tv (UserTyVar lname@(L _ name))
1476 = do { tv_pair@(tv, scoped) <- tcHsTyVarName Nothing name
1477
1478 -- Open type/data families default their variables to kind *.
1479 ; when (open_fam && not scoped) $ -- (don't default class tyvars)
1480 discardResult $ unifyKind (Just (HsTyVar NotPromoted lname)) liftedTypeKind
1481 (tyVarKind tv)
1482
1483 ; return tv_pair }
1484
1485 kc_hs_tv (KindedTyVar (L _ name) lhs_kind)
1486 = do { kind <- tcLHsKindSig lhs_kind
1487 ; tcHsTyVarName (Just kind) name }
1488
1489 report_non_cusk_tvs all_tvs
1490 = do { all_tvs <- mapM zonkTyCoVarKind all_tvs
1491 ; let (_, tidy_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
1492 (meta_tvs, other_tvs) = partition isMetaTyVar tidy_tvs
1493
1494 ; addErr $
1495 vcat [ text "You have written a *complete user-suppled kind signature*,"
1496 , hang (text "but the following variable" <> plural meta_tvs <+>
1497 isOrAre meta_tvs <+> text "undetermined:")
1498 2 (vcat (map pp_tv meta_tvs))
1499 , text "Perhaps add a kind signature."
1500 , hang (text "Inferred kinds of user-written variables:")
1501 2 (vcat (map pp_tv other_tvs)) ] }
1502 where
1503 pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
1504
1505
1506 tcImplicitTKBndrs :: [Name]
1507 -> TcM (a, TyVarSet) -- vars are bound somewhere in the scope
1508 -- see Note [Scope-check inferred kinds]
1509 -> TcM ([TcTyVar], a)
1510 tcImplicitTKBndrs = tcImplicitTKBndrsX (tcHsTyVarName Nothing)
1511
1512 -- | Convenient specialization
1513 tcImplicitTKBndrsType :: [Name]
1514 -> TcM Type
1515 -> TcM ([TcTyVar], Type)
1516 tcImplicitTKBndrsType var_ns thing_inside
1517 = tcImplicitTKBndrs var_ns $
1518 do { res_ty <- thing_inside
1519 ; return (res_ty, allBoundVariables res_ty) }
1520
1521 -- this more general variant is needed in tcHsPatSigType.
1522 -- See Note [Pattern signature binders]
1523 tcImplicitTKBndrsX :: (Name -> TcM (TcTyVar, Bool)) -- new_tv function
1524 -> [Name]
1525 -> TcM (a, TyVarSet)
1526 -> TcM ([TcTyVar], a)
1527 -- Returned TcTyVars have the supplied Names,
1528 -- but may be in different order to the original [Name]
1529 -- (because of sorting to respect dependency)
1530 -- Returned TcTyVars have zonked kinds
1531 tcImplicitTKBndrsX new_tv var_ns thing_inside
1532 = do { tkvs_pairs <- mapM new_tv var_ns
1533 ; let must_scope_tkvs = [ tkv | (tkv, False) <- tkvs_pairs ]
1534 tkvs = map fst tkvs_pairs
1535 ; (result, bound_tvs) <- tcExtendTyVarEnv must_scope_tkvs $
1536 thing_inside
1537
1538 -- Check that the implicitly-bound kind variable
1539 -- really can go at the beginning.
1540 -- e.g. forall (a :: k) (b :: *). ...(forces k :: b)...
1541 ; tkvs <- mapM zonkTyCoVarKind tkvs
1542 -- NB: /not/ zonkTcTyVarToTyVar. tcImplicitTKBndrsX
1543 -- guarantees to return TcTyVars with the same Names
1544 -- as the var_ns. See [Pattern signature binders]
1545
1546 ; let extra = text "NB: Implicitly-bound variables always come" <+>
1547 text "before other ones."
1548 ; checkValidInferredKinds tkvs bound_tvs extra
1549
1550 ; let final_tvs = toposortTyVars tkvs
1551 ; traceTc "tcImplicitTKBndrs" (ppr var_ns $$ ppr final_tvs)
1552
1553 ; return (final_tvs, result) }
1554
1555 tcExplicitTKBndrs :: [LHsTyVarBndr GhcRn]
1556 -> ([TyVar] -> TcM (a, TyVarSet))
1557 -- ^ Thing inside returns the set of variables bound
1558 -- in the scope. See Note [Scope-check inferred kinds]
1559 -> TcM (a, TyVarSet) -- ^ returns augmented bound vars
1560 -- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs
1561 tcExplicitTKBndrs orig_hs_tvs thing_inside
1562 = tcExplicitTKBndrsX newSkolemTyVar orig_hs_tvs thing_inside
1563
1564 tcExplicitTKBndrsX :: (Name -> Kind -> TcM TyVar)
1565 -> [LHsTyVarBndr GhcRn]
1566 -> ([TyVar] -> TcM (a, TyVarSet))
1567 -- ^ Thing inside returns the set of variables bound
1568 -- in the scope. See Note [Scope-check inferred kinds]
1569 -> TcM (a, TyVarSet) -- ^ returns augmented bound vars
1570 tcExplicitTKBndrsX new_tv orig_hs_tvs thing_inside
1571 = go orig_hs_tvs $ \ tvs ->
1572 do { (result, bound_tvs) <- thing_inside tvs
1573
1574 -- Issue an error if the ordering is bogus.
1575 -- See Note [Bad telescopes] in TcValidity.
1576 ; tvs <- checkZonkValidTelescope (interppSP orig_hs_tvs) tvs empty
1577 ; checkValidInferredKinds tvs bound_tvs empty
1578
1579 ; traceTc "tcExplicitTKBndrs" $
1580 vcat [ text "Hs vars:" <+> ppr orig_hs_tvs
1581 , text "tvs:" <+> sep (map pprTyVar tvs) ]
1582
1583 ; return (result, bound_tvs `unionVarSet` mkVarSet tvs)
1584 }
1585 where
1586 go [] thing = thing []
1587 go (L _ hs_tv : hs_tvs) thing
1588 = do { tv <- tcHsTyVarBndr new_tv hs_tv
1589 ; tcExtendTyVarEnv [tv] $
1590 go hs_tvs $ \ tvs ->
1591 thing (tv : tvs) }
1592
1593 tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
1594 -> HsTyVarBndr GhcRn -> TcM TcTyVar
1595 -- Return a SkolemTv TcTyVar, initialised with a kind variable.
1596 -- Typically the Kind inside the HsTyVarBndr will be a tyvar
1597 -- with a mutable kind in it.
1598 -- NB: These variables must not be in scope. This function
1599 -- is not appropriate for use with associated types, for example.
1600 --
1601 -- Returned TcTyVar has the same name; no cloning
1602 --
1603 -- See also Note [Associated type tyvar names] in Class
1604 --
1605 tcHsTyVarBndr new_tv (UserTyVar (L _ name))
1606 = do { kind <- newMetaKindVar
1607 ; new_tv name kind }
1608
1609 tcHsTyVarBndr new_tv (KindedTyVar (L _ name) kind)
1610 = do { kind <- tcLHsKindSig kind
1611 ; new_tv name kind }
1612
1613 newWildTyVar :: Name -> TcM TcTyVar
1614 -- ^ New unification variable for a wildcard
1615 newWildTyVar _name
1616 = do { kind <- newMetaKindVar
1617 ; uniq <- newUnique
1618 ; details <- newMetaDetails TauTv
1619 ; let name = mkSysTvName uniq (fsLit "w")
1620 ; return (mkTcTyVar name kind details) }
1621
1622 -- | Produce a tyvar of the given name (with the kind provided, or
1623 -- otherwise a meta-var kind). If
1624 -- the name is already in scope, return the scoped variable, checking
1625 -- to make sure the known kind matches any kind provided. The
1626 -- second return value says whether the variable is in scope (True)
1627 -- or not (False). (Use this for associated types, for example.)
1628 tcHsTyVarName :: Maybe Kind -> Name -> TcM (TcTyVar, Bool)
1629 tcHsTyVarName m_kind name
1630 = do { mb_tv <- tcLookupLcl_maybe name
1631 ; case mb_tv of
1632 Just (ATyVar _ tv)
1633 -> do { whenIsJust m_kind $ \ kind ->
1634 discardResult $
1635 unifyKind (Just (HsTyVar NotPromoted (noLoc name))) kind (tyVarKind tv)
1636 ; return (tv, True) }
1637 _ -> do { kind <- case m_kind of
1638 Just kind -> return kind
1639 Nothing -> newMetaKindVar
1640 ; tv <- newSkolemTyVar name kind
1641 ; return (tv, False) }}
1642
1643 -- makes a new skolem tv
1644 newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
1645 newSkolemTyVar name kind = do { lvl <- getTcLevel
1646 ; return (mk_skolem_tv lvl name kind) }
1647
1648 mk_skolem_tv :: TcLevel -> Name -> Kind -> TcTyVar
1649 mk_skolem_tv lvl n k = mkTcTyVar n k (SkolemTv lvl False)
1650
1651 ------------------
1652 kindGeneralizeType :: Type -> TcM Type
1653 -- Result is zonked
1654 kindGeneralizeType ty
1655 = do { kvs <- kindGeneralize ty
1656 ; ty <- zonkSigType (mkInvForAllTys kvs ty)
1657 ; return ty }
1658
1659 kindGeneralize :: TcType -> TcM [KindVar]
1660 -- Quantify the free kind variables of a kind or type
1661 -- In the latter case the type is closed, so it has no free
1662 -- type variables. So in both cases, all the free vars are kind vars
1663 kindGeneralize kind_or_type
1664 = do { kvs <- zonkTcTypeAndFV kind_or_type
1665 ; let dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet }
1666 ; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
1667 ; quantifyTyVars gbl_tvs dvs }
1668
1669 {-
1670 Note [Kind generalisation]
1671 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1672 We do kind generalisation only at the outer level of a type signature.
1673 For example, consider
1674 T :: forall k. k -> *
1675 f :: (forall a. T a -> Int) -> Int
1676 When kind-checking f's type signature we generalise the kind at
1677 the outermost level, thus:
1678 f1 :: forall k. (forall (a:k). T k a -> Int) -> Int -- YES!
1679 and *not* at the inner forall:
1680 f2 :: (forall k. forall (a:k). T k a -> Int) -> Int -- NO!
1681 Reason: same as for HM inference on value level declarations,
1682 we want to infer the most general type. The f2 type signature
1683 would be *less applicable* than f1, because it requires a more
1684 polymorphic argument.
1685
1686 NB: There are no explicit kind variables written in f's signature.
1687 When there are, the renamer adds these kind variables to the list of
1688 variables bound by the forall, so you can indeed have a type that's
1689 higher-rank in its kind. But only by explicit request.
1690
1691 Note [Kinds of quantified type variables]
1692 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1693 tcTyVarBndrsGen quantifies over a specified list of type variables,
1694 *and* over the kind variables mentioned in the kinds of those tyvars.
1695
1696 Note that we must zonk those kinds (obviously) but less obviously, we
1697 must return type variables whose kinds are zonked too. Example
1698 (a :: k7) where k7 := k9 -> k9
1699 We must return
1700 [k9, a:k9->k9]
1701 and NOT
1702 [k9, a:k7]
1703 Reason: we're going to turn this into a for-all type,
1704 forall k9. forall (a:k7). blah
1705 which the type checker will then instantiate, and instantiate does not
1706 look through unification variables!
1707
1708 Hence using zonked_kinds when forming tvs'.
1709
1710 Note [Free-floating kind vars]
1711 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1712 Consider
1713
1714 data T = MkT (forall (a :: k). Proxy a)
1715 -- from test ghci/scripts/T7873
1716
1717 This is not an existential datatype, but a higher-rank one (the forall
1718 to the right of MkT). Also consider
1719
1720 data S a = MkS (Proxy (a :: k))
1721
1722 According to the rules around implicitly-bound kind variables, in both
1723 cases those k's scope over the whole declaration. The renamer grabs
1724 it and adds it to the hsq_implicits field of the HsQTyVars of the
1725 tycon. So it must be in scope during type-checking, but we want to
1726 reject T while accepting S.
1727
1728 Why reject T? Because the kind variable isn't fixed by anything. For
1729 a variable like k to be implicit, it needs to be mentioned in the kind
1730 of a tycon tyvar. But it isn't.
1731
1732 Why accept S? Because kind inference tells us that a has kind k, so it's
1733 all OK.
1734
1735 Our approach depends on whether or not the datatype has a CUSK.
1736
1737 Non-CUSK: In the first pass (kcTyClTyVars) we just bring
1738 k into scope. In the second pass (tcTyClTyVars),
1739 we check to make sure that k has been unified with some other variable
1740 (or generalized over, making k into a skolem). If it hasn't been, then
1741 it must be a free-floating kind var. Error.
1742
1743 CUSK: When we determine the tycon's final, never-to-be-changed kind
1744 in kcHsTyVarBndrs, we check to make sure all implicitly-bound kind
1745 vars are indeed mentioned in a kind somewhere. If not, error.
1746
1747 -}
1748
1749 --------------------
1750 -- getInitialKind has made a suitably-shaped kind for the type or class
1751 -- Look it up in the local environment. This is used only for tycons
1752 -- that we're currently type-checking, so we're sure to find a TcTyCon.
1753 kcLookupTcTyCon :: Name -> TcM TcTyCon
1754 kcLookupTcTyCon nm
1755 = do { tc_ty_thing <- tcLookup nm
1756 ; return $ case tc_ty_thing of
1757 ATcTyCon tc -> tc
1758 _ -> pprPanic "kcLookupTcTyCon" (ppr tc_ty_thing) }
1759
1760 -----------------------
1761 -- | Bring tycon tyvars into scope. This is used during the "kind-checking"
1762 -- pass in TcTyClsDecls. (Never in getInitialKind, never in the
1763 -- "type-checking"/desugaring pass.)
1764 -- Never emits constraints, though the thing_inside might.
1765 kcTyClTyVars :: Name -> TcM a -> TcM a
1766 kcTyClTyVars tycon_name thing_inside
1767 = do { tycon <- kcLookupTcTyCon tycon_name
1768 ; tcExtendTyVarEnv (tcTyConScopedTyVars tycon) $ thing_inside }
1769
1770 tcTyClTyVars :: Name
1771 -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
1772 -- ^ Used for the type variables of a type or class decl
1773 -- on the second full pass (type-checking/desugaring) in TcTyClDecls.
1774 -- This is *not* used in the initial-kind run, nor in the "kind-checking" pass.
1775 -- Accordingly, everything passed to the continuation is fully zonked.
1776 --
1777 -- (tcTyClTyVars T [a,b] thing_inside)
1778 -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
1779 -- calls thing_inside with arguments
1780 -- [k1,k2,a,b] [k1:*, k2:*, Anon (k1 -> *), Anon k1] (k2 -> *)
1781 -- having also extended the type environment with bindings
1782 -- for k1,k2,a,b
1783 --
1784 -- Never emits constraints.
1785 --
1786 -- The LHsTyVarBndrs is always user-written, and the full, generalised
1787 -- kind of the tycon is available in the local env.
1788 tcTyClTyVars tycon_name thing_inside
1789 = do { tycon <- kcLookupTcTyCon tycon_name
1790
1791 ; let scoped_tvs = tcTyConScopedTyVars tycon
1792 -- these are all zonked:
1793 binders = tyConBinders tycon
1794 res_kind = tyConResKind tycon
1795
1796 -- See Note [Free-floating kind vars]
1797 ; zonked_scoped_tvs <- mapM zonkTcTyVarToTyVar scoped_tvs
1798 ; let still_sig_tvs = filter isSigTyVar zonked_scoped_tvs
1799 ; checkNoErrs $ reportFloatingKvs tycon_name (tyConFlavour tycon)
1800 zonked_scoped_tvs still_sig_tvs
1801
1802 -- Add the *unzonked* tyvars to the env't, because those
1803 -- are the ones mentioned in the source.
1804 ; traceTc "tcTyClTyVars" (ppr tycon_name <+> ppr binders)
1805 ; tcExtendTyVarEnv scoped_tvs $
1806 thing_inside binders res_kind }
1807
1808 -----------------------------------
1809 tcDataKindSig :: Bool -- ^ Do we require the result to be *?
1810 -> Kind -> TcM ([TyConBinder], Kind)
1811 -- GADT decls can have a (perhaps partial) kind signature
1812 -- e.g. data T :: * -> * -> * where ...
1813 -- This function makes up suitable (kinded) type variables for
1814 -- the argument kinds, and checks that the result kind is indeed * if requested.
1815 -- (Otherwise, checks to make sure that the result kind is either * or a type variable.)
1816 -- See Note [Arity of data families] in FamInstEnv for more info.
1817 -- We use it also to make up argument type variables for for data instances.
1818 -- Never emits constraints.
1819 -- Returns the new TyVars, the extracted TyBinders, and the new, reduced
1820 -- result kind (which should always be Type or a synonym thereof)
1821 tcDataKindSig check_for_type kind
1822 = do { checkTc (isLiftedTypeKind res_kind || (not check_for_type &&
1823 isJust (tcGetCastedTyVar_maybe res_kind)))
1824 (badKindSig check_for_type kind)
1825 ; span <- getSrcSpanM
1826 ; us <- newUniqueSupply
1827 ; rdr_env <- getLocalRdrEnv
1828 ; let uniqs = uniqsFromSupply us
1829 occs = [ occ | str <- allNameStrings
1830 , let occ = mkOccName tvName str
1831 , isNothing (lookupLocalRdrOcc rdr_env occ) ]
1832 -- Note [Avoid name clashes for associated data types]
1833
1834 -- NB: Use the tv from a binder if there is one. Otherwise,
1835 -- we end up inventing a new Unique for it, and any other tv
1836 -- that mentions the first ends up with the wrong kind.
1837 extra_bndrs = zipWith4 mkTyBinderTyConBinder
1838 tv_bndrs (repeat span) uniqs occs
1839
1840 ; return (extra_bndrs, res_kind) }
1841 where
1842 (tv_bndrs, res_kind) = splitPiTys kind
1843
1844 badKindSig :: Bool -> Kind -> SDoc
1845 badKindSig check_for_type kind
1846 = hang (sep [ text "Kind signature on data type declaration has non-*"
1847 , (if check_for_type then empty else text "and non-variable") <+>
1848 text "return kind" ])
1849 2 (ppr kind)
1850
1851 {-
1852 Note [Avoid name clashes for associated data types]
1853 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1854 Consider class C a b where
1855 data D b :: * -> *
1856 When typechecking the decl for D, we'll invent an extra type variable
1857 for D, to fill out its kind. Ideally we don't want this type variable
1858 to be 'a', because when pretty printing we'll get
1859 class C a b where
1860 data D b a0
1861 (NB: the tidying happens in the conversion to IfaceSyn, which happens
1862 as part of pretty-printing a TyThing.)
1863
1864 That's why we look in the LocalRdrEnv to see what's in scope. This is
1865 important only to get nice-looking output when doing ":info C" in GHCi.
1866 It isn't essential for correctness.
1867
1868
1869 ************************************************************************
1870 * *
1871 Partial signatures and pattern signatures
1872 * *
1873 ************************************************************************
1874
1875 -}
1876
1877 tcHsPartialSigType
1878 :: UserTypeCtxt
1879 -> LHsSigWcType GhcRn -- The type signature
1880 -> TcM ( [(Name, TcTyVar)] -- Wildcards
1881 , Maybe TcTyVar -- Extra-constraints wildcard
1882 , [TcTyVar] -- Implicitly and explicitly bound type variables
1883 , TcThetaType -- Theta part
1884 , TcType ) -- Tau part
1885 tcHsPartialSigType ctxt sig_ty
1886 | HsWC { hswc_wcs = sig_wcs, hswc_body = ib_ty } <- sig_ty
1887 , HsIB { hsib_vars = implicit_hs_tvs, hsib_body = hs_ty } <- ib_ty
1888 , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
1889 = addSigCtxt ctxt hs_ty $
1890 do { (implicit_tvs, (wcs, wcx, explicit_tvs, theta, tau))
1891 <- tcWildCardBindersX newWildTyVar sig_wcs $ \ wcs ->
1892 tcImplicitTKBndrsX new_implicit_tv implicit_hs_tvs $
1893 tcExplicitTKBndrsX newSigTyVar explicit_hs_tvs $ \ explicit_tvs ->
1894 do { -- Instantiate the type-class context; but if there
1895 -- is an extra-constraints wildcard, just discard it here
1896 (theta, wcx) <- tcPartialContext hs_ctxt
1897
1898 ; tau <- tcHsOpenType hs_tau
1899
1900 ; let bound_tvs = unionVarSets [ allBoundVariables tau
1901 , mkVarSet explicit_tvs
1902 , mkVarSet (map snd wcs) ]
1903
1904 ; return ( (wcs, wcx, explicit_tvs, theta, tau)
1905 , bound_tvs) }
1906
1907 ; emitWildCardHoleConstraints wcs
1908
1909 ; explicit_tvs <- mapM zonkTyCoVarKind explicit_tvs
1910 ; let all_tvs = implicit_tvs ++ explicit_tvs
1911 -- The implicit_tvs already have zonked kinds
1912
1913 ; theta <- mapM zonkTcType theta
1914 ; tau <- zonkTcType tau
1915 ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
1916
1917 ; traceTc "tcHsPartialSigType" (ppr all_tvs)
1918 ; return (wcs, wcx, all_tvs, theta, tau) }
1919 where
1920 new_implicit_tv name = do { kind <- newMetaKindVar
1921 ; tv <- newSigTyVar name kind
1922 ; return (tv, False) }
1923
1924 tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcTyVar)
1925 tcPartialContext hs_theta
1926 | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
1927 , L _ (HsWildCardTy wc) <- ignoreParens hs_ctxt_last
1928 = do { wc_tv <- tcWildCardOcc wc constraintKind
1929 ; theta <- mapM tcLHsPredType hs_theta1
1930 ; return (theta, Just wc_tv) }
1931 | otherwise
1932 = do { theta <- mapM tcLHsPredType hs_theta
1933 ; return (theta, Nothing) }
1934
1935 tcHsPatSigType :: UserTypeCtxt
1936 -> LHsSigWcType GhcRn -- The type signature
1937 -> TcM ( [(Name, TcTyVar)] -- Wildcards
1938 , [(Name, TcTyVar)] -- The new bit of type environment, binding
1939 -- the scoped type variables
1940 , TcType) -- The type
1941 -- Used for type-checking type signatures in
1942 -- (a) patterns e.g f (x::Int) = e
1943 -- (b) RULE forall bndrs e.g. forall (x::Int). f x = x
1944 --
1945 -- This may emit constraints
1946
1947 tcHsPatSigType ctxt sig_ty
1948 | HsWC { hswc_wcs = sig_wcs, hswc_body = ib_ty } <- sig_ty
1949 , HsIB { hsib_vars = sig_vars, hsib_body = hs_ty } <- ib_ty
1950 = addSigCtxt ctxt hs_ty $
1951 do { (implicit_tvs, (wcs, sig_ty))
1952 <- tcWildCardBindersX newWildTyVar sig_wcs $ \ wcs ->
1953 tcImplicitTKBndrsX new_implicit_tv sig_vars $
1954 do { sig_ty <- tcHsOpenType hs_ty
1955 ; return ((wcs, sig_ty), allBoundVariables sig_ty) }
1956
1957 ; emitWildCardHoleConstraints wcs
1958
1959 ; sig_ty <- zonkTcType sig_ty
1960 ; checkValidType ctxt sig_ty
1961
1962 ; tv_pairs <- mapM mk_tv_pair implicit_tvs
1963
1964 ; traceTc "tcHsPatSigType" (ppr sig_vars)
1965 ; return (wcs, tv_pairs, sig_ty) }
1966 where
1967 new_implicit_tv name = do { kind <- newMetaKindVar
1968 ; tv <- new_tv name kind
1969 ; return (tv, False) }
1970 -- "False" means that these tyvars aren't yet in scope
1971 new_tv = case ctxt of
1972 RuleSigCtxt {} -> newSkolemTyVar
1973 _ -> newSigTyVar
1974 -- See Note [Pattern signature binders]
1975 -- See Note [Unifying SigTvs]
1976
1977 mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv
1978 ; return (tyVarName tv, tv') }
1979 -- The Name is one of sig_vars, the lexically scoped name
1980 -- But if it's a SigTyVar, it might have been unified
1981 -- with an existing in-scope skolem, so we must zonk
1982 -- here. See Note [Pattern signature binders]
1983
1984 tcPatSig :: Bool -- True <=> pattern binding
1985 -> LHsSigWcType GhcRn
1986 -> ExpSigmaType
1987 -> TcM (TcType, -- The type to use for "inside" the signature
1988 [(Name,TcTyVar)], -- The new bit of type environment, binding
1989 -- the scoped type variables
1990 [(Name,TcTyVar)], -- The wildcards
1991 HsWrapper) -- Coercion due to unification with actual ty
1992 -- Of shape: res_ty ~ sig_ty
1993 tcPatSig in_pat_bind sig res_ty
1994 = do { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
1995 -- sig_tvs are the type variables free in 'sig',
1996 -- and not already in scope. These are the ones
1997 -- that should be brought into scope
1998
1999 ; if null sig_tvs then do {
2000 -- Just do the subsumption check and return
2001 wrap <- addErrCtxtM (mk_msg sig_ty) $
2002 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
2003 ; return (sig_ty, [], sig_wcs, wrap)
2004 } else do
2005 -- Type signature binds at least one scoped type variable
2006
2007 -- A pattern binding cannot bind scoped type variables
2008 -- It is more convenient to make the test here
2009 -- than in the renamer
2010 { when in_pat_bind (addErr (patBindSigErr sig_tvs))
2011
2012 -- Check that all newly-in-scope tyvars are in fact
2013 -- constrained by the pattern. This catches tiresome
2014 -- cases like
2015 -- type T a = Int
2016 -- f :: Int -> Int
2017 -- f (x :: T a) = ...
2018 -- Here 'a' doesn't get a binding. Sigh
2019 ; let bad_tvs = [ tv | (_,tv) <- sig_tvs
2020 , not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ]
2021 ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
2022
2023 -- Now do a subsumption check of the pattern signature against res_ty
2024 ; wrap <- addErrCtxtM (mk_msg sig_ty) $
2025 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
2026
2027 -- Phew!
2028 ; return (sig_ty, sig_tvs, sig_wcs, wrap)
2029 } }
2030 where
2031 mk_msg sig_ty tidy_env
2032 = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
2033 ; res_ty <- readExpType res_ty -- should be filled in by now
2034 ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
2035 ; let msg = vcat [ hang (text "When checking that the pattern signature:")
2036 4 (ppr sig_ty)
2037 , nest 2 (hang (text "fits the type of its context:")
2038 2 (ppr res_ty)) ]
2039 ; return (tidy_env, msg) }
2040
2041 patBindSigErr :: [(Name,TcTyVar)] -> SDoc
2042 patBindSigErr sig_tvs
2043 = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
2044 <+> pprQuotedList (map fst sig_tvs))
2045 2 (text "in a pattern binding signature")
2046
2047 {- Note [Pattern signature binders]
2048 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2049 Consider
2050 data T = forall a. T a (a->Int)
2051 f (T x (f :: b->Int)) = blah
2052
2053 Here
2054 * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk',
2055 It must be a skolem so that that it retains its identity, and
2056 TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
2057
2058 * The type signature pattern (f :: b->Int) makes a fresh meta-tyvar b_sig
2059 (a SigTv), and binds "b" :-> b_sig in the envt
2060
2061 * Then unification makes b_sig := a_sk
2062 That's why we must make b_sig a MetaTv (albeit a SigTv),
2063 not a SkolemTv, so that it can unify to a_sk.
2064
2065 * Finally, in 'blah' we must have the envt "b" :-> a_sk. The pair
2066 ("b" :-> a_sk) is returned by tcHsPatSigType, constructed by
2067 mk_tv_pair in that funcion.
2068
2069 Another example (Trac #13881):
2070 fl :: forall (l :: [a]). Sing l -> Sing l
2071 fl (SNil :: Sing (l :: [y])) = SNil
2072 When we reach the pattern signature, 'l' is in scope from the
2073 outer 'forall':
2074 "a" :-> a_sk :: *
2075 "l" :-> l_sk :: [a_sk]
2076 We make up a fresh meta-SigTv, y_sig, for 'y', and kind-check
2077 the pattern signature
2078 Sing (l :: [y])
2079 That unifies y_sig := a_sk. We return from tcHsPatSigType with
2080 the pair ("y" :-> a_sk).
2081
2082 For RULE binders, though, things are a bit different (yuk).
2083 RULE "foo" forall (x::a) (y::[a]). f x y = ...
2084 Here this really is the binding site of the type variable so we'd like
2085 to use a skolem, so that we get a complaint if we unify two of them
2086 together.
2087
2088 Note [Unifying SigTvs]
2089 ~~~~~~~~~~~~~~~~~~~~~~
2090 ALAS we have no decent way of avoiding two SigTvs getting unified.
2091 Consider
2092 f (x::(a,b)) (y::c)) = [fst x, y]
2093 Here we'd really like to complain that 'a' and 'c' are unified. But
2094 for the reasons above we can't make a,b,c into skolems, so they
2095 are just SigTvs that can unify. And indeed, this would be ok,
2096 f x (y::c) = case x of
2097 (x1 :: a1, True) -> [x,y]
2098 (x1 :: a2, False) -> [x,y,y]
2099 Here the type of x's first component is called 'a1' in one branch and
2100 'a2' in the other. We could try insisting on the same OccName, but
2101 they definitely won't have the sane lexical Name.
2102
2103 I think we could solve this by recording in a SigTv a list of all the
2104 in-scope variables that it should not unify with, but it's fiddly.
2105
2106
2107 ************************************************************************
2108 * *
2109 Checking kinds
2110 * *
2111 ************************************************************************
2112
2113 -}
2114
2115 unifyKinds :: [LHsType GhcRn] -> [(TcType, TcKind)] -> TcM ([TcType], TcKind)
2116 unifyKinds rn_tys act_kinds
2117 = do { kind <- newMetaKindVar
2118 ; let check rn_ty (ty, act_kind) = checkExpectedKind (unLoc rn_ty) ty act_kind kind
2119 ; tys' <- zipWithM check rn_tys act_kinds
2120 ; return (tys', kind) }
2121
2122 {-
2123 ************************************************************************
2124 * *
2125 Sort checking kinds
2126 * *
2127 ************************************************************************
2128
2129 tcLHsKindSig converts a user-written kind to an internal, sort-checked kind.
2130 It does sort checking and desugaring at the same time, in one single pass.
2131 -}
2132
2133 tcLHsKindSig :: LHsKind GhcRn -> TcM Kind
2134 tcLHsKindSig hs_kind
2135 = do { kind <- tc_lhs_kind kindLevelMode hs_kind
2136 ; zonkTcType kind }
2137 -- This zonk is very important in the case of higher rank kinds
2138 -- E.g. Trac #13879 f :: forall (p :: forall z (y::z). <blah>).
2139 -- <more blah>
2140 -- When instantiating p's kind at occurrences of p in <more blah>
2141 -- it's crucial that the kind we instantiate is fully zonked,
2142 -- else we may fail to substitute properly
2143
2144 tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind
2145 tc_lhs_kind mode k
2146 = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $
2147 tc_lhs_type (kindLevel mode) k liftedTypeKind
2148
2149 promotionErr :: Name -> PromotionErr -> TcM a
2150 promotionErr name err
2151 = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here")
2152 2 (parens reason))
2153 where
2154 reason = case err of
2155 FamDataConPE -> text "it comes from a data family instance"
2156 NoDataKindsTC -> text "Perhaps you intended to use DataKinds"
2157 NoDataKindsDC -> text "Perhaps you intended to use DataKinds"
2158 NoTypeInTypeTC -> text "Perhaps you intended to use TypeInType"
2159 NoTypeInTypeDC -> text "Perhaps you intended to use TypeInType"
2160 PatSynPE -> text "Pattern synonyms cannot be promoted"
2161 _ -> text "it is defined and used in the same recursive group"
2162
2163 {-
2164 ************************************************************************
2165 * *
2166 Scoped type variables
2167 * *
2168 ************************************************************************
2169 -}
2170
2171 badPatSigTvs :: TcType -> [TyVar] -> SDoc
2172 badPatSigTvs sig_ty bad_tvs
2173 = vcat [ fsep [text "The type variable" <> plural bad_tvs,
2174 quotes (pprWithCommas ppr bad_tvs),
2175 text "should be bound by the pattern signature" <+> quotes (ppr sig_ty),
2176 text "but are actually discarded by a type synonym" ]
2177 , text "To fix this, expand the type synonym"
2178 , text "[Note: I hope to lift this restriction in due course]" ]
2179
2180 {-
2181 ************************************************************************
2182 * *
2183 Error messages and such
2184 * *
2185 ************************************************************************
2186 -}
2187
2188 -- | Make an appropriate message for an error in a function argument.
2189 -- Used for both expressions and types.
2190 funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
2191 funAppCtxt fun arg arg_no
2192 = hang (hsep [ text "In the", speakNth arg_no, ptext (sLit "argument of"),
2193 quotes (ppr fun) <> text ", namely"])
2194 2 (quotes (ppr arg))
2195
2196 -- See Note [Free-floating kind vars]
2197 reportFloatingKvs :: Name -- of the tycon
2198 -> TyConFlavour -- What sort of TyCon it is
2199 -> [TcTyVar] -- all tyvars, not necessarily zonked
2200 -> [TcTyVar] -- floating tyvars
2201 -> TcM ()
2202 reportFloatingKvs tycon_name flav all_tvs bad_tvs
2203 = unless (null bad_tvs) $ -- don't bother zonking if there's no error
2204 do { all_tvs <- mapM zonkTcTyVarToTyVar all_tvs
2205 ; bad_tvs <- mapM zonkTcTyVarToTyVar bad_tvs
2206 ; let (tidy_env, tidy_all_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
2207 tidy_bad_tvs = map (tidyTyVarOcc tidy_env) bad_tvs
2208 ; typeintype <- xoptM LangExt.TypeInType
2209 ; mapM_ (report typeintype tidy_all_tvs) tidy_bad_tvs }
2210 where
2211 report typeintype tidy_all_tvs tidy_bad_tv
2212 = addErr $
2213 vcat [ text "Kind variable" <+> quotes (ppr tidy_bad_tv) <+>
2214 text "is implicitly bound in" <+> ppr flav
2215 , quotes (ppr tycon_name) <> comma <+>
2216 text "but does not appear as the kind of any"
2217 , text "of its type variables. Perhaps you meant"
2218 , text "to bind it" <+> ppWhen (not typeintype)
2219 (text "(with TypeInType)") <+>
2220 text "explicitly somewhere?"
2221 , ppWhen (not (null tidy_all_tvs)) $
2222 hang (text "Type variables with inferred kinds:")
2223 2 (ppr_tv_bndrs tidy_all_tvs) ]
2224
2225 ppr_tv_bndrs tvs = sep (map pp_tv tvs)
2226 pp_tv tv = parens (ppr tv <+> dcolon <+> ppr (tyVarKind tv))