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