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