[project @ 2002-06-07 07:16:04 by chak]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
index d57b53b..cf12315 100644 (file)
@@ -4,64 +4,55 @@
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}
-module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta, 
+module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta, tcHsPred,
                    UserTypeCtxt(..),
 
                        -- Kind checking
                    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
                    kcHsType, kcHsSigType, kcHsSigTypes, 
                    kcHsLiftedSigType, kcHsContext,
-                   tcScopedTyVars, tcHsTyVars, mkImmutTyVars,
+                   tcAddScopedTyVars, tcHsTyVars, mkImmutTyVars,
 
-                   TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
-                   checkSigTyVars, sigCtxt, sigPatCtxt
+                   TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId
                  ) where
 
 #include "HsVersions.h"
 
-import HsSyn           ( HsType(..), HsTyVarBndr(..),
+import HsSyn           ( HsType(..), HsTyVarBndr(..), HsTyOp(..),
                           Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
-import RnHsSyn         ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig )
+import RnHsSyn         ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars )
 import TcHsSyn         ( TcId )
 
 import TcMonad
 import TcEnv           ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
-                         tcGetGlobalTyVars, tcEnvTcIds, tcEnvTyVars,
+                         tcInLocalScope,
                          TyThing(..), TcTyThing(..), tcExtendKindEnv
                        )
-import TcMType         ( newKindVar, tcInstSigVars, 
-                         zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar,
-                         unifyKind, unifyOpenTypeKind,
+import TcMType         ( newKindVar, zonkKindEnv, tcInstType,
                          checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
                        )
-import TcType          ( Type, Kind, SourceType(..), ThetaType,
-                         mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
-                         tcSplitForAllTys, tcSplitRhoTy,
-                         hoistForAllTys, allDistinctTyVars,
-                          zipFunTys, 
-                         mkSigmaTy, mkPredTy, mkTyConApp,
-                         mkAppTys, mkRhoTy,
+import TcUnify         ( unifyKind, unifyOpenTypeKind )
+import TcType          ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
+                         TcTyVar, TcKind, TcThetaType, TcTauType,
+                         mkTyVarTy, mkTyVarTys, mkFunTy, 
+                         hoistForAllTys, zipFunTys, 
+                         mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys, 
                          liftedTypeKind, unliftedTypeKind, mkArrowKind,
-                         mkArrowKinds, tcGetTyVar_maybe, tcGetTyVar, tcSplitFunTy_maybe,
-                         tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
-                         tyVarsOfType, mkForAllTys
+                         mkArrowKinds, tcSplitFunTy_maybe
                        )
 import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
-import PprType         ( pprType )
-import Subst           ( mkTopTyVarSubst, substTy )
-import CoreFVs         ( idFreeTyVars )
+
 import Id              ( mkLocalId, idName, idType )
-import Var             ( Id, Var, TyVar, mkTyVar, tyVarKind )
-import VarEnv
-import VarSet
+import Var             ( TyVar, mkTyVar, tyVarKind )
 import ErrUtils                ( Message )
-import TyCon           ( TyCon, isSynTyCon, tyConArity, tyConKind )
+import TyCon           ( TyCon, tyConKind )
 import Class           ( classTyCon )
 import Name            ( Name )
-import TysWiredIn      ( mkListTy, mkTupleTy, genUnitTyCon )
+import NameSet
+import TysWiredIn      ( mkListTy, mkPArrTy, mkTupleTy, genUnitTyCon )
 import BasicTypes      ( Boxity(..) )
 import SrcLoc          ( SrcLoc )
-import Util            ( mapAccumL, isSingleton )
+import Util            ( lengthIs )
 import Outputable
 
 \end{code}
@@ -77,7 +68,7 @@ Generally speaking we now type-check types in three phases
 
        1.  Kind check the HsType [kcHsType]
        2.  Convert from HsType to Type, and hoist the foralls [tcHsType]
-       3.  Check the validity of the resultint type [checkValidType]
+       3.  Check the validity of the resulting type [checkValidType]
 
 Often these steps are done one after the othe (tcHsSigType).
 But in mutually recursive groups of type and class decls we do
@@ -194,21 +185,41 @@ tcHsTyVars tv_names kind_check thing_inside
     in
     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 
--- tcScopedTyVars is used for scoped type variables
+
+
+tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
+-- tcAddScopedTyVars is used for scoped type variables
+-- added by pattern type signatures
 --     e.g.  \ (x::a) (y::a) -> x+y
 -- They never have explicit kinds (because this is source-code only)
 -- They are mutable (because they can get bound to a more specific type)
-tcScopedTyVars :: [Name] 
-              -> TcM a                         -- The kind checker
-              -> TcM b
-              -> TcM b
-tcScopedTyVars [] kind_check thing_inside = thing_inside
-
-tcScopedTyVars tv_names kind_check thing_inside
-  = mapNF_Tc newNamedKindVar tv_names          `thenTc` \ kind_env ->
-    tcExtendKindEnv kind_env kind_check                `thenTc_`
-    zonkKindEnv kind_env                       `thenNF_Tc` \ tvs_w_kinds ->
-    listTc [tcNewMutTyVar name kind | (name, kind) <- tvs_w_kinds]     `thenNF_Tc` \ tyvars ->
+
+-- Find the not-already-in-scope signature type variables,
+-- kind-check them, and bring them into scope
+--
+-- We no longer specify that these type variables must be univerally 
+-- quantified (lots of email on the subject).  If you want to put that 
+-- back in, you need to
+--     a) Do a checkSigTyVars after thing_inside
+--     b) More insidiously, don't pass in expected_ty, else
+--        we unify with it too early and checkSigTyVars barfs
+--        Instead you have to pass in a fresh ty var, and unify
+--        it with expected_ty afterwards
+tcAddScopedTyVars [] thing_inside
+  = thing_inside       -- Quick get-out for the empty case
+
+tcAddScopedTyVars sig_tys thing_inside
+  = tcGetEnv                                   `thenNF_Tc` \ env ->
+    let
+       all_sig_tvs     = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
+       sig_tvs         = filter not_in_scope (nameSetToList all_sig_tvs)
+       not_in_scope tv = not (tcInLocalScope env tv)
+    in       
+    mapNF_Tc newNamedKindVar sig_tvs                   `thenTc` \ kind_env ->
+    tcExtendKindEnv kind_env (kcHsSigTypes sig_tys)    `thenTc_`
+    zonkKindEnv kind_env                               `thenNF_Tc` \ tvs_w_kinds ->
+    listTc [ tcNewMutTyVar name kind PatSigTv
+          | (name, kind) <- tvs_w_kinds]               `thenNF_Tc` \ tyvars ->
     tcExtendTyVarEnv tyvars thing_inside
 \end{code}
     
