[project @ 2002-04-02 13:21:36 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcUnify.lhs
index 87cd14e..9a574b3 100644 (file)
@@ -6,8 +6,8 @@
 \begin{code}
 module TcUnify (
        -- Full-blown subsumption
-  tcSub, tcGen, subFunTy,
-  checkSigTyVars, sigCtxt, sigPatCtxt,
+  tcSubOff, tcSubExp, tcGen, subFunTy, TcHoleType,
+  checkSigTyVars, checkSigTyVarsWrt, sigCtxt, 
 
        -- Various unifications
   unifyTauTy, unifyTauTyList, unifyTauTyLists, 
@@ -25,49 +25,50 @@ module TcUnify (
 
 
 import HsSyn           ( HsExpr(..) )
-import TcHsSyn         ( TypecheckedHsExpr, TcPat, 
-                         mkHsDictApp, mkHsTyApp, mkHsLet )
+import TcHsSyn         ( TypecheckedHsExpr, TcPat, mkHsLet )
 import TypeRep         ( Type(..), SourceType(..), TyNote(..),
                          openKindCon, typeCon )
 
 import TcMonad          -- TcType, amongst others
-import TcType          ( TcKind, TcType, TcSigmaType, TcPhiType, TcTyVar, TcTauType,
-                         TcTyVarSet, TcThetaType,
+import TcType          ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
+                         TcTyVarSet, TcThetaType, TyVarDetails(SigTv),
                          isTauTy, isSigmaTy, 
                          tcSplitAppTy_maybe, tcSplitTyConApp_maybe, 
                          tcGetTyVar_maybe, tcGetTyVar, 
-                         mkTyConApp, mkTyVarTys, mkFunTy, tyVarsOfType, mkRhoTy,
+                         mkTyConApp, mkFunTy, tyVarsOfType, mkPhiTy,
                          typeKind, tcSplitFunTy_maybe, mkForAllTys,
-                         isHoleTyVar, isSkolemTyVar, isUserTyVar, allDistinctTyVars, 
+                         isHoleTyVar, isSkolemTyVar, isUserTyVar, 
                          tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
                          eqKind, openTypeKind, liftedTypeKind, isTypeKind,
-                         hasMoreBoxityInfo, tyVarBindingInfo
+                         hasMoreBoxityInfo, tyVarBindingInfo, allDistinctTyVars
                        )
 import qualified Type  ( getTyVar_maybe )
-import Inst            ( LIE, emptyLIE, plusLIE, mkLIE, 
-                         newDicts, instToId
+import Inst            ( LIE, emptyLIE, plusLIE, 
+                         newDicts, instToId, tcInstCall
                        )
-import TcMType         ( getTcTyVar, putTcTyVar, tcInstType, 
+import TcMType         ( getTcTyVar, putTcTyVar, tcInstType, readHoleResult,
                          newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy,
-                         zonkTcType, zonkTcTyVars, zonkTcTyVar )
+                         zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcTyVar )
 import TcSimplify      ( tcSimplifyCheck )
 import TysWiredIn      ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy )
-import TcEnv           ( TcTyThing(..), tcExtendGlobalTyVars, tcGetGlobalTyVars, tcLEnvElts )
+import TcEnv           ( TcTyThing(..), tcGetGlobalTyVars, tcLEnvElts )
 import TyCon           ( tyConArity, isTupleTyCon, tupleTyConBoxity )
 import PprType         ( pprType )
-import CoreFVs         ( idFreeTyVars )
-import Id              ( mkSysLocal, idType )
+import Id              ( Id, mkSysLocal, idType )
 import Var             ( Var, varName, tyVarKind )
-import VarSet          ( elemVarSet, varSetElems )
+import VarSet          ( emptyVarSet, unionVarSet, elemVarSet, varSetElems )
 import VarEnv
 import Name            ( isSystemName, getSrcLoc )
 import ErrUtils                ( Message )
 import BasicTypes      ( Boxity, Arity, isBoxed )
-import Util            ( isSingleton, equalLength )
+import Util            ( equalLength )
 import Maybe           ( isNothing )
 import Outputable
 \end{code}
 
+Notes on holes
+~~~~~~~~~~~~~~
+* A hole is always filled in with an ordinary type, not another hole.
 
 %************************************************************************
 %*                                                                     *
@@ -75,24 +76,59 @@ import Outputable
 %*                                                                     *
 %************************************************************************
 
-\begin{code}
-tcSub :: TcSigmaType           -- expected_ty; can be a type scheme;
-                               --              can be a "hole" type variable
-      -> TcSigmaType           -- actual_ty; can be a type scheme
-      -> TcM (ExprCoFn, LIE)
-\end{code}
+All the tcSub calls have the form
+       
+               tcSub expected_ty offered_ty
+which checks
+               offered_ty <= expected_ty
 
-(tcSub expected_ty actual_ty) checks that 
-       actual_ty <= expected_ty
-That is, that a value of type actual_ty is acceptable in
+That is, that a value of type offered_ty is acceptable in
 a place expecting a value of type expected_ty.
 
 It returns a coercion function 
-       co_fn :: actual_ty -> expected_ty
-which takes an HsExpr of type actual_ty into one of type
+       co_fn :: offered_ty -> expected_ty
+which takes an HsExpr of type offered_ty into one of type
 expected_ty.
 
 \begin{code}
+type TcHoleType = TcSigmaType  -- Either a TcSigmaType, 
+                               -- or else a hole
+
+tcSubExp :: TcHoleType  -> TcSigmaType -> TcM (ExprCoFn, LIE)
+tcSubOff :: TcSigmaType -> TcHoleType  -> TcM (ExprCoFn, LIE)
+tcSub    :: TcSigmaType -> TcSigmaType -> TcM (ExprCoFn, LIE)
+\end{code}
+
+These two check for holes
+
+\begin{code}
+tcSubExp expected_ty offered_ty
+  = checkHole expected_ty offered_ty tcSub
+
+tcSubOff expected_ty offered_ty
+  = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off)
+
+-- checkHole looks for a hole in its first arg; 
+-- If so, and it is uninstantiated, it fills in the hole 
+--       with its second arg
+-- Otherwise it calls thing_inside, passing the two args, looking
+-- through any instantiated hole
+
+checkHole (TyVarTy tv) other_ty thing_inside
+  | isHoleTyVar tv
+  = getTcTyVar tv      `thenNF_Tc` \ maybe_ty ->
+    case maybe_ty of
+       Just ty -> thing_inside ty other_ty
+       Nothing -> putTcTyVar tv other_ty       `thenNF_Tc_`
+                  returnTc (idCoercion, emptyLIE)
+
+checkHole ty other_ty thing_inside 
+  = thing_inside ty other_ty
+\end{code}
+
+No holes expected now.  Add some error-check context info.
+
+\begin{code}
 tcSub expected_ty actual_ty
   = traceTc (text "tcSub" <+> details)         `thenNF_Tc_`
     tcAddErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
@@ -117,24 +153,6 @@ tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty
 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
 
 -----------------------------------
--- "Hole type variable" case
--- Do this case before unwrapping for-alls in the actual_ty
-
-tc_sub _ (TyVarTy tv) act_sty act_ty
-  | isHoleTyVar tv
-  =    -- It's a "hole" type variable
-    getTcTyVar tv      `thenNF_Tc` \ maybe_ty ->
-    case maybe_ty of
-
-       Just ty ->      -- Already been assigned
-                   tc_sub ty ty act_sty act_ty ;
-
-       Nothing ->      -- Assign it
-                   putTcTyVar tv act_sty               `thenNF_Tc_`
-                   returnTc (idCoercion, emptyLIE)
-
-
------------------------------------
 -- Generalisation case
 --     actual_ty:   d:Eq b => b->b
 --     expected_ty: forall a. Ord a => a->a
@@ -147,7 +165,9 @@ tc_sub _ (TyVarTy tv) act_sty act_ty
 
 tc_sub exp_sty expected_ty act_sty actual_ty
   | isSigmaTy expected_ty
-  = tcGen expected_ty (
+  = tcGen expected_ty (tyVarsOfType actual_ty) (
+       -- It's really important to check for escape wrt the free vars of
+       -- both expected_ty *and* actual_ty
        \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
     )                          `thenTc` \ (gen_fn, co_fn, lie) ->
     returnTc (gen_fn <.> co_fn, lie)
@@ -160,16 +180,9 @@ tc_sub exp_sty expected_ty act_sty actual_ty
 
 tc_sub exp_sty expected_ty act_sty actual_ty
   | isSigmaTy actual_ty
-  = tcInstType actual_ty       `thenNF_Tc` \ (tvs, theta, body_ty) ->
-    newDicts orig theta                `thenNF_Tc` \ dicts ->
-    let
-       inst_fn e = mkHsDictApp (mkHsTyApp e (mkTyVarTys tvs))
-                               (map instToId dicts)
-    in
-    tc_sub exp_sty expected_ty body_ty body_ty `thenTc` \ (co_fn, lie) ->
-    returnTc (co_fn <.> mkCoercion inst_fn, lie `plusLIE` mkLIE dicts)
-  where
-    orig = Rank2Origin
+  = tcInstCall Rank2Origin actual_ty           `thenNF_Tc` \ (inst_fn, lie1, body_ty) ->
+    tc_sub exp_sty expected_ty body_ty body_ty `thenTc` \ (co_fn, lie2) ->
+    returnTc (co_fn <.> mkCoercion inst_fn, lie1 `plusLIE` lie2)
 
 -----------------------------------
 -- Function case
@@ -192,14 +205,16 @@ tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
 --     is perfectly fine!
 
 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
-  = getTcTyVar tv      `thenNF_Tc` \ maybe_ty ->
+  = ASSERT( not (isHoleTyVar tv) )
+    getTcTyVar tv      `thenNF_Tc` \ maybe_ty ->
     case maybe_ty of
        Just ty -> tc_sub exp_sty exp_ty ty ty
        Nothing -> imitateFun tv exp_sty        `thenNF_Tc` \ (act_arg, act_res) ->
                   tcSub_fun exp_arg exp_res act_arg act_res
 
 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
-  = getTcTyVar tv      `thenNF_Tc` \ maybe_ty ->
+  = ASSERT( not (isHoleTyVar tv) )
+    getTcTyVar tv      `thenNF_Tc` \ maybe_ty ->
     case maybe_ty of
        Just ty -> tc_sub ty ty act_sty act_ty
        Nothing -> imitateFun tv act_sty        `thenNF_Tc` \ (exp_arg, exp_res) ->
@@ -221,14 +236,14 @@ tc_sub exp_sty expected_ty act_sty actual_ty
 
 \begin{code}
 tcSub_fun exp_arg exp_res act_arg act_res
-  = tcSub act_arg exp_arg      `thenTc` \ (co_fn_arg, lie1) ->
-    tcSub exp_res act_res      `thenTc` \ (co_fn_res, lie2) ->
-    tcGetUnique                        `thenNF_Tc` \ uniq ->
+  = tc_sub act_arg act_arg exp_arg exp_arg     `thenTc` \ (co_fn_arg, lie1) ->
+    tc_sub exp_res exp_res act_res act_res     `thenTc` \ (co_fn_res, lie2) ->
+    tcGetUnique                                        `thenNF_Tc` \ uniq ->
     let
        -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
        -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
        -- co_fn     :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
-       arg_id = mkSysLocal SLIT("sub") uniq exp_arg
+       arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
        coercion | isIdCoercion co_fn_arg,
                   isIdCoercion co_fn_res = idCoercion
                 | otherwise              = mkCoercion co_fn
@@ -269,16 +284,19 @@ imitateFun tv ty
 
 \begin{code}
 tcGen :: TcSigmaType                           -- expected_ty
-      -> (TcPhiType -> TcM (result, LIE))      -- spec_ty
+      -> TcTyVarSet                            -- Extra tyvars that the universally
+                                               --      quantified tyvars of expected_ty
+                                               --      must not be unified
+      -> (TcRhoType -> TcM (result, LIE))      -- spec_ty
       -> TcM (ExprCoFn, result, LIE)
        -- The expression has type: spec_ty -> expected_ty
 
-tcGen expected_ty thing_inside -- We expect expected_ty to be a forall-type
-                               -- If not, the call is a no-op
-  = tcInstType expected_ty             `thenNF_Tc` \ (forall_tvs, theta, phi_ty) ->
+tcGen expected_ty extra_tvs thing_inside       -- We expect expected_ty to be a forall-type
+                                               -- If not, the call is a no-op
+  = tcInstType SigTv expected_ty       `thenNF_Tc` \ (forall_tvs, theta, phi_ty) ->
 
        -- Type-check the arg and unify with poly type
-    thing_inside phi_ty                `thenTc` \ (result, lie) ->
+    thing_inside phi_ty                        `thenTc` \ (result, lie) ->
 
        -- Check that the "forall_tvs" havn't been constrained
        -- The interesting bit here is that we must include the free variables
@@ -291,12 +309,21 @@ tcGen expected_ty thing_inside    -- We expect expected_ty to be a forall-type
        -- Conclusion: include the free vars of the expected_ty in the
        -- list of "free vars" for the signature check.
 
-    tcExtendGlobalTyVars free_tvs                              $
-    tcAddErrCtxtM (sigCtxt forall_tvs theta phi_ty)    $
-
     newDicts SignatureOrigin theta                     `thenNF_Tc` \ dicts ->
     tcSimplifyCheck sig_msg forall_tvs dicts lie       `thenTc` \ (free_lie, inst_binds) ->
-    checkSigTyVars forall_tvs free_tvs                 `thenTc` \ zonked_tvs ->
+
+#ifdef DEBUG
+    zonkTcTyVars forall_tvs `thenNF_Tc` \ forall_tys ->
+    traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
+                                   text "expected_ty" <+> ppr expected_ty,
+                                   text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr phi_ty,
+                                   text "free_tvs" <+> ppr free_tvs,
+                                   text "forall_tys" <+> ppr forall_tys])      `thenNF_Tc_`
+#endif
+
+    checkSigTyVarsWrt free_tvs forall_tvs              `thenTc` \ zonked_tvs ->
+
+    traceTc (text "tcGen:done") `thenNF_Tc_`
 
     let
            -- This HsLet binds any Insts which came out of the simplification.
@@ -307,7 +334,7 @@ tcGen expected_ty thing_inside      -- We expect expected_ty to be a forall-type
     in
     returnTc (mkCoercion co_fn, result, free_lie)
   where
-    free_tvs = tyVarsOfType expected_ty
+    free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
     sig_msg  = ptext SLIT("When generalising the type of an expression")
 \end{code}    
 
@@ -720,32 +747,46 @@ creation of type variables.
   type variables, so we should create new ordinary type variables
 
 \begin{code}
-subFunTy :: TcSigmaType                        -- Fail if ty isn't a function type
-        -> TcM (TcType, TcType)        -- otherwise return arg and result types
-subFunTy ty@(TyVarTy tyvar)
-  
-  = getTcTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
-    case maybe_ty of
-       Just ty -> subFunTy ty
-       Nothing | isHoleTyVar tyvar
-               -> newHoleTyVarTy       `thenNF_Tc` \ arg ->
-                  newHoleTyVarTy       `thenNF_Tc` \ res ->
-                  putTcTyVar tyvar (mkFunTy arg res)   `thenNF_Tc_` 
-                  returnTc (arg,res)
-               | otherwise 
-               -> unify_fun_ty_help ty
-
-subFunTy ty
-  = case tcSplitFunTy_maybe ty of
-       Just arg_and_res -> returnTc arg_and_res
-       Nothing          -> unify_fun_ty_help ty
+subFunTy :: TcHoleType -- Fail if ty isn't a function type
+                       -- If it's a hole, make two holes, feed them to...
+        -> (TcHoleType -> TcHoleType -> TcM a) -- the thing inside
+        -> TcM a       -- and bind the function type to the hole
+
+subFunTy ty@(TyVarTy tyvar) thing_inside
+  | isHoleTyVar tyvar
+  =    -- This is the interesting case
+    getTcTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
+    case maybe_ty of {
+       Just ty' -> subFunTy ty' thing_inside ;
+       Nothing  -> 
+
+    newHoleTyVarTy             `thenNF_Tc` \ arg_ty ->
+    newHoleTyVarTy             `thenNF_Tc` \ res_ty ->
+
+       -- Do the business
+    thing_inside arg_ty res_ty `thenTc` \ answer ->
+
+       -- Extract the answers
+    readHoleResult arg_ty      `thenNF_Tc` \ arg_ty' ->
+    readHoleResult res_ty      `thenNF_Tc` \ res_ty' ->
+
+       -- Write the answer into the incoming hole
+    putTcTyVar tyvar (mkFunTy arg_ty' res_ty') `thenNF_Tc_` 
+
+       -- And return the answer
+    returnTc answer }
+
+subFunTy ty thing_inside
+  = unifyFunTy ty      `thenTc` \ (arg,res) ->
+    thing_inside arg res
 
                 
-unifyFunTy :: TcPhiType                        -- Fail if ty isn't a function type
+unifyFunTy :: TcRhoType                        -- Fail if ty isn't a function type
           -> TcM (TcType, TcType)      -- otherwise return arg and result types
 
 unifyFunTy ty@(TyVarTy tyvar)
-  = getTcTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
+  = ASSERT( not (isHoleTyVar tyvar) )
+    getTcTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
     case maybe_ty of
        Just ty' -> unifyFunTy ty'
        Nothing  -> unify_fun_ty_help ty
@@ -1007,20 +1048,36 @@ 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 ->
+checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar]
+checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
+
+checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar]
+checkSigTyVarsWrt extra_tvs sig_tvs
+  = zonkTcTyVarsAndFV (varSetElems extra_tvs)  `thenNF_Tc` \ extra_tvs' ->
+    check_sig_tyvars extra_tvs' sig_tvs
+
+check_sig_tyvars
+       :: TcTyVarSet           -- Global type variables. The universally quantified
+                               --      tyvars should not mention any of these
+                               --      Guaranteed already zonked.
+       -> [TcTyVar]            -- Universally-quantified type variables in the signature
+                               --      Not guaranteed zonked.
+       -> TcM [TcTyVar]        -- Zonked signature type variables
+
+check_sig_tyvars extra_tvs []
+  = returnTc []
+check_sig_tyvars extra_tvs sig_tvs 
+  = zonkTcTyVars sig_tvs       `thenNF_Tc` \ sig_tys ->
+    tcGetGlobalTyVars          `thenNF_Tc` \ gbl_tvs ->
+    let
+       env_tvs = gbl_tvs `unionVarSet` extra_tvs
+    in
+    traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tys,
+                                     text "gbl_tvs" <+> ppr gbl_tvs,
+                                     text "extra_tvs" <+> ppr extra_tvs]))     `thenNF_Tc_`
 
