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