Check quantification for partial type signatues
[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 NotPromoted (L loc_op op)) op' op_kind' [lhs, rhs] }
499 tc_infer_hs_type mode (HsKindSig ty sig)
500 = do { sig' <- tc_lhs_kind (kindLevel mode) sig
501 ; ty' <- tc_lhs_type mode ty sig'
502 ; return (ty', sig') }
503 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
504 -- the splice location to the typechecker. Here we skip over it in order to have
505 -- the same kind inferred for a given expression whether it was produced from
506 -- splices or not.
507 --
508 -- See Note [Delaying modFinalizers in untyped splices].
509 tc_infer_hs_type mode (HsSpliceTy (HsSpliced _ (HsSplicedTy ty)) _)
510 = tc_infer_hs_type mode ty
511 tc_infer_hs_type mode (HsDocTy ty _) = tc_infer_lhs_type mode ty
512 tc_infer_hs_type _ (HsCoreTy ty) = return (ty, typeKind ty)
513 tc_infer_hs_type mode other_ty
514 = do { kv <- newMetaKindVar
515 ; ty' <- tc_hs_type mode other_ty kv
516 ; return (ty', kv) }
517
518 ------------------------------------------
519 tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
520 tc_lhs_type mode (L span ty) exp_kind
521 = setSrcSpan span $
522 do { ty' <- tc_hs_type mode ty exp_kind
523 ; return ty' }
524
525 ------------------------------------------
526 tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
527 -> TcM TcType
528 tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
529 TypeLevel ->
530 do { arg_k <- newOpenTypeKind
531 ; res_k <- newOpenTypeKind
532 ; ty1' <- tc_lhs_type mode ty1 arg_k
533 ; ty2' <- tc_lhs_type mode ty2 res_k
534 ; checkExpectedKind (HsFunTy ty1 ty2) (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
535 KindLevel -> -- no representation polymorphism in kinds. yet.
536 do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
537 ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
538 ; checkExpectedKind (HsFunTy ty1 ty2) (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
539
540 ------------------------------------------
541 -- See also Note [Bidirectional type checking]
542 tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
543 tc_hs_type mode (HsParTy ty) exp_kind = tc_lhs_type mode ty exp_kind
544 tc_hs_type mode (HsDocTy ty _) exp_kind = tc_lhs_type mode ty exp_kind
545 tc_hs_type _ ty@(HsBangTy {}) _
546 -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
547 -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
548 -- bangs are invalid, so fail. (#7210)
549 = failWithTc (text "Unexpected strictness annotation:" <+> ppr ty)
550 tc_hs_type _ ty@(HsRecTy _) _
551 -- Record types (which only show up temporarily in constructor
552 -- signatures) should have been removed by now
553 = failWithTc (text "Record syntax is illegal here:" <+> ppr ty)
554
555 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType'.
556 -- Here we get rid of it and add the finalizers to the global environment
557 -- while capturing the local environment.
558 --
559 -- See Note [Delaying modFinalizers in untyped splices].
560 tc_hs_type mode (HsSpliceTy (HsSpliced mod_finalizers (HsSplicedTy ty))
561 _
562 )
563 exp_kind
564 = do addModFinalizersWithLclEnv mod_finalizers
565 tc_hs_type mode ty exp_kind
566
567 -- This should never happen; type splices are expanded by the renamer
568 tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind
569 = failWithTc (text "Unexpected type splice:" <+> ppr ty)
570
571 ---------- Functions and applications
572 tc_hs_type mode (HsFunTy ty1 ty2) exp_kind
573 = tc_fun_type mode ty1 ty2 exp_kind
574
575 tc_hs_type mode (HsOpTy ty1 (L _ op) ty2) exp_kind
576 | op `hasKey` funTyConKey
577 = tc_fun_type mode ty1 ty2 exp_kind
578
579 --------- Foralls
580 tc_hs_type mode (HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
581 = fmap fst $
582 tcExplicitTKBndrs hs_tvs $ \ tvs' ->
583 -- Do not kind-generalise here! See Note [Kind generalisation]
584 -- Why exp_kind? See Note [Body kind of HsForAllTy]
585 do { ty' <- tc_lhs_type mode ty exp_kind
586 ; let bound_vars = allBoundVariables ty'
587 bndrs = mkTyVarBinders Specified tvs'
588 ; return (mkForAllTys bndrs ty', bound_vars) }
589
590 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
591 | null (unLoc ctxt)
592 = tc_lhs_type mode ty exp_kind
593
594 | otherwise
595 = do { ctxt' <- tc_hs_context mode ctxt
596
597 -- See Note [Body kind of a HsQualTy]
598 ; ty' <- if isConstraintKind exp_kind
599 then tc_lhs_type mode ty constraintKind
600 else do { ek <- newOpenTypeKind
601 -- The body kind (result of the function)
602 -- can be * or #, hence newOpenTypeKind
603 ; ty' <- tc_lhs_type mode ty ek
604 ; checkExpectedKind (unLoc ty) ty' liftedTypeKind exp_kind }
605
606 ; return (mkPhiTy ctxt' ty') }
607
608 --------- Lists, arrays, and tuples
609 tc_hs_type mode rn_ty@(HsListTy elt_ty) exp_kind
610 = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
611 ; checkWiredInTyCon listTyCon
612 ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
613
614 tc_hs_type mode rn_ty@(HsPArrTy elt_ty) exp_kind
615 = do { MASSERT( isTypeLevel (mode_level mode) )
616 ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
617 ; checkWiredInTyCon parrTyCon
618 ; checkExpectedKind rn_ty (mkPArrTy tau_ty) liftedTypeKind exp_kind }
619
620 -- See Note [Distinguishing tuple kinds] in HsTypes
621 -- See Note [Inferring tuple kinds]
622 tc_hs_type mode rn_ty@(HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind
623 -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
624 | Just tup_sort <- tupKindSort_maybe exp_kind
625 = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
626 tc_tuple rn_ty mode tup_sort hs_tys exp_kind
627 | otherwise
628 = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
629 ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
630 ; kinds <- mapM zonkTcType kinds
631 -- Infer each arg type separately, because errors can be
632 -- confusing if we give them a shared kind. Eg Trac #7410
633 -- (Either Int, Int), we do not want to get an error saying
634 -- "the second argument of a tuple should have kind *->*"
635
636 ; let (arg_kind, tup_sort)
637 = case [ (k,s) | k <- kinds
638 , Just s <- [tupKindSort_maybe k] ] of
639 ((k,s) : _) -> (k,s)
640 [] -> (liftedTypeKind, BoxedTuple)
641 -- In the [] case, it's not clear what the kind is, so guess *
642
643 ; tys' <- sequence [ setSrcSpan loc $
644 checkExpectedKind hs_ty ty kind arg_kind
645 | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
646
647 ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
648
649
650 tc_hs_type mode rn_ty@(HsTupleTy hs_tup_sort tys) exp_kind
651 = tc_tuple rn_ty mode tup_sort tys exp_kind
652 where
653 tup_sort = case hs_tup_sort of -- Fourth case dealt with above
654 HsUnboxedTuple -> UnboxedTuple
655 HsBoxedTuple -> BoxedTuple
656 HsConstraintTuple -> ConstraintTuple
657 _ -> panic "tc_hs_type HsTupleTy"
658
659 tc_hs_type mode rn_ty@(HsSumTy hs_tys) exp_kind
660 = do { let arity = length hs_tys
661 ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
662 ; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
663 ; let arg_reps = map getRuntimeRepFromKind arg_kinds
664 arg_tys = arg_reps ++ tau_tys
665 ; checkExpectedKind rn_ty
666 (mkTyConApp (sumTyCon arity) arg_tys)
667 (unboxedSumKind arg_reps)
668 exp_kind
669 }
670
671 --------- Promoted lists and tuples
672 tc_hs_type mode rn_ty@(HsExplicitListTy _ _k tys) exp_kind
673 = do { tks <- mapM (tc_infer_lhs_type mode) tys
674 ; (taus', kind) <- unifyKinds tys tks
675 ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
676 ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
677 where
678 mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
679 mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k]
680
681 tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
682 -- using newMetaKindVar means that we force instantiations of any polykinded
683 -- types. At first, I just used tc_infer_lhs_type, but that led to #11255.
684 = do { ks <- replicateM arity newMetaKindVar
685 ; taus <- zipWithM (tc_lhs_type mode) tys ks
686 ; let kind_con = tupleTyCon Boxed arity
687 ty_con = promotedTupleDataCon Boxed arity
688 tup_k = mkTyConApp kind_con ks
689 ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
690 where
691 arity = length tys
692
693 --------- Constraint types
694 tc_hs_type mode rn_ty@(HsIParamTy (L _ n) ty) exp_kind
695 = do { MASSERT( isTypeLevel (mode_level mode) )
696 ; ty' <- tc_lhs_type mode ty liftedTypeKind
697 ; let n' = mkStrLitTy $ hsIPNameFS n
698 ; ipClass <- tcLookupClass ipClassName
699 ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
700 constraintKind exp_kind }
701
702 tc_hs_type mode rn_ty@(HsEqTy ty1 ty2) exp_kind
703 = do { (ty1', kind1) <- tc_infer_lhs_type mode ty1
704 ; (ty2', kind2) <- tc_infer_lhs_type mode ty2
705 ; ty2'' <- checkExpectedKind (unLoc ty2) ty2' kind2 kind1
706 ; eq_tc <- tcLookupTyCon eqTyConName
707 ; let ty' = mkNakedTyConApp eq_tc [kind1, ty1', ty2'']
708 ; checkExpectedKind rn_ty ty' constraintKind exp_kind }
709
710 --------- Literals
711 tc_hs_type _ rn_ty@(HsTyLit (HsNumTy _ n)) exp_kind
712 = do { checkWiredInTyCon typeNatKindCon
713 ; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
714
715 tc_hs_type _ rn_ty@(HsTyLit (HsStrTy _ s)) exp_kind
716 = do { checkWiredInTyCon typeSymbolKindCon
717 ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
718
719 --------- Potentially kind-polymorphic types: call the "up" checker
720 -- See Note [Future-proofing the type checker]
721 tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
722 tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek
723 tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
724 tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
725 tc_hs_type mode ty@(HsCoreTy {}) ek = tc_infer_hs_type_ek mode ty ek
726
727 tc_hs_type _ (HsWildCardTy wc) exp_kind
728 = do { wc_tv <- tcWildCardOcc wc exp_kind
729 ; return (mkTyVarTy wc_tv) }
730
731 -- disposed of by renamer
732 tc_hs_type _ ty@(HsAppsTy {}) _
733 = pprPanic "tc_hs_tyep HsAppsTy" (ppr ty)
734
735 tcWildCardOcc :: HsWildCardInfo GhcRn -> Kind -> TcM TcTyVar
736 tcWildCardOcc wc_info exp_kind
737 = do { wc_tv <- tcLookupTyVar (wildCardName wc_info)
738 -- The wildcard's kind should be an un-filled-in meta tyvar
739 ; let Just wc_kind_var = tcGetTyVar_maybe (tyVarKind wc_tv)
740 ; writeMetaTyVar wc_kind_var exp_kind
741 ; return wc_tv }
742
743 ---------------------------
744 -- | Call 'tc_infer_hs_type' and check its result against an expected kind.
745 tc_infer_hs_type_ek :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
746 tc_infer_hs_type_ek mode hs_ty ek
747 = do { (ty, k) <- tc_infer_hs_type mode hs_ty
748 ; checkExpectedKind hs_ty ty k ek }
749
750 ---------------------------
751 tupKindSort_maybe :: TcKind -> Maybe TupleSort
752 tupKindSort_maybe k
753 | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
754 | Just k' <- tcView k = tupKindSort_maybe k'
755 | isConstraintKind k = Just ConstraintTuple
756 | isLiftedTypeKind k = Just BoxedTuple
757 | otherwise = Nothing
758
759 tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
760 tc_tuple rn_ty mode tup_sort tys exp_kind
761 = do { arg_kinds <- case tup_sort of
762 BoxedTuple -> return (nOfThem arity liftedTypeKind)
763 UnboxedTuple -> mapM (\_ -> newOpenTypeKind) tys
764 ConstraintTuple -> return (nOfThem arity constraintKind)
765 ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
766 ; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
767 where
768 arity = length tys
769
770 finish_tuple :: HsType GhcRn
771 -> TupleSort
772 -> [TcType] -- ^ argument types
773 -> [TcKind] -- ^ of these kinds
774 -> TcKind -- ^ expected kind of the whole tuple
775 -> TcM TcType
776 finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
777 = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
778 ; let arg_tys = case tup_sort of
779 -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
780 UnboxedTuple -> tau_reps ++ tau_tys
781 BoxedTuple -> tau_tys
782 ConstraintTuple -> tau_tys
783 ; tycon <- case tup_sort of
784 ConstraintTuple
785 | arity > mAX_CTUPLE_SIZE
786 -> failWith (bigConstraintTuple arity)
787 | otherwise -> tcLookupTyCon (cTupleTyConName arity)
788 BoxedTuple -> do { let tc = tupleTyCon Boxed arity
789 ; checkWiredInTyCon tc
790 ; return tc }
791 UnboxedTuple -> return (tupleTyCon Unboxed arity)
792 ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind }
793 where
794 arity = length tau_tys
795 tau_reps = map getRuntimeRepFromKind tau_kinds
796 res_kind = case tup_sort of
797 UnboxedTuple -> unboxedTupleKind tau_reps
798 BoxedTuple -> liftedTypeKind
799 ConstraintTuple -> constraintKind
800
801 bigConstraintTuple :: Arity -> MsgDoc
802 bigConstraintTuple arity
803 = hang (text "Constraint tuple arity too large:" <+> int arity
804 <+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
805 2 (text "Instead, use a nested tuple")
806
807 ---------------------------
808 -- | Apply a type of a given kind to a list of arguments. This instantiates
809 -- invisible parameters as necessary. Always consumes all the arguments,
810 -- using matchExpectedFunKind as necessary.
811 -- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.
812 -- These kinds should be used to instantiate invisible kind variables;
813 -- they come from an enclosing class for an associated type/data family.
814 tcInferApps :: TcTyMode
815 -> Maybe (VarEnv Kind) -- ^ Possibly, kind info (see above)
816 -> LHsType GhcRn -- ^ Function (for printing only)
817 -> TcType -- ^ Function (could be knot-tied)
818 -> TcKind -- ^ Function kind (zonked)
819 -> [LHsType GhcRn] -- ^ Args
820 -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
821 tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
822 = do { traceTc "tcInferApps" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki)
823 ; go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args }
824 where
825 empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
826 tyCoVarsOfType fun_ki
827 (orig_ki_binders, orig_inner_ki) = tcSplitPiTys fun_ki
828
829 go :: Int -- the # of the next argument
830 -> [TcType] -- already type-checked args, in reverse order
831 -> TCvSubst -- instantiating substitution
832 -> TcType -- function applied to some args, could be knot-tied
833 -> [TyBinder] -- binders in function kind (both vis. and invis.)
834 -> TcKind -- function kind body (not a Pi-type)
835 -> [LHsType GhcRn] -- un-type-checked args
836 -> TcM (TcType, [TcType], TcKind) -- same as overall return type
837
838 -- no user-written args left. We're done!
839 go _ acc_args subst fun ki_binders inner_ki []
840 = return (fun, reverse acc_args, substTy subst $ mkPiTys ki_binders inner_ki)
841
842 -- The function's kind has a binder. Is it visible or invisible?
843 go n acc_args subst fun (ki_binder:ki_binders) inner_ki
844 all_args@(arg:args)
845 | isInvisibleBinder ki_binder
846 -- It's invisible. Instantiate.
847 = do { traceTc "tcInferApps (invis)" (ppr ki_binder $$ ppr subst)
848 ; (subst', arg') <- tcInstBinder mb_kind_info subst ki_binder
849 ; go n (arg' : acc_args) subst' (mkNakedAppTy fun arg')
850 ki_binders inner_ki all_args }
851
852 | otherwise
853 -- It's visible. Check the next user-written argument
854 = do { traceTc "tcInferApps (vis)" (vcat [ ppr ki_binder, ppr arg
855 , ppr (tyBinderType ki_binder)
856 , ppr subst ])
857 ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
858 tc_lhs_type mode arg (substTy subst $ tyBinderType ki_binder)
859 ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
860 ; go (n+1) (arg' : acc_args) subst' (mkNakedAppTy fun arg')
861 ki_binders inner_ki args }
862
863 -- We've run out of known binders in the functions's kind.
864 go n acc_args subst fun [] inner_ki all_args
865 | not (null new_ki_binders)
866 -- But, after substituting, we have more binders.
867 = go n acc_args zapped_subst fun new_ki_binders new_inner_ki all_args
868
869 | otherwise
870 -- Even after substituting, still no binders. Use matchExpectedFunKind
871 = do { traceTc "tcInferApps (no binder)" (ppr new_inner_ki $$ ppr zapped_subst)
872 ; (co, arg_k, res_k)
873 <- matchExpectedFunKind (mkHsAppTys orig_hs_ty (take (n-1) orig_hs_args))
874 substed_inner_ki
875 ; let subst' = zapped_subst `extendTCvInScopeSet` tyCoVarsOfTypes [arg_k, res_k]
876 ; go n acc_args subst' (fun `mkNakedCastTy` co)
877 [mkAnonBinder arg_k] res_k all_args }
878 where
879 substed_inner_ki = substTy subst inner_ki
880 (new_ki_binders, new_inner_ki) = tcSplitPiTys substed_inner_ki
881 zapped_subst = zapTCvSubst subst
882
883 -- | Applies a type to a list of arguments.
884 -- Always consumes all the arguments, using 'matchExpectedFunKind' as
885 -- necessary. If you wish to apply a type to a list of HsTypes, this is
886 -- your function.
887 -- Used for type-checking types only.
888 tcTyApps :: TcTyMode
889 -> LHsType GhcRn -- ^ Function (for printing only)
890 -> TcType -- ^ Function (could be knot-tied)
891 -> TcKind -- ^ Function kind (zonked)
892 -> [LHsType GhcRn] -- ^ Args
893 -> TcM (TcType, TcKind) -- ^ (f args, result kind)
894 tcTyApps mode orig_hs_ty ty ki args
895 = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty ty ki args
896 ; return (ty', ki') }
897
898 --------------------------
899 -- like checkExpectedKindX, but returns only the final type; convenient wrapper
900 checkExpectedKind :: HsType GhcRn
901 -> TcType
902 -> TcKind
903 -> TcKind
904 -> TcM TcType
905 checkExpectedKind hs_ty ty act exp
906 = fstOf3 <$> checkExpectedKindX Nothing (ppr hs_ty) ty act exp
907
908 checkExpectedKindX :: Maybe (VarEnv Kind) -- Possibly, instantiations for kind vars
909 -> SDoc -- HsType whose kind we're checking
910 -> TcType -- the type whose kind we're checking
911 -> TcKind -- the known kind of that type, k
912 -> TcKind -- the expected kind, exp_kind
913 -> TcM (TcType, [TcType], TcCoercionN)
914 -- (an possibly-inst'ed, casted type :: exp_kind, the new args, the coercion)
915 -- Instantiate a kind (if necessary) and then call unifyType
916 -- (checkExpectedKind ty act_kind exp_kind)
917 -- checks that the actual kind act_kind is compatible
918 -- with the expected kind exp_kind
919 checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
920 = do { (ty', new_args, act_kind') <- instantiate ty act_kind exp_kind
921 ; let origin = TypeEqOrigin { uo_actual = act_kind'
922 , uo_expected = exp_kind
923 , uo_thing = Just pp_hs_ty
924 , uo_visible = True } -- the hs_ty is visible
925 ; co_k <- uType KindLevel origin act_kind' exp_kind
926 ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
927 , ppr exp_kind
928 , ppr co_k ])
929 ; let result_ty = ty' `mkNakedCastTy` co_k
930 ; return (result_ty, new_args, co_k) }
931 where
932 -- we need to make sure that both kinds have the same number of implicit
933 -- foralls out front. If the actual kind has more, instantiate accordingly.
934 -- Otherwise, just pass the type & kind through -- the errors are caught
935 -- in unifyType.
936 instantiate :: TcType -- the type
937 -> TcKind -- of this kind
938 -> TcKind -- but expected to be of this one
939 -> TcM ( TcType -- the inst'ed type
940 , [TcType] -- the new args
941 , TcKind ) -- its new kind
942 instantiate ty act_ki exp_ki
943 = let (exp_bndrs, _) = splitPiTysInvisible exp_ki in
944 instantiateTyUntilN mb_kind_env (length exp_bndrs) ty act_ki
945
946 -- | Instantiate @n@ invisible arguments to a type. If @n <= 0@, no instantiation
947 -- occurs. If @n@ is too big, then all available invisible arguments are instantiated.
948 -- (In other words, this function is very forgiving about bad values of @n@.)
949 instantiateTyN :: Maybe (VarEnv Kind) -- ^ Predetermined instantiations
950 -- (for assoc. type patterns)
951 -> Int -- ^ @n@
952 -> TcType -- ^ the type
953 -> [TyBinder] -> TcKind -- ^ its kind
954 -> TcM (TcType, [TcType], TcKind) -- ^ The inst'ed type, new args, kind
955 instantiateTyN mb_kind_env n ty bndrs inner_ki
956 = let -- NB: splitAt is forgiving with invalid numbers
957 (inst_bndrs, leftover_bndrs) = splitAt n bndrs
958 ki = mkPiTys bndrs inner_ki
959 empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ki))
960 in
961 if n <= 0 then return (ty, [], ki) else
962 do { (subst, inst_args) <- tcInstBinders empty_subst mb_kind_env inst_bndrs
963 ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
964 ki' = substTy subst rebuilt_ki
965 ; traceTc "instantiateTyN" (vcat [ ppr ki
966 , ppr n
967 , ppr subst
968 , ppr rebuilt_ki
969 , ppr ki' ])
970 ; return (mkNakedAppTys ty inst_args, inst_args, ki') }
971
972 -- | Instantiate a type to have at most @n@ invisible arguments.
973 instantiateTyUntilN :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
974 -> Int -- ^ @n@
975 -> TcType -- ^ the type
976 -> TcKind -- ^ its kind
977 -> TcM (TcType, [TcType], TcKind) -- ^ The inst'ed type, new args,
978 -- final kind
979 instantiateTyUntilN mb_kind_env n ty ki
980 = let (bndrs, inner_ki) = splitPiTysInvisible ki
981 num_to_inst = length bndrs - n
982 in
983 instantiateTyN mb_kind_env num_to_inst ty bndrs inner_ki
984
985 ---------------------------
986 tcHsContext :: LHsContext GhcRn -> TcM [PredType]
987 tcHsContext = tc_hs_context typeLevelMode
988
989 tcLHsPredType :: LHsType GhcRn -> TcM PredType
990 tcLHsPredType = tc_lhs_pred typeLevelMode
991
992 tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
993 tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)
994
995 tc_lhs_pred :: TcTyMode -> LHsType GhcRn -> TcM PredType
996 tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
997
998 ---------------------------
999 tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
1000 -- See Note [Type checking recursive type and class declarations]
1001 -- in TcTyClsDecls
1002 tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
1003 = do { traceTc "lk1" (ppr name)
1004 ; thing <- tcLookup name
1005 ; case thing of
1006 ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
1007
1008 ATcTyCon tc_tc -> do { -- See Note [GADT kind self-reference]
1009 unless
1010 (isTypeLevel (mode_level mode))
1011 (promotionErr name TyConPE)
1012 ; check_tc tc_tc
1013 ; tc <- get_loopy_tc name tc_tc
1014 ; handle_tyfams tc tc_tc }
1015 -- mkNakedTyConApp: see Note [Type-checking inside the knot]
1016 -- NB: we really should check if we're at the kind level
1017 -- and if the tycon is promotable if -XNoTypeInType is set.
1018 -- But this is a terribly large amount of work! Not worth it.
1019
1020 AGlobal (ATyCon tc)
1021 -> do { check_tc tc
1022 ; handle_tyfams tc tc }
1023
1024 AGlobal (AConLike (RealDataCon dc))
1025 -> do { data_kinds <- xoptM LangExt.DataKinds
1026 ; unless (data_kinds || specialPromotedDc dc) $
1027 promotionErr name NoDataKindsDC
1028 ; type_in_type <- xoptM LangExt.TypeInType
1029 ; unless ( type_in_type ||
1030 ( isTypeLevel (mode_level mode) &&
1031 isLegacyPromotableDataCon dc ) ||
1032 ( isKindLevel (mode_level mode) &&
1033 specialPromotedDc dc ) ) $
1034 promotionErr name NoTypeInTypeDC
1035 ; let tc = promoteDataCon dc
1036 ; return (mkNakedTyConApp tc [], tyConKind tc) }
1037
1038 APromotionErr err -> promotionErr name err
1039
1040 _ -> wrongThingErr "type" thing name }
1041 where
1042 check_tc :: TyCon -> TcM ()
1043 check_tc tc = do { type_in_type <- xoptM LangExt.TypeInType
1044 ; data_kinds <- xoptM LangExt.DataKinds
1045 ; unless (isTypeLevel (mode_level mode) ||
1046 data_kinds ||
1047 isKindTyCon tc) $
1048 promotionErr name NoDataKindsTC
1049 ; unless (isTypeLevel (mode_level mode) ||
1050 type_in_type ||
1051 isLegacyPromotableTyCon tc) $
1052 promotionErr name NoTypeInTypeTC }
1053
1054 -- if we are type-checking a type family tycon, we must instantiate
1055 -- any invisible arguments right away. Otherwise, we get #11246
1056 handle_tyfams :: TyCon -- the tycon to instantiate (might be loopy)
1057 -> TcTyCon -- a non-loopy version of the tycon
1058 -> TcM (TcType, TcKind)
1059 handle_tyfams tc tc_tc
1060 | mightBeUnsaturatedTyCon tc_tc || mode_unsat mode
1061 -- This is where mode_unsat is used
1062 = do { traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind)
1063 ; return (ty, tc_kind) }
1064
1065 | otherwise
1066 = do { (tc_ty, _, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc))
1067 ty tc_kind_bndrs tc_inner_ki
1068 -- tc and tc_ty must not be traced here, because that would
1069 -- force the evaluation of a potentially knot-tied variable (tc),
1070 -- and the typechecker would hang, as per #11708
1071 ; traceTc "tcTyVar2b" (vcat [ ppr tc_tc <+> dcolon <+> ppr tc_kind
1072 , ppr kind ])
1073 ; return (tc_ty, kind) }
1074 where
1075 ty = mkNakedTyConApp tc []
1076 tc_kind = tyConKind tc_tc
1077 (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
1078
1079 get_loopy_tc :: Name -> TyCon -> TcM TyCon
1080 -- Return the knot-tied global TyCon if there is one
1081 -- Otherwise the local TcTyCon; we must be doing kind checking
1082 -- but we still want to return a TyCon of some sort to use in
1083 -- error messages
1084 get_loopy_tc name tc_tc
1085 = do { env <- getGblEnv
1086 ; case lookupNameEnv (tcg_type_env env) name of
1087 Just (ATyCon tc) -> return tc
1088 _ -> do { traceTc "lk1 (loopy)" (ppr name)
1089 ; return tc_tc } }
1090
1091 tcClass :: Name -> TcM (Class, TcKind)
1092 tcClass cls -- Must be a class
1093 = do { thing <- tcLookup cls
1094 ; case thing of
1095 ATcTyCon tc -> return (aThingErr "tcClass" cls, tyConKind tc)
1096 AGlobal (ATyCon tc)
1097 | Just cls <- tyConClass_maybe tc
1098 -> return (cls, tyConKind tc)
1099 _ -> wrongThingErr "class" thing cls }
1100
1101
1102 aThingErr :: String -> Name -> b
1103 -- The type checker for types is sometimes called simply to
1104 -- do *kind* checking; and in that case it ignores the type
1105 -- returned. Which is a good thing since it may not be available yet!
1106 aThingErr str x = pprPanic "AThing evaluated unexpectedly" (text str <+> ppr x)
1107
1108 {-
1109 Note [Type-checking inside the knot]
1110 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1111 Suppose we are checking the argument types of a data constructor. We
1112 must zonk the types before making the DataCon, because once built we
1113 can't change it. So we must traverse the type.
1114
1115 BUT the parent TyCon is knot-tied, so we can't look at it yet.
1116
1117 So we must be careful not to use "smart constructors" for types that
1118 look at the TyCon or Class involved.
1119
1120 * Hence the use of mkNakedXXX functions. These do *not* enforce
1121 the invariants (for example that we use (FunTy s t) rather
1122 than (TyConApp (->) [s,t])).
1123
1124 * The zonking functions establish invariants (even zonkTcType, a change from
1125 previous behaviour). So we must never inspect the result of a
1126 zonk that might mention a knot-tied TyCon. This is generally OK
1127 because we zonk *kinds* while kind-checking types. And the TyCons
1128 in kinds shouldn't be knot-tied, because they come from a previous
1129 mutually recursive group.
1130
1131 * TcHsSyn.zonkTcTypeToType also can safely check/establish
1132 invariants.
1133
1134 This is horribly delicate. I hate it. A good example of how
1135 delicate it is can be seen in Trac #7903.
1136
1137 Note [GADT kind self-reference]
1138 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1139
1140 A promoted type cannot be used in the body of that type's declaration.
1141 Trac #11554 shows this example, which made GHC loop:
1142
1143 import Data.Kind
1144 data P (x :: k) = Q
1145 data A :: Type where
1146 B :: forall (a :: A). P a -> A
1147
1148 In order to check the constructor B, we need to have the promoted type A, but in
1149 order to get that promoted type, B must first be checked. To prevent looping, a
1150 TyConPE promotion error is given when tcTyVar checks an ATcTyCon in kind mode.
1151 Any ATcTyCon is a TyCon being defined in the current recursive group (see data
1152 type decl for TcTyThing), and all such TyCons are illegal in kinds.
1153
1154 Trac #11962 proposes checking the head of a data declaration separately from
1155 its constructors. This would allow the example above to pass.
1156
1157 Note [Body kind of a HsForAllTy]
1158 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1159 The body of a forall is usually a type, but in principle
1160 there's no reason to prohibit *unlifted* types.
1161 In fact, GHC can itself construct a function with an
1162 unboxed tuple inside a for-all (via CPR analysis; see
1163 typecheck/should_compile/tc170).
1164
1165 Moreover in instance heads we get forall-types with
1166 kind Constraint.
1167
1168 It's tempting to check that the body kind is either * or #. But this is
1169 wrong. For example:
1170
1171 class C a b
1172 newtype N = Mk Foo deriving (C a)
1173
1174 We're doing newtype-deriving for C. But notice how `a` isn't in scope in
1175 the predicate `C a`. So we quantify, yielding `forall a. C a` even though
1176 `C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
1177 convenient. Bottom line: don't check for * or # here.
1178
1179 Note [Body kind of a HsQualTy]
1180 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1181 If ctxt is non-empty, the HsQualTy really is a /function/, so the
1182 kind of the result really is '*', and in that case the kind of the
1183 body-type can be lifted or unlifted.
1184
1185 However, consider
1186 instance Eq a => Eq [a] where ...
1187 or
1188 f :: (Eq a => Eq [a]) => blah
1189 Here both body-kind of the HsQualTy is Constraint rather than *.
1190 Rather crudely we tell the difference by looking at exp_kind. It's
1191 very convenient to typecheck instance types like any other HsSigType.
1192
1193 Admittedly the '(Eq a => Eq [a]) => blah' case is erroneous, but it's
1194 better to reject in checkValidType. If we say that the body kind
1195 should be '*' we risk getting TWO error messages, one saying that Eq
1196 [a] doens't have kind '*', and one saying that we need a Constraint to
1197 the left of the outer (=>).
1198
1199 How do we figure out the right body kind? Well, it's a bit of a
1200 kludge: I just look at the expected kind. If it's Constraint, we
1201 must be in this instance situation context. It's a kludge because it
1202 wouldn't work if any unification was involved to compute that result
1203 kind -- but it isn't. (The true way might be to use the 'mode'
1204 parameter, but that seemed like a sledgehammer to crack a nut.)
1205
1206 Note [Inferring tuple kinds]
1207 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1208 Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
1209 we try to figure out whether it's a tuple of kind * or Constraint.
1210 Step 1: look at the expected kind
1211 Step 2: infer argument kinds
1212
1213 If after Step 2 it's not clear from the arguments that it's
1214 Constraint, then it must be *. Once having decided that we re-check
1215 the Check the arguments again to give good error messages
1216 in eg. `(Maybe, Maybe)`
1217
1218 Note that we will still fail to infer the correct kind in this case:
1219
1220 type T a = ((a,a), D a)
1221 type family D :: Constraint -> Constraint
1222
1223 While kind checking T, we do not yet know the kind of D, so we will default the
1224 kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
1225
1226 Note [Desugaring types]
1227 ~~~~~~~~~~~~~~~~~~~~~~~
1228 The type desugarer is phase 2 of dealing with HsTypes. Specifically:
1229
1230 * It transforms from HsType to Type
1231
1232 * It zonks any kinds. The returned type should have no mutable kind
1233 or type variables (hence returning Type not TcType):
1234 - any unconstrained kind variables are defaulted to (Any *) just
1235 as in TcHsSyn.
1236 - there are no mutable type variables because we are
1237 kind-checking a type
1238 Reason: the returned type may be put in a TyCon or DataCon where
1239 it will never subsequently be zonked.
1240
1241 You might worry about nested scopes:
1242 ..a:kappa in scope..
1243 let f :: forall b. T '[a,b] -> Int
1244 In this case, f's type could have a mutable kind variable kappa in it;
1245 and we might then default it to (Any *) when dealing with f's type
1246 signature. But we don't expect this to happen because we can't get a
1247 lexically scoped type variable with a mutable kind variable in it. A
1248 delicate point, this. If it becomes an issue we might need to
1249 distinguish top-level from nested uses.
1250
1251 Moreover
1252 * it cannot fail,
1253 * it does no unifications
1254 * it does no validity checking, except for structural matters, such as
1255 (a) spurious ! annotations.
1256 (b) a class used as a type
1257
1258 Note [Kind of a type splice]
1259 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1260 Consider these terms, each with TH type splice inside:
1261 [| e1 :: Maybe $(..blah..) |]
1262 [| e2 :: $(..blah..) |]
1263 When kind-checking the type signature, we'll kind-check the splice
1264 $(..blah..); we want to give it a kind that can fit in any context,
1265 as if $(..blah..) :: forall k. k.
1266
1267 In the e1 example, the context of the splice fixes kappa to *. But
1268 in the e2 example, we'll desugar the type, zonking the kind unification
1269 variables as we go. When we encounter the unconstrained kappa, we
1270 want to default it to '*', not to (Any *).
1271
1272
1273 Help functions for type applications
1274 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1275 -}
1276
1277 addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
1278 -- Wrap a context around only if we want to show that contexts.
1279 -- Omit invisible ones and ones user's won't grok
1280 addTypeCtxt (L _ ty) thing
1281 = addErrCtxt doc thing
1282 where
1283 doc = text "In the type" <+> quotes (ppr ty)
1284
1285 {-
1286 ************************************************************************
1287 * *
1288 Type-variable binders
1289 %* *
1290 %************************************************************************
1291
1292 Note [Scope-check inferred kinds]
1293 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1294 Consider
1295
1296 data SameKind :: k -> k -> *
1297 foo :: forall a (b :: Proxy a) (c :: Proxy d). SameKind b c
1298
1299 d has no binding site. So it gets bound implicitly, at the top. The
1300 problem is that d's kind mentions `a`. So it's all ill-scoped.
1301
1302 The way we check for this is to gather all variables *bound* in a
1303 type variable's scope. The type variable's kind should not mention
1304 any of these variables. That is, d's kind can't mention a, b, or c.
1305 We can't just check to make sure that d's kind is in scope, because
1306 we might be about to kindGeneralize.
1307
1308 A little messy, but it works.
1309
1310 Note [Dependent LHsQTyVars]
1311 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1312 We track (in the renamer) which explicitly bound variables in a
1313 LHsQTyVars are manifestly dependent; only precisely these variables
1314 may be used within the LHsQTyVars. We must do this so that kcHsTyVarBndrs
1315 can produce the right TyConBinders, and tell Anon vs. Required.
1316
1317 Example data T k1 (a:k1) (b:k2) c
1318 = MkT (Proxy a) (Proxy b) (Proxy c)
1319
1320 Here
1321 (a:k1),(b:k2),(c:k3)
1322 are Anon (explicitly specified as a binder, not used
1323 in the kind of any other binder
1324 k1 is Required (explicitly specifed as a binder, but used
1325 in the kind of another binder i.e. dependently)
1326 k2 is Specified (not explicitly bound, but used in the kind
1327 of another binder)
1328 k3 in Inferred (not lexically in scope at all, but inferred
1329 by kind inference)
1330 and
1331 T :: forall {k3} k1. forall k3 -> k1 -> k2 -> k3 -> *
1332
1333 See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility]
1334 in TyCoRep.
1335
1336 kcHsTyVarBndrs uses the hsq_dependent field to decide whether
1337 k1, a, b, c should be Required or Anon.
1338
1339 Earlier, thought it would work simply to do a free-variable check
1340 during kcHsTyVarBndrs, but this is bogus, because there may be
1341 unsolved equalities about. And we don't want to eagerly solve the
1342 equalities, because we may get further information after
1343 kcHsTyVarBndrs is called. (Recall that kcHsTyVarBndrs is usually
1344 called from getInitialKind. The only other case is in kcConDecl.)
1345 This is what implements the rule that all variables intended to be
1346 dependent must be manifestly so.
1347
1348 Sidenote: It's quite possible that later, we'll consider (t -> s)
1349 as a degenerate case of some (pi (x :: t) -> s) and then this will
1350 all get more permissive.
1351
1352 -}
1353
1354 tcWildCardBinders :: [Name]
1355 -> ([(Name, TcTyVar)] -> TcM a)
1356 -> TcM a
1357 tcWildCardBinders = tcWildCardBindersX new_tv
1358 where
1359 new_tv name = do { kind <- newMetaKindVar
1360 ; newSkolemTyVar name kind }
1361
1362 tcWildCardBindersX :: (Name -> TcM TcTyVar)
1363 -> [Name]
1364 -> ([(Name, TcTyVar)] -> TcM a)
1365 -> TcM a
1366 tcWildCardBindersX new_wc wc_names thing_inside
1367 = do { wcs <- mapM new_wc wc_names
1368 ; let wc_prs = wc_names `zip` wcs
1369 ; tcExtendTyVarEnv2 wc_prs $
1370 thing_inside wc_prs }
1371
1372 -- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
1373 -- user-supplied kind signature (CUSK), generalise the result.
1374 -- Used in 'getInitialKind' (for tycon kinds and other kinds)
1375 -- and in kind-checking (but not for tycon kinds, which are checked with
1376 -- tcTyClDecls). See also Note [Complete user-supplied kind signatures] in
1377 -- HsDecls.
1378 --
1379 -- This function does not do telescope checking.
1380 kcHsTyVarBndrs :: Name -- ^ of the thing being checked
1381 -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
1382 -> Bool -- ^ True <=> the decl being checked has a CUSK
1383 -> Bool -- ^ True <=> all the hsq_implicit are *kind* vars
1384 -- (will give these kind * if -XNoTypeInType)
1385 -> LHsQTyVars GhcRn
1386 -> TcM (Kind, r) -- ^ The result kind, possibly with other info
1387 -> TcM (TcTyCon, r) -- ^ A suitably-kinded TcTyCon
1388 kcHsTyVarBndrs name flav cusk all_kind_vars
1389 (HsQTvs { hsq_implicit = kv_ns, hsq_explicit = hs_tvs
1390 , hsq_dependent = dep_names }) thing_inside
1391 | cusk
1392 = do { kv_kinds <- mk_kv_kinds
1393 ; lvl <- getTcLevel
1394 ; let scoped_kvs = zipWith (mk_skolem_tv lvl) kv_ns kv_kinds
1395 ; tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $
1396 do { (tc_binders, res_kind, stuff) <- solveEqualities $
1397 bind_telescope hs_tvs thing_inside
1398
1399 -- Now, because we're in a CUSK, quantify over the mentioned
1400 -- kind vars, in dependency order.
1401 ; tc_binders <- mapM zonkTcTyVarBinder tc_binders
1402 ; res_kind <- zonkTcType res_kind
1403 ; let tc_tvs = binderVars tc_binders
1404 qkvs = tyCoVarsOfTypeWellScoped (mkTyConKind tc_binders res_kind)
1405 -- the visibility of tvs doesn't matter here; we just
1406 -- want the free variables not to include the tvs
1407
1408 -- If there are any meta-tvs left, the user has
1409 -- lied about having a CUSK. Error.
1410 ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
1411 ; when (not (null meta_tvs)) $
1412 report_non_cusk_tvs (qkvs ++ tc_tvs)
1413
1414 -- If any of the scoped_kvs aren't actually mentioned in a binder's
1415 -- kind (or the return kind), then we're in the CUSK case from
1416 -- Note [Free-floating kind vars]
1417 ; let all_tc_tvs = good_tvs ++ tc_tvs
1418 all_mentioned_tvs = mapUnionVarSet (tyCoVarsOfType . tyVarKind)
1419 all_tc_tvs
1420 `unionVarSet` tyCoVarsOfType res_kind
1421 unmentioned_kvs = filterOut (`elemVarSet` all_mentioned_tvs)
1422 scoped_kvs
1423 ; reportFloatingKvs name flav all_tc_tvs unmentioned_kvs
1424
1425 ; let final_binders = map (mkNamedTyConBinder Specified) good_tvs
1426 ++ tc_binders
1427 tycon = mkTcTyCon name final_binders res_kind
1428 (scoped_kvs ++ tc_tvs) flav
1429 -- the tvs contain the binders already
1430 -- in scope from an enclosing class, but
1431 -- re-adding tvs to the env't doesn't cause
1432 -- harm
1433
1434 ; traceTc "kcHsTyVarBndrs: cusk" $
1435 vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
1436 , ppr tc_binders, ppr (mkTyConKind tc_binders res_kind)
1437 , ppr qkvs, ppr meta_tvs, ppr good_tvs, ppr final_binders ]
1438
1439 ; return (tycon, stuff) }}
1440
1441 | otherwise
1442 = do { kv_kinds <- mk_kv_kinds
1443 ; scoped_kvs <- zipWithM newSigTyVar kv_ns kv_kinds
1444 -- the names must line up in splitTelescopeTvs
1445 ; (binders, res_kind, stuff)
1446 <- tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $
1447 bind_telescope hs_tvs thing_inside
1448 ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they
1449 -- must remain lined up with the binders
1450 tycon = mkTcTyCon name binders res_kind
1451 (scoped_kvs ++ binderVars binders) flav
1452
1453 ; traceTc "kcHsTyVarBndrs: not-cusk" $
1454 vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
1455 , ppr binders, ppr (mkTyConKind binders res_kind) ]
1456 ; return (tycon, stuff) }
1457 where
1458 open_fam = tcFlavourIsOpen flav
1459
1460 -- if -XNoTypeInType and we know all the implicits are kind vars,
1461 -- just give the kind *. This prevents test
1462 -- dependent/should_fail/KindLevelsB from compiling, as it should
1463 mk_kv_kinds :: TcM [Kind]
1464 mk_kv_kinds = do { typeintype <- xoptM LangExt.TypeInType
1465 ; if not typeintype && all_kind_vars
1466 then return (map (const liftedTypeKind) kv_ns)
1467 else mapM (const newMetaKindVar) kv_ns }
1468
1469 -- there may be dependency between the explicit "ty" vars. So, we have
1470 -- to handle them one at a time.
1471 bind_telescope :: [LHsTyVarBndr GhcRn]
1472 -> TcM (Kind, r)
1473 -> TcM ([TyConBinder], TcKind, r)
1474 bind_telescope [] thing
1475 = do { (res_kind, stuff) <- thing
1476 ; return ([], res_kind, stuff) }
1477 bind_telescope (L _ hs_tv : hs_tvs) thing
1478 = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
1479 -- NB: Bring all tvs into scope, even non-dependent ones,
1480 -- as they're needed in type synonyms, data constructors, etc.
1481 ; (binders, res_kind, stuff) <- bind_unless_scoped tv_pair $
1482 bind_telescope hs_tvs $
1483 thing
1484 -- See Note [Dependent LHsQTyVars]
1485 ; let new_binder | hsTyVarName hs_tv `elemNameSet` dep_names
1486 = mkNamedTyConBinder Required tv
1487 | otherwise
1488 = mkAnonTyConBinder tv
1489 ; return ( new_binder : binders
1490 , res_kind, stuff ) }
1491
1492 -- | Bind the tyvar in the env't unless the bool is True
1493 bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a
1494 bind_unless_scoped (_, True) thing_inside = thing_inside
1495 bind_unless_scoped (tv, False) thing_inside
1496 = tcExtendTyVarEnv [tv] thing_inside
1497
1498 kc_hs_tv :: HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
1499 kc_hs_tv (UserTyVar lname@(L _ name))
1500 = do { tv_pair@(tv, scoped) <- tcHsTyVarName Nothing name
1501
1502 -- Open type/data families default their variables to kind *.
1503 ; when (open_fam && not scoped) $ -- (don't default class tyvars)
1504 discardResult $ unifyKind (Just (HsTyVar NotPromoted lname)) liftedTypeKind
1505 (tyVarKind tv)
1506
1507 ; return tv_pair }
1508
1509 kc_hs_tv (KindedTyVar (L _ name) lhs_kind)
1510 = do { kind <- tcLHsKindSig lhs_kind
1511 ; tcHsTyVarName (Just kind) name }
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 newWildTyVar :: Name -> TcM TcTyVar
1638 -- ^ New unification variable for a wildcard
1639 newWildTyVar _name
1640 = do { kind <- newMetaKindVar
1641 ; uniq <- newUnique
1642 ; details <- newMetaDetails TauTv
1643 ; let name = mkSysTvName uniq (fsLit "w")
1644 ; return (mkTcTyVar name kind details) }
1645
1646 -- | Produce a tyvar of the given name (with the kind provided, or
1647 -- otherwise a meta-var kind). If
1648 -- the name is already in scope, return the scoped variable, checking
1649 -- to make sure the known kind matches any kind provided. The
1650 -- second return value says whether the variable is in scope (True)
1651 -- or not (False). (Use this for associated types, for example.)
1652 tcHsTyVarName :: Maybe Kind -> Name -> TcM (TcTyVar, Bool)
1653 tcHsTyVarName m_kind name
1654 = do { mb_tv <- tcLookupLcl_maybe name
1655 ; case mb_tv of
1656 Just (ATyVar _ tv)
1657 -> do { whenIsJust m_kind $ \ kind ->
1658 discardResult $
1659 unifyKind (Just (HsTyVar NotPromoted (noLoc name))) kind (tyVarKind tv)
1660 ; return (tv, True) }
1661 _ -> do { kind <- case m_kind of
1662 Just kind -> return kind
1663 Nothing -> newMetaKindVar
1664 ; tv <- newSkolemTyVar name kind
1665 ; return (tv, False) }}
1666
1667 -- makes a new skolem tv
1668 newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
1669 newSkolemTyVar name kind = do { lvl <- getTcLevel
1670 ; return (mk_skolem_tv lvl name kind) }
1671
1672 mk_skolem_tv :: TcLevel -> Name -> Kind -> TcTyVar
1673 mk_skolem_tv lvl n k = mkTcTyVar n k (SkolemTv lvl False)
1674
1675 ------------------
1676 kindGeneralizeType :: Type -> TcM Type
1677 -- Result is zonked
1678 kindGeneralizeType ty
1679 = do { kvs <- kindGeneralize ty
1680 ; ty <- zonkSigType (mkInvForAllTys kvs ty)
1681 ; return ty }
1682
1683 kindGeneralize :: TcType -> TcM [KindVar]
1684 -- Quantify the free kind variables of a kind or type
1685 -- In the latter case the type is closed, so it has no free
1686 -- type variables. So in both cases, all the free vars are kind vars
1687 kindGeneralize kind_or_type
1688 = do { kvs <- zonkTcTypeAndFV kind_or_type
1689 ; let dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet }
1690 ; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked
1691 ; quantifyTyVars gbl_tvs dvs }
1692
1693 {-
1694 Note [Kind generalisation]
1695 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1696 We do kind generalisation only at the outer level of a type signature.
1697 For example, consider
1698 T :: forall k. k -> *
1699 f :: (forall a. T a -> Int) -> Int
1700 When kind-checking f's type signature we generalise the kind at
1701 the outermost level, thus:
1702 f1 :: forall k. (forall (a:k). T k a -> Int) -> Int -- YES!
1703 and *not* at the inner forall:
1704 f2 :: (forall k. forall (a:k). T k a -> Int) -> Int -- NO!
1705 Reason: same as for HM inference on value level declarations,
1706 we want to infer the most general type. The f2 type signature
1707 would be *less applicable* than f1, because it requires a more
1708 polymorphic argument.
1709
1710 NB: There are no explicit kind variables written in f's signature.
1711 When there are, the renamer adds these kind variables to the list of
1712 variables bound by the forall, so you can indeed have a type that's
1713 higher-rank in its kind. But only by explicit request.
1714
1715 Note [Kinds of quantified type variables]
1716 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1717 tcTyVarBndrsGen quantifies over a specified list of type variables,
1718 *and* over the kind variables mentioned in the kinds of those tyvars.
1719
1720 Note that we must zonk those kinds (obviously) but less obviously, we
1721 must return type variables whose kinds are zonked too. Example
1722 (a :: k7) where k7 := k9 -> k9
1723 We must return
1724 [k9, a:k9->k9]
1725 and NOT
1726 [k9, a:k7]
1727 Reason: we're going to turn this into a for-all type,
1728 forall k9. forall (a:k7). blah
1729 which the type checker will then instantiate, and instantiate does not
1730 look through unification variables!
1731
1732 Hence using zonked_kinds when forming tvs'.
1733
1734 Note [Free-floating kind vars]
1735 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1736 Consider
1737
1738 data T = MkT (forall (a :: k). Proxy a)
1739 -- from test ghci/scripts/T7873
1740
1741 This is not an existential datatype, but a higher-rank one (the forall
1742 to the right of MkT). Also consider
1743
1744 data S a = MkS (Proxy (a :: k))
1745
1746 According to the rules around implicitly-bound kind variables, in both
1747 cases those k's scope over the whole declaration. The renamer grabs
1748 it and adds it to the hsq_implicits field of the HsQTyVars of the
1749 tycon. So it must be in scope during type-checking, but we want to
1750 reject T while accepting S.
1751
1752 Why reject T? Because the kind variable isn't fixed by anything. For
1753 a variable like k to be implicit, it needs to be mentioned in the kind
1754 of a tycon tyvar. But it isn't.
1755
1756 Why accept S? Because kind inference tells us that a has kind k, so it's
1757 all OK.
1758
1759 Our approach depends on whether or not the datatype has a CUSK.
1760
1761 Non-CUSK: In the first pass (kcTyClTyVars) we just bring
1762 k into scope. In the second pass (tcTyClTyVars),
1763 we check to make sure that k has been unified with some other variable
1764 (or generalized over, making k into a skolem). If it hasn't been, then
1765 it must be a free-floating kind var. Error.
1766
1767 CUSK: When we determine the tycon's final, never-to-be-changed kind
1768 in kcHsTyVarBndrs, we check to make sure all implicitly-bound kind
1769 vars are indeed mentioned in a kind somewhere. If not, error.
1770
1771 We also perform free-floating kind var analysis for type family instances
1772 (see #13985). Here is an interesting example:
1773
1774 type family T :: k
1775 type instance T = (Nothing :: Maybe a)
1776
1777 Upon a cursory glance, it may appear that the kind variable `a` is
1778 free-floating above, since there are no (visible) LHS patterns in `T`. However,
1779 there is an *invisible* pattern due to the return kind, so inside of GHC, the
1780 instance looks closer to this:
1781
1782 type family T @k :: k
1783 type instance T @(Maybe a) = (Nothing :: Maybe a)
1784
1785 Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in
1786 fact not free-floating. Contrast that with this example:
1787
1788 type instance T = Proxy (Nothing :: Maybe a)
1789
1790 This would looks like this inside of GHC:
1791
1792 type instance T @(*) = Proxy (Nothing :: Maybe a)
1793
1794 So this time, `a` is neither bound by a visible nor invisible type pattern on
1795 the LHS, so it would be reported as free-floating.
1796
1797 Finally, here's one more brain-teaser (from #9574). In the example below:
1798
1799 class Funct f where
1800 type Codomain f :: *
1801 instance Funct ('KProxy :: KProxy o) where
1802 type Codomain 'KProxy = NatTr (Proxy :: o -> *)
1803
1804 As it turns out, `o` is not free-floating in this example. That is because `o`
1805 bound by the kind signature of the LHS type pattern 'KProxy. To make this more
1806 obvious, one can also write the instance like so:
1807
1808 instance Funct ('KProxy :: KProxy o) where
1809 type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *)
1810
1811 -}
1812
1813 --------------------
1814 -- getInitialKind has made a suitably-shaped kind for the type or class
1815 -- Look it up in the local environment. This is used only for tycons
1816 -- that we're currently type-checking, so we're sure to find a TcTyCon.
1817 kcLookupTcTyCon :: Name -> TcM TcTyCon
1818 kcLookupTcTyCon nm
1819 = do { tc_ty_thing <- tcLookup nm
1820 ; return $ case tc_ty_thing of
1821 ATcTyCon tc -> tc
1822 _ -> pprPanic "kcLookupTcTyCon" (ppr tc_ty_thing) }
1823
1824 -----------------------
1825 -- | Bring tycon tyvars into scope. This is used during the "kind-checking"
1826 -- pass in TcTyClsDecls. (Never in getInitialKind, never in the
1827 -- "type-checking"/desugaring pass.)
1828 -- Never emits constraints, though the thing_inside might.
1829 kcTyClTyVars :: Name -> TcM a -> TcM a
1830 kcTyClTyVars tycon_name thing_inside
1831 = do { tycon <- kcLookupTcTyCon tycon_name
1832 ; tcExtendTyVarEnv (tcTyConScopedTyVars tycon) $ thing_inside }
1833
1834 tcTyClTyVars :: Name
1835 -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
1836 -- ^ Used for the type variables of a type or class decl
1837 -- on the second full pass (type-checking/desugaring) in TcTyClDecls.
1838 -- This is *not* used in the initial-kind run, nor in the "kind-checking" pass.
1839 -- Accordingly, everything passed to the continuation is fully zonked.
1840 --
1841 -- (tcTyClTyVars T [a,b] thing_inside)
1842 -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
1843 -- calls thing_inside with arguments
1844 -- [k1,k2,a,b] [k1:*, k2:*, Anon (k1 -> *), Anon k1] (k2 -> *)
1845 -- having also extended the type environment with bindings
1846 -- for k1,k2,a,b
1847 --
1848 -- Never emits constraints.
1849 --
1850 -- The LHsTyVarBndrs is always user-written, and the full, generalised
1851 -- kind of the tycon is available in the local env.
1852 tcTyClTyVars tycon_name thing_inside
1853 = do { tycon <- kcLookupTcTyCon tycon_name
1854
1855 ; let scoped_tvs = tcTyConScopedTyVars tycon
1856 -- these are all zonked:
1857 res_kind = tyConResKind tycon
1858 binders = correct_binders (tyConBinders tycon) res_kind
1859
1860 -- See Note [Free-floating kind vars]
1861 ; zonked_scoped_tvs <- mapM zonkTcTyVarToTyVar scoped_tvs
1862 ; let still_sig_tvs = filter isSigTyVar zonked_scoped_tvs
1863 ; checkNoErrs $ reportFloatingKvs tycon_name (tyConFlavour tycon)
1864 zonked_scoped_tvs still_sig_tvs
1865
1866 -- Add the *unzonked* tyvars to the env't, because those
1867 -- are the ones mentioned in the source.
1868 ; traceTc "tcTyClTyVars" (ppr tycon_name <+> ppr binders)
1869 ; tcExtendTyVarEnv scoped_tvs $
1870 thing_inside binders res_kind }
1871 where
1872 -- Given some TyConBinders and a TyCon's result kind, make sure that the
1873 -- correct any wrong Named/Anon choices. For example, consider
1874 -- type Syn k = forall (a :: k). Proxy a
1875 -- At first, it looks like k should be named -- after all, it appears on the RHS.
1876 -- However, the correct kind for Syn is (* -> *).
1877 -- (Why? Because k is the kind of a type, so k's kind is *. And the RHS also has
1878 -- kind *.) See also #13963.
1879 correct_binders :: [TyConBinder] -> Kind -> [TyConBinder]
1880 correct_binders binders kind
1881 = binders'
1882 where
1883 (_, binders') = mapAccumR go (tyCoVarsOfType kind) binders
1884
1885 go :: TyCoVarSet -> TyConBinder -> (TyCoVarSet, TyConBinder)
1886 go fvs binder
1887 | isNamedTyConBinder binder
1888 , not (tv `elemVarSet` fvs)
1889 = (new_fvs, mkAnonTyConBinder tv)
1890
1891 | not (isNamedTyConBinder binder)
1892 , tv `elemVarSet` fvs
1893 = (new_fvs, mkNamedTyConBinder Required tv)
1894 -- always Required, because it was anonymous (i.e. visible) previously
1895
1896 | otherwise
1897 = (new_fvs, binder)
1898
1899 where
1900 tv = binderVar binder
1901 new_fvs = fvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv)
1902
1903
1904
1905 -----------------------------------
1906 data DataKindCheck
1907 -- Plain old data type; better be lifted
1908 = LiftedDataKind
1909 -- Data families might have a variable return kind.
1910 -- See See Note [Arity of data families] in FamInstEnv for more info.
1911 | LiftedOrVarDataKind
1912 -- Abstract data in hsig files can have any kind at all;
1913 -- even unlifted. This is because they might not actually
1914 -- be implemented with a data declaration at the end of the day.
1915 | AnyDataKind
1916
1917 tcDataKindSig :: DataKindCheck -- ^ Do we require the result to be *?
1918 -> Kind -> TcM ([TyConBinder], Kind)
1919 -- GADT decls can have a (perhaps partial) kind signature
1920 -- e.g. data T :: * -> * -> * where ...
1921 -- This function makes up suitable (kinded) type variables for
1922 -- the argument kinds, and checks that the result kind is indeed * if requested.
1923 -- (Otherwise, checks to make sure that the result kind is either * or a type variable.)
1924 -- See Note [Arity of data families] in FamInstEnv for more info.
1925 -- We use it also to make up argument type variables for for data instances.
1926 -- Never emits constraints.
1927 -- Returns the new TyVars, the extracted TyBinders, and the new, reduced
1928 -- result kind (which should always be Type or a synonym thereof)
1929 tcDataKindSig kind_check kind
1930 = do { case kind_check of
1931 LiftedDataKind ->
1932 checkTc (isLiftedTypeKind res_kind)
1933 (badKindSig True kind)
1934 LiftedOrVarDataKind ->
1935 checkTc (isLiftedTypeKind res_kind || isJust (tcGetCastedTyVar_maybe res_kind))
1936 (badKindSig False kind)
1937 AnyDataKind -> return ()
1938 ; span <- getSrcSpanM
1939 ; us <- newUniqueSupply
1940 ; rdr_env <- getLocalRdrEnv
1941 ; let uniqs = uniqsFromSupply us
1942 occs = [ occ | str <- allNameStrings
1943 , let occ = mkOccName tvName str
1944 , isNothing (lookupLocalRdrOcc rdr_env occ) ]
1945 -- Note [Avoid name clashes for associated data types]
1946
1947 -- NB: Use the tv from a binder if there is one. Otherwise,
1948 -- we end up inventing a new Unique for it, and any other tv
1949 -- that mentions the first ends up with the wrong kind.
1950 extra_bndrs = zipWith4 mkTyBinderTyConBinder
1951 tv_bndrs (repeat span) uniqs occs
1952
1953 ; return (extra_bndrs, res_kind) }
1954 where
1955 (tv_bndrs, res_kind) = splitPiTys kind
1956
1957 badKindSig :: Bool -> Kind -> SDoc
1958 badKindSig check_for_type kind
1959 = hang (sep [ text "Kind signature on data type declaration has non-*"
1960 , (if check_for_type then empty else text "and non-variable") <+>
1961 text "return kind" ])
1962 2 (ppr kind)
1963
1964 {-
1965 Note [Avoid name clashes for associated data types]
1966 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1967 Consider class C a b where
1968 data D b :: * -> *
1969 When typechecking the decl for D, we'll invent an extra type variable
1970 for D, to fill out its kind. Ideally we don't want this type variable
1971 to be 'a', because when pretty printing we'll get
1972 class C a b where
1973 data D b a0
1974 (NB: the tidying happens in the conversion to IfaceSyn, which happens
1975 as part of pretty-printing a TyThing.)
1976
1977 That's why we look in the LocalRdrEnv to see what's in scope. This is
1978 important only to get nice-looking output when doing ":info C" in GHCi.
1979 It isn't essential for correctness.
1980
1981
1982 ************************************************************************
1983 * *
1984 Partial signatures
1985 * *
1986 ************************************************************************
1987
1988 -}
1989
1990 tcHsPartialSigType
1991 :: UserTypeCtxt
1992 -> LHsSigWcType GhcRn -- The type signature
1993 -> TcM ( [(Name, TcTyVar)] -- Wildcards
1994 , Maybe TcTyVar -- Extra-constraints wildcard
1995 , [TcTyVar] -- Implicitly and explicitly bound type variables
1996 , TcThetaType -- Theta part
1997 , TcType ) -- Tau part
1998 tcHsPartialSigType ctxt sig_ty
1999 | HsWC { hswc_wcs = sig_wcs, hswc_body = ib_ty } <- sig_ty
2000 , HsIB { hsib_vars = implicit_hs_tvs, hsib_body = hs_ty } <- ib_ty
2001 , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
2002 = addSigCtxt ctxt hs_ty $
2003 do { (implicit_tvs, (wcs, wcx, explicit_tvs, theta, tau))
2004 <- tcWildCardBindersX newWildTyVar sig_wcs $ \ wcs ->
2005 tcImplicitTKBndrsX new_implicit_tv implicit_hs_tvs $
2006 tcExplicitTKBndrsX newSigTyVar explicit_hs_tvs $ \ explicit_tvs ->
2007 -- Why newSigTyVar? See TcBinds
2008 -- Note [Quantified variables in partial type signatures]
2009 do { -- Instantiate the type-class context; but if there
2010 -- is an extra-constraints wildcard, just discard it here
2011 (theta, wcx) <- tcPartialContext hs_ctxt
2012
2013 ; tau <- tcHsOpenType hs_tau
2014
2015 ; let bound_tvs = unionVarSets [ allBoundVariables tau
2016 , mkVarSet explicit_tvs
2017 , mkVarSet (map snd wcs) ]
2018
2019 ; return ( (wcs, wcx, explicit_tvs, theta, tau)
2020 , bound_tvs) }
2021
2022 -- Spit out the wildcards (including the extra-constraints one)
2023 -- as "hole" constraints, so that they'll be reported if necessary
2024 -- See Note [Extra-constraint holes in partial type signatures]
2025 ; emitWildCardHoleConstraints wcs
2026
2027 ; explicit_tvs <- mapM zonkTyCoVarKind explicit_tvs
2028 ; let all_tvs = implicit_tvs ++ explicit_tvs
2029 -- The implicit_tvs already have zonked kinds
2030
2031 ; theta <- mapM zonkTcType theta
2032 ; tau <- zonkTcType tau
2033 ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
2034
2035 ; traceTc "tcHsPartialSigType" (ppr all_tvs)
2036 ; return (wcs, wcx, all_tvs, theta, tau) }
2037 where
2038 new_implicit_tv name
2039 = do { kind <- newMetaKindVar
2040 ; tv <- newSigTyVar name kind
2041 -- Why newSigTyVar? See TcBinds
2042 -- Note [Quantified variables in partial type signatures]
2043 ; return (tv, False) }
2044
2045 tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcTyVar)
2046 tcPartialContext hs_theta
2047 | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
2048 , L _ (HsWildCardTy wc) <- ignoreParens hs_ctxt_last
2049 = do { wc_tv <- tcWildCardOcc wc constraintKind
2050 ; theta <- mapM tcLHsPredType hs_theta1
2051 ; return (theta, Just wc_tv) }
2052 | otherwise
2053 = do { theta <- mapM tcLHsPredType hs_theta
2054 ; return (theta, Nothing) }
2055
2056 {- Note [Extra-constraint holes in partial type signatures]
2057 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2058 Consider
2059 f :: (_) => a -> a
2060 f x = ...
2061
2062 * The renamer makes a wildcard name for the "_", and puts it in
2063 the hswc_wcs field.
2064
2065 * Then, in tcHsPartialSigType, we make a new hole TcTyVar, in
2066 tcWildCardBindersX.
2067
2068 * TcBinds.chooseInferredQuantifiers fills in that hole TcTyVar
2069 with the inferred constraints, e.g. (Eq a, Show a)
2070
2071 * TcErrors.mkHoleError finally reports the error.
2072
2073 An annoying difficulty happens if there are more than 62 inferred
2074 constraints. Then we need to fill in the TcTyVar with (say) a 70-tuple.
2075 Where do we find the TyCon? For good reasons we only have constraint
2076 tuples up to 62 (see Note [How tuples work] in TysWiredIn). So how
2077 can we make a 70-tuple? This was the root cause of Trac #14217.
2078
2079 It's incredibly tiresome, because we only need this type to fill
2080 in the hole, to communicate to the error reporting machinery. Nothing
2081 more. So I use a HACK:
2082
2083 * I make an /ordinary/ tuple of the constraints, in
2084 TcBinds.chooseInferredQuantifiers. This is ill-kinded because
2085 ordinary tuples can't contain constraints, but it works fine. And for
2086 ordinary tuples we don't have the same limit as for constraint
2087 tuples (which need selectors and an assocated class).
2088
2089 * Because it is ill-kinded, it trips an assert in writeMetaTyVar,
2090 so now I disable the assertion if we are writing a type of
2091 kind Constraint. (That seldom/never normally happens so we aren't
2092 losing much.)
2093
2094 Result works fine, but it may eventually bite us.
2095
2096
2097 ************************************************************************
2098 * *
2099 Pattern signatures (i.e signatures that occur in patterns)
2100 * *
2101 ********************************************************************* -}
2102
2103 tcHsPatSigType :: UserTypeCtxt
2104 -> LHsSigWcType GhcRn -- The type signature
2105 -> TcM ( [(Name, TcTyVar)] -- Wildcards
2106 , [(Name, TcTyVar)] -- The new bit of type environment, binding
2107 -- the scoped type variables
2108 , TcType) -- The type
2109 -- Used for type-checking type signatures in
2110 -- (a) patterns e.g f (x::Int) = e
2111 -- (b) RULE forall bndrs e.g. forall (x::Int). f x = x
2112 --
2113 -- This may emit constraints
2114
2115 tcHsPatSigType ctxt sig_ty
2116 | HsWC { hswc_wcs = sig_wcs, hswc_body = ib_ty } <- sig_ty
2117 , HsIB { hsib_vars = sig_vars, hsib_body = hs_ty } <- ib_ty
2118 = addSigCtxt ctxt hs_ty $
2119 do { (implicit_tvs, (wcs, sig_ty))
2120 <- tcWildCardBindersX newWildTyVar sig_wcs $ \ wcs ->
2121 tcImplicitTKBndrsX new_implicit_tv sig_vars $
2122 do { sig_ty <- tcHsOpenType hs_ty
2123 ; return ((wcs, sig_ty), allBoundVariables sig_ty) }
2124
2125 ; emitWildCardHoleConstraints wcs
2126
2127 ; sig_ty <- zonkTcType sig_ty
2128 ; checkValidType ctxt sig_ty
2129
2130 ; tv_pairs <- mapM mk_tv_pair implicit_tvs
2131
2132 ; traceTc "tcHsPatSigType" (ppr sig_vars)
2133 ; return (wcs, tv_pairs, sig_ty) }
2134 where
2135 new_implicit_tv name = do { kind <- newMetaKindVar
2136 ; tv <- new_tv name kind
2137 ; return (tv, False) }
2138 -- "False" means that these tyvars aren't yet in scope
2139 new_tv = case ctxt of
2140 RuleSigCtxt {} -> newSkolemTyVar
2141 _ -> newSigTyVar
2142 -- See Note [Pattern signature binders]
2143 -- See Note [Unifying SigTvs]
2144
2145 mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv
2146 ; return (tyVarName tv, tv') }
2147 -- The Name is one of sig_vars, the lexically scoped name
2148 -- But if it's a SigTyVar, it might have been unified
2149 -- with an existing in-scope skolem, so we must zonk
2150 -- here. See Note [Pattern signature binders]
2151
2152 tcPatSig :: Bool -- True <=> pattern binding
2153 -> LHsSigWcType GhcRn
2154 -> ExpSigmaType
2155 -> TcM (TcType, -- The type to use for "inside" the signature
2156 [(Name,TcTyVar)], -- The new bit of type environment, binding
2157 -- the scoped type variables
2158 [(Name,TcTyVar)], -- The wildcards
2159 HsWrapper) -- Coercion due to unification with actual ty
2160 -- Of shape: res_ty ~ sig_ty
2161 tcPatSig in_pat_bind sig res_ty
2162 = do { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
2163 -- sig_tvs are the type variables free in 'sig',
2164 -- and not already in scope. These are the ones
2165 -- that should be brought into scope
2166
2167 ; if null sig_tvs then do {
2168 -- Just do the subsumption check and return
2169 wrap <- addErrCtxtM (mk_msg sig_ty) $
2170 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
2171 ; return (sig_ty, [], sig_wcs, wrap)
2172 } else do
2173 -- Type signature binds at least one scoped type variable
2174
2175 -- A pattern binding cannot bind scoped type variables
2176 -- It is more convenient to make the test here
2177 -- than in the renamer
2178 { when in_pat_bind (addErr (patBindSigErr sig_tvs))
2179
2180 -- Check that all newly-in-scope tyvars are in fact
2181 -- constrained by the pattern. This catches tiresome
2182 -- cases like
2183 -- type T a = Int
2184 -- f :: Int -> Int
2185 -- f (x :: T a) = ...
2186 -- Here 'a' doesn't get a binding. Sigh
2187 ; let bad_tvs = [ tv | (_,tv) <- sig_tvs
2188 , not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ]
2189 ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
2190
2191 -- Now do a subsumption check of the pattern signature against res_ty
2192 ; wrap <- addErrCtxtM (mk_msg sig_ty) $
2193 tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty
2194
2195 -- Phew!
2196 ; return (sig_ty, sig_tvs, sig_wcs, wrap)
2197 } }
2198 where
2199 mk_msg sig_ty tidy_env
2200 = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
2201 ; res_ty <- readExpType res_ty -- should be filled in by now
2202 ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
2203 ; let msg = vcat [ hang (text "When checking that the pattern signature:")
2204 4 (ppr sig_ty)
2205 , nest 2 (hang (text "fits the type of its context:")
2206 2 (ppr res_ty)) ]
2207 ; return (tidy_env, msg) }
2208
2209 patBindSigErr :: [(Name,TcTyVar)] -> SDoc
2210 patBindSigErr sig_tvs
2211 = hang (text "You cannot bind scoped type variable" <> plural sig_tvs
2212 <+> pprQuotedList (map fst sig_tvs))
2213 2 (text "in a pattern binding signature")
2214
2215 {- Note [Pattern signature binders]
2216 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2217 Consider
2218 data T = forall a. T a (a->Int)
2219 f (T x (f :: b->Int)) = blah
2220
2221 Here
2222 * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk',
2223 It must be a skolem so that that it retains its identity, and
2224 TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
2225
2226 * The type signature pattern (f :: b->Int) makes a fresh meta-tyvar b_sig
2227 (a SigTv), and binds "b" :-> b_sig in the envt
2228
2229 * Then unification makes b_sig := a_sk
2230 That's why we must make b_sig a MetaTv (albeit a SigTv),
2231 not a SkolemTv, so that it can unify to a_sk.
2232
2233 * Finally, in 'blah' we must have the envt "b" :-> a_sk. The pair
2234 ("b" :-> a_sk) is returned by tcHsPatSigType, constructed by
2235 mk_tv_pair in that function.
2236
2237 Another example (Trac #13881):
2238 fl :: forall (l :: [a]). Sing l -> Sing l
2239 fl (SNil :: Sing (l :: [y])) = SNil
2240 When we reach the pattern signature, 'l' is in scope from the
2241 outer 'forall':
2242 "a" :-> a_sk :: *
2243 "l" :-> l_sk :: [a_sk]
2244 We make up a fresh meta-SigTv, y_sig, for 'y', and kind-check
2245 the pattern signature
2246 Sing (l :: [y])
2247 That unifies y_sig := a_sk. We return from tcHsPatSigType with
2248 the pair ("y" :-> a_sk).
2249
2250 For RULE binders, though, things are a bit different (yuk).
2251 RULE "foo" forall (x::a) (y::[a]). f x y = ...
2252 Here this really is the binding site of the type variable so we'd like
2253 to use a skolem, so that we get a complaint if we unify two of them
2254 together.
2255
2256 Note [Unifying SigTvs]
2257 ~~~~~~~~~~~~~~~~~~~~~~
2258 ALAS we have no decent way of avoiding two SigTvs getting unified.
2259 Consider
2260 f (x::(a,b)) (y::c)) = [fst x, y]
2261 Here we'd really like to complain that 'a' and 'c' are unified. But
2262 for the reasons above we can't make a,b,c into skolems, so they
2263 are just SigTvs that can unify. And indeed, this would be ok,
2264 f x (y::c) = case x of
2265 (x1 :: a1, True) -> [x,y]
2266 (x1 :: a2, False) -> [x,y,y]
2267 Here the type of x's first component is called 'a1' in one branch and
2268 'a2' in the other. We could try insisting on the same OccName, but
2269 they definitely won't have the sane lexical Name.
2270
2271 I think we could solve this by recording in a SigTv a list of all the
2272 in-scope variables that it should not unify with, but it's fiddly.
2273
2274
2275 ************************************************************************
2276 * *
2277 Checking kinds
2278 * *
2279 ************************************************************************
2280
2281 -}
2282
2283 unifyKinds :: [LHsType GhcRn] -> [(TcType, TcKind)] -> TcM ([TcType], TcKind)
2284 unifyKinds rn_tys act_kinds
2285 = do { kind <- newMetaKindVar
2286 ; let check rn_ty (ty, act_kind) = checkExpectedKind (unLoc rn_ty) ty act_kind kind
2287 ; tys' <- zipWithM check rn_tys act_kinds
2288 ; return (tys', kind) }
2289
2290 {-
2291 ************************************************************************
2292 * *
2293 Sort checking kinds
2294 * *
2295 ************************************************************************
2296
2297 tcLHsKindSig converts a user-written kind to an internal, sort-checked kind.
2298 It does sort checking and desugaring at the same time, in one single pass.
2299 -}
2300
2301 tcLHsKindSig :: LHsKind GhcRn -> TcM Kind
2302 tcLHsKindSig hs_kind
2303 = do { kind <- tc_lhs_kind kindLevelMode hs_kind
2304 ; zonkTcType kind }
2305 -- This zonk is very important in the case of higher rank kinds
2306 -- E.g. Trac #13879 f :: forall (p :: forall z (y::z). <blah>).
2307 -- <more blah>
2308 -- When instantiating p's kind at occurrences of p in <more blah>
2309 -- it's crucial that the kind we instantiate is fully zonked,
2310 -- else we may fail to substitute properly
2311
2312 tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind
2313 tc_lhs_kind mode k
2314 = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $
2315 tc_lhs_type (kindLevel mode) k liftedTypeKind
2316
2317 promotionErr :: Name -> PromotionErr -> TcM a
2318 promotionErr name err
2319 = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here")
2320 2 (parens reason))
2321 where
2322 reason = case err of
2323 FamDataConPE -> text "it comes from a data family instance"
2324 NoDataKindsTC -> text "Perhaps you intended to use DataKinds"
2325 NoDataKindsDC -> text "Perhaps you intended to use DataKinds"
2326 NoTypeInTypeTC -> text "Perhaps you intended to use TypeInType"
2327 NoTypeInTypeDC -> text "Perhaps you intended to use TypeInType"
2328 PatSynPE -> text "Pattern synonyms cannot be promoted"
2329 _ -> text "it is defined and used in the same recursive group"
2330
2331 {-
2332 ************************************************************************
2333 * *
2334 Scoped type variables
2335 * *
2336 ************************************************************************
2337 -}
2338
2339 badPatSigTvs :: TcType -> [TyVar] -> SDoc
2340 badPatSigTvs sig_ty bad_tvs
2341 = vcat [ fsep [text "The type variable" <> plural bad_tvs,
2342 quotes (pprWithCommas ppr bad_tvs),
2343 text "should be bound by the pattern signature" <+> quotes (ppr sig_ty),
2344 text "but are actually discarded by a type synonym" ]
2345 , text "To fix this, expand the type synonym"
2346 , text "[Note: I hope to lift this restriction in due course]" ]
2347
2348 {-
2349 ************************************************************************
2350 * *
2351 Error messages and such
2352 * *
2353 ************************************************************************
2354 -}
2355
2356 -- | Make an appropriate message for an error in a function argument.
2357 -- Used for both expressions and types.
2358 funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
2359 funAppCtxt fun arg arg_no
2360 = hang (hsep [ text "In the", speakNth arg_no, ptext (sLit "argument of"),
2361 quotes (ppr fun) <> text ", namely"])
2362 2 (quotes (ppr arg))
2363
2364 -- See Note [Free-floating kind vars]
2365 reportFloatingKvs :: Name -- of the tycon
2366 -> TyConFlavour -- What sort of TyCon it is
2367 -> [TcTyVar] -- all tyvars, not necessarily zonked
2368 -> [TcTyVar] -- floating tyvars
2369 -> TcM ()
2370 reportFloatingKvs tycon_name flav all_tvs bad_tvs
2371 = unless (null bad_tvs) $ -- don't bother zonking if there's no error
2372 do { all_tvs <- mapM zonkTcTyVarToTyVar all_tvs
2373 ; bad_tvs <- mapM zonkTcTyVarToTyVar bad_tvs
2374 ; let (tidy_env, tidy_all_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
2375 tidy_bad_tvs = map (tidyTyVarOcc tidy_env) bad_tvs
2376 ; typeintype <- xoptM LangExt.TypeInType
2377 ; mapM_ (report typeintype tidy_all_tvs) tidy_bad_tvs }
2378 where
2379 report typeintype tidy_all_tvs tidy_bad_tv
2380 = addErr $
2381 vcat [ text "Kind variable" <+> quotes (ppr tidy_bad_tv) <+>
2382 text "is implicitly bound in" <+> ppr flav
2383 , quotes (ppr tycon_name) <> comma <+>
2384 text "but does not appear as the kind of any"
2385 , text "of its type variables. Perhaps you meant"
2386 , text "to bind it" <+> ppWhen (not typeintype)
2387 (text "(with TypeInType)") <+>
2388 text "explicitly somewhere?"
2389 , ppWhen (not (null tidy_all_tvs)) $
2390 hang (text "Type variables with inferred kinds:")
2391 2 (ppr_tv_bndrs tidy_all_tvs) ]
2392
2393 ppr_tv_bndrs tvs = sep (map pp_tv tvs)
2394 pp_tv tv = parens (ppr tv <+> dcolon <+> ppr (tyVarKind tv))