2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
7 module TcMonoType ( tcHsType, tcHsSigType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType, tcHsTopTypeKind,
8 tcContext, tcHsTyVar, kcHsTyVar, kcHsType,
9 tcExtendTyVarScope, tcExtendTopTyVarScope,
10 TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
11 checkSigTyVars, sigCtxt, sigPatCtxt
14 #include "HsVersions.h"
16 import HsSyn ( HsType(..), HsTyVarBndr(..), HsUsageAnn(..),
17 Sig(..), HsPred(..), pprParendHsType, HsTupCon(..) )
18 import RnHsSyn ( RenamedHsType, RenamedContext, RenamedSig )
19 import TcHsSyn ( TcId )
22 import TcEnv ( tcExtendTyVarEnv, tcLookupTy, tcGetValueEnv, tcGetInScopeTyVars,
23 tcExtendUVarEnv, tcLookupUVar,
24 tcGetGlobalTyVars, valueEnvIds, TcTyThing(..)
26 import TcType ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
27 typeToTcType, kindToTcKind,
28 newKindVar, tcInstSigVar,
29 zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType, zonkTcTyVar
31 import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr )
32 import TcUnify ( unifyKind, unifyKinds, unifyTypeKind )
33 import Type ( Type, PredType(..), ThetaType, UsageAnn(..),
34 mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
35 mkUsForAllTy, zipFunTys, hoistForAllTys,
36 mkSigmaTy, mkDictTy, mkPredTy, mkTyConApp,
37 mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
38 boxedTypeKind, unboxedTypeKind, tyVarsOfType,
39 mkArrowKinds, getTyVar_maybe, getTyVar,
40 tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
41 tyVarsOfType, tyVarsOfTypes, mkForAllTys
43 import PprType ( pprConstraint, pprType )
44 import Subst ( mkTopTyVarSubst, substTy )
45 import Id ( mkVanillaId, idName, idType, idFreeTyVars )
46 import Var ( TyVar, mkTyVar, mkNamedUVar, varName )
49 import Bag ( bagToList )
50 import ErrUtils ( Message )
51 import TyCon ( TyCon )
52 import Name ( Name, OccName, isLocallyDefined )
53 import TysWiredIn ( mkListTy, mkTupleTy )
54 import UniqFM ( elemUFM, foldUFM )
55 import BasicTypes ( Boxity(..) )
56 import SrcLoc ( SrcLoc )
57 import Unique ( Unique, Uniquable(..) )
58 import Util ( mapAccumL, isSingleton, removeDups )
63 %************************************************************************
65 \subsection{Checking types}
67 %************************************************************************
69 tcHsType and tcHsTypeKind
70 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
72 tcHsType checks that the type really is of kind Type!
75 kcHsType :: RenamedHsType -> TcM c ()
76 -- Kind-check the type
77 kcHsType ty = tc_type ty `thenTc_`
80 tcHsSigType :: RenamedHsType -> TcM s TcType
81 -- Used for type sigs written by the programmer
82 -- Hoist any inner for-alls to the top
84 = tcHsType ty `thenTc` \ ty' ->
85 returnTc (hoistForAllTys ty')
87 tcHsType :: RenamedHsType -> TcM s TcType
89 = -- tcAddErrCtxt (typeCtxt ty) $
92 tcHsTypeKind :: RenamedHsType -> TcM s (TcKind, TcType)
94 = -- tcAddErrCtxt (typeCtxt ty) $
97 -- Type-check a type, *and* then lazily zonk it. The important
98 -- point is that this zonks all the uncommitted *kind* variables
99 -- in kinds of any any nested for-all tyvars.
100 -- There won't be any mutable *type* variables at all.
102 -- NOTE the forkNF_Tc. This makes the zonking lazy, which is
103 -- absolutely necessary. During the type-checking of a recursive
104 -- group of tycons/classes (TcTyClsDecls.tcGroup) we use an
105 -- environment in which we aren't allowed to look at the actual
106 -- tycons/classes returned from a lookup. Because tc_app does
107 -- look at the tycon to build the type, we can't look at the type
108 -- either, until we get out of the loop. The fork delays the
109 -- zonking till we've completed the loop. Sigh.
111 tcHsTopType :: RenamedHsType -> TcM s Type
113 = -- tcAddErrCtxt (typeCtxt ty) $
114 tc_type ty `thenTc` \ ty' ->
115 forkNF_Tc (zonkTcTypeToType ty') `thenTc` \ ty'' ->
116 returnTc (hoistForAllTys ty'')
118 tcHsTopBoxedType :: RenamedHsType -> TcM s Type
120 = -- tcAddErrCtxt (typeCtxt ty) $
121 tc_boxed_type ty `thenTc` \ ty' ->
122 forkNF_Tc (zonkTcTypeToType ty') `thenTc` \ ty'' ->
123 returnTc (hoistForAllTys ty'')
125 tcHsTopTypeKind :: RenamedHsType -> TcM s (TcKind, Type)
127 = -- tcAddErrCtxt (typeCtxt ty) $
128 tc_type_kind ty `thenTc` \ (kind, ty') ->
129 forkNF_Tc (zonkTcTypeToType ty') `thenTc` \ zonked_ty ->
130 returnNF_Tc (kind, hoistForAllTys zonked_ty)
138 tc_boxed_type :: RenamedHsType -> TcM s Type
140 = tc_type_kind ty `thenTc` \ (actual_kind, tc_ty) ->
141 tcAddErrCtxt (typeKindCtxt ty)
142 (unifyKind boxedTypeKind actual_kind) `thenTc_`
145 tc_type :: RenamedHsType -> TcM s Type
147 -- The type ty must be a *type*, but it can be boxed
148 -- or unboxed. So we check that is is of form (Type bv)
149 -- using unifyTypeKind
150 = tc_type_kind ty `thenTc` \ (actual_kind, tc_ty) ->
151 tcAddErrCtxt (typeKindCtxt ty)
152 (unifyTypeKind actual_kind) `thenTc_`
155 tc_type_kind :: RenamedHsType -> TcM s (TcKind, Type)
156 tc_type_kind ty@(HsTyVar name)
159 tc_type_kind (HsListTy ty)
160 = tc_boxed_type ty `thenTc` \ tau_ty ->
161 returnTc (boxedTypeKind, mkListTy tau_ty)
163 tc_type_kind (HsTupleTy (HsTupCon _ Boxed) tys)
164 = mapTc tc_boxed_type tys `thenTc` \ tau_tys ->
165 returnTc (boxedTypeKind, mkTupleTy Boxed (length tys) tau_tys)
167 tc_type_kind (HsTupleTy (HsTupCon _ Unboxed) tys)
168 = mapTc tc_type tys `thenTc` \ tau_tys ->
169 returnTc (unboxedTypeKind, mkTupleTy Unboxed (length tys) tau_tys)
171 tc_type_kind (HsFunTy ty1 ty2)
172 = tc_type ty1 `thenTc` \ tau_ty1 ->
173 tc_type ty2 `thenTc` \ tau_ty2 ->
174 returnTc (boxedTypeKind, mkFunTy tau_ty1 tau_ty2)
176 tc_type_kind (HsAppTy ty1 ty2)
179 tc_type_kind (HsPredTy pred)
180 = tcClassAssertion True pred `thenTc` \ pred' ->
181 returnTc (boxedTypeKind, mkPredTy pred')
183 tc_type_kind (HsUsgTy usg ty)
184 = newUsg usg `thenTc` \ usg' ->
185 tc_type_kind ty `thenTc` \ (kind, tc_ty) ->
186 returnTc (kind, mkUsgTy usg' tc_ty)
188 newUsg usg = case usg of
189 HsUsOnce -> returnTc UsOnce
190 HsUsMany -> returnTc UsMany
191 HsUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
194 tc_type_kind (HsUsgForAllTy uv_name ty)
196 uv = mkNamedUVar uv_name
198 tcExtendUVarEnv uv_name uv $
199 tc_type_kind ty `thenTc` \ (kind, tc_ty) ->
200 returnTc (kind, mkUsForAllTy uv tc_ty)
202 tc_type_kind (HsForAllTy (Just tv_names) context ty)
203 = tcExtendTyVarScope tv_names $ \ tyvars ->
204 tcContext context `thenTc` \ theta ->
205 tc_type_kind ty `thenTc` \ (kind, tau) ->
206 tcGetInScopeTyVars `thenTc` \ in_scope_vars ->
208 body_kind | null theta = kind
209 | otherwise = boxedTypeKind
210 -- Context behaves like a function type
211 -- This matters. Return-unboxed-tuple analysis can
212 -- give overloaded functions like
213 -- f :: forall a. Num a => (# a->a, a->a #)
214 -- And we want these to get through the type checker
215 check ct@(Class c tys) | ambiguous = failWithTc (ambigErr (c,tys) tau)
216 where ct_vars = tyVarsOfTypes tys
217 forall_tyvars = map varName in_scope_vars
218 tau_vars = tyVarsOfType tau
219 ambig ct_var = (varName ct_var `elem` forall_tyvars) &&
220 not (ct_var `elemUFM` tau_vars)
221 ambiguous = foldUFM ((||) . ambig) False ct_vars
222 check _ = returnTc ()
224 mapTc check theta `thenTc_`
225 returnTc (body_kind, mkSigmaTy tyvars theta tau)
228 Help functions for type applications
229 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
232 tc_app (HsAppTy ty1 ty2) tys
233 = tc_app ty1 (ty2:tys)
240 = tcAddErrCtxt (appKindCtxt pp_app) $
241 mapAndUnzipTc tc_type_kind tys `thenTc` \ (arg_kinds, arg_tys) ->
242 tc_fun_type ty arg_tys `thenTc` \ (fun_kind, result_ty) ->
244 -- Check argument compatibility
245 newKindVar `thenNF_Tc` \ result_kind ->
246 unifyKind fun_kind (mkArrowKinds arg_kinds result_kind)
248 returnTc (result_kind, result_ty)
250 pp_app = ppr ty <+> sep (map pprParendHsType tys)
252 -- (tc_fun_type ty arg_tys) returns (kind-of ty, mkAppTys ty arg_tys)
253 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
254 -- hence the rather strange functionality.
256 tc_fun_type (HsTyVar name) arg_tys
257 = tcLookupTy name `thenTc` \ (tycon_kind, thing) ->
259 ATyVar tv -> returnTc (tycon_kind, mkAppTys (mkTyVarTy tv) arg_tys)
260 AClass clas _ -> failWithTc (classAsTyConErr name)
262 ADataTyCon tc -> -- Data or newtype
263 returnTc (tycon_kind, mkTyConApp tc arg_tys)
265 ASynTyCon tc arity -> -- Type synonym
266 checkTc (arity <= n_args) err_msg `thenTc_`
267 returnTc (tycon_kind, result_ty)
269 -- It's OK to have an *over-applied* type synonym
270 -- data Tree a b = ...
271 -- type Foo a = Tree [a]
272 -- f :: Foo a b -> ...
273 result_ty = mkAppTys (mkSynTy tc (take arity arg_tys))
275 err_msg = arityErr "type synonym" name arity n_args
276 n_args = length arg_tys
278 tc_fun_type ty arg_tys
279 = tc_type_kind ty `thenTc` \ (fun_kind, fun_ty) ->
280 returnTc (fun_kind, mkAppTys fun_ty arg_tys)
288 tcContext :: RenamedContext -> TcM s ThetaType
289 tcContext context = mapTc (tcClassAssertion False) context
291 tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
292 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
293 mapAndUnzipTc tc_type_kind tys `thenTc` \ (arg_kinds, arg_tys) ->
294 tcLookupTy class_name `thenTc` \ (kind, thing) ->
297 -- Check with kind mis-match
298 checkTc (arity == n_tys) err `thenTc_`
299 unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind) `thenTc_`
300 returnTc (Class clas arg_tys)
303 err = arityErr "Class" class_name arity n_tys
304 other -> failWithTc (tyVarAsClassErr class_name)
306 tcClassAssertion ccall_ok assn@(HsPIParam name ty)
307 = tcAddErrCtxt (appKindCtxt (ppr assn)) $
308 tc_type_kind ty `thenTc` \ (arg_kind, arg_ty) ->
309 returnTc (IParam name arg_ty)
313 %************************************************************************
315 \subsection{Type variables, with knot tying!}
317 %************************************************************************
320 tcExtendTopTyVarScope :: TcKind -> [HsTyVarBndr Name]
321 -> ([TcTyVar] -> TcKind -> TcM s a)
323 tcExtendTopTyVarScope kind tyvar_names thing_inside
325 (tyvars_w_kinds, result_kind) = zipFunTys tyvar_names kind
326 tyvars = map mk_tv tyvars_w_kinds
328 tcExtendTyVarEnv tyvars (thing_inside tyvars result_kind)
330 mk_tv (UserTyVar name, kind) = mkTyVar name kind
331 mk_tv (IfaceTyVar name _, kind) = mkTyVar name kind
332 -- NB: immutable tyvars, but perhaps with mutable kinds
334 tcExtendTyVarScope :: [HsTyVarBndr Name]
335 -> ([TcTyVar] -> TcM s a) -> TcM s a
336 tcExtendTyVarScope tv_names thing_inside
337 = mapNF_Tc tcHsTyVar tv_names `thenNF_Tc` \ tyvars ->
338 tcExtendTyVarEnv tyvars $
341 tcHsTyVar :: HsTyVarBndr Name -> NF_TcM s TcTyVar
342 tcHsTyVar (UserTyVar name) = newKindVar `thenNF_Tc` \ kind ->
343 tcNewMutTyVar name kind
344 -- NB: mutable kind => mutable tyvar, so that zonking can bind
345 -- the tyvar to its immutable form
347 tcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (mkTyVar name (kindToTcKind kind))
349 kcHsTyVar :: HsTyVarBndr name -> NF_TcM s TcKind
350 kcHsTyVar (UserTyVar name) = newKindVar
351 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (kindToTcKind kind)
355 %************************************************************************
357 \subsection{Signatures}
359 %************************************************************************
361 @tcSigs@ checks the signatures for validity, and returns a list of
362 {\em freshly-instantiated} signatures. That is, the types are already
363 split up, and have fresh type variables installed. All non-type-signature
364 "RenamedSigs" are ignored.
366 The @TcSigInfo@ contains @TcTypes@ because they are unified with
367 the variable's type, and after that checked to see whether they've
373 Name -- N, the Name in corresponding binding
375 TcId -- *Polymorphic* binder for this value...
382 TcId -- *Monomorphic* binder for this value
383 -- Does *not* have name = N
386 Inst -- Empty if theta is null, or
387 -- (method mono_id) otherwise
389 SrcLoc -- Of the signature
391 instance Outputable TcSigInfo where
392 ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
393 ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
395 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
396 -- Search for a particular signature
397 maybeSig [] name = Nothing
398 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
399 | name == sig_name = Just sig
400 | otherwise = maybeSig sigs name
405 tcTySig :: RenamedSig -> TcM s TcSigInfo
407 tcTySig (Sig v ty src_loc)
408 = tcAddSrcLoc src_loc $
409 tcHsSigType ty `thenTc` \ sigma_tc_ty ->
410 mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
413 mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
414 mkTcSig poly_id src_loc
415 = -- Instantiate this type
416 -- It's important to do this even though in the error-free case
417 -- we could just split the sigma_tc_ty (since the tyvars don't
418 -- unified with anything). But in the case of an error, when
419 -- the tyvars *do* get unified with something, we want to carry on
420 -- typechecking the rest of the program with the function bound
421 -- to a pristine type, namely sigma_tc_ty
423 (tyvars, rho) = splitForAllTys (idType poly_id)
425 mapNF_Tc tcInstSigVar tyvars `thenNF_Tc` \ tyvars' ->
426 -- Make *signature* type variables
429 tyvar_tys' = mkTyVarTys tyvars'
430 rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
431 -- mkTopTyVarSubst because the tyvars' are fresh
432 (theta', tau') = splitRhoTy rho'
433 -- This splitRhoTy tries hard to make sure that tau' is a type synonym
434 -- wherever possible, which can improve interface files.
436 newMethodWithGivenTy SignatureOrigin
439 theta' tau' `thenNF_Tc` \ inst ->
440 -- We make a Method even if it's not overloaded; no harm
442 returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) inst src_loc)
444 name = idName poly_id
449 %************************************************************************
451 \subsection{Checking signature type variables}
453 %************************************************************************
455 @checkSigTyVars@ is used after the type in a type signature has been unified with
456 the actual type found. It then checks that the type variables of the type signature
458 (a) Still all type variables
459 eg matching signature [a] against inferred type [(p,q)]
460 [then a will be unified to a non-type variable]
462 (b) Still all distinct
463 eg matching signature [(a,b)] against inferred type [(p,p)]
464 [then a and b will be unified together]
466 (c) Not mentioned in the environment
467 eg the signature for f in this:
473 Here, f is forced to be monorphic by the free occurence of x.
475 (d) Not (unified with another type variable that is) in scope.
476 eg f x :: (r->r) = (\y->y) :: forall a. a->r
477 when checking the expression type signature, we find that
478 even though there is nothing in scope whose type mentions r,
479 nevertheless the type signature for the expression isn't right.
481 Another example is in a class or instance declaration:
483 op :: forall b. a -> b
485 Here, b gets unified with a
487 Before doing this, the substitution is applied to the signature type variable.
489 We used to have the notion of a "DontBind" type variable, which would
490 only be bound to itself or nothing. Then points (a) and (b) were
491 self-checking. But it gave rise to bogus consequential error messages.
494 f = (*) -- Monomorphic
499 Here, we get a complaint when checking the type signature for g,
500 that g isn't polymorphic enough; but then we get another one when
501 dealing with the (Num x) context arising from f's definition;
502 we try to unify x with Int (to default it), but find that x has already
503 been unified with the DontBind variable "a" from g's signature.
504 This is really a problem with side-effecting unification; we'd like to
505 undo g's effects when its type signature fails, but unification is done
506 by side effect, so we can't (easily).
508 So we revert to ordinary type variables for signatures, and try to
509 give a helpful message in checkSigTyVars.
512 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
513 -> TcTyVarSet -- Tyvars that are free in the type signature
514 -- These should *already* be in the global-var set, and are
515 -- used here only to improve the error message
516 -> TcM s [TcTyVar] -- Zonked signature type variables
518 checkSigTyVars [] free = returnTc []
520 checkSigTyVars sig_tyvars free_tyvars
521 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
522 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
524 checkTcM (all_ok sig_tys globals)
525 (complain sig_tys globals) `thenTc_`
527 returnTc (map (getTyVar "checkSigTyVars") sig_tys)
531 all_ok (ty:tys) acc = case getTyVar_maybe ty of
532 Nothing -> False -- Point (a)
533 Just tv | tv `elemVarSet` acc -> False -- Point (b) or (c)
534 | otherwise -> all_ok tys (acc `extendVarSet` tv)
537 complain sig_tys globals
538 = -- For the in-scope ones, zonk them and construct a map
539 -- from the zonked tyvar to the in-scope one
540 -- If any of the in-scope tyvars zonk to a type, then ignore them;
541 -- that'll be caught later when we back up to their type sig
542 tcGetInScopeTyVars `thenNF_Tc` \ in_scope_tvs ->
543 zonkTcTyVars in_scope_tvs `thenNF_Tc` \ in_scope_tys ->
545 in_scope_assoc = [ (zonked_tv, in_scope_tv)
546 | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
547 Just zonked_tv <- [getTyVar_maybe z_ty]
549 in_scope_env = mkVarEnv in_scope_assoc
552 -- "check" checks each sig tyvar in turn
554 (env2, in_scope_env, [])
555 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
557 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
559 (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
560 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
562 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
564 check (env, acc, msgs) (sig_tyvar,ty)
565 -- sig_tyvar is from the signature;
566 -- ty is what you get if you zonk sig_tyvar and then tidy it
568 -- acc maps a zonked type variable back to a signature type variable
569 = case getTyVar_maybe ty of {
570 Nothing -> -- Error (a)!
571 returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
575 case lookupVarEnv acc tv of {
576 Just sig_tyvar' -> -- Error (b) or (d)!
577 returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
581 if tv `elemVarSet` globals -- Error (c)! Type variable escapes
582 -- The least comprehensible, so put it last
583 then tcGetValueEnv `thenNF_Tc` \ ve ->
584 find_globals tv env [] (valueEnvIds ve) `thenNF_Tc` \ (env1, globs) ->
585 find_frees tv env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (env2, frees) ->
586 returnNF_Tc (env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
589 returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
592 -- find_globals looks at the value environment and finds values
593 -- whose types mention the offending type variable. It has to be
594 -- careful to zonk the Id's type first, so it has to be in the monad.
595 -- We must be careful to pass it a zonked type variable, too.
596 find_globals tv tidy_env acc []
597 = returnNF_Tc (tidy_env, acc)
599 find_globals tv tidy_env acc (id:ids)
600 | not (isLocallyDefined id) ||
601 isEmptyVarSet (idFreeTyVars id)
602 = find_globals tv tidy_env acc ids
605 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
606 if tv `elemVarSet` tyVarsOfType id_ty then
608 (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
609 acc' = (idName id, id_ty') : acc
611 find_globals tv tidy_env' acc' ids
613 find_globals tv tidy_env acc ids
615 find_frees tv tidy_env acc []
616 = returnNF_Tc (tidy_env, acc)
617 find_frees tv tidy_env acc (ftv:ftvs)
618 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
619 if tv `elemVarSet` tyVarsOfType ty then
621 (tidy_env', ftv') = tidyTyVar tidy_env ftv
623 find_frees tv tidy_env' (ftv':acc) ftvs
625 find_frees tv tidy_env acc ftvs
628 escape_msg sig_tv tv globs frees
629 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
630 if not (null globs) then
631 vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
632 ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
633 nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
635 else if not (null frees) then
636 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
637 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
640 empty -- Sigh. It's really hard to give a good error message
641 -- all the time. One bad case is an existential pattern match
643 is_are | isSingleton frees = ptext SLIT("is")
644 | otherwise = ptext SLIT("are")
645 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
646 | otherwise = ptext SLIT("It")
648 vcat_first :: Int -> [SDoc] -> SDoc
649 vcat_first n [] = empty
650 vcat_first 0 (x:xs) = text "...others omitted..."
651 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
653 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
654 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
657 These two context are used with checkSigTyVars
660 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
661 -> TidyEnv -> NF_TcM s (TidyEnv, Message)
662 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
663 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
665 (env1, tidy_sig_tyvars) = tidyTyVars tidy_env sig_tyvars
666 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
667 (env3, tidy_actual_tau) = tidyOpenType env1 actual_tau
668 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
669 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
673 returnNF_Tc (env3, msg)
675 sigPatCtxt bound_tvs bound_ids tidy_env
677 sep [ptext SLIT("When checking a pattern that binds"),
678 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
680 show_ids = filter is_interesting bound_ids
681 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
683 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
684 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
685 -- Don't zonk the types so we get the separate, un-unified versions
689 %************************************************************************
691 \subsection{Errors and contexts}
693 %************************************************************************
696 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
698 typeKindCtxt :: RenamedHsType -> Message
699 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
700 nest 2 (quotes (ppr ty)),
701 ptext SLIT("is a type")]
703 appKindCtxt :: SDoc -> Message
704 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
707 = ptext SLIT("Class used as a type constructor:") <+> ppr name
710 = ptext SLIT("Type constructor used as a class:") <+> ppr name
713 = ptext SLIT("Type variable used as a class:") <+> ppr name
716 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprConstraint c ts),
717 nest 4 (ptext SLIT("for the type:") <+> ppr ty),
718 nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]