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