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