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