2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
7 module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta,
11 kcHsTyVar, kcHsTyVars, mkTyClTyVars,
12 kcHsType, kcHsSigType, kcHsSigTypes,
13 kcHsLiftedSigType, kcHsContext,
14 tcAddScopedTyVars, tcHsTyVars, mkImmutTyVars,
16 TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
17 checkSigTyVars, sigCtxt, sigPatCtxt
20 #include "HsVersions.h"
22 import HsSyn ( HsType(..), HsTyVarBndr(..),
23 Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
24 import RnHsSyn ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars )
25 import TcHsSyn ( TcId )
28 import TcEnv ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
29 tcGetGlobalTyVars, tcLEnvElts, tcInLocalScope,
30 TyThing(..), TcTyThing(..), tcExtendKindEnv
32 import TcMType ( newKindVar, tcInstSigTyVars,
33 zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar,
34 unifyKind, unifyOpenTypeKind,
35 checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
37 import TcType ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
38 TcTyVar, TcTyVarSet, TcKind, TcThetaType, TcTauType,
39 mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
40 tcSplitForAllTys, tcSplitRhoTy,
41 hoistForAllTys, allDistinctTyVars, zipFunTys,
42 mkSigmaTy, mkPredTy, mkTyConApp, mkAppTys, mkRhoTy,
43 liftedTypeKind, unliftedTypeKind, mkArrowKind,
44 mkArrowKinds, tcGetTyVar_maybe, tcGetTyVar, tcSplitFunTy_maybe,
45 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
46 tyVarsOfType, mkForAllTys
48 import qualified Type ( getTyVar_maybe )
50 import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
51 import PprType ( pprType )
52 import Subst ( mkTopTyVarSubst, substTy )
53 import CoreFVs ( idFreeTyVars )
54 import Id ( mkLocalId, idName, idType )
55 import Var ( Var, TyVar, mkTyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
58 import ErrUtils ( Message )
59 import TyCon ( TyCon, isSynTyCon, tyConKind )
60 import Class ( classTyCon )
61 import Name ( Name, getSrcLoc )
63 import TysWiredIn ( mkListTy, mkTupleTy, genUnitTyCon )
64 import BasicTypes ( Boxity(..) )
65 import SrcLoc ( SrcLoc )
66 import Util ( isSingleton, lengthIs )
72 %************************************************************************
74 \subsection{Checking types}
76 %************************************************************************
78 Generally speaking we now type-check types in three phases
80 1. Kind check the HsType [kcHsType]
81 2. Convert from HsType to Type, and hoist the foralls [tcHsType]
82 3. Check the validity of the resulting type [checkValidType]
84 Often these steps are done one after the othe (tcHsSigType).
85 But in mutually recursive groups of type and class decls we do
86 1 kind-check the whole group
87 2 build TyCons/Classes in a knot-tied wa
88 3 check the validity of types in the now-unknotted TyCons/Classes
91 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
92 -- Do kind checking, and hoist for-alls to the top
93 tcHsSigType ctxt ty = tcAddErrCtxt (checkTypeCtxt ctxt ty) (
94 kcTypeType ty `thenTc_`
97 checkValidType ctxt ty' `thenTc_`
100 checkTypeCtxt ctxt ty
101 = vcat [ptext SLIT("In the type:") <+> ppr ty,
102 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
104 tcHsType :: RenamedHsType -> TcM Type
105 -- Don't do kind checking, nor validity checking,
106 -- but do hoist for-alls to the top
107 -- This is used in type and class decls, where kinding is
108 -- done in advance, and validity checking is done later
109 -- [Validity checking done later because of knot-tying issues.]
110 tcHsType ty = tc_type ty `thenTc` \ ty' ->
111 returnTc (hoistForAllTys ty')
113 tcHsTheta :: RenamedContext -> TcM ThetaType
114 -- Used when we are expecting a ClassContext (i.e. no implicit params)
115 -- Does not do validity checking, like tcHsType
116 tcHsTheta hs_theta = mapTc tc_pred hs_theta
118 -- In interface files the type is already kinded,
119 -- and we definitely don't want to hoist for-alls.
120 -- Otherwise we'll change
121 -- dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
123 -- dmfail :: forall m:(*->*) a:* Monad m => String -> m a
124 -- which definitely isn't right!
125 tcIfaceType ty = tc_type ty
129 %************************************************************************
131 \subsection{Kind checking}
133 %************************************************************************
137 When we come across the binding site for some type variables, we
138 proceed in two stages
140 1. Figure out what kind each tyvar has
142 2. Create suitably-kinded tyvars,
144 and typecheck the body
146 To do step 1, we proceed thus:
148 1a. Bind each type variable to a kind variable
149 1b. Apply the kind checker
150 1c. Zonk the resulting kinds
152 The kind checker is passed to tcHsTyVars as an argument.
154 For example, when we find
155 (forall a m. m a -> m a)
156 we bind a,m to kind varibles and kind-check (m a -> m a). This
157 makes a get kind *, and m get kind *->*. Now we typecheck (m a -> m a)
158 in an environment that binds a and m suitably.
160 The kind checker passed to tcHsTyVars needs to look at enough to
161 establish the kind of the tyvar:
162 * For a group of type and class decls, it's just the group, not
163 the rest of the program
164 * For a tyvar bound in a pattern type signature, its the types
165 mentioned in the other type signatures in that bunch of patterns
166 * For a tyvar bound in a RULE, it's the type signatures on other
167 universally quantified variables in the rule
169 Note that this may occasionally give surprising results. For example:
171 data T a b = MkT (a b)
173 Here we deduce a::*->*, b::*.
174 But equally valid would be
175 a::(*->*)-> *, b::*->*
178 -- tcHsTyVars is used for type variables in type signatures
179 -- e.g. forall a. a->a
180 -- They are immutable, because they scope only over the signature
181 -- They may or may not be explicitly-kinded
182 tcHsTyVars :: [HsTyVarBndr Name]
183 -> TcM a -- The kind checker
184 -> ([TyVar] -> TcM b)
187 tcHsTyVars [] kind_check thing_inside = thing_inside []
188 -- A useful short cut for a common case!
190 tcHsTyVars tv_names kind_check thing_inside
191 = kcHsTyVars tv_names `thenNF_Tc` \ tv_names_w_kinds ->
192 tcExtendKindEnv tv_names_w_kinds kind_check `thenTc_`
193 zonkKindEnv tv_names_w_kinds `thenNF_Tc` \ tvs_w_kinds ->
195 tyvars = mkImmutTyVars tvs_w_kinds
197 tcExtendTyVarEnv tyvars (thing_inside tyvars)
201 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
202 -- tcAddScopedTyVars is used for scoped type variables
203 -- added by pattern type signatures
204 -- e.g. \ (x::a) (y::a) -> x+y
205 -- They never have explicit kinds (because this is source-code only)
206 -- They are mutable (because they can get bound to a more specific type)
208 -- Find the not-already-in-scope signature type variables,
209 -- kind-check them, and bring them into scope
211 -- We no longer specify that these type variables must be univerally
212 -- quantified (lots of email on the subject). If you want to put that
213 -- back in, you need to
214 -- a) Do a checkSigTyVars after thing_inside
215 -- b) More insidiously, don't pass in expected_ty, else
216 -- we unify with it too early and checkSigTyVars barfs
217 -- Instead you have to pass in a fresh ty var, and unify
218 -- it with expected_ty afterwards
219 tcAddScopedTyVars [] thing_inside
220 = thing_inside -- Quick get-out for the empty case
222 tcAddScopedTyVars sig_tys thing_inside
223 = tcGetEnv `thenNF_Tc` \ env ->
225 all_sig_tvs = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
226 sig_tvs = filter not_in_scope (nameSetToList all_sig_tvs)
227 not_in_scope tv = not (tcInLocalScope env tv)
229 mapNF_Tc newNamedKindVar sig_tvs `thenTc` \ kind_env ->
230 tcExtendKindEnv kind_env (kcHsSigTypes sig_tys) `thenTc_`
231 zonkKindEnv kind_env `thenNF_Tc` \ tvs_w_kinds ->
232 listTc [ tcNewMutTyVar name kind PatSigTv
233 | (name, kind) <- tvs_w_kinds] `thenNF_Tc` \ tyvars ->
234 tcExtendTyVarEnv tyvars thing_inside
239 kcHsTyVar :: HsTyVarBndr name -> NF_TcM (name, TcKind)
240 kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
242 kcHsTyVar (UserTyVar name) = newNamedKindVar name
243 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
245 kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
247 newNamedKindVar name = newKindVar `thenNF_Tc` \ kind ->
248 returnNF_Tc (name, kind)
250 ---------------------------
251 kcLiftedType :: RenamedHsType -> TcM ()
252 -- The type ty must be a *lifted* *type*
254 = kcHsType ty `thenTc` \ kind ->
255 tcAddErrCtxt (typeKindCtxt ty) $
256 unifyKind liftedTypeKind kind
258 ---------------------------
259 kcTypeType :: RenamedHsType -> TcM ()
260 -- The type ty must be a *type*, but it can be lifted or unlifted.
262 = kcHsType ty `thenTc` \ kind ->
263 tcAddErrCtxt (typeKindCtxt ty) $
264 unifyOpenTypeKind kind
266 ---------------------------
267 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
268 -- Used for type signatures
269 kcHsSigType = kcTypeType
270 kcHsSigTypes tys = mapTc_ kcHsSigType tys
271 kcHsLiftedSigType = kcLiftedType
273 ---------------------------
274 kcHsType :: RenamedHsType -> TcM TcKind
275 kcHsType (HsTyVar name) = kcTyVar name
277 kcHsType (HsListTy ty)
278 = kcLiftedType ty `thenTc` \ tau_ty ->
279 returnTc liftedTypeKind
281 kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
282 = mapTc kcTypeType tys `thenTc_`
283 returnTc (case boxity of
284 Boxed -> liftedTypeKind
285 Unboxed -> unliftedTypeKind)
287 kcHsType (HsFunTy ty1 ty2)
288 = kcTypeType ty1 `thenTc_`
289 kcTypeType ty2 `thenTc_`
290 returnTc liftedTypeKind
292 kcHsType (HsNumTy _) -- The unit type for generics
293 = returnTc liftedTypeKind
295 kcHsType ty@(HsOpTy ty1 op ty2)
296 = kcTyVar op `thenTc` \ op_kind ->
297 kcHsType ty1 `thenTc` \ ty1_kind ->
298 kcHsType ty2 `thenTc` \ ty2_kind ->
299 tcAddErrCtxt (appKindCtxt (ppr ty)) $
300 kcAppKind op_kind ty1_kind `thenTc` \ op_kind' ->
301 kcAppKind op_kind' ty2_kind
303 kcHsType (HsPredTy pred)
304 = kcHsPred pred `thenTc_`
305 returnTc liftedTypeKind
307 kcHsType ty@(HsAppTy ty1 ty2)
308 = kcHsType ty1 `thenTc` \ tc_kind ->
309 kcHsType ty2 `thenTc` \ arg_kind ->
310 tcAddErrCtxt (appKindCtxt (ppr ty)) $
311 kcAppKind tc_kind arg_kind
313 kcHsType (HsForAllTy (Just tv_names) context ty)
314 = kcHsTyVars tv_names `thenNF_Tc` \ kind_env ->
315 tcExtendKindEnv kind_env $
316 kcHsContext context `thenTc_`
317 kcHsType ty `thenTc_`
318 returnTc liftedTypeKind
320 ---------------------------
321 kcAppKind fun_kind arg_kind
322 = case tcSplitFunTy_maybe fun_kind of
323 Just (arg_kind', res_kind)
324 -> unifyKind arg_kind arg_kind' `thenTc_`
327 Nothing -> newKindVar `thenNF_Tc` \ res_kind ->
328 unifyKind fun_kind (mkArrowKind arg_kind res_kind) `thenTc_`
332 ---------------------------
333 kcHsContext ctxt = mapTc_ kcHsPred ctxt
335 kcHsPred :: RenamedHsPred -> TcM ()
336 kcHsPred pred@(HsIParam name ty)
337 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
340 kcHsPred pred@(HsClassP cls tys)
341 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
342 kcClass cls `thenTc` \ kind ->
343 mapTc kcHsType tys `thenTc` \ arg_kinds ->
344 unifyKind kind (mkArrowKinds arg_kinds liftedTypeKind)
346 ---------------------------
347 kcTyVar name -- Could be a tyvar or a tycon
348 = tcLookup name `thenTc` \ thing ->
350 AThing kind -> returnTc kind
351 ATyVar tv -> returnTc (tyVarKind tv)
352 AGlobal (ATyCon tc) -> returnTc (tyConKind tc)
353 other -> failWithTc (wrongThingErr "type" thing name)
355 kcClass cls -- Must be a class
356 = tcLookup cls `thenNF_Tc` \ thing ->
358 AThing kind -> returnTc kind
359 AGlobal (AClass cls) -> returnTc (tyConKind (classTyCon cls))
360 other -> failWithTc (wrongThingErr "class" thing cls)
363 %************************************************************************
367 %************************************************************************
369 tc_type, the main work horse
370 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
376 tc_type is used to typecheck the types in the RHS of data
377 constructors. In the case of recursive data types, that means that
378 the type constructors themselves are (partly) black holes. e.g.
380 data T a = MkT a [T a]
382 While typechecking the [T a] on the RHS, T itself is not yet fully
383 defined. That in turn places restrictions on what you can check in
384 tcHsType; if you poke on too much you get a black hole. I keep
385 forgetting this, hence this warning!
387 So tc_type does no validity-checking. Instead that's all done
388 by TcMType.checkValidType
390 --------------------------
391 *** END OF BIG WARNING ***
392 --------------------------
396 tc_type :: RenamedHsType -> TcM Type
398 tc_type ty@(HsTyVar name)
401 tc_type (HsListTy ty)
402 = tc_type ty `thenTc` \ tau_ty ->
403 returnTc (mkListTy tau_ty)
405 tc_type (HsTupleTy (HsTupCon _ boxity arity) tys)
406 = ASSERT( tys `lengthIs` arity )
407 tc_types tys `thenTc` \ tau_tys ->
408 returnTc (mkTupleTy boxity arity tau_tys)
410 tc_type (HsFunTy ty1 ty2)
411 = tc_type ty1 `thenTc` \ tau_ty1 ->
412 tc_type ty2 `thenTc` \ tau_ty2 ->
413 returnTc (mkFunTy tau_ty1 tau_ty2)
417 returnTc (mkTyConApp genUnitTyCon [])
419 tc_type (HsOpTy ty1 op ty2)
420 = tc_type ty1 `thenTc` \ tau_ty1 ->
421 tc_type ty2 `thenTc` \ tau_ty2 ->
422 tc_fun_type op [tau_ty1,tau_ty2]
424 tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
426 tc_type (HsPredTy pred)
427 = tc_pred pred `thenTc` \ pred' ->
428 returnTc (mkPredTy pred')
430 tc_type full_ty@(HsForAllTy (Just tv_names) ctxt ty)
432 kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
434 tcHsTyVars tv_names kind_check $ \ tyvars ->
435 mapTc tc_pred ctxt `thenTc` \ theta ->
436 tc_type ty `thenTc` \ tau ->
437 returnTc (mkSigmaTy tyvars theta tau)
439 tc_types arg_tys = mapTc tc_type arg_tys
442 Help functions for type applications
443 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
446 tc_app :: RenamedHsType -> [RenamedHsType] -> TcM Type
447 tc_app (HsAppTy ty1 ty2) tys
448 = tc_app ty1 (ty2:tys)
451 = tcAddErrCtxt (appKindCtxt pp_app) $
452 tc_types tys `thenTc` \ arg_tys ->
454 HsTyVar fun -> tc_fun_type fun arg_tys
455 other -> tc_type ty `thenTc` \ fun_ty ->
456 returnNF_Tc (mkAppTys fun_ty arg_tys)
458 pp_app = ppr ty <+> sep (map pprParendHsType tys)
460 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
461 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
462 -- hence the rather strange functionality.
464 tc_fun_type name arg_tys
465 = tcLookup name `thenTc` \ thing ->
467 ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
470 | isSynTyCon tc -> returnTc (mkSynTy tc arg_tys)
471 | otherwise -> returnTc (mkTyConApp tc arg_tys)
473 other -> failWithTc (wrongThingErr "type constructor" thing name)
480 tc_pred assn@(HsClassP class_name tys)
481 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
482 tc_types tys `thenTc` \ arg_tys ->
483 tcLookupGlobal class_name `thenTc` \ thing ->
485 AClass clas -> returnTc (ClassP clas arg_tys)
486 other -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
488 tc_pred assn@(HsIParam name ty)
489 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
490 tc_type ty `thenTc` \ arg_ty ->
491 returnTc (IParam name arg_ty)
496 %************************************************************************
498 \subsection{Type variables, with knot tying!}
500 %************************************************************************
503 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
504 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
506 mkTyClTyVars :: Kind -- Kind of the tycon or class
507 -> [HsTyVarBndr Name]
509 mkTyClTyVars kind tyvar_names
510 = mkImmutTyVars tyvars_w_kinds
512 (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
516 %************************************************************************
518 \subsection{Signatures}
520 %************************************************************************
522 @tcSigs@ checks the signatures for validity, and returns a list of
523 {\em freshly-instantiated} signatures. That is, the types are already
524 split up, and have fresh type variables installed. All non-type-signature
525 "RenamedSigs" are ignored.
527 The @TcSigInfo@ contains @TcTypes@ because they are unified with
528 the variable's type, and after that checked to see whether they've
534 Name -- N, the Name in corresponding binding
536 TcId -- *Polymorphic* binder for this value...
543 TcId -- *Monomorphic* binder for this value
544 -- Does *not* have name = N
547 [Inst] -- Empty if theta is null, or
548 -- (method mono_id) otherwise
550 SrcLoc -- Of the signature
552 instance Outputable TcSigInfo where
553 ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
554 ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
556 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
557 -- Search for a particular signature
558 maybeSig [] name = Nothing
559 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
560 | name == sig_name = Just sig
561 | otherwise = maybeSig sigs name
566 tcTySig :: RenamedSig -> TcM TcSigInfo
568 tcTySig (Sig v ty src_loc)
569 = tcAddSrcLoc src_loc $
570 tcHsSigType (FunSigCtxt v) ty `thenTc` \ sigma_tc_ty ->
571 mkTcSig (mkLocalId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
574 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
575 mkTcSig poly_id src_loc
576 = -- Instantiate this type
577 -- It's important to do this even though in the error-free case
578 -- we could just split the sigma_tc_ty (since the tyvars don't
579 -- unified with anything). But in the case of an error, when
580 -- the tyvars *do* get unified with something, we want to carry on
581 -- typechecking the rest of the program with the function bound
582 -- to a pristine type, namely sigma_tc_ty
584 (tyvars, rho) = tcSplitForAllTys (idType poly_id)
586 tcInstSigTyVars SigTv tyvars `thenNF_Tc` \ tyvars' ->
587 -- Make *signature* type variables
590 tyvar_tys' = mkTyVarTys tyvars'
591 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
592 -- mkTopTyVarSubst because the tyvars' are fresh
594 (theta', tau') = tcSplitRhoTy rho'
595 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
596 -- wherever possible, which can improve interface files.
598 newMethodWithGivenTy SignatureOrigin
601 theta' tau' `thenNF_Tc` \ inst ->
602 -- We make a Method even if it's not overloaded; no harm
604 returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
606 name = idName poly_id
611 %************************************************************************
613 \subsection{Checking signature type variables}
615 %************************************************************************
617 @checkSigTyVars@ is used after the type in a type signature has been unified with
618 the actual type found. It then checks that the type variables of the type signature
620 (a) Still all type variables
621 eg matching signature [a] against inferred type [(p,q)]
622 [then a will be unified to a non-type variable]
624 (b) Still all distinct
625 eg matching signature [(a,b)] against inferred type [(p,p)]
626 [then a and b will be unified together]
628 (c) Not mentioned in the environment
629 eg the signature for f in this:
635 Here, f is forced to be monorphic by the free occurence of x.
637 (d) Not (unified with another type variable that is) in scope.
638 eg f x :: (r->r) = (\y->y) :: forall a. a->r
639 when checking the expression type signature, we find that
640 even though there is nothing in scope whose type mentions r,
641 nevertheless the type signature for the expression isn't right.
643 Another example is in a class or instance declaration:
645 op :: forall b. a -> b
647 Here, b gets unified with a
649 Before doing this, the substitution is applied to the signature type variable.
651 We used to have the notion of a "DontBind" type variable, which would
652 only be bound to itself or nothing. Then points (a) and (b) were
653 self-checking. But it gave rise to bogus consequential error messages.
656 f = (*) -- Monomorphic
661 Here, we get a complaint when checking the type signature for g,
662 that g isn't polymorphic enough; but then we get another one when
663 dealing with the (Num x) context arising from f's definition;
664 we try to unify x with Int (to default it), but find that x has already
665 been unified with the DontBind variable "a" from g's signature.
666 This is really a problem with side-effecting unification; we'd like to
667 undo g's effects when its type signature fails, but unification is done
668 by side effect, so we can't (easily).
670 So we revert to ordinary type variables for signatures, and try to
671 give a helpful message in checkSigTyVars.
674 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
675 -> TcTyVarSet -- Tyvars that are free in the type signature
676 -- Not necessarily zonked
677 -- These should *already* be in the free-in-env set,
678 -- and are used here only to improve the error message
679 -> TcM [TcTyVar] -- Zonked signature type variables
681 checkSigTyVars [] free = returnTc []
682 checkSigTyVars sig_tyvars free_tyvars
683 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
684 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
686 checkTcM (allDistinctTyVars sig_tys globals)
687 (complain sig_tys globals) `thenTc_`
689 returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
692 complain sig_tys globals
693 = -- "check" checks each sig tyvar in turn
695 (env2, emptyVarEnv, [])
696 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
698 failWithTcM (env3, main_msg $$ vcat msgs)
700 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
701 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
703 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
705 check (tidy_env, acc, msgs) (sig_tyvar,ty)
706 -- sig_tyvar is from the signature;
707 -- ty is what you get if you zonk sig_tyvar and then tidy it
709 -- acc maps a zonked type variable back to a signature type variable
710 = case tcGetTyVar_maybe ty of {
711 Nothing -> -- Error (a)!
712 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
716 case lookupVarEnv acc tv of {
717 Just sig_tyvar' -> -- Error (b)!
718 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
720 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
724 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
725 -- The least comprehensible, so put it last
727 -- a) get the local TcIds and TyVars from the environment,
728 -- and pass them to find_globals (they might have tv free)
729 -- b) similarly, find any free_tyvars that mention tv
730 then tcGetEnv `thenNF_Tc` \ ve ->
731 find_globals tv tidy_env (tcLEnvElts ve) `thenNF_Tc` \ (tidy_env1, globs) ->
732 find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
733 returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
736 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
739 -----------------------
740 -- find_globals looks at the value environment and finds values
741 -- whose types mention the offending type variable. It has to be
742 -- careful to zonk the Id's type first, so it has to be in the monad.
743 -- We must be careful to pass it a zonked type variable, too.
748 -> NF_TcM (TidyEnv, [SDoc])
750 find_globals tv tidy_env things
751 = go tidy_env [] things
753 go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
754 go tidy_env acc (thing : things)
755 = find_thing ignore_it tidy_env thing `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
757 Just d -> go tidy_env1 (d:acc) things
758 Nothing -> go tidy_env1 acc things
760 ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
762 -----------------------
763 find_thing ignore_it tidy_env (ATcId id)
764 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
765 if ignore_it id_ty then
766 returnNF_Tc (tidy_env, Nothing)
768 (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
769 msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
770 nest 2 (parens (ptext SLIT("bound at") <+>
771 ppr (getSrcLoc id)))]
773 returnNF_Tc (tidy_env', Just msg)
775 find_thing ignore_it tidy_env (ATyVar tv)
776 = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
777 if ignore_it tv_ty then
778 returnNF_Tc (tidy_env, Nothing)
780 (tidy_env1, tv1) = tidyOpenTyVar tidy_env tv
781 (tidy_env2, tidy_ty) = tidyOpenType tidy_env1 tv_ty
782 msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
784 eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
785 | otherwise = equals <+> ppr tv_ty
786 -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
788 bound_at | isMutTyVar tv = mut_info -- The expected case
791 mut_info = sep [ptext SLIT("is bound by the") <+> ppr (mutTyVarDetails tv),
792 ptext SLIT("at") <+> ppr (getSrcLoc tv)]
794 returnNF_Tc (tidy_env2, Just msg)
796 -----------------------
797 find_frees tv tidy_env acc []
798 = returnNF_Tc (tidy_env, acc)
799 find_frees tv tidy_env acc (ftv:ftvs)
800 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
801 if tv `elemVarSet` tyVarsOfType ty then
803 (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
805 find_frees tv tidy_env' (ftv':acc) ftvs
807 find_frees tv tidy_env acc ftvs
810 escape_msg sig_tv tv globs frees
811 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
812 if not (null globs) then
813 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
815 else if not (null frees) then
816 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
817 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
820 empty -- Sigh. It's really hard to give a good error message
821 -- all the time. One bad case is an existential pattern match
823 is_are | isSingleton frees = ptext SLIT("is")
824 | otherwise = ptext SLIT("are")
825 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
826 | otherwise = ptext SLIT("It")
828 vcat_first :: Int -> [SDoc] -> SDoc
829 vcat_first n [] = empty
830 vcat_first 0 (x:xs) = text "...others omitted..."
831 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
834 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
835 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
838 These two context are used with checkSigTyVars
841 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
842 -> TidyEnv -> NF_TcM (TidyEnv, Message)
843 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
844 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
846 (env1, tidy_sig_tyvars) = tidyOpenTyVars tidy_env sig_tyvars
847 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
848 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
849 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
850 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
854 returnNF_Tc (env3, msg)
856 sigPatCtxt bound_tvs bound_ids tidy_env
858 sep [ptext SLIT("When checking a pattern that binds"),
859 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
861 show_ids = filter is_interesting bound_ids
862 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
864 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
865 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
866 -- Don't zonk the types so we get the separate, un-unified versions
870 %************************************************************************
872 \subsection{Errors and contexts}
874 %************************************************************************
877 typeKindCtxt :: RenamedHsType -> Message
878 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
879 nest 2 (quotes (ppr ty)),
880 ptext SLIT("is a type")]
882 appKindCtxt :: SDoc -> Message
883 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
885 wrongThingErr expected thing name
886 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
888 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
889 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
890 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
891 pp_thing (ATyVar _) = ptext SLIT("Type variable")
892 pp_thing (ATcId _) = ptext SLIT("Local identifier")
893 pp_thing (AThing _) = ptext SLIT("Utterly bogus")