[project @ 1999-04-20 12:59:51 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
1 %
2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
3 %
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
5
6 \begin{code}
7 module TcMonoType ( tcHsType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType,
8                     tcContext, tcHsTyVar, kcHsTyVar,
9                     tcExtendTyVarScope, tcExtendTopTyVarScope,
10                     TcSigInfo(..), tcTySig, mkTcSig, noSigs, maybeSig,
11                     checkSigTyVars, sigCtxt, sigPatCtxt
12                   ) where
13
14 #include "HsVersions.h"
15
16 import HsSyn            ( HsType(..), HsTyVar(..), Sig(..), pprClassAssertion, pprParendHsType )
17 import RnHsSyn          ( RenamedHsType, RenamedContext, RenamedSig )
18 import TcHsSyn          ( TcId )
19
20 import TcMonad
21 import TcEnv            ( tcExtendTyVarEnv, tcLookupTy, tcGetValueEnv, tcGetInScopeTyVars,
22                           tcGetGlobalTyVars, TcTyThing(..)
23                         )
24 import TcType           ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
25                           typeToTcType, kindToTcKind,
26                           newKindVar, tcInstSigVar,
27                           zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType
28                         )
29 import Inst             ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr )
30 import TcUnify          ( unifyKind, unifyKinds, unifyTypeKind )
31 import Type             ( Type, ThetaType, 
32                           mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, zipFunTys,
33                           mkSigmaTy, mkDictTy, mkTyConApp, mkAppTys, splitForAllTys, splitRhoTy,
34                           boxedTypeKind, unboxedTypeKind, tyVarsOfType,
35                           mkArrowKinds, getTyVar_maybe, getTyVar,
36                           tidyOpenType, tidyOpenTypes, tidyTyVar, fullSubstTy
37                         )
38 import Id               ( mkUserId, idName, idType, idFreeTyVars )
39 import Var              ( TyVar, mkTyVar )
40 import VarEnv
41 import VarSet
42 import Bag              ( bagToList )
43 import ErrUtils         ( Message )
44 import PrelInfo         ( cCallishClassKeys )
45 import TyCon            ( TyCon )
46 import Name             ( Name, OccName, isLocallyDefined )
47 import TysWiredIn       ( mkListTy, mkTupleTy, mkUnboxedTupleTy )
48 import SrcLoc           ( SrcLoc )
49 import Unique           ( Unique, Uniquable(..) )
50 import UniqFM           ( eltsUFM )
51 import Util             ( zipWithEqual, zipLazy, mapAccumL )
52 import Outputable
53 \end{code}
54
55
56 %************************************************************************
57 %*                                                                      *
58 \subsection{Checking types}
59 %*                                                                      *
60 %************************************************************************
61
62 tcHsType and tcHsTypeKind
63 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
64
65 tcHsType checks that the type really is of kind Type!
66
67 \begin{code}
68 tcHsType :: RenamedHsType -> TcM s TcType
69 tcHsType ty
70   = -- tcAddErrCtxt (typeCtxt ty)               $
71     tc_type ty
72
73 tcHsTypeKind    :: RenamedHsType -> TcM s (TcKind, TcType)
74 tcHsTypeKind ty 
75   = -- tcAddErrCtxt (typeCtxt ty)               $
76     tc_type_kind ty
77
78 -- Type-check a type, *and* then lazily zonk it.  The important
79 -- point is that this zonks all the uncommitted *kind* variables
80 -- in kinds of any any nested for-all tyvars.
81 -- There won't be any mutable *type* variables at all.
82 --
83 -- NOTE the forkNF_Tc.  This makes the zonking lazy, which is
84 -- absolutely necessary.  During the type-checking of a recursive
85 -- group of tycons/classes (TcTyClsDecls.tcGroup) we use an
86 -- environment in which we aren't allowed to look at the actual
87 -- tycons/classes returned from a lookup. Because tc_app does
88 -- look at the tycon to build the type, we can't look at the type
89 -- either, until we get out of the loop.   The fork delays the
90 -- zonking till we've completed the loop.  Sigh.
91
92 tcHsTopType :: RenamedHsType -> TcM s Type
93 tcHsTopType ty
94   = -- tcAddErrCtxt (typeCtxt ty)               $
95     tc_type ty                          `thenTc` \ ty' ->
96     forkNF_Tc (zonkTcTypeToType ty')
97
98 tcHsTopBoxedType :: RenamedHsType -> TcM s Type
99 tcHsTopBoxedType ty
100   = -- tcAddErrCtxt (typeCtxt ty)               $
101     tc_boxed_type ty                    `thenTc` \ ty' ->
102     forkNF_Tc (zonkTcTypeToType ty')
103 \end{code}
104
105
106 The main work horse
107 ~~~~~~~~~~~~~~~~~~~
108
109 \begin{code}
110 tc_boxed_type :: RenamedHsType -> TcM s Type
111 tc_boxed_type ty
112   = tc_type_kind ty                                     `thenTc` \ (actual_kind, tc_ty) ->
113     tcAddErrCtxt (typeKindCtxt ty)
114                  (unifyKind boxedTypeKind actual_kind)  `thenTc_`
115     returnTc tc_ty
116
117 tc_type :: RenamedHsType -> TcM s Type
118 tc_type ty
119         -- The type ty must be a *type*, but it can be boxed
120         -- or unboxed.  So we check that is is of form (Type bv)
121         -- using unifyTypeKind
122   = tc_type_kind ty                             `thenTc` \ (actual_kind, tc_ty) ->
123     tcAddErrCtxt (typeKindCtxt ty)
124                  (unifyTypeKind actual_kind)    `thenTc_`
125     returnTc tc_ty
126
127 tc_type_kind :: RenamedHsType -> TcM s (TcKind, Type)
128 tc_type_kind ty@(MonoTyVar name)
129   = tc_app ty []
130     
131 tc_type_kind (MonoListTy ty)
132   = tc_boxed_type ty            `thenTc` \ tau_ty ->
133     returnTc (boxedTypeKind, mkListTy tau_ty)
134
135 tc_type_kind (MonoTupleTy tys True {-boxed-})
136   = mapTc tc_boxed_type tys     `thenTc` \ tau_tys ->
137     returnTc (boxedTypeKind, mkTupleTy (length tys) tau_tys)
138
139 tc_type_kind (MonoTupleTy tys False {-unboxed-})
140   = mapTc tc_type tys                   `thenTc` \ tau_tys ->
141     returnTc (unboxedTypeKind, mkUnboxedTupleTy (length tys) tau_tys)
142
143 tc_type_kind (MonoFunTy ty1 ty2)
144   = tc_type ty1 `thenTc` \ tau_ty1 ->
145     tc_type ty2 `thenTc` \ tau_ty2 ->
146     returnTc (boxedTypeKind, mkFunTy tau_ty1 tau_ty2)
147
148 tc_type_kind (MonoTyApp ty1 ty2)
149   = tc_app ty1 [ty2]
150
151 tc_type_kind (MonoDictTy class_name tys)
152   = tcClassAssertion (class_name, tys)  `thenTc` \ (clas, arg_tys) ->
153     returnTc (boxedTypeKind, mkDictTy clas arg_tys)
154
155 tc_type_kind (HsForAllTy (Just tv_names) context ty)
156   = tcExtendTyVarScope tv_names         $ \ tyvars -> 
157     tcContext context                   `thenTc` \ theta ->
158     case theta of
159         []    ->        -- No context, so propagate body type
160                  tc_type_kind ty        `thenTc` \ (kind, tau) ->
161                  returnTc (kind, mkSigmaTy tyvars [] tau)
162
163         other ->        -- Context; behave like a function type
164                         -- This matters.  Return-unboxed-tuple analysis can
165                         -- give overloaded functions like
166                         --      f :: forall a. Num a => (# a->a, a->a #)
167                         -- And we want these to get through the type checker
168
169                  tc_type ty             `thenTc` \ tau ->
170                  returnTc (boxedTypeKind, mkSigmaTy tyvars theta tau)
171 \end{code}
172
173 Help functions for type applications
174 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
175
176 \begin{code}
177 tc_app (MonoTyApp ty1 ty2) tys
178   = tc_app ty1 (ty2:tys)
179
180 tc_app ty tys
181   | null tys
182   = tc_fun_type ty []
183
184   | otherwise
185   = tcAddErrCtxt (appKindCtxt pp_app)   $
186     mapAndUnzipTc tc_type_kind tys      `thenTc` \ (arg_kinds, arg_tys) ->
187     tc_fun_type ty arg_tys              `thenTc` \ (fun_kind, result_ty) ->
188
189         -- Check argument compatibility
190     newKindVar                                  `thenNF_Tc` \ result_kind ->
191     unifyKind fun_kind (mkArrowKinds arg_kinds result_kind)
192                                         `thenTc_`
193     returnTc (result_kind, result_ty)
194   where
195     pp_app = ppr ty <+> sep (map pprParendHsType tys)
196
197 -- (tc_fun_type ty arg_tys) returns (kind-of ty, mkAppTys ty arg_tys)
198 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
199 --      hence the rather strange functionality.
200
201 tc_fun_type (MonoTyVar name) arg_tys
202   = tcLookupTy name                     `thenTc` \ (tycon_kind, maybe_arity, thing) ->
203     case thing of
204         ATyVar tv   -> returnTc (tycon_kind, mkAppTys (mkTyVarTy tv) arg_tys)
205         AClass clas -> failWithTc (classAsTyConErr name)
206         ATyCon tc   -> case maybe_arity of
207                          Nothing ->     -- Data or newtype
208                                         returnTc (tycon_kind, mkTyConApp tc arg_tys)
209
210                          Just arity ->  -- Type synonym
211                                   checkTc (arity <= n_args) err_msg     `thenTc_`
212                                   returnTc (tycon_kind, result_ty)
213                            where
214                                 -- It's OK to have an *over-applied* type synonym
215                                 --      data Tree a b = ...
216                                 --      type Foo a = Tree [a]
217                                 --      f :: Foo a b -> ...
218                               result_ty = mkAppTys (mkSynTy tc (take arity arg_tys))
219                                                    (drop arity arg_tys)
220                               err_msg = arityErr "type synonym" name arity n_args
221                               n_args  = length arg_tys
222
223 tc_fun_type ty arg_tys
224   = tc_type_kind ty             `thenTc` \ (fun_kind, fun_ty) ->
225     returnTc (fun_kind, mkAppTys fun_ty arg_tys)
226 \end{code}
227
228
229 Contexts
230 ~~~~~~~~
231 \begin{code}
232
233 tcContext :: RenamedContext -> TcM s ThetaType
234 tcContext context
235   =     --Someone discovered that @CCallable@ and @CReturnable@
236         -- could be used in contexts such as:
237         --      foo :: CCallable a => a -> PrimIO Int
238         -- Doing this utterly wrecks the whole point of introducing these
239         -- classes so we specifically check that this isn't being done.
240         --
241         -- We *don't* do this check in tcClassAssertion, because that's
242         -- called when checking a HsDictTy, and we don't want to reject
243         --      instance CCallable Int 
244         -- etc. Ugh!
245     mapTc check_naughty context `thenTc_`
246
247     mapTc tcClassAssertion context
248
249  where
250    check_naughty (class_name, _) 
251      = checkTc (not (getUnique class_name `elem` cCallishClassKeys))
252                (naughtyCCallContextErr class_name)
253
254 tcClassAssertion assn@(class_name, tys)
255   = tcAddErrCtxt (appKindCtxt (pprClassAssertion assn)) $
256     mapAndUnzipTc tc_type_kind tys      `thenTc` \ (arg_kinds, arg_tys) ->
257     tcLookupTy class_name               `thenTc` \ (kind, ~(Just arity), thing) ->
258     case thing of
259         ATyVar  _   -> failWithTc (tyVarAsClassErr class_name)
260         ATyCon  _   -> failWithTc (tyConAsClassErr class_name)
261         AClass clas ->
262                         -- Check with kind mis-match
263                 checkTc (arity == n_tys) err                            `thenTc_`
264                 unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)   `thenTc_`
265                 returnTc (clas, arg_tys)
266             where
267                 n_tys = length tys
268                 err   = arityErr "Class" class_name arity n_tys
269 \end{code}
270
271
272 %************************************************************************
273 %*                                                                      *
274 \subsection{Type variables, with knot tying!}
275 %*                                                                      *
276 %************************************************************************
277
278 \begin{code}
279 tcExtendTopTyVarScope :: TcKind -> [HsTyVar Name]
280                       -> ([TcTyVar] -> TcKind -> TcM s a)
281                       -> TcM s a
282 tcExtendTopTyVarScope kind tyvar_names thing_inside
283   = let
284         (tyvars_w_kinds, result_kind) = zipFunTys tyvar_names kind
285         tyvars                        = map mk_tv tyvars_w_kinds
286     in
287     tcExtendTyVarEnv tyvars (thing_inside tyvars result_kind)   
288   where
289     mk_tv (UserTyVar name,    kind) = mkTyVar name kind
290     mk_tv (IfaceTyVar name _, kind) = mkTyVar name kind
291         -- NB: immutable tyvars, but perhaps with mutable kinds
292
293 tcExtendTyVarScope :: [HsTyVar Name] 
294                    -> ([TcTyVar] -> TcM s a) -> TcM s a
295 tcExtendTyVarScope tv_names thing_inside
296   = mapNF_Tc tcHsTyVar tv_names         `thenNF_Tc` \ tyvars ->
297     tcExtendTyVarEnv tyvars             $
298     thing_inside tyvars
299     
300 tcHsTyVar :: HsTyVar Name -> NF_TcM s TcTyVar
301 tcHsTyVar (UserTyVar name)       = newKindVar           `thenNF_Tc` \ kind ->
302                                    tcNewMutTyVar name kind
303         -- NB: mutable kind => mutable tyvar, so that zonking can bind
304         -- the tyvar to its immutable form
305
306 tcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (mkTyVar name (kindToTcKind kind))
307
308 kcHsTyVar :: HsTyVar name -> NF_TcM s TcKind
309 kcHsTyVar (UserTyVar name)       = newKindVar
310 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (kindToTcKind kind)
311 \end{code}
312
313
314 %************************************************************************
315 %*                                                                      *
316 \subsection{Signatures}
317 %*                                                                      *
318 %************************************************************************
319
320 @tcSigs@ checks the signatures for validity, and returns a list of
321 {\em freshly-instantiated} signatures.  That is, the types are already
322 split up, and have fresh type variables installed.  All non-type-signature
323 "RenamedSigs" are ignored.
324
325 The @TcSigInfo@ contains @TcTypes@ because they are unified with
326 the variable's type, and after that checked to see whether they've
327 been instantiated.
328
329 \begin{code}
330 data TcSigInfo
331   = TySigInfo       
332         Name                    -- N, the Name in corresponding binding
333
334         TcId                    -- *Polymorphic* binder for this value...
335                                 -- Has name = N
336
337         [TcTyVar]               -- tyvars
338         TcThetaType             -- theta
339         TcTauType               -- tau
340
341         TcId                    -- *Monomorphic* binder for this value
342                                 -- Does *not* have name = N
343                                 -- Has type tau
344
345         Inst                    -- Empty if theta is null, or 
346                                 -- (method mono_id) otherwise
347
348         SrcLoc                  -- Of the signature
349
350
351 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
352         -- Search for a particular signature
353 maybeSig [] name = Nothing
354 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
355   | name == sig_name = Just sig
356   | otherwise        = maybeSig sigs name
357
358 -- This little helper is useful to pass to tcPat
359 noSigs :: Name -> Maybe TcId
360 noSigs name = Nothing
361 \end{code}
362
363
364 \begin{code}
365 tcTySig :: RenamedSig -> TcM s TcSigInfo
366
367 tcTySig (Sig v ty src_loc)
368  = tcAddSrcLoc src_loc $
369    tcHsType ty                                  `thenTc` \ sigma_tc_ty ->
370    mkTcSig (mkUserId v sigma_tc_ty) src_loc     `thenNF_Tc` \ sig -> 
371    returnTc sig
372
373 mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
374 mkTcSig poly_id src_loc
375   =     -- Instantiate this type
376         -- It's important to do this even though in the error-free case
377         -- we could just split the sigma_tc_ty (since the tyvars don't
378         -- unified with anything).  But in the case of an error, when
379         -- the tyvars *do* get unified with something, we want to carry on
380         -- typechecking the rest of the program with the function bound
381         -- to a pristine type, namely sigma_tc_ty
382    let
383         (tyvars, rho) = splitForAllTys (idType poly_id)
384    in
385    mapNF_Tc tcInstSigVar tyvars         `thenNF_Tc` \ tyvars' ->
386         -- Make *signature* type variables
387
388    let
389      tyvar_tys' = mkTyVarTys tyvars'
390      rho' = fullSubstTy (zipVarEnv tyvars tyvar_tys') emptyVarSet rho
391      (theta', tau') = splitRhoTy rho'
392         -- This splitRhoTy tries hard to make sure that tau' is a type synonym
393         -- wherever possible, which can improve interface files.
394    in
395    newMethodWithGivenTy SignatureOrigin 
396                 poly_id
397                 tyvar_tys'
398                 theta' tau'                     `thenNF_Tc` \ inst ->
399         -- We make a Method even if it's not overloaded; no harm
400         
401    returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) inst src_loc)
402   where
403     name = idName poly_id
404 \end{code}
405
406
407
408 %************************************************************************
409 %*                                                                      *
410 \subsection{Checking signature type variables}
411 %*                                                                      *
412 %************************************************************************
413
414 @checkSigTyVars@ is used after the type in a type signature has been unified with
415 the actual type found.  It then checks that the type variables of the type signature
416 are
417         (a) Still all type variables
418                 eg matching signature [a] against inferred type [(p,q)]
419                 [then a will be unified to a non-type variable]
420
421         (b) Still all distinct
422                 eg matching signature [(a,b)] against inferred type [(p,p)]
423                 [then a and b will be unified together]
424
425         (c) Not mentioned in the environment
426                 eg the signature for f in this:
427
428                         g x = ... where
429                                         f :: a->[a]
430                                         f y = [x,y]
431
432                 Here, f is forced to be monorphic by the free occurence of x.
433
434         (d) Not (unified with another type variable that is) in scope.
435                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
436             when checking the expression type signature, we find that
437             even though there is nothing in scope whose type mentions r,
438             nevertheless the type signature for the expression isn't right.
439
440             Another example is in a class or instance declaration:
441                 class C a where
442                    op :: forall b. a -> b
443                    op x = x
444             Here, b gets unified with a
445
446 Before doing this, the substitution is applied to the signature type variable.
447
448 We used to have the notion of a "DontBind" type variable, which would
449 only be bound to itself or nothing.  Then points (a) and (b) were 
450 self-checking.  But it gave rise to bogus consequential error messages.
451 For example:
452
453    f = (*)      -- Monomorphic
454
455    g :: Num a => a -> a
456    g x = f x x
457
458 Here, we get a complaint when checking the type signature for g,
459 that g isn't polymorphic enough; but then we get another one when
460 dealing with the (Num x) context arising from f's definition;
461 we try to unify x with Int (to default it), but find that x has already
462 been unified with the DontBind variable "a" from g's signature.
463 This is really a problem with side-effecting unification; we'd like to
464 undo g's effects when its type signature fails, but unification is done
465 by side effect, so we can't (easily).
466
467 So we revert to ordinary type variables for signatures, and try to
468 give a helpful message in checkSigTyVars.
469
470 \begin{code}
471 checkSigTyVars :: [TcTyVar]             -- The original signature type variables
472                -> TcM s [TcTyVar]       -- Zonked signature type variables
473
474 checkSigTyVars [] = returnTc []
475
476 checkSigTyVars sig_tyvars
477   = zonkTcTyVars sig_tyvars             `thenNF_Tc` \ sig_tys ->
478     tcGetGlobalTyVars                   `thenNF_Tc` \ globals ->
479
480     checkTcM (all_ok sig_tys globals)
481              (complain sig_tys globals) `thenTc_`
482
483     returnTc (map (getTyVar "checkSigTyVars") sig_tys)
484
485   where
486     all_ok []       acc = True
487     all_ok (ty:tys) acc = case getTyVar_maybe ty of
488                             Nothing                       -> False      -- Point (a)
489                             Just tv | tv `elemVarSet` acc -> False      -- Point (b) or (c)
490                                     | otherwise           -> all_ok tys (acc `extendVarSet` tv)
491     
492
493     complain sig_tys globals
494       = -- For the in-scope ones, zonk them and construct a map
495         -- from the zonked tyvar to the in-scope one
496         -- If any of the in-scope tyvars zonk to a type, then ignore them;
497         -- that'll be caught later when we back up to their type sig
498         tcGetInScopeTyVars                      `thenNF_Tc` \ in_scope_tvs ->
499         zonkTcTyVars in_scope_tvs               `thenNF_Tc` \ in_scope_tys ->
500         let
501             in_scope_assoc = [ (zonked_tv, in_scope_tv) 
502                              | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
503                                Just zonked_tv <- [getTyVar_maybe z_ty]
504                              ]
505             in_scope_env = mkVarEnv in_scope_assoc
506         in
507
508         -- "check" checks each sig tyvar in turn
509         foldlNF_Tc check
510                    (env2, in_scope_env, [])
511                    (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
512
513         failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
514       where
515         (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
516         (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
517
518         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
519
520         check (env, acc, msgs) (sig_tyvar,ty)
521                 -- sig_tyvar is from the signature;
522                 -- ty is what you get if you zonk sig_tyvar and then tidy it
523                 --
524                 -- acc maps a zonked type variable back to a signature type variable
525           = case getTyVar_maybe ty of {
526               Nothing ->                        -- Error (a)!
527                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
528
529               Just tv ->
530
531             case lookupVarEnv acc tv of {
532                 Just sig_tyvar' ->      -- Error (b) or (d)!
533                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
534
535                 Nothing ->
536
537             if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
538                                         -- The least comprehensible, so put it last
539             then   tcGetValueEnv                        `thenNF_Tc` \ ve ->
540                    find_globals tv env (eltsUFM ve)     `thenNF_Tc` \ (env1, globs) ->
541                    returnNF_Tc (env1, acc, escape_msg sig_tyvar tv globs : msgs)
542
543             else        -- All OK
544             returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
545             }}
546
547 -- find_globals looks at the value environment and finds values
548 -- whose types mention the offending type variable.  It has to be 
549 -- careful to zonk the Id's type first, so it has to be in the monad.
550 -- We must be careful to pass it a zonked type variable, too.
551 find_globals tv tidy_env ids
552   | null ids
553   = returnNF_Tc (tidy_env, [])
554
555 find_globals tv tidy_env (id:ids) 
556   | not (isLocallyDefined id) ||
557     isEmptyVarSet (idFreeTyVars id)
558   = find_globals tv tidy_env ids
559
560   | otherwise
561   = zonkTcType (idType id)      `thenNF_Tc` \ id_ty ->
562     if tv `elemVarSet` tyVarsOfType id_ty then
563         let 
564            (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
565         in
566         find_globals tv tidy_env' ids   `thenNF_Tc` \ (tidy_env'', globs) ->
567         returnNF_Tc (tidy_env'', (idName id, id_ty') : globs)
568     else
569         find_globals tv tidy_env ids
570
571 escape_msg sig_tv tv globs
572   = vcat [mk_msg sig_tv <+> ptext SLIT("escapes"),
573           pp_escape,
574           ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
575           nest 4 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
576     ]
577   where
578     pp_escape | sig_tv /= tv = ptext SLIT("It unifies with") <+>
579                                quotes (ppr tv) <> comma <+>
580                                ptext SLIT("which is mentioned in the environment")
581               | otherwise    = ptext SLIT("It is mentioned in the environment")
582
583     vcat_first :: Int -> [SDoc] -> SDoc
584     vcat_first n []     = empty
585     vcat_first 0 (x:xs) = text "...others omitted..."
586     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
587
588 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
589 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
590 \end{code}
591
592 These two context are used with checkSigTyVars
593     
594 \begin{code}
595 sigCtxt :: (Type -> Message) -> Type
596         -> TidyEnv -> NF_TcM s (TidyEnv, Message)
597 sigCtxt mk_msg sig_ty tidy_env
598   = let
599         (env1, tidy_sig_ty) = tidyOpenType tidy_env sig_ty
600     in
601     returnNF_Tc (env1, mk_msg tidy_sig_ty)
602
603 sigPatCtxt bound_tvs bound_ids tidy_env
604   = returnNF_Tc (env1,
605                  sep [ptext SLIT("When checking a pattern that binds"),
606                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
607   where
608     show_ids = filter is_interesting bound_ids
609     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
610
611     (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
612     ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
613         -- Don't zonk the types so we get the separate, un-unified versions
614 \end{code}
615
616
617 %************************************************************************
618 %*                                                                      *
619 \subsection{Errors and contexts}
620 %*                                                                      *
621 %************************************************************************
622
623 \begin{code}
624 naughtyCCallContextErr clas_name
625   = sep [ptext SLIT("Can't use class") <+> quotes (ppr clas_name), 
626          ptext SLIT("in a context")]
627
628 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
629
630 typeKindCtxt :: RenamedHsType -> Message
631 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
632                        nest 2 (quotes (ppr ty)),
633                        ptext SLIT("is a type")]
634
635 appKindCtxt :: SDoc -> Message
636 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
637
638 classAsTyConErr name
639   = ptext SLIT("Class used as a type constructor:") <+> ppr name
640
641 tyConAsClassErr name
642   = ptext SLIT("Type constructor used as a class:") <+> ppr name
643
644 tyVarAsClassErr name
645   = ptext SLIT("Type variable used as a class:") <+> ppr name
646 \end{code}