[project @ 2000-05-25 12:41:14 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
index ef3c670..cb6c3be 100644 (file)
@@ -4,51 +4,58 @@
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}
-module TcMonoType ( tcHsType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType,
-                   tcContext, tcHsTyVar, kcHsTyVar,
+module TcMonoType ( tcHsType, tcHsSigType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType, tcHsTopTypeKind,
+                   tcContext, tcHsTyVar, kcHsTyVar, kcHsType,
                    tcExtendTyVarScope, tcExtendTopTyVarScope,
-                   TcSigInfo(..), tcTySig, mkTcSig, noSigs, maybeSig,
+                   TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
                    checkSigTyVars, sigCtxt, sigPatCtxt
                  ) where
 
 #include "HsVersions.h"
 
-import HsSyn           ( HsType(..), HsTyVar(..), 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,
-                         tcGetGlobalTyVars, TcTyThing(..)
+                          tcExtendUVarEnv, tcLookupUVar,
+                         tcGetGlobalTyVars, valueEnvIds, TcTyThing(..)
                        )
 import TcType          ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
-                         typeToTcType, tcInstTcType, kindToTcKind,
-                         newKindVar,
-                         zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType
+                         typeToTcType, kindToTcKind,
+                         newKindVar, tcInstSigVar,
+                         zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType, zonkTcTyVar
                        )
 import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr )
 import TcUnify         ( unifyKind, unifyKinds, unifyTypeKind )
-import Type            ( Type, ThetaType, 
-                         mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, zipFunTys,
-                         mkSigmaTy, mkDictTy, mkTyConApp, mkAppTys, splitRhoTy,
+import Type            ( Type, PredType(..), ThetaType, UsageAnn(..),
+                         mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
+                          mkUsForAllTy, zipFunTys, hoistForAllTys,
+                         mkSigmaTy, mkDictTy, mkPredTy, mkTyConApp,
+                         mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
                          boxedTypeKind, unboxedTypeKind, tyVarsOfType,
                          mkArrowKinds, getTyVar_maybe, getTyVar,
-                         tidyOpenType, tidyOpenTypes, tidyTyVar
+                         tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
+                         tyVarsOfType, tyVarsOfTypes, mkForAllTys
                        )
-import Id              ( mkUserId, idName, idType, idFreeTyVars )
-import Var             ( TyVar, mkTyVar )
+import PprType         ( pprConstraint, pprType )
+import Subst           ( mkTopTyVarSubst, substTy )
+import Id              ( mkVanillaId, idName, idType, idFreeTyVars )
+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}
 
@@ -65,6 +72,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)              $
@@ -93,13 +112,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')
+    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, hoistForAllTys zonked_ty)
 \end{code}
 
 
@@ -125,46 +153,83 @@ 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 (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
+                   HsUsOnce        -> returnTc UsOnce
+                   HsUsMany        -> returnTc UsMany
+                   HsUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
+                                        returnTc (UsVar uv)
 
-tc_type_kind (HsForAllTy tv_names context ty)
-  = tcExtendTyVarScope tv_names                $ \ tyvars -> 
+tc_type_kind (HsUsgForAllTy uv_name ty)
+  = let
+        uv = mkNamedUVar uv_name
+    in
+    tcExtendUVarEnv uv_name uv $
+      tc_type_kind ty                     `thenTc` \ (kind, tc_ty) ->
+      returnTc (kind, mkUsForAllTy uv tc_ty)
+
+tc_type_kind (HsForAllTy (Just tv_names) context ty)
+  = tcExtendTyVarScope tv_names                $ \ tyvars ->
     tcContext context                  `thenTc` \ theta ->
-    tc_boxed_type ty                   `thenTc` \ tau ->
-               -- Body of a for-all is a boxed type!
-    returnTc (boxedTypeKind, mkSigmaTy tyvars theta tau)
+    tc_type_kind ty                    `thenTc` \ (kind, tau) ->
+    tcGetInScopeTyVars                 `thenTc` \ in_scope_vars ->
+    let
+       body_kind | null theta = kind
+                 | otherwise  = boxedTypeKind
+               -- Context behaves like a function type
+               -- This matters.  Return-unboxed-tuple analysis can
+               -- give overloaded functions like
+               --      f :: forall a. Num a => (# a->a, a->a #)
+               -- And we want these to get through the type checker
+        check ct@(Class c tys) | ambiguous = failWithTc (ambigErr (c,tys) tau)
+         where ct_vars       = tyVarsOfTypes tys
+               forall_tyvars = map varName in_scope_vars
+               tau_vars      = tyVarsOfType tau
+               ambig ct_var  = (varName ct_var `elem` forall_tyvars) &&
+                               not (ct_var `elemUFM` tau_vars)
+               ambiguous     = foldUFM ((||) . ambig) False ct_vars
+       check _ = returnTc ()
+    in
+    mapTc check theta                  `thenTc_`
+    returnTc (body_kind, mkSigmaTy 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
@@ -188,16 +253,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
@@ -221,41 +286,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
-
- 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) ->
+tcContext context = mapTc (tcClassAssertion False) context
+
+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}
 
 
@@ -266,7 +317,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
@@ -280,14 +331,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
@@ -295,7 +346,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}
@@ -337,6 +388,9 @@ data TcSigInfo
 
        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