-    checkTcM (allDistinctTyVars sig_tys globals)
-            (complain sig_tys globals) `thenTc_`
+    checkTcM (allDistinctTyVars sig_tys env_tvs)
+            (complain sig_tys env_tvs)         `thenTc_`
 
     returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
 
@@ -1031,9 +1088,9 @@ checkSigTyVars sig_tyvars free_tyvars
                   (env2, emptyVarEnv, [])
                   (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
 
-        failWithTcM (env3, main_msg $$ vcat msgs)
+        failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
       where
-       (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
+       (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
        (env2, tidy_tys) = tidyOpenTypes  env1         sig_tys
 
        main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
@@ -1060,18 +1117,19 @@ checkSigTyVars sig_tyvars free_tyvars
            if tv `elemVarSet` globals  -- Error (c) or (d)! Type variable escapes
                                        -- The least comprehensible, so put it last
                        -- Game plan: 
-                       --    a) get the local TcIds and TyVars from the environment,
+                       --       get the local TcIds and TyVars 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  (tcLEnvElts 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)
+           then   tcGetEnv                                     `thenNF_Tc` \ ve ->
+                  find_globals tv tidy_env  (tcLEnvElts ve)    `thenNF_Tc` \ (tidy_env1, globs) ->
+                  returnNF_Tc (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
 
            else        -- All OK
            returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
            }}
+\end{code}
 
+
+\begin{code}
 -----------------------
 -- find_globals looks at the value environment and finds values
 -- whose types mention the offending type variable.  It has to be 
@@ -1115,7 +1173,7 @@ find_thing ignore_it tidy_env (ATyVar tv)
     else let
        (tidy_env1, tv1)     = tidyOpenTyVar tidy_env  tv
        (tidy_env2, tidy_ty) = tidyOpenType  tidy_env1 tv_ty
-       msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
+       msg = sep [ppr tv1 <+> eq_stuff, nest 2 bound_at]
 
        eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
                 | otherwise                                        = equals <+> ppr tv_ty
@@ -1126,42 +1184,19 @@ find_thing ignore_it tidy_env (ATyVar tv)
     returnNF_Tc (tidy_env2, Just msg)
 
 -----------------------
-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') = tidyOpenTyVar 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
+escape_msg sig_tv tv globs
   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
     if not (null globs) then
        vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"), 
              nest 2 (vcat 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
+               -- all the time.   One bad case is an existential pattern match.
+               -- We rely on the "When..." context to help.
   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)
@@ -1170,31 +1205,19 @@ mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 These two context are used with checkSigTyVars
     
 \begin{code}
-sigCtxt :: [TcTyVar] -> TcThetaType -> TcTauType
+sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
        -> TidyEnv -> NF_TcM (TidyEnv, Message)
-sigCtxt sig_tyvars sig_theta sig_tau tidy_env
+sigCtxt id sig_tvs sig_theta sig_tau tidy_env
   = zonkTcType sig_tau         `thenNF_Tc` \ actual_tau ->
     let
-       (env1, tidy_sig_tyvars)  = tidyOpenTyVars 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
+       (env1, tidy_sig_tvs)    = tidyOpenTyVars tidy_env sig_tvs
+       (env2, tidy_sig_rho)    = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
+       (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
+       sub_msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
+                       ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
                   ]
+       msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),
+                   nest 4 sub_msg]
     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}
-
-