@@ -252,10 +263,19 @@ kcHsLiftedSigType = kcLiftedType
 kcHsType :: RenamedHsType -> TcM TcKind
 kcHsType (HsTyVar name)              = kcTyVar name
 
+kcHsType (HsKindSig ty k)
+  = kcHsType ty                        `thenTc` \ k' ->
+    unifyKind k k'             `thenTc_`
+    returnTc k
+
 kcHsType (HsListTy ty)
   = kcLiftedType ty            `thenTc` \ tau_ty ->
     returnTc liftedTypeKind
 
+kcHsType (HsPArrTy ty)
+  = kcLiftedType ty            `thenTc` \ tau_ty ->
+    returnTc liftedTypeKind
+
 kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
   = mapTc kcTypeType tys       `thenTc_`
     returnTc (case boxity of
@@ -267,17 +287,25 @@ kcHsType (HsFunTy ty1 ty2)
     kcTypeType ty2     `thenTc_`
     returnTc liftedTypeKind
 
-kcHsType (HsNumTy _)           -- The unit type for generics
-  = returnTc liftedTypeKind
+kcHsType (HsOpTy ty1 HsArrow ty2)
+  = kcTypeType ty1     `thenTc_`
+    kcTypeType ty2     `thenTc_`
+    returnTc liftedTypeKind
 
-kcHsType ty@(HsOpTy ty1 op ty2)
+kcHsType ty@(HsOpTy ty1 (HsTyOp op) ty2)
   = kcTyVar op                         `thenTc` \ op_kind ->
     kcHsType ty1                       `thenTc` \ ty1_kind ->
     kcHsType ty2                       `thenTc` \ ty2_kind ->
     tcAddErrCtxt (appKindCtxt (ppr ty))        $
     kcAppKind op_kind  ty1_kind                `thenTc` \ op_kind' ->
     kcAppKind op_kind' ty2_kind
+
+kcHsType (HsParTy ty)          -- Skip parentheses markers
+  = kcHsType ty
    
+kcHsType (HsNumTy _)           -- The unit type for generics
+  = returnTc liftedTypeKind
+
 kcHsType (HsPredTy pred)
   = kcHsPred pred              `thenTc_`
     returnTc liftedTypeKind
@@ -308,18 +336,27 @@ kcAppKind fun_kind arg_kind
 
 
 ---------------------------
-kcHsContext ctxt = mapTc_ kcHsPred ctxt
+kc_pred :: RenamedHsPred -> TcM TcKind -- Does *not* check for a saturated
+                                       -- application (reason: used from TcDeriv)
+kc_pred pred@(HsIParam name ty)
+  = kcHsType ty
+
+kc_pred pred@(HsClassP cls tys)
+  = kcClass cls                                `thenTc` \ kind ->
+    mapTc kcHsType tys                 `thenTc` \ arg_kinds ->
+    newKindVar                                 `thenNF_Tc` \ kv -> 
+    unifyKind kind (mkArrowKinds arg_kinds kv) `thenTc_` 
+    returnTc kv
 
-kcHsPred :: RenamedHsPred -> TcM ()
-kcHsPred pred@(HsIParam name ty)
-  = tcAddErrCtxt (appKindCtxt (ppr pred))      $
-    kcLiftedType ty
+---------------------------
+kcHsContext ctxt = mapTc_ kcHsPred ctxt
 
-kcHsPred pred@(HsClassP cls tys)
+kcHsPred pred          -- Checks that the result is of kind liftedType
   = tcAddErrCtxt (appKindCtxt (ppr pred))      $
-    kcClass cls                                        `thenTc` \ kind ->
-    mapTc kcHsType tys                         `thenTc` \ arg_kinds ->
-    unifyKind kind (mkArrowKinds arg_kinds liftedTypeKind)
+    kc_pred pred                               `thenTc` \ kind ->
+    unifyKind liftedTypeKind kind              `thenTc_`
+    returnTc ()
+    
 
  ---------------------------
 kcTyVar name   -- Could be a tyvar or a tycon
@@ -376,12 +413,19 @@ tc_type :: RenamedHsType -> TcM Type
 tc_type ty@(HsTyVar name)
   = tc_app ty []
 
+tc_type (HsKindSig ty k)
+  = tc_type ty -- Kind checking done already
+
 tc_type (HsListTy ty)
   = tc_type ty `thenTc` \ tau_ty ->
     returnTc (mkListTy tau_ty)
 
+tc_type (HsPArrTy ty)
+  = tc_type ty `thenTc` \ tau_ty ->
+    returnTc (mkPArrTy tau_ty)
+
 tc_type (HsTupleTy (HsTupCon _ boxity arity) tys)
-  = ASSERT( arity == length tys )
+  = ASSERT( tys `lengthIs` arity )
     tc_types tys       `thenTc` \ tau_tys ->
     returnTc (mkTupleTy boxity arity tau_tys)
 
@@ -390,15 +434,23 @@ tc_type (HsFunTy ty1 ty2)
     tc_type ty2                        `thenTc` \ tau_ty2 ->
     returnTc (mkFunTy tau_ty1 tau_ty2)
 
-tc_type (HsNumTy n)
-  = ASSERT(n== 1)
-    returnTc (mkTyConApp genUnitTyCon [])
+tc_type (HsOpTy ty1 HsArrow ty2)
+  = tc_type ty1 `thenTc` \ tau_ty1 ->
+    tc_type ty2 `thenTc` \ tau_ty2 ->
+    returnTc (mkFunTy tau_ty1 tau_ty2)
 
-tc_type (HsOpTy ty1 op ty2)
+tc_type (HsOpTy ty1 (HsTyOp op) ty2)
   = tc_type ty1 `thenTc` \ tau_ty1 ->
     tc_type ty2 `thenTc` \ tau_ty2 ->
     tc_fun_type op [tau_ty1,tau_ty2]
 
+tc_type (HsParTy ty)           -- Remove the parentheses markers
+  = tc_type ty
+
+tc_type (HsNumTy n)
+  = ASSERT(n== 1)
+    returnTc (mkTyConApp genUnitTyCon [])
+
 tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
 
 tc_type (HsPredTy pred)
@@ -444,13 +496,7 @@ tc_fun_type name arg_tys
     case thing of
        ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
 
-       AGlobal (ATyCon tc)
-               | isSynTyCon tc ->  returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
-                                                      (drop arity arg_tys))
-               | otherwise     ->  returnTc (mkTyConApp tc arg_tys)
-               where
-                   arity = tyConArity tc
-
+       AGlobal (ATyCon tc) -> returnTc (mkGenTyConApp tc arg_tys)
 
        other -> failWithTc (wrongThingErr "type constructor" thing name)
 \end{code}