@@ -344,10 +398,6 @@ maybeSig [] name = Nothing
 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
   | name == sig_name = Just sig
   | otherwise       = maybeSig sigs name
-
--- This little helper is useful to pass to tcPat
-noSigs :: Name -> Maybe TcId
-noSigs name = Nothing
 \end{code}
 
 
@@ -356,8 +406,8 @@ tcTySig :: RenamedSig -> TcM s TcSigInfo
 
 tcTySig (Sig v ty src_loc)
  = tcAddSrcLoc src_loc $
-   tcHsType ty                                 `thenTc` \ sigma_tc_ty ->
-   mkTcSig (mkUserId v sigma_tc_ty) src_loc    `thenNF_Tc` \ sig -> 
+   tcHsSigType ty                              `thenTc` \ sigma_tc_ty ->
+   mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig -> 
    returnTc sig
 
 mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
@@ -369,19 +419,27 @@ mkTcSig poly_id src_loc
        -- the tyvars *do* get unified with something, we want to carry on
        -- typechecking the rest of the program with the function bound
        -- to a pristine type, namely sigma_tc_ty
-   tcInstTcType (idType poly_id)               `thenNF_Tc` \ (tyvars, rho) ->
    let
-     (theta, tau) = splitRhoTy rho
-       -- This splitSigmaTy tries hard to make sure that tau' is a type synonym
+       (tyvars, rho) = splitForAllTys (idType poly_id)
+   in
+   mapNF_Tc tcInstSigVar tyvars                `thenNF_Tc` \ tyvars' ->
+       -- Make *signature* type variables
+
+   let
+     tyvar_tys' = mkTyVarTys tyvars'
+     rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
+       -- mkTopTyVarSubst because the tyvars' are fresh
+     (theta', tau') = splitRhoTy rho'
+       -- This splitRhoTy tries hard to make sure that tau' is a type synonym
        -- wherever possible, which can improve interface files.
    in
    newMethodWithGivenTy SignatureOrigin 
                poly_id
-               (mkTyVarTys tyvars) 
-               theta tau                       `thenNF_Tc` \ inst ->
+               tyvar_tys'
+               theta' tau'                     `thenNF_Tc` \ inst ->
        -- We make a Method even if it's not overloaded; no harm
        
-   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 src_loc)
   where
     name = idName poly_id
 \end{code}
@@ -451,12 +509,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 ->
 
@@ -519,9 +580,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)
@@ -531,38 +593,59 @@ 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
-
-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_globals tv tidy_env  acc  ids
+
+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
     vcat_first 0 (x:xs) = text "...others omitted..."
     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
@@ -574,13 +657,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,
@@ -603,10 +693,6 @@ 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")]
-
 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
 
 typeKindCtxt :: RenamedHsType -> Message
@@ -625,4 +711,9 @@ tyConAsClassErr name
 
 tyVarAsClassErr name
   = ptext SLIT("Type variable used as a class:") <+> ppr name
+
+ambigErr (c, ts) ty
+  = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprConstraint c ts),
+        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 =>"))]
 \end{code}