[project @ 2000-06-18 08:37:17 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
index 6569592..2e6a570 100644 (file)
@@ -4,8 +4,8 @@
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}
-module TcMonoType ( tcHsType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType, tcHsTopTypeKind,
-                   tcContext, tcHsTyVar, kcHsTyVar,
+module TcMonoType ( tcHsType, tcHsSigType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType, tcHsTopTypeKind,
+                   tcContext, tcHsTyVar, kcHsTyVar, kcHsType,
                    tcExtendTyVarScope, tcExtendTopTyVarScope,
                    TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
                    checkSigTyVars, sigCtxt, sigPatCtxt
@@ -13,46 +13,51 @@ module TcMonoType ( tcHsType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType, tcHsT
 
 #include "HsVersions.h"
 
-import HsSyn           ( HsType(..), HsTyVar(..), MonoUsageAnn(..),
-                          Sig(..), pprClassAssertion, pprParendHsType )
+import HsSyn           ( HsType(..), HsTyVarBndr(..), HsUsageAnn(..),
+                          Sig(..), HsPred(..), pprParendHsType, HsTupCon(..) )
 import RnHsSyn         ( RenamedHsType, RenamedContext, RenamedSig )
 import TcHsSyn         ( TcId )
 
 import TcMonad
 import TcEnv           ( tcExtendTyVarEnv, tcLookupTy, tcGetValueEnv, tcGetInScopeTyVars,
                           tcExtendUVarEnv, tcLookupUVar,
-                         tcGetGlobalTyVars, TcTyThing(..)
+                         tcGetGlobalTyVars, valueEnvIds, TcTyThing(..)
                        )
 import TcType          ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
                          typeToTcType, kindToTcKind,
                          newKindVar, tcInstSigVar,
-                         zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType
+                         zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType, zonkTcTyVar
                        )
-import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr )
+import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr,
+                         instFunDeps, instFunDepsOfTheta )
+import FunDeps         ( tyVarFunDep, oclose )
 import TcUnify         ( unifyKind, unifyKinds, unifyTypeKind )
