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