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