-import Type            ( Type, ThetaType, UsageAnn(..),
+import Type            ( Type, PredType(..), ThetaType, UsageAnn(..),
                          mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
-                          mkUsForAllTy, zipFunTys,
-                         mkSigmaTy, mkDictTy, mkTyConApp, mkAppTys, splitForAllTys, splitRhoTy,
-                         boxedTypeKind, unboxedTypeKind, tyVarsOfType,
+                          mkUsForAllTy, zipFunTys, hoistForAllTys,
+                         mkSigmaTy, mkDictTy, mkPredTy, mkTyConApp,
+                         mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
+                         boxedTypeKind, unboxedTypeKind, 
                          mkArrowKinds, getTyVar_maybe, getTyVar,
-                         tidyOpenType, tidyOpenTypes, tidyTyVar
+                         tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
+                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, mkForAllTys
                        )
+import PprType         ( pprConstraint, pprType, pprPred )
 import Subst           ( mkTopTyVarSubst, substTy )
 import Id              ( mkVanillaId, idName, idType, idFreeTyVars )
-import Var             ( TyVar, mkTyVar, mkNamedUVar )
+import Var             ( TyVar, mkTyVar, mkNamedUVar, varName )
 import VarEnv
 import VarSet
 import Bag             ( bagToList )
 import ErrUtils                ( Message )
-import PrelInfo                ( cCallishClassKeys )
 import TyCon           ( TyCon )
 import Name            ( Name, OccName, isLocallyDefined )
-import TysWiredIn      ( mkListTy, mkTupleTy, mkUnboxedTupleTy )
+import TysWiredIn      ( mkListTy, mkTupleTy )
+import UniqFM          ( elemUFM, foldUFM )
+import BasicTypes      ( Boxity(..) )
 import SrcLoc          ( SrcLoc )
 import Unique          ( Unique, Uniquable(..) )
-import UniqFM          ( eltsUFM )
-import Util            ( zipWithEqual, zipLazy, mapAccumL )
+import Util            ( mapAccumL, isSingleton, removeDups )
 import Outputable
 \end{code}
 
@@ -69,6 +74,18 @@ tcHsType and tcHsTypeKind
 tcHsType checks that the type really is of kind Type!
 
 \begin{code}
+kcHsType :: RenamedHsType -> TcM c ()
+  -- Kind-check the type
+kcHsType ty = tc_type ty       `thenTc_`
+             returnTc ()
+
+tcHsSigType :: RenamedHsType -> TcM s TcType
+  -- Used for type sigs written by the programmer
+  -- Hoist any inner for-alls to the top
+tcHsSigType ty
+  = tcHsType ty                `thenTc` \ ty' ->
+    returnTc (hoistForAllTys ty')
+
 tcHsType :: RenamedHsType -> TcM s TcType
 tcHsType ty
   = -- tcAddErrCtxt (typeCtxt ty)              $
@@ -97,20 +114,22 @@ tcHsTopType :: RenamedHsType -> TcM s Type
 tcHsTopType ty
   = -- tcAddErrCtxt (typeCtxt ty)              $
     tc_type ty                         `thenTc` \ ty' ->
-    forkNF_Tc (zonkTcTypeToType ty')
+    forkNF_Tc (zonkTcTypeToType ty')   `thenTc` \ ty'' ->
+    returnTc (hoistForAllTys ty'')
+
+tcHsTopBoxedType :: RenamedHsType -> TcM s Type
+tcHsTopBoxedType ty
+  = -- tcAddErrCtxt (typeCtxt ty)              $
+    tc_boxed_type ty                   `thenTc` \ ty' ->
+    forkNF_Tc (zonkTcTypeToType ty')   `thenTc` \ ty'' ->
+    returnTc (hoistForAllTys ty'')
 
 tcHsTopTypeKind :: RenamedHsType -> TcM s (TcKind, Type)
 tcHsTopTypeKind ty
   = -- tcAddErrCtxt (typeCtxt ty)              $
     tc_type_kind ty                            `thenTc` \ (kind, ty') ->
     forkNF_Tc (zonkTcTypeToType ty')           `thenTc` \ zonked_ty ->
-    returnNF_Tc (kind, zonked_ty)
-
-tcHsTopBoxedType :: RenamedHsType -> TcM s Type
-tcHsTopBoxedType ty
-  = -- tcAddErrCtxt (typeCtxt ty)              $
-    tc_boxed_type ty                   `thenTc` \ ty' ->
-    forkNF_Tc (zonkTcTypeToType ty')
+    returnNF_Tc (kind, hoistForAllTys zonked_ty)
 \end{code}
 
 
@@ -136,45 +155,45 @@ tc_type ty
     returnTc tc_ty
 
 tc_type_kind :: RenamedHsType -> TcM s (TcKind, Type)
-tc_type_kind ty@(MonoTyVar name)
+tc_type_kind ty@(HsTyVar name)
   = tc_app ty []
-    
-tc_type_kind (MonoListTy ty)
+
+tc_type_kind (HsListTy ty)
   = tc_boxed_type ty           `thenTc` \ tau_ty ->
     returnTc (boxedTypeKind, mkListTy tau_ty)
 
-tc_type_kind (MonoTupleTy tys True {-boxed-})
+tc_type_kind (HsTupleTy (HsTupCon _ Boxed) tys)
   = mapTc tc_boxed_type tys    `thenTc` \ tau_tys ->
-    returnTc (boxedTypeKind, mkTupleTy (length tys) tau_tys)
+    returnTc (boxedTypeKind, mkTupleTy Boxed (length tys) tau_tys)
 
-tc_type_kind (MonoTupleTy tys False {-unboxed-})
+tc_type_kind (HsTupleTy (HsTupCon _ Unboxed) tys)
   = mapTc tc_type tys                  `thenTc` \ tau_tys ->
-    returnTc (unboxedTypeKind, mkUnboxedTupleTy (length tys) tau_tys)
+    returnTc (unboxedTypeKind, mkTupleTy Unboxed (length tys) tau_tys)
 
-tc_type_kind (MonoFunTy ty1 ty2)
+tc_type_kind (HsFunTy ty1 ty2)
   = tc_type ty1        `thenTc` \ tau_ty1 ->
     tc_type ty2        `thenTc` \ tau_ty2 ->
     returnTc (boxedTypeKind, mkFunTy tau_ty1 tau_ty2)
 
-tc_type_kind (MonoTyApp ty1 ty2)
+tc_type_kind (HsAppTy ty1 ty2)
   = tc_app ty1 [ty2]
 
-tc_type_kind (MonoDictTy class_name tys)
-  = tcClassAssertion (class_name, tys) `thenTc` \ (clas, arg_tys) ->
-    returnTc (boxedTypeKind, mkDictTy clas arg_tys)
+tc_type_kind (HsPredTy pred)
+  = tcClassAssertion True pred `thenTc` \ pred' ->
+    returnTc (boxedTypeKind, mkPredTy pred')
 
-tc_type_kind (MonoUsgTy usg ty)
+tc_type_kind (HsUsgTy usg ty)
   = newUsg usg                          `thenTc` \ usg' ->
     tc_type_kind ty                     `thenTc` \ (kind, tc_ty) ->
     returnTc (kind, mkUsgTy usg' tc_ty)
   where
     newUsg usg = case usg of
-                   MonoUsOnce        -> returnTc UsOnce
-                   MonoUsMany        -> returnTc UsMany
-                   MonoUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
+                   HsUsOnce        -> returnTc UsOnce
+                   HsUsMany        -> returnTc UsMany
+                   HsUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
                                         returnTc (UsVar uv)
 
-tc_type_kind (MonoUsgForAllTy uv_name ty)
+tc_type_kind (HsUsgForAllTy uv_name ty)
   = let
         uv = mkNamedUVar uv_name
     in
@@ -183,7 +202,7 @@ tc_type_kind (MonoUsgForAllTy uv_name ty)
       returnTc (kind, mkUsForAllTy uv tc_ty)
 
 tc_type_kind (HsForAllTy (Just tv_names) context ty)
-  = tcExtendTyVarScope tv_names                $ \ tyvars -> 
+  = tcExtendTyVarScope tv_names                $ \ forall_tyvars ->
     tcContext context                  `thenTc` \ theta ->
     tc_type_kind ty                    `thenTc` \ (kind, tau) ->
     let
@@ -194,15 +213,67 @@ tc_type_kind (HsForAllTy (Just tv_names) context ty)
                -- give overloaded functions like
                --      f :: forall a. Num a => (# a->a, a->a #)
                -- And we want these to get through the type checker
+
+       -- Check for ambiguity
+       --   forall V. P => tau
+       -- is ambiguous if P contains generic variables
+       -- (i.e. one of the Vs) that are not mentioned in tau
+       --
+       -- However, we need to take account of functional dependencies
+       -- when we speak of 'mentioned in tau'.  Example:
+       --      class C a b | a -> b where ...
+       -- Then the type
+       --      forall x y. (C x y) => x
+       -- is not ambiguous because x is mentioned and x determines y
+       --
+       -- NOTE: In addition, GHC insists that at least one type variable
+       -- in each constraint is in V.  So we disallow a type like
+       --      forall a. Eq b => b -> b
+       -- even in a scope where b is in scope.
+       -- This is the is_free test below.
+
+       tau_vars            = tyVarsOfType tau
+       fds                 = instFunDepsOfTheta theta
+       tvFundep            = tyVarFunDep fds
+       extended_tau_vars   = oclose tvFundep tau_vars
+       is_ambig ct_var     = (ct_var `elem` forall_tyvars) &&
+                             not (ct_var `elemUFM` extended_tau_vars)
+       is_free ct_var      = not (ct_var `elem` forall_tyvars)
+
+       check_pred pred = checkTc (not any_ambig) (ambigErr pred ty) `thenTc_`
+                         checkTc (not all_free)  (freeErr  pred ty)
+             where 
+               ct_vars   = varSetElems (tyVarsOfPred pred)
+               any_ambig = is_source_polytype && any is_ambig ct_vars
+               all_free  = all is_free  ct_vars
+
+       -- Check ambiguity only for source-program types, not
+       -- for types coming from inteface files.  The latter can
+       -- legitimately have ambiguous types. Example
+       --    class S a where s :: a -> (Int,Int)
+       --    instance S Char where s _ = (1,1)
+       --    f:: S a => [a] -> Int -> (Int,Int)
+       --    f (_::[a]) x = (a*x,b)
+       --      where (a,b) = s (undefined::a)
+       -- Here the worker for f gets the type
+       --      fw :: forall a. S a => Int -> (# Int, Int #)
+       --
+       -- If the list of tv_names is empty, we have a monotype,
+       -- and then we don't need to check for ambiguity either,
+       -- because the test can't fail (see is_ambig).
+       is_source_polytype = case tv_names of
+                               (UserTyVar _ : _) -> True
+                               other             -> False
     in
-    returnTc (body_kind, mkSigmaTy tyvars theta tau)
+    mapTc check_pred theta             `thenTc_`
+    returnTc (body_kind, mkSigmaTy forall_tyvars theta tau)
 \end{code}
 
 Help functions for type applications
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 \begin{code}
-tc_app (MonoTyApp ty1 ty2) tys
+tc_app (HsAppTy ty1 ty2) tys
   = tc_app ty1 (ty2:tys)
 
 tc_app ty tys
@@ -226,16 +297,16 @@ tc_app ty tys
 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 --     hence the rather strange functionality.
 
-tc_fun_type (MonoTyVar name) arg_tys
-  = tcLookupTy name                    `thenTc` \ (tycon_kind, maybe_arity, thing) ->
+tc_fun_type (HsTyVar name) arg_tys
+  = tcLookupTy name                    `thenTc` \ (tycon_kind, thing) ->
     case thing of
-       ATyVar tv   -> returnTc (tycon_kind, mkAppTys (mkTyVarTy tv) arg_tys)
-       AClass clas -> failWithTc (classAsTyConErr name)
-       ATyCon tc   -> case maybe_arity of
-                        Nothing ->     -- Data or newtype
-                                       returnTc (tycon_kind, mkTyConApp tc arg_tys)
+       ATyVar tv     -> returnTc (tycon_kind, mkAppTys (mkTyVarTy tv) arg_tys)
+       AClass clas _ -> failWithTc (classAsTyConErr name)
+
+       ADataTyCon tc ->  -- Data or newtype
+                         returnTc (tycon_kind, mkTyConApp tc arg_tys)
 
-                        Just arity ->  -- Type synonym
+       ASynTyCon tc arity ->   -- Type synonym
                                  checkTc (arity <= n_args) err_msg     `thenTc_`
                                  returnTc (tycon_kind, result_ty)
                           where
@@ -259,41 +330,27 @@ Contexts
 \begin{code}
 
 tcContext :: RenamedContext -> TcM s ThetaType
-tcContext context
-  =    --Someone discovered that @CCallable@ and @CReturnable@
-       -- could be used in contexts such as:
-       --      foo :: CCallable a => a -> PrimIO Int
-       -- Doing this utterly wrecks the whole point of introducing these
-       -- classes so we specifically check that this isn't being done.
-       --
-       -- We *don't* do this check in tcClassAssertion, because that's
-       -- called when checking a HsDictTy, and we don't want to reject
-       --      instance CCallable Int 
-       -- etc. Ugh!
-    mapTc check_naughty context `thenTc_`
-
-    mapTc tcClassAssertion context
+tcContext context = mapTc (tcClassAssertion False) context
 
- where
-   check_naughty (class_name, _) 
-     = checkTc (not (getUnique class_name `elem` cCallishClassKeys))
-              (naughtyCCallContextErr class_name)
-
-tcClassAssertion assn@(class_name, tys)
-  = tcAddErrCtxt (appKindCtxt (pprClassAssertion assn))        $
-    mapAndUnzipTc tc_type_kind tys     `thenTc` \ (arg_kinds, arg_tys) ->
-    tcLookupTy class_name              `thenTc` \ (kind, ~(Just arity), thing) ->
+tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
+  = tcAddErrCtxt (appKindCtxt (ppr assn))      $
+    mapAndUnzipTc tc_type_kind tys             `thenTc` \ (arg_kinds, arg_tys) ->
+    tcLookupTy class_name                      `thenTc` \ (kind, thing) ->
     case thing of
-       ATyVar  _   -> failWithTc (tyVarAsClassErr class_name)
-       ATyCon  _   -> failWithTc (tyConAsClassErr class_name)
-       AClass clas ->
+       AClass clas arity ->
                        -- Check with kind mis-match
                checkTc (arity == n_tys) err                            `thenTc_`
                unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)   `thenTc_`
-               returnTc (clas, arg_tys)
+               returnTc (Class clas arg_tys)
            where
                n_tys = length tys
                err   = arityErr "Class" class_name arity n_tys
+       other -> failWithTc (tyVarAsClassErr class_name)
+
+tcClassAssertion ccall_ok assn@(HsPIParam name ty)
+  = tcAddErrCtxt (appKindCtxt (ppr assn))      $
+    tc_type_kind ty    `thenTc` \ (arg_kind, arg_ty) ->
+    returnTc (IParam name arg_ty)
 \end{code}
 
 
@@ -304,7 +361,7 @@ tcClassAssertion assn@(class_name, tys)
 %************************************************************************
 
 \begin{code}
-tcExtendTopTyVarScope :: TcKind -> [HsTyVar Name]
+tcExtendTopTyVarScope :: TcKind -> [HsTyVarBndr Name]
                      -> ([TcTyVar] -> TcKind -> TcM s a)
                      -> TcM s a
 tcExtendTopTyVarScope kind tyvar_names thing_inside
@@ -318,14 +375,14 @@ tcExtendTopTyVarScope kind tyvar_names thing_inside
     mk_tv (IfaceTyVar name _, kind) = mkTyVar name kind
        -- NB: immutable tyvars, but perhaps with mutable kinds
 
-tcExtendTyVarScope :: [HsTyVar Name] 
+tcExtendTyVarScope :: [HsTyVarBndr Name] 
                   -> ([TcTyVar] -> TcM s a) -> TcM s a
 tcExtendTyVarScope tv_names thing_inside
   = mapNF_Tc tcHsTyVar tv_names        `thenNF_Tc` \ tyvars ->
     tcExtendTyVarEnv tyvars            $
     thing_inside tyvars
     
-tcHsTyVar :: HsTyVar Name -> NF_TcM s TcTyVar
+tcHsTyVar :: HsTyVarBndr Name -> NF_TcM s TcTyVar
 tcHsTyVar (UserTyVar name)       = newKindVar          `thenNF_Tc` \ kind ->
                                   tcNewMutTyVar name kind
        -- NB: mutable kind => mutable tyvar, so that zonking can bind
@@ -333,7 +390,7 @@ tcHsTyVar (UserTyVar name)       = newKindVar               `thenNF_Tc` \ kind ->
 
 tcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (mkTyVar name (kindToTcKind kind))
 
-kcHsTyVar :: HsTyVar name -> NF_TcM s TcKind
+kcHsTyVar :: HsTyVarBndr name -> NF_TcM s TcKind
 kcHsTyVar (UserTyVar name)       = newKindVar
 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (kindToTcKind kind)
 \end{code}
@@ -370,11 +427,14 @@ data TcSigInfo
                                -- Does *not* have name = N
                                -- Has type tau
 
-       Inst                    -- Empty if theta is null, or 
+       [Inst]                  -- Empty if theta is null, or
                                -- (method mono_id) otherwise
 
        SrcLoc                  -- Of the signature
 
+instance Outputable TcSigInfo where
+    ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
+       ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
 
 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
        -- Search for a particular signature
@@ -389,8 +449,9 @@ maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
 tcTySig :: RenamedSig -> TcM s TcSigInfo
 
 tcTySig (Sig v ty src_loc)
- = tcAddSrcLoc src_loc $
-   tcHsType ty                                 `thenTc` \ sigma_tc_ty ->
+ = tcAddSrcLoc src_loc                         $ 
+   tcAddErrCtxt (tcsigCtxt v)                  $
+   tcHsSigType ty                              `thenTc` \ sigma_tc_ty ->
    mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig -> 
    returnTc sig
 
@@ -422,8 +483,9 @@ mkTcSig poly_id src_loc
                tyvar_tys'
                theta' tau'                     `thenNF_Tc` \ inst ->
        -- We make a Method even if it's not overloaded; no harm
+   instFunDeps SignatureOrigin theta'          `thenNF_Tc` \ fds ->
        
-   returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) inst src_loc)
+   returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
   where
     name = idName poly_id
 \end{code}
@@ -493,12 +555,15 @@ So we revert to ordinary type variables for signatures, and try to
 give a helpful message in checkSigTyVars.
 
 \begin{code}
-checkSigTyVars :: [TcTyVar]            -- The original signature type variables
+checkSigTyVars :: [TcTyVar]            -- Universally-quantified type variables in the signature
+              -> TcTyVarSet            -- Tyvars that are free in the type signature
+                                       -- These should *already* be in the global-var set, and are
+                                       -- used here only to improve the error message
               -> TcM s [TcTyVar]       -- Zonked signature type variables
 
-checkSigTyVars [] = returnTc []
+checkSigTyVars [] free = returnTc []
 
-checkSigTyVars sig_tyvars
+checkSigTyVars sig_tyvars free_tyvars
   = zonkTcTyVars sig_tyvars            `thenNF_Tc` \ sig_tys ->
     tcGetGlobalTyVars                  `thenNF_Tc` \ globals ->
 
@@ -561,9 +626,10 @@ checkSigTyVars sig_tyvars
 
            if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
                                        -- The least comprehensible, so put it last
-           then   tcGetValueEnv                        `thenNF_Tc` \ ve ->
-                  find_globals tv env (eltsUFM ve)     `thenNF_Tc` \ (env1, globs) ->
-                  returnNF_Tc (env1, acc, escape_msg sig_tyvar tv globs : msgs)
+           then   tcGetValueEnv                                        `thenNF_Tc` \ ve ->
+                  find_globals tv env  [] (valueEnvIds ve)             `thenNF_Tc` \ (env1, globs) ->
+                  find_frees   tv env1 [] (varSetElems free_tyvars)    `thenNF_Tc` \ (env2, frees) ->
+                  returnNF_Tc (env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
 
            else        -- All OK
            returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
@@ -573,37 +639,57 @@ checkSigTyVars sig_tyvars
 -- whose types mention the offending type variable.  It has to be 
 -- careful to zonk the Id's type first, so it has to be in the monad.
 -- We must be careful to pass it a zonked type variable, too.
-find_globals tv tidy_env ids
-  | null ids
-  = returnNF_Tc (tidy_env, [])
+find_globals tv tidy_env acc []
+  = returnNF_Tc (tidy_env, acc)
 
-find_globals tv tidy_env (id:ids) 
+find_globals tv tidy_env acc (id:ids) 
   | not (isLocallyDefined id) ||
     isEmptyVarSet (idFreeTyVars id)
-  = find_globals tv tidy_env ids
+  = find_globals tv tidy_env acc ids
 
   | otherwise
   = zonkTcType (idType id)     `thenNF_Tc` \ id_ty ->
     if tv `elemVarSet` tyVarsOfType id_ty then
        let 
           (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
+          acc'                = (idName id, id_ty') : acc
        in
-       find_globals tv tidy_env' ids   `thenNF_Tc` \ (tidy_env'', globs) ->
-       returnNF_Tc (tidy_env'', (idName id, id_ty') : globs)
+       find_globals tv tidy_env' acc' ids
     else
-       find_globals tv tidy_env ids
+       find_globals tv tidy_env  acc  ids
 
-escape_msg sig_tv tv globs
-  = vcat [mk_msg sig_tv <+> ptext SLIT("escapes"),
-         pp_escape,
-         ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
-         nest 4 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
-    ]
+find_frees tv tidy_env acc []
+  = returnNF_Tc (tidy_env, acc)
+find_frees tv tidy_env acc (ftv:ftvs)
+  = zonkTcTyVar ftv    `thenNF_Tc` \ ty ->
+    if tv `elemVarSet` tyVarsOfType ty then
+       let
+           (tidy_env', ftv') = tidyTyVar tidy_env ftv
+       in
+       find_frees tv tidy_env' (ftv':acc) ftvs
+    else
+       find_frees tv tidy_env  acc        ftvs
+
+
+escape_msg sig_tv tv globs frees
+  = mk_msg sig_tv <+> ptext SLIT("escapes") $$
+    if not (null globs) then
+       vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
+             ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
+             nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
+       ]
+     else if not (null frees) then
+       vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
+             nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
+       ]
+     else
+       empty   -- Sigh.  It's really hard to give a good error message
+               -- all the time.   One bad case is an existential pattern match
   where
-    pp_escape | sig_tv /= tv = ptext SLIT("It unifies with") <+>
-                              quotes (ppr tv) <> comma <+>
-                              ptext SLIT("which is mentioned in the environment")
-             | otherwise    = ptext SLIT("It is mentioned in the environment")
+    is_are | isSingleton frees = ptext SLIT("is")
+          | otherwise         = ptext SLIT("are")
+    pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
+         | otherwise    = ptext SLIT("It")
 
     vcat_first :: Int -> [SDoc] -> SDoc
     vcat_first n []     = empty
@@ -617,13 +703,20 @@ mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 These two context are used with checkSigTyVars
     
 \begin{code}
-sigCtxt :: (Type -> Message) -> Type
+sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
        -> TidyEnv -> NF_TcM s (TidyEnv, Message)
-sigCtxt mk_msg sig_ty tidy_env
-  = let
-       (env1, tidy_sig_ty) = tidyOpenType tidy_env sig_ty
+sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
+  = zonkTcType sig_tau         `thenNF_Tc` \ actual_tau ->
+    let
+       (env1, tidy_sig_tyvars)  = tidyTyVars tidy_env sig_tyvars
+       (env2, tidy_sig_rho)     = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
+       (env3, tidy_actual_tau)  = tidyOpenType env1 actual_tau
+       msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
+                   ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
+                   when
+                  ]
     in
-    returnNF_Tc (env1, mk_msg tidy_sig_ty)
+    returnNF_Tc (env3, msg)
 
 sigPatCtxt bound_tvs bound_ids tidy_env
   = returnNF_Tc (env1,
@@ -646,9 +739,7 @@ sigPatCtxt bound_tvs bound_ids tidy_env
 %************************************************************************
 
 \begin{code}
-naughtyCCallContextErr clas_name
-  = sep [ptext SLIT("Can't use class") <+> quotes (ppr clas_name), 
-        ptext SLIT("in a context")]
+tcsigCtxt v   = ptext SLIT("In a type signature for") <+> quotes (ppr v)
 
 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
 
@@ -668,4 +759,15 @@ tyConAsClassErr name
 
 tyVarAsClassErr name
   = ptext SLIT("Type variable used as a class:") <+> ppr name
+
+ambigErr pred ty
+  = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
+        nest 4 (ptext SLIT("for the type:") <+> ppr ty),
+        nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]
+
+freeErr pred ty
+  = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
+                  ptext SLIT("does not mention any of the universally quantified type variables"),
+        nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
+    ]
 \end{code}