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