@@ -459,6 +505,10 @@ tc_fun_type name arg_tys
 Contexts
 ~~~~~~~~
 \begin{code}
+tcHsPred pred = kc_pred pred `thenTc_`  tc_pred pred
+       -- Is happy with a partial application, e.g. (ST s)
+       -- Used from TcDeriv
+
 tc_pred assn@(HsClassP class_name tys)
   = tcAddErrCtxt (appKindCtxt (ppr assn))      $
     tc_types tys                       `thenTc` \ arg_tys ->
@@ -513,8 +563,6 @@ been instantiated.
 \begin{code}
 data TcSigInfo
   = TySigInfo      
-       Name                    -- N, the Name in corresponding binding
-
        TcId                    -- *Polymorphic* binder for this value...
                                -- Has name = N
 
@@ -532,15 +580,21 @@ 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
+    ppr (TySigInfo id tyvars theta tau _ inst loc) =
+       ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
+
+tcSigPolyId :: TcSigInfo -> TcId
+tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
+
+tcSigMonoId :: TcSigInfo -> TcId
+tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
 
 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
        -- Search for a particular signature
 maybeSig [] name = Nothing
-maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
-  | name == sig_name = Just sig
-  | otherwise       = maybeSig sigs name
+maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
+  | name == idName sig_id = Just sig
+  | otherwise            = maybeSig sigs name
 \end{code}
 
 
