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