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