@@ -562,280 +616,18 @@ 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
-   let
-       (tyvars, rho) = tcSplitForAllTys (idType poly_id)
-   in
-   tcInstSigVars 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') = tcSplitRhoTy rho'
-       -- This splitRhoTy tries hard to make sure that tau' is a type synonym
-       -- wherever possible, which can improve interface files.
-   in
+   tcInstType SigTv (idType poly_id)           `thenNF_Tc` \ (tyvars', theta', tau') ->
+
    newMethodWithGivenTy SignatureOrigin 
-               poly_id
-               tyvar_tys'
-               theta' tau'                     `thenNF_Tc` \ inst ->
+                       poly_id
+                       (mkTyVarTys tyvars')
+                       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' (instToId inst) [inst] src_loc)
-  where
-    name = idName poly_id
-\end{code}
-
-
-
-%************************************************************************
-%*                                                                     *
-\subsection{Checking signature type variables}
-%*                                                                     *
-%************************************************************************
-
-@checkSigTyVars@ is used after the type in a type signature has been unified with
-the actual type found.  It then checks that the type variables of the type signature
-are
-       (a) Still all type variables
-               eg matching signature [a] against inferred type [(p,q)]
-               [then a will be unified to a non-type variable]
-
-       (b) Still all distinct
-               eg matching signature [(a,b)] against inferred type [(p,p)]
-               [then a and b will be unified together]
-
-       (c) Not mentioned in the environment
-               eg the signature for f in this:
-
-                       g x = ... where
-                                       f :: a->[a]
-                                       f y = [x,y]
-
-               Here, f is forced to be monorphic by the free occurence of x.
-
-       (d) Not (unified with another type variable that is) in scope.
-               eg f x :: (r->r) = (\y->y) :: forall a. a->r
-           when checking the expression type signature, we find that
-           even though there is nothing in scope whose type mentions r,
-           nevertheless the type signature for the expression isn't right.
-
-           Another example is in a class or instance declaration:
-               class C a where
-                  op :: forall b. a -> b
-                  op x = x
-           Here, b gets unified with a
-
-Before doing this, the substitution is applied to the signature type variable.
-
-We used to have the notion of a "DontBind" type variable, which would
-only be bound to itself or nothing.  Then points (a) and (b) were 
-self-checking.  But it gave rise to bogus consequential error messages.
-For example:
-
-   f = (*)     -- Monomorphic
-
-   g :: Num a => a -> a
-   g x = f x x
-
-Here, we get a complaint when checking the type signature for g,
-that g isn't polymorphic enough; but then we get another one when
-dealing with the (Num x) context arising from f's definition;
-we try to unify x with Int (to default it), but find that x has already
-been unified with the DontBind variable "a" from g's signature.
-This is really a problem with side-effecting unification; we'd like to
-undo g's effects when its type signature fails, but unification is done
-by side effect, so we can't (easily).
-
-So we revert to ordinary type variables for signatures, and try to
-give a helpful message in checkSigTyVars.
-
-\begin{code}
-checkSigTyVars :: [TcTyVar]            -- Universally-quantified type variables in the signature
-              -> TcTyVarSet            -- Tyvars that are free in the type signature
-                                       --      Not necessarily zonked
-                                       --      These should *already* be in the free-in-env set, 
-                                       --      and are used here only to improve the error message
-              -> TcM [TcTyVar]         -- Zonked signature type variables
-
-checkSigTyVars [] free = returnTc []
-checkSigTyVars sig_tyvars free_tyvars
-  = zonkTcTyVars sig_tyvars            `thenNF_Tc` \ sig_tys ->
-    tcGetGlobalTyVars                  `thenNF_Tc` \ globals ->
-
-    checkTcM (allDistinctTyVars sig_tys globals)
-            (complain sig_tys globals) `thenTc_`
-
-    returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
-
-  where
-    complain sig_tys globals
-      = -- For the in-scope ones, zonk them and construct a map
-       -- from the zonked tyvar to the in-scope one
-       -- If any of the in-scope tyvars zonk to a type, then ignore them;
-       -- that'll be caught later when we back up to their type sig
-       tcGetEnv                                `thenNF_Tc` \ env ->
-       let
-          in_scope_tvs = tcEnvTyVars env
-       in
-       zonkTcTyVars in_scope_tvs               `thenNF_Tc` \ in_scope_tys ->
-       let
-           in_scope_assoc = [ (zonked_tv, in_scope_tv) 
-                            | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
-                              Just zonked_tv <- [tcGetTyVar_maybe z_ty]
-                            ]
-           in_scope_env = mkVarEnv in_scope_assoc
-       in
-
-       -- "check" checks each sig tyvar in turn
-        foldlNF_Tc check
-                  (env2, in_scope_env, [])
-                  (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
-
-        failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
-      where
-       (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
-       (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
-
-       main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
-
-       check (tidy_env, acc, msgs) (sig_tyvar,ty)
-               -- sig_tyvar is from the signature;
-               -- ty is what you get if you zonk sig_tyvar and then tidy it
-               --
-               -- acc maps a zonked type variable back to a signature type variable
-         = case tcGetTyVar_maybe ty of {
-             Nothing ->                        -- Error (a)!
-                       returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
-
-             Just tv ->
-
-           case lookupVarEnv acc tv of {
-               Just sig_tyvar' ->      -- Error (b) or (d)!
-                       returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
-                   where
-                       thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
-
-             ; Nothing ->
-
-           if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
-                                       -- The least comprehensible, so put it last
-                       -- Game plan: 
-                       --    a) get the local TcIds from the environment,
-                       --       and pass them to find_globals (they might have tv free)
-                       --    b) similarly, find any free_tyvars that mention tv
-           then   tcGetEnv                                                     `thenNF_Tc` \ ve ->
-                  find_globals tv tidy_env  [] (tcEnvTcIds ve)                 `thenNF_Tc` \ (tidy_env1, globs) ->
-                  find_frees   tv tidy_env1 [] (varSetElems free_tyvars)       `thenNF_Tc` \ (tidy_env2, frees) ->
-                  returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
-
-           else        -- All OK
-           returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
-           }}
-
--- find_globals looks at the value environment and finds values
--- 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 :: Var 
-             -> TidyEnv 
-             -> [(Name,Type)] 
-             -> [Id] 
-             -> NF_TcM (TidyEnv,[(Name,Type)])
-
-find_globals tv tidy_env acc []
-  = returnNF_Tc (tidy_env, acc)
-
-find_globals tv tidy_env acc (id:ids) 
-  | isEmptyVarSet (idFreeTyVars id)
-  = 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' acc' ids
-    else
-       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
-    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
-
-unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
-mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
+   returnNF_Tc (TySigInfo poly_id tyvars' theta' tau' 
+                         (instToId inst) [inst] src_loc)
 \end{code}
 
-These two context are used with checkSigTyVars
-    
-\begin{code}
-sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
-       -> TidyEnv -> NF_TcM (TidyEnv, Message)
-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 env2 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 (env3, msg)
-
-sigPatCtxt bound_tvs bound_ids tidy_env
-  = returnNF_Tc (env1,
-                sep [ptext SLIT("When checking a pattern that binds"),
-                     nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
-  where
-    show_ids = filter is_interesting bound_ids
-    is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
-
-    (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
-    ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
-       -- Don't zonk the types so we get the separate, un-unified versions
-\end{code}
 
 
 %************************************************************************