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, tcInstTcType, kindToTcKind,
  26                           newKindVar,
  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, splitRhoTy,
  34                           boxedTypeKind, unboxedTypeKind, tyVarsOfType,
  35                           mkArrowKinds, getTyVar_maybe, getTyVar,
  36                           tidyOpenType, tidyOpenTypes, tidyTyVar
  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    tcInstTcType (idType poly_id)                `thenNF_Tc` \ (tyvars, rho) ->
 383    let
 384      (theta, tau) = splitRhoTy rho
 385         -- This splitSigmaTy tries hard to make sure that tau' is a type synonym
 386         -- wherever possible, which can improve interface files.
 387    in
 388    newMethodWithGivenTy SignatureOrigin
 389                 poly_id
 390                 (mkTyVarTys tyvars)
 391                 theta tau                       `thenNF_Tc` \ inst ->
 392         -- We make a Method even if it's not overloaded; no harm
 393
 394    returnNF_Tc (TySigInfo name poly_id tyvars theta tau (instToIdBndr inst) inst src_loc)
 395   where
 396     name = idName poly_id
 397 \end{code}
 398
 399
 400
 401 %************************************************************************
 402 %*                                                                      *
 403 \subsection{Checking signature type variables}
 404 %*                                                                      *
 405 %************************************************************************
 406
 407 @checkSigTyVars@ is used after the type in a type signature has been unified with
 408 the actual type found.  It then checks that the type variables of the type signature
 409 are
 410         (a) Still all type variables
 411                 eg matching signature [a] against inferred type [(p,q)]
 412                 [then a will be unified to a non-type variable]
 413
 414         (b) Still all distinct
 415                 eg matching signature [(a,b)] against inferred type [(p,p)]
 416                 [then a and b will be unified together]
 417
 418         (c) Not mentioned in the environment
 419                 eg the signature for f in this:
 420
 421                         g x = ... where
 422                                         f :: a->[a]
 423                                         f y = [x,y]
 424
 425                 Here, f is forced to be monorphic by the free occurence of x.
 426
 427         (d) Not (unified with another type variable that is) in scope.
 428                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
 429             when checking the expression type signature, we find that
 430             even though there is nothing in scope whose type mentions r,
 431             nevertheless the type signature for the expression isn't right.
 432
 433             Another example is in a class or instance declaration:
 434                 class C a where
 435                    op :: forall b. a -> b
 436                    op x = x
 437             Here, b gets unified with a
 438
 439 Before doing this, the substitution is applied to the signature type variable.
 440
 441 We used to have the notion of a "DontBind" type variable, which would
 442 only be bound to itself or nothing.  Then points (a) and (b) were
 443 self-checking.  But it gave rise to bogus consequential error messages.
 444 For example:
 445
 446    f = (*)      -- Monomorphic
 447
 448    g :: Num a => a -> a
 449    g x = f x x
 450
 451 Here, we get a complaint when checking the type signature for g,
 452 that g isn't polymorphic enough; but then we get another one when
 453 dealing with the (Num x) context arising from f's definition;
 454 we try to unify x with Int (to default it), but find that x has already
 455 been unified with the DontBind variable "a" from g's signature.
 456 This is really a problem with side-effecting unification; we'd like to
 457 undo g's effects when its type signature fails, but unification is done
 458 by side effect, so we can't (easily).
 459
 460 So we revert to ordinary type variables for signatures, and try to
 461 give a helpful message in checkSigTyVars.
 462
 463 \begin{code}
 464 checkSigTyVars :: [TcTyVar]             -- The original signature type variables
 465                -> TcM s [TcTyVar]       -- Zonked signature type variables
 466
 467 checkSigTyVars [] = returnTc []
 468
 469 checkSigTyVars sig_tyvars
 470   = zonkTcTyVars sig_tyvars             `thenNF_Tc` \ sig_tys ->
 471     tcGetGlobalTyVars                   `thenNF_Tc` \ globals ->
 472
 473     checkTcM (all_ok sig_tys globals)
 474              (complain sig_tys globals) `thenTc_`
 475
 476     returnTc (map (getTyVar "checkSigTyVars") sig_tys)
 477
 478   where
 479     all_ok []       acc = True
 480     all_ok (ty:tys) acc = case getTyVar_maybe ty of
 481                             Nothing                       -> False      -- Point (a)
 482                             Just tv | tv `elemVarSet` acc -> False      -- Point (b) or (c)
 483                                     | otherwise           -> all_ok tys (acc `extendVarSet` tv)
 484
 485
 486     complain sig_tys globals
 487       = -- For the in-scope ones, zonk them and construct a map
 488         -- from the zonked tyvar to the in-scope one
 489         -- If any of the in-scope tyvars zonk to a type, then ignore them;
 490         -- that'll be caught later when we back up to their type sig
 491         tcGetInScopeTyVars                      `thenNF_Tc` \ in_scope_tvs ->
 492         zonkTcTyVars in_scope_tvs               `thenNF_Tc` \ in_scope_tys ->
 493         let
 494             in_scope_assoc = [ (zonked_tv, in_scope_tv)
 495                              | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
 496                                Just zonked_tv <- [getTyVar_maybe z_ty]
 497                              ]
 498             in_scope_env = mkVarEnv in_scope_assoc
 499         in
 500
 501         -- "check" checks each sig tyvar in turn
 502         foldlNF_Tc check
 503                    (env2, in_scope_env, [])
 504                    (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
 505
 506         failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
 507       where
 508         (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
 509         (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
 510
 511         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
 512
 513         check (env, acc, msgs) (sig_tyvar,ty)
 514                 -- sig_tyvar is from the signature;
 515                 -- ty is what you get if you zonk sig_tyvar and then tidy it
 516                 --
 517                 -- acc maps a zonked type variable back to a signature type variable
 518           = case getTyVar_maybe ty of {
 519               Nothing ->                        -- Error (a)!
 520                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
 521
 522               Just tv ->
 523
 524             case lookupVarEnv acc tv of {
 525                 Just sig_tyvar' ->      -- Error (b) or (d)!
 526                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
 527
 528                 Nothing ->
 529
 530             if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
 531                                         -- The least comprehensible, so put it last
 532             then   tcGetValueEnv                        `thenNF_Tc` \ ve ->
 533                    find_globals tv env (eltsUFM ve)     `thenNF_Tc` \ (env1, globs) ->
 534                    returnNF_Tc (env1, acc, escape_msg sig_tyvar tv globs : msgs)
 535
 536             else        -- All OK
 537             returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
 538             }}
 539
 540 -- find_globals looks at the value environment and finds values
 541 -- whose types mention the offending type variable.  It has to be
 542 -- careful to zonk the Id's type first, so it has to be in the monad.
 543 -- We must be careful to pass it a zonked type variable, too.
 544 find_globals tv tidy_env ids
 545   | null ids
 546   = returnNF_Tc (tidy_env, [])
 547
 548 find_globals tv tidy_env (id:ids)
 549   | not (isLocallyDefined id) ||
 550     isEmptyVarSet (idFreeTyVars id)
 551   = find_globals tv tidy_env ids
 552
 553   | otherwise
 554   = zonkTcType (idType id)      `thenNF_Tc` \ id_ty ->
 555     if tv `elemVarSet` tyVarsOfType id_ty then
 556         let
 557            (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
 558         in
 559         find_globals tv tidy_env' ids   `thenNF_Tc` \ (tidy_env'', globs) ->
 560         returnNF_Tc (tidy_env'', (idName id, id_ty') : globs)
 561     else
 562         find_globals tv tidy_env ids
 563
 564 escape_msg sig_tv tv globs
 565   = vcat [mk_msg sig_tv <+> ptext SLIT("escapes"),
 566           pp_escape,
 567           ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
 568           nest 4 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
 569     ]
 570   where
 571     pp_escape | sig_tv /= tv = ptext SLIT("It unifies with") <+>
 572                                quotes (ppr tv) <> comma <+>
 573                                ptext SLIT("which is mentioned in the environment")
 574               | otherwise    = ptext SLIT("It is mentioned in the environment")
 575
 576     vcat_first :: Int -> [SDoc] -> SDoc
 577     vcat_first n []     = empty
 578     vcat_first 0 (x:xs) = text "...others omitted..."
 579     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
 580
 581 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
 582 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 583 \end{code}
 584
 585 These two context are used with checkSigTyVars
 586
 587 \begin{code}
 588 sigCtxt :: (Type -> Message) -> Type
 589         -> TidyEnv -> NF_TcM s (TidyEnv, Message)
 590 sigCtxt mk_msg sig_ty tidy_env
 591   = let
 592         (env1, tidy_sig_ty) = tidyOpenType tidy_env sig_ty
 593     in
 594     returnNF_Tc (env1, mk_msg tidy_sig_ty)
 595
 596 sigPatCtxt bound_tvs bound_ids tidy_env
 597   = returnNF_Tc (env1,
 598                  sep [ptext SLIT("When checking a pattern that binds"),
 599                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
 600   where
 601     show_ids = filter is_interesting bound_ids
 602     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
 603
 604     (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
 605     ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
 606         -- Don't zonk the types so we get the separate, un-unified versions
 607 \end{code}
 608
 609
 610 %************************************************************************
 611 %*                                                                      *
 612 \subsection{Errors and contexts}
 613 %*                                                                      *
 614 %************************************************************************
 615
 616 \begin{code}
 617 naughtyCCallContextErr clas_name
 618   = sep [ptext SLIT("Can't use class") <+> quotes (ppr clas_name),
 619          ptext SLIT("in a context")]
 620
 621 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
 622
 623 typeKindCtxt :: RenamedHsType -> Message
 624 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
 625                        nest 2 (quotes (ppr ty)),
 626                        ptext SLIT("is a type")]
 627
 628 appKindCtxt :: SDoc -> Message
 629 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 630
 631 classAsTyConErr name
 632   = ptext SLIT("Class used as a type constructor:") <+> ppr name
 633
 634 tyConAsClassErr name
 635   = ptext SLIT("Type constructor used as a class:") <+> ppr name
 636
 637 tyVarAsClassErr name
 638   = ptext SLIT("Type variable used as a class:") <+> ppr name
 639 \end{code}