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