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