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 tcScopedTyVars, 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 )
25 import TcHsSyn ( TcId )
28 import TcEnv ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
29 tcGetGlobalTyVars, tcEnvTcIds, tcEnvTyVars,
30 TyThing(..), TcTyThing(..), tcExtendKindEnv
32 import TcMType ( newKindVar, tcInstSigVars,
33 zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar,
34 unifyKind, unifyOpenTypeKind,
35 checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
37 import TcType ( Type, Kind, SourceType(..), ThetaType,
38 mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
39 tcSplitForAllTys, tcSplitRhoTy,
40 hoistForAllTys, allDistinctTyVars,
42 mkSigmaTy, mkPredTy, mkTyConApp,
44 liftedTypeKind, unliftedTypeKind, mkArrowKind,
45 mkArrowKinds, tcGetTyVar_maybe, tcGetTyVar, tcSplitFunTy_maybe,
46 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
47 tyVarsOfType, mkForAllTys
49 import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
50 import PprType ( pprType )
51 import Subst ( mkTopTyVarSubst, substTy )
52 import CoreFVs ( idFreeTyVars )
53 import Id ( mkLocalId, idName, idType )
54 import Var ( Id, Var, TyVar, mkTyVar, tyVarKind )
57 import ErrUtils ( Message )
58 import TyCon ( TyCon, isSynTyCon, tyConArity, tyConKind )
59 import Class ( classTyCon )
61 import TysWiredIn ( mkListTy, mkTupleTy, genUnitTyCon )
62 import BasicTypes ( Boxity(..) )
63 import SrcLoc ( SrcLoc )
64 import Util ( isSingleton )
70 %************************************************************************
72 \subsection{Checking types}
74 %************************************************************************
76 Generally speaking we now type-check types in three phases
78 1. Kind check the HsType [kcHsType]
79 2. Convert from HsType to Type, and hoist the foralls [tcHsType]
80 3. Check the validity of the resultint type [checkValidType]
82 Often these steps are done one after the othe (tcHsSigType).
83 But in mutually recursive groups of type and class decls we do
84 1 kind-check the whole group
85 2 build TyCons/Classes in a knot-tied wa
86 3 check the validity of types in the now-unknotted TyCons/Classes
89 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
90 -- Do kind checking, and hoist for-alls to the top
91 tcHsSigType ctxt ty = tcAddErrCtxt (checkTypeCtxt ctxt ty) (
92 kcTypeType ty `thenTc_`
95 checkValidType ctxt ty' `thenTc_`
99 = vcat [ptext SLIT("In the type:") <+> ppr ty,
100 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
102 tcHsType :: RenamedHsType -> TcM Type
103 -- Don't do kind checking, nor validity checking,
104 -- but do hoist for-alls to the top
105 -- This is used in type and class decls, where kinding is
106 -- done in advance, and validity checking is done later
107 -- [Validity checking done later because of knot-tying issues.]
108 tcHsType ty = tc_type ty `thenTc` \ ty' ->
109 returnTc (hoistForAllTys ty')
111 tcHsTheta :: RenamedContext -> TcM ThetaType
112 -- Used when we are expecting a ClassContext (i.e. no implicit params)
113 -- Does not do validity checking, like tcHsType
114 tcHsTheta hs_theta = mapTc tc_pred hs_theta
116 -- In interface files the type is already kinded,
117 -- and we definitely don't want to hoist for-alls.
118 -- Otherwise we'll change
119 -- dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
121 -- dmfail :: forall m:(*->*) a:* Monad m => String -> m a
122 -- which definitely isn't right!
123 tcIfaceType ty = tc_type ty
127 %************************************************************************
129 \subsection{Kind checking}
131 %************************************************************************
135 When we come across the binding site for some type variables, we
136 proceed in two stages
138 1. Figure out what kind each tyvar has
140 2. Create suitably-kinded tyvars,
142 and typecheck the body
144 To do step 1, we proceed thus:
146 1a. Bind each type variable to a kind variable
147 1b. Apply the kind checker
148 1c. Zonk the resulting kinds
150 The kind checker is passed to tcHsTyVars as an argument.
152 For example, when we find
153 (forall a m. m a -> m a)
154 we bind a,m to kind varibles and kind-check (m a -> m a). This
155 makes a get kind *, and m get kind *->*. Now we typecheck (m a -> m a)
156 in an environment that binds a and m suitably.
158 The kind checker passed to tcHsTyVars needs to look at enough to
159 establish the kind of the tyvar:
160 * For a group of type and class decls, it's just the group, not
161 the rest of the program
162 * For a tyvar bound in a pattern type signature, its the types
163 mentioned in the other type signatures in that bunch of patterns
164 * For a tyvar bound in a RULE, it's the type signatures on other
165 universally quantified variables in the rule
167 Note that this may occasionally give surprising results. For example:
169 data T a b = MkT (a b)
171 Here we deduce a::*->*, b::*.
172 But equally valid would be
173 a::(*->*)-> *, b::*->*
176 -- tcHsTyVars is used for type variables in type signatures
177 -- e.g. forall a. a->a
178 -- They are immutable, because they scope only over the signature
179 -- They may or may not be explicitly-kinded
180 tcHsTyVars :: [HsTyVarBndr Name]
181 -> TcM a -- The kind checker
182 -> ([TyVar] -> TcM b)
185 tcHsTyVars [] kind_check thing_inside = thing_inside []
186 -- A useful short cut for a common case!
188 tcHsTyVars tv_names kind_check thing_inside
189 = kcHsTyVars tv_names `thenNF_Tc` \ tv_names_w_kinds ->
190 tcExtendKindEnv tv_names_w_kinds kind_check `thenTc_`
191 zonkKindEnv tv_names_w_kinds `thenNF_Tc` \ tvs_w_kinds ->
193 tyvars = mkImmutTyVars tvs_w_kinds
195 tcExtendTyVarEnv tyvars (thing_inside tyvars)
197 -- tcScopedTyVars is used for scoped type variables
198 -- e.g. \ (x::a) (y::a) -> x+y
199 -- They never have explicit kinds (because this is source-code only)
200 -- They are mutable (because they can get bound to a more specific type)
201 tcScopedTyVars :: [Name]
202 -> TcM a -- The kind checker
205 tcScopedTyVars [] kind_check thing_inside = thing_inside
207 tcScopedTyVars tv_names kind_check thing_inside
208 = mapNF_Tc newNamedKindVar tv_names `thenTc` \ kind_env ->
209 tcExtendKindEnv kind_env kind_check `thenTc_`
210 zonkKindEnv kind_env `thenNF_Tc` \ tvs_w_kinds ->
211 listTc [tcNewMutTyVar name kind | (name, kind) <- tvs_w_kinds] `thenNF_Tc` \ tyvars ->
212 tcExtendTyVarEnv tyvars thing_inside
217 kcHsTyVar :: HsTyVarBndr name -> NF_TcM (name, TcKind)
218 kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
220 kcHsTyVar (UserTyVar name) = newNamedKindVar name
221 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
223 kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
225 newNamedKindVar name = newKindVar `thenNF_Tc` \ kind ->
226 returnNF_Tc (name, kind)
228 ---------------------------
229 kcLiftedType :: RenamedHsType -> TcM ()
230 -- The type ty must be a *lifted* *type*
232 = kcHsType ty `thenTc` \ kind ->
233 tcAddErrCtxt (typeKindCtxt ty) $
234 unifyKind liftedTypeKind kind
236 ---------------------------
237 kcTypeType :: RenamedHsType -> TcM ()
238 -- The type ty must be a *type*, but it can be lifted or unlifted.
240 = kcHsType ty `thenTc` \ kind ->
241 tcAddErrCtxt (typeKindCtxt ty) $
242 unifyOpenTypeKind kind
244 ---------------------------
245 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
246 -- Used for type signatures
247 kcHsSigType = kcTypeType
248 kcHsSigTypes tys = mapTc_ kcHsSigType tys
249 kcHsLiftedSigType = kcLiftedType
251 ---------------------------
252 kcHsType :: RenamedHsType -> TcM TcKind
253 kcHsType (HsTyVar name) = kcTyVar name
255 kcHsType (HsListTy ty)
256 = kcLiftedType ty `thenTc` \ tau_ty ->
257 returnTc liftedTypeKind
259 kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
260 = mapTc kcTypeType tys `thenTc_`
261 returnTc (case boxity of
262 Boxed -> liftedTypeKind
263 Unboxed -> unliftedTypeKind)
265 kcHsType (HsFunTy ty1 ty2)
266 = kcTypeType ty1 `thenTc_`
267 kcTypeType ty2 `thenTc_`
268 returnTc liftedTypeKind
270 kcHsType (HsNumTy _) -- The unit type for generics
271 = returnTc liftedTypeKind
273 kcHsType ty@(HsOpTy ty1 op ty2)
274 = kcTyVar op `thenTc` \ op_kind ->
275 kcHsType ty1 `thenTc` \ ty1_kind ->
276 kcHsType ty2 `thenTc` \ ty2_kind ->
277 tcAddErrCtxt (appKindCtxt (ppr ty)) $
278 kcAppKind op_kind ty1_kind `thenTc` \ op_kind' ->
279 kcAppKind op_kind' ty2_kind
281 kcHsType (HsPredTy pred)
282 = kcHsPred pred `thenTc_`
283 returnTc liftedTypeKind
285 kcHsType ty@(HsAppTy ty1 ty2)
286 = kcHsType ty1 `thenTc` \ tc_kind ->
287 kcHsType ty2 `thenTc` \ arg_kind ->
288 tcAddErrCtxt (appKindCtxt (ppr ty)) $
289 kcAppKind tc_kind arg_kind
291 kcHsType (HsForAllTy (Just tv_names) context ty)
292 = kcHsTyVars tv_names `thenNF_Tc` \ kind_env ->
293 tcExtendKindEnv kind_env $
294 kcHsContext context `thenTc_`
295 kcHsType ty `thenTc_`
296 returnTc liftedTypeKind
298 ---------------------------
299 kcAppKind fun_kind arg_kind
300 = case tcSplitFunTy_maybe fun_kind of
301 Just (arg_kind', res_kind)
302 -> unifyKind arg_kind arg_kind' `thenTc_`
305 Nothing -> newKindVar `thenNF_Tc` \ res_kind ->
306 unifyKind fun_kind (mkArrowKind arg_kind res_kind) `thenTc_`
310 ---------------------------
311 kcHsContext ctxt = mapTc_ kcHsPred ctxt
313 kcHsPred :: RenamedHsPred -> TcM ()
314 kcHsPred pred@(HsIParam name ty)
315 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
318 kcHsPred pred@(HsClassP cls tys)
319 = tcAddErrCtxt (appKindCtxt (ppr pred)) $
320 kcClass cls `thenTc` \ kind ->
321 mapTc kcHsType tys `thenTc` \ arg_kinds ->
322 unifyKind kind (mkArrowKinds arg_kinds liftedTypeKind)
324 ---------------------------
325 kcTyVar name -- Could be a tyvar or a tycon
326 = tcLookup name `thenTc` \ thing ->
328 AThing kind -> returnTc kind
329 ATyVar tv -> returnTc (tyVarKind tv)
330 AGlobal (ATyCon tc) -> returnTc (tyConKind tc)
331 other -> failWithTc (wrongThingErr "type" thing name)
333 kcClass cls -- Must be a class
334 = tcLookup cls `thenNF_Tc` \ thing ->
336 AThing kind -> returnTc kind
337 AGlobal (AClass cls) -> returnTc (tyConKind (classTyCon cls))
338 other -> failWithTc (wrongThingErr "class" thing cls)
341 %************************************************************************
345 %************************************************************************
347 tc_type, the main work horse
348 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
354 tc_type is used to typecheck the types in the RHS of data
355 constructors. In the case of recursive data types, that means that
356 the type constructors themselves are (partly) black holes. e.g.
358 data T a = MkT a [T a]
360 While typechecking the [T a] on the RHS, T itself is not yet fully
361 defined. That in turn places restrictions on what you can check in
362 tcHsType; if you poke on too much you get a black hole. I keep
363 forgetting this, hence this warning!
365 So tc_type does no validity-checking. Instead that's all done
366 by TcMType.checkValidType
368 --------------------------
369 *** END OF BIG WARNING ***
370 --------------------------
374 tc_type :: RenamedHsType -> TcM Type
376 tc_type ty@(HsTyVar name)
379 tc_type (HsListTy ty)
380 = tc_type ty `thenTc` \ tau_ty ->
381 returnTc (mkListTy tau_ty)
383 tc_type (HsTupleTy (HsTupCon _ boxity arity) tys)
384 = ASSERT( arity == length tys )
385 tc_types tys `thenTc` \ tau_tys ->
386 returnTc (mkTupleTy boxity arity tau_tys)
388 tc_type (HsFunTy ty1 ty2)
389 = tc_type ty1 `thenTc` \ tau_ty1 ->
390 tc_type ty2 `thenTc` \ tau_ty2 ->
391 returnTc (mkFunTy tau_ty1 tau_ty2)
395 returnTc (mkTyConApp genUnitTyCon [])
397 tc_type (HsOpTy ty1 op ty2)
398 = tc_type ty1 `thenTc` \ tau_ty1 ->
399 tc_type ty2 `thenTc` \ tau_ty2 ->
400 tc_fun_type op [tau_ty1,tau_ty2]
402 tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
404 tc_type (HsPredTy pred)
405 = tc_pred pred `thenTc` \ pred' ->
406 returnTc (mkPredTy pred')
408 tc_type full_ty@(HsForAllTy (Just tv_names) ctxt ty)
410 kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
412 tcHsTyVars tv_names kind_check $ \ tyvars ->
413 mapTc tc_pred ctxt `thenTc` \ theta ->
414 tc_type ty `thenTc` \ tau ->
415 returnTc (mkSigmaTy tyvars theta tau)
417 tc_types arg_tys = mapTc tc_type arg_tys
420 Help functions for type applications
421 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
424 tc_app :: RenamedHsType -> [RenamedHsType] -> TcM Type
425 tc_app (HsAppTy ty1 ty2) tys
426 = tc_app ty1 (ty2:tys)
429 = tcAddErrCtxt (appKindCtxt pp_app) $
430 tc_types tys `thenTc` \ arg_tys ->
432 HsTyVar fun -> tc_fun_type fun arg_tys
433 other -> tc_type ty `thenTc` \ fun_ty ->
434 returnNF_Tc (mkAppTys fun_ty arg_tys)
436 pp_app = ppr ty <+> sep (map pprParendHsType tys)
438 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
439 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
440 -- hence the rather strange functionality.
442 tc_fun_type name arg_tys
443 = tcLookup name `thenTc` \ thing ->
445 ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
448 | isSynTyCon tc -> returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
449 (drop arity arg_tys))
450 | otherwise -> returnTc (mkTyConApp tc arg_tys)
452 arity = tyConArity tc
455 other -> failWithTc (wrongThingErr "type constructor" thing name)
462 tc_pred assn@(HsClassP class_name tys)
463 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
464 tc_types tys `thenTc` \ arg_tys ->
465 tcLookupGlobal class_name `thenTc` \ thing ->
467 AClass clas -> returnTc (ClassP clas arg_tys)
468 other -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
470 tc_pred assn@(HsIParam name ty)
471 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
472 tc_type ty `thenTc` \ arg_ty ->
473 returnTc (IParam name arg_ty)
478 %************************************************************************
480 \subsection{Type variables, with knot tying!}
482 %************************************************************************
485 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
486 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
488 mkTyClTyVars :: Kind -- Kind of the tycon or class
489 -> [HsTyVarBndr Name]
491 mkTyClTyVars kind tyvar_names
492 = mkImmutTyVars tyvars_w_kinds
494 (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
498 %************************************************************************
500 \subsection{Signatures}
502 %************************************************************************
504 @tcSigs@ checks the signatures for validity, and returns a list of
505 {\em freshly-instantiated} signatures. That is, the types are already
506 split up, and have fresh type variables installed. All non-type-signature
507 "RenamedSigs" are ignored.
509 The @TcSigInfo@ contains @TcTypes@ because they are unified with
510 the variable's type, and after that checked to see whether they've
516 Name -- N, the Name in corresponding binding
518 TcId -- *Polymorphic* binder for this value...
525 TcId -- *Monomorphic* binder for this value
526 -- Does *not* have name = N
529 [Inst] -- Empty if theta is null, or
530 -- (method mono_id) otherwise
532 SrcLoc -- Of the signature
534 instance Outputable TcSigInfo where
535 ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
536 ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
538 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
539 -- Search for a particular signature
540 maybeSig [] name = Nothing
541 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
542 | name == sig_name = Just sig
543 | otherwise = maybeSig sigs name
548 tcTySig :: RenamedSig -> TcM TcSigInfo
550 tcTySig (Sig v ty src_loc)
551 = tcAddSrcLoc src_loc $
552 tcHsSigType (FunSigCtxt v) ty `thenTc` \ sigma_tc_ty ->
553 mkTcSig (mkLocalId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
556 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
557 mkTcSig poly_id src_loc
558 = -- Instantiate this type
559 -- It's important to do this even though in the error-free case
560 -- we could just split the sigma_tc_ty (since the tyvars don't
561 -- unified with anything). But in the case of an error, when
562 -- the tyvars *do* get unified with something, we want to carry on
563 -- typechecking the rest of the program with the function bound
564 -- to a pristine type, namely sigma_tc_ty
566 (tyvars, rho) = tcSplitForAllTys (idType poly_id)
568 tcInstSigVars tyvars `thenNF_Tc` \ tyvars' ->
569 -- Make *signature* type variables
572 tyvar_tys' = mkTyVarTys tyvars'
573 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
574 -- mkTopTyVarSubst because the tyvars' are fresh
576 (theta', tau') = tcSplitRhoTy rho'
577 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
578 -- wherever possible, which can improve interface files.
580 newMethodWithGivenTy SignatureOrigin
583 theta' tau' `thenNF_Tc` \ inst ->
584 -- We make a Method even if it's not overloaded; no harm
586 returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
588 name = idName poly_id
593 %************************************************************************
595 \subsection{Checking signature type variables}
597 %************************************************************************
599 @checkSigTyVars@ is used after the type in a type signature has been unified with
600 the actual type found. It then checks that the type variables of the type signature
602 (a) Still all type variables
603 eg matching signature [a] against inferred type [(p,q)]
604 [then a will be unified to a non-type variable]
606 (b) Still all distinct
607 eg matching signature [(a,b)] against inferred type [(p,p)]
608 [then a and b will be unified together]
610 (c) Not mentioned in the environment
611 eg the signature for f in this:
617 Here, f is forced to be monorphic by the free occurence of x.
619 (d) Not (unified with another type variable that is) in scope.
620 eg f x :: (r->r) = (\y->y) :: forall a. a->r
621 when checking the expression type signature, we find that
622 even though there is nothing in scope whose type mentions r,
623 nevertheless the type signature for the expression isn't right.
625 Another example is in a class or instance declaration:
627 op :: forall b. a -> b
629 Here, b gets unified with a
631 Before doing this, the substitution is applied to the signature type variable.
633 We used to have the notion of a "DontBind" type variable, which would
634 only be bound to itself or nothing. Then points (a) and (b) were
635 self-checking. But it gave rise to bogus consequential error messages.
638 f = (*) -- Monomorphic
643 Here, we get a complaint when checking the type signature for g,
644 that g isn't polymorphic enough; but then we get another one when
645 dealing with the (Num x) context arising from f's definition;
646 we try to unify x with Int (to default it), but find that x has already
647 been unified with the DontBind variable "a" from g's signature.
648 This is really a problem with side-effecting unification; we'd like to
649 undo g's effects when its type signature fails, but unification is done
650 by side effect, so we can't (easily).
652 So we revert to ordinary type variables for signatures, and try to
653 give a helpful message in checkSigTyVars.
656 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
657 -> TcTyVarSet -- Tyvars that are free in the type signature
658 -- Not necessarily zonked
659 -- These should *already* be in the free-in-env set,
660 -- and are used here only to improve the error message
661 -> TcM [TcTyVar] -- Zonked signature type variables
663 checkSigTyVars [] free = returnTc []
664 checkSigTyVars sig_tyvars free_tyvars
665 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
666 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
668 checkTcM (allDistinctTyVars sig_tys globals)
669 (complain sig_tys globals) `thenTc_`
671 returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
674 complain sig_tys globals
675 = -- For the in-scope ones, zonk them and construct a map
676 -- from the zonked tyvar to the in-scope one
677 -- If any of the in-scope tyvars zonk to a type, then ignore them;
678 -- that'll be caught later when we back up to their type sig
679 tcGetEnv `thenNF_Tc` \ env ->
681 in_scope_tvs = tcEnvTyVars env
683 zonkTcTyVars in_scope_tvs `thenNF_Tc` \ in_scope_tys ->
685 in_scope_assoc = [ (zonked_tv, in_scope_tv)
686 | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
687 Just zonked_tv <- [tcGetTyVar_maybe z_ty]
689 in_scope_env = mkVarEnv in_scope_assoc
692 -- "check" checks each sig tyvar in turn
694 (env2, in_scope_env, [])
695 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
697 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
699 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
700 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
702 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
704 check (tidy_env, acc, msgs) (sig_tyvar,ty)
705 -- sig_tyvar is from the signature;
706 -- ty is what you get if you zonk sig_tyvar and then tidy it
708 -- acc maps a zonked type variable back to a signature type variable
709 = case tcGetTyVar_maybe ty of {
710 Nothing -> -- Error (a)!
711 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
715 case lookupVarEnv acc tv of {
716 Just sig_tyvar' -> -- Error (b) or (d)!
717 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
719 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
723 if tv `elemVarSet` globals -- Error (c)! Type variable escapes
724 -- The least comprehensible, so put it last
726 -- a) get the local TcIds from the environment,
727 -- and pass them to find_globals (they might have tv free)
728 -- b) similarly, find any free_tyvars that mention tv
729 then tcGetEnv `thenNF_Tc` \ ve ->
730 find_globals tv tidy_env [] (tcEnvTcIds ve) `thenNF_Tc` \ (tidy_env1, globs) ->
731 find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
732 returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
735 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
738 -- find_globals looks at the value environment and finds values
739 -- whose types mention the offending type variable. It has to be
740 -- careful to zonk the Id's type first, so it has to be in the monad.
741 -- We must be careful to pass it a zonked type variable, too.
747 -> NF_TcM (TidyEnv,[(Name,Type)])
749 find_globals tv tidy_env acc []
750 = returnNF_Tc (tidy_env, acc)
752 find_globals tv tidy_env acc (id:ids)
753 | isEmptyVarSet (idFreeTyVars id)
754 = find_globals tv tidy_env acc ids
757 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
758 if tv `elemVarSet` tyVarsOfType id_ty then
760 (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
761 acc' = (idName id, id_ty') : acc
763 find_globals tv tidy_env' acc' ids
765 find_globals tv tidy_env acc ids
767 find_frees tv tidy_env acc []
768 = returnNF_Tc (tidy_env, acc)
769 find_frees tv tidy_env acc (ftv:ftvs)
770 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
771 if tv `elemVarSet` tyVarsOfType ty then
773 (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
775 find_frees tv tidy_env' (ftv':acc) ftvs
777 find_frees tv tidy_env acc ftvs
780 escape_msg sig_tv tv globs frees
781 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
782 if not (null globs) then
783 vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
784 ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
785 nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
787 else if not (null frees) then
788 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
789 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
792 empty -- Sigh. It's really hard to give a good error message
793 -- all the time. One bad case is an existential pattern match
795 is_are | isSingleton frees = ptext SLIT("is")
796 | otherwise = ptext SLIT("are")
797 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
798 | otherwise = ptext SLIT("It")
800 vcat_first :: Int -> [SDoc] -> SDoc
801 vcat_first n [] = empty
802 vcat_first 0 (x:xs) = text "...others omitted..."
803 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
805 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
806 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
809 These two context are used with checkSigTyVars
812 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
813 -> TidyEnv -> NF_TcM (TidyEnv, Message)
814 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
815 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
817 (env1, tidy_sig_tyvars) = tidyOpenTyVars tidy_env sig_tyvars
818 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
819 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
820 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
821 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
825 returnNF_Tc (env3, msg)
827 sigPatCtxt bound_tvs bound_ids tidy_env
829 sep [ptext SLIT("When checking a pattern that binds"),
830 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
832 show_ids = filter is_interesting bound_ids
833 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
835 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
836 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
837 -- Don't zonk the types so we get the separate, un-unified versions
841 %************************************************************************
843 \subsection{Errors and contexts}
845 %************************************************************************
848 typeKindCtxt :: RenamedHsType -> Message
849 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
850 nest 2 (quotes (ppr ty)),
851 ptext SLIT("is a type")]
853 appKindCtxt :: SDoc -> Message
854 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
856 wrongThingErr expected thing name
857 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
859 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
860 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
861 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
862 pp_thing (ATyVar _) = ptext SLIT("Type variable")
863 pp_thing (ATcId _) = ptext SLIT("Local identifier")
864 pp_thing (AThing _) = ptext SLIT("Utterly bogus")