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