[project @ 2003-09-20 17:26:46 by ross]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcBinds.lhs
index a50bc50..b5d2cb7 100644 (file)
@@ -4,58 +4,50 @@
 \section[TcBinds]{TcBinds}
 
 \begin{code}
-module TcBinds ( tcBindsAndThen, tcTopBinds,
-                tcSpecSigs, tcBindWithSigs ) where
+module TcBinds ( tcBindsAndThen, tcTopBinds, tcMonoBinds, tcSpecSigs ) where
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} TcMatches ( tcGRHSs, tcMatchesFun )
-import {-# SOURCE #-} TcExpr  ( tcExpr )
+import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
+import {-# SOURCE #-} TcExpr  ( tcCheckSigma, tcCheckRho )
 
-import CmdLineOpts     ( opt_NoMonomorphismRestriction )
+import CmdLineOpts     ( DynFlag(Opt_NoMonomorphismRestriction) )
 import HsSyn           ( HsExpr(..), HsBinds(..), MonoBinds(..), Sig(..), 
-                         Match(..), HsMatchContext(..), 
-                         collectMonoBinders, andMonoBinds
+                         Match(..), mkMonoBind,
+                         collectMonoBinders, andMonoBinds,
+                         collectSigTysFromMonoBinds
                        )
 import RnHsSyn         ( RenamedHsBinds, RenamedSig, RenamedMonoBinds )
-import TcHsSyn         ( TcMonoBinds, TcId, zonkId, mkHsLet )
-
-import TcMonad
-import Inst            ( LIE, emptyLIE, mkLIE, plusLIE, InstOrigin(..),
-                         newDicts, instToId
-                       )
-import TcEnv           ( tcExtendLocalValEnv,
-                         newSpecPragmaId, newLocalId
-                       )
-import TcSimplify      ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyCheck, tcSimplifyRestricted, tcSimplifyToDicts )
-import TcMonoType      ( tcHsSigType, checkSigTyVars,
-                         TcSigInfo(..), tcTySig, maybeSig, sigCtxt
+import TcHsSyn         ( TcHsBinds, TcMonoBinds, TcId, zonkId, mkHsLet )
+
+import TcRnMonad
+import Inst            ( InstOrigin(..), newDicts, newIPDict, instToId )
+import TcEnv           ( tcExtendLocalValEnv, tcExtendLocalValEnv2, newLocalName )
+import TcUnify         ( Expected(..), newHole, unifyTauTyLists, checkSigTyVarsWrt, sigCtxt )
+import TcSimplify      ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted, 
+                         tcSimplifyToDicts, tcSimplifyIPs )
+import TcMonoType      ( tcHsSigType, UserTypeCtxt(..), TcSigInfo(..), 
+                         tcTySig, maybeSig, tcSigPolyId, tcSigMonoId, tcAddScopedTyVars
                        )
-import TcPat           ( tcPat )
+import TcPat           ( tcPat, tcSubPat, tcMonoPatBndr )
 import TcSimplify      ( bindInstsOfLocalFuns )
-import TcType          ( newTyVarTy, newTyVar, 
-                         zonkTcTyVarToTyVar
+import TcMType         ( newTyVar, newTyVarTy, zonkTcTyVarToTyVar )
+import TcType          ( TcTyVar, mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType, 
+                         mkPredTy, mkForAllTy, isUnLiftedType, 
+                         unliftedTypeKind, liftedTypeKind, openTypeKind, eqKind
                        )
-import TcUnify         ( unifyTauTy, unifyTauTyLists )
 
 import CoreFVs         ( idFreeTyVars )
-import Id              ( mkLocalId, setInlinePragma )
+import Id              ( mkLocalId, mkSpecPragmaId, setInlinePragma )
 import Var             ( idType, idName )
-import IdInfo          ( InlinePragInfo(..) )
-import Name            ( Name, getOccName, getSrcLoc )
+import Name            ( Name, getSrcLoc )
 import NameSet
-import Type            ( mkTyVarTy, tyVarsOfTypes,
-                         mkForAllTys, mkFunTys, tyVarsOfType, 
-                         mkPredTy, mkForAllTy, isUnLiftedType, 
-                         unliftedTypeKind, liftedTypeKind, openTypeKind
-                       )
 import Var             ( tyVarKind )
 import VarSet
 import Bag
-import Util            ( isIn )
-import ListSetOps      ( minusList )
-import Maybes          ( maybeToBool )
-import BasicTypes      ( TopLevelFlag(..), RecFlag(..), isNonRec, isNotTopLevel )
+import Util            ( isIn, equalLength )
+import BasicTypes      ( TopLevelFlag(..), RecFlag(..), isNonRec, isRec, 
+                         isNotTopLevel, isAlwaysActive )
 import FiniteMap       ( listToFM, lookupFM )
 import Outputable
 \end{code}
@@ -93,20 +85,29 @@ At the top-level the LIE is sure to contain nothing but constant
 dictionaries, which we resolve at the module level.
 
 \begin{code}
-tcTopBinds :: RenamedHsBinds -> TcM ((TcMonoBinds, TcEnv), LIE)
+tcTopBinds :: RenamedHsBinds -> TcM (TcMonoBinds, TcLclEnv)
+       -- Note: returning the TcLclEnv is more than we really
+       --       want.  The bit we care about is the local bindings
+       --       and the free type variables thereof
 tcTopBinds binds
   = tc_binds_and_then TopLevel glue binds      $
-    tcGetEnv                                   `thenNF_Tc` \ env ->
-    returnTc ((EmptyMonoBinds, env), emptyLIE)
+    getLclEnv                                  `thenM` \ env ->
+    returnM (EmptyMonoBinds, env)
   where
-    glue is_rec binds1 (binds2, thing) = (binds1 `AndMonoBinds` binds2, thing)
+       -- The top level bindings are flattened into a giant 
+       -- implicitly-mutually-recursive MonoBinds
+    glue binds1 (binds2, env) = (flatten binds1 `AndMonoBinds` binds2, env)
+    flatten EmptyBinds                 = EmptyMonoBinds
+    flatten (b1 `ThenBinds` b2) = flatten b1 `AndMonoBinds` flatten b2
+    flatten (MonoBind b _ _)   = b
+       -- Can't have a IPBinds at top level
 
 
 tcBindsAndThen
-       :: (RecFlag -> TcMonoBinds -> thing -> thing)           -- Combinator
+       :: (TcHsBinds -> thing -> thing)                -- Combinator
        -> RenamedHsBinds
-       -> TcM (thing, LIE)
-       -> TcM (thing, LIE)
+       -> TcM thing
+       -> TcM thing
 
 tcBindsAndThen = tc_binds_and_then NotTopLevel
 
@@ -120,63 +121,86 @@ tc_binds_and_then top_lvl combiner (ThenBinds b1 b2) do_next
     tc_binds_and_then top_lvl combiner b2      $
     do_next
 
+tc_binds_and_then top_lvl combiner (IPBinds binds is_with) do_next
+  = getLIE do_next                     `thenM` \ (result, expr_lie) ->
+    mapAndUnzipM tc_ip_bind binds      `thenM` \ (avail_ips, binds') ->
+
+       -- If the binding binds ?x = E, we  must now 
+       -- discharge any ?x constraints in expr_lie
+    tcSimplifyIPs avail_ips expr_lie   `thenM` \ dict_binds ->
+
+    returnM (combiner (IPBinds binds' is_with) $
+            combiner (mkMonoBind Recursive dict_binds) result)
+  where
+       -- I wonder if we should do these one at at time
+       -- Consider     ?x = 4
+       --              ?y = ?x + 1
+    tc_ip_bind (ip, expr)
+      = newTyVarTy openTypeKind                `thenM` \ ty ->
+       getSrcLocM                      `thenM` \ loc ->
+       newIPDict (IPBind ip) ip ty     `thenM` \ (ip', ip_inst) ->
+       tcCheckRho expr ty              `thenM` \ expr' ->
+       returnM (ip_inst, (ip', expr'))
+
 tc_binds_and_then top_lvl combiner (MonoBind bind sigs is_rec) do_next
-  =    -- TYPECHECK THE SIGNATURES
-      mapTc tcTySig [sig | sig@(Sig name _ _) <- sigs] `thenTc` \ tc_ty_sigs ->
+  =    -- BRING ANY SCOPED TYPE VARIABLES INTO SCOPE
+       -- Notice that they scope over 
+       --      a) the type signatures in the binding group
+       --      b) the bindings in the group
+       --      c) the scope of the binding group (the "in" part)
+      tcAddScopedTyVars (collectSigTysFromMonoBinds bind)      $
+
+      tcBindWithSigs top_lvl bind sigs is_rec  `thenM` \ (poly_binds, poly_ids) ->
   
-      tcBindWithSigs top_lvl bind tc_ty_sigs
-                    sigs is_rec                        `thenTc` \ (poly_binds, poly_lie, poly_ids) ->
-  
-         -- Extend the environment to bind the new polymorphic Ids
-      tcExtendLocalValEnv [(idName poly_id, poly_id) | poly_id <- poly_ids] $
-  
-         -- Build bindings and IdInfos corresponding to user pragmas
-      tcSpecSigs sigs          `thenTc` \ (prag_binds, prag_lie) ->
-
-       -- Now do whatever happens next, in the augmented envt
-      do_next                  `thenTc` \ (thing, thing_lie) ->
-
-       -- Create specialisations of functions bound here
-       -- We want to keep non-recursive things non-recursive
-       -- so that we desugar unlifted bindings correctly
-      case (top_lvl, is_rec) of
-
-               -- For the top level don't bother will all this bindInstsOfLocalFuns stuff
-               -- All the top level things are rec'd together anyway, so it's fine to
-               -- leave them to the tcSimplifyTop, and quite a bit faster too
-       (TopLevel, _)
-               -> returnTc (combiner Recursive (poly_binds `andMonoBinds` prag_binds) thing,
-                            thing_lie `plusLIE` prag_lie `plusLIE` poly_lie)
-
-       (NotTopLevel, NonRecursive) 
-               -> bindInstsOfLocalFuns 
-                               (thing_lie `plusLIE` prag_lie)
-                               poly_ids                        `thenTc` \ (thing_lie', lie_binds) ->
-
-                  returnTc (
-                       combiner NonRecursive poly_binds $
-                       combiner NonRecursive prag_binds $
-                       combiner Recursive lie_binds  $
+      case top_lvl of
+       TopLevel        -- For the top level don't bother will all this
+                       --  bindInstsOfLocalFuns stuff. All the top level 
+                       -- things are rec'd together anyway, so it's fine to
+                       -- leave them to the tcSimplifyTop, and quite a bit faster too
+                       --
+                       -- Subtle (and ugly) point: furthermore at top level we
+                       -- return the TcLclEnv, which contains the LIE var; we
+                       -- don't want to return the wrong one!
+               -> tc_body poly_ids                     `thenM` \ (prag_binds, thing) ->
+                  returnM (combiner (mkMonoBind Recursive (poly_binds `andMonoBinds` prag_binds)) 
+                                    thing)
+
+       NotTopLevel     -- For nested bindings we must do teh bindInstsOfLocalFuns thing
+               -> getLIE (tc_body poly_ids)            `thenM` \ ((prag_binds, thing), lie) ->
+
+                       -- Create specialisations of functions bound here
+                   bindInstsOfLocalFuns lie poly_ids   `thenM` \ lie_binds ->
+
+                       -- We want to keep non-recursive things non-recursive
+                       -- so that we desugar unlifted bindings correctly
+                  if isRec is_rec then
+                    returnM (
+                       combiner (mkMonoBind Recursive (
+                               poly_binds `andMonoBinds`
+                               lie_binds  `andMonoBinds`
+                               prag_binds)) thing
+                    )
+                  else
+                    returnM (
+                       combiner (mkMonoBind NonRecursive poly_binds) $
+                       combiner (mkMonoBind NonRecursive prag_binds) $
+                       combiner (mkMonoBind Recursive lie_binds)     $
                                -- NB: the binds returned by tcSimplify and bindInstsOfLocalFuns
                                -- aren't guaranteed in dependency order (though we could change
                                -- that); hence the Recursive marker.
-                       thing,
-
-                       thing_lie' `plusLIE` poly_lie
-                  )
+                       thing)
+  where
+    tc_body poly_ids   -- Type check the pragmas and "thing inside"
+      =   -- Extend the environment to bind the new polymorphic Ids
+         tcExtendLocalValEnv poly_ids  $
+  
+         -- Build bindings and IdInfos corresponding to user pragmas
+         tcSpecSigs sigs               `thenM` \ prag_binds ->
 
-       (NotTopLevel, Recursive)
-               -> bindInstsOfLocalFuns 
-                               (thing_lie `plusLIE` poly_lie `plusLIE` prag_lie) 
-                               poly_ids                        `thenTc` \ (final_lie, lie_binds) ->
+         -- Now do whatever happens next, in the augmented envt
+         do_next                       `thenM` \ thing ->
 
-                  returnTc (
-                       combiner Recursive (
-                               poly_binds `andMonoBinds`
-                               lie_binds  `andMonoBinds`
-                               prag_binds) thing,
-                       final_lie
-                  )
+         returnM (prag_binds, thing)
 \end{code}
 
 
@@ -200,37 +224,48 @@ so all the clever stuff is in here.
 tcBindWithSigs 
        :: TopLevelFlag
        -> RenamedMonoBinds
-       -> [TcSigInfo]
        -> [RenamedSig]         -- Used solely to get INLINE, NOINLINE sigs
        -> RecFlag
-       -> TcM (TcMonoBinds, LIE, [TcId])
+       -> TcM (TcMonoBinds, [TcId])
+
+tcBindWithSigs top_lvl mbind sigs is_rec
+  =    -- TYPECHECK THE SIGNATURES
+     recoverM (returnM []) (
+       mappM tcTySig [sig | sig@(Sig name _ _) <- sigs]
+     )                                         `thenM` \ tc_ty_sigs ->
 
-tcBindWithSigs top_lvl mbind tc_ty_sigs inline_sigs is_rec
-  = recoverTc (
+       -- SET UP THE MAIN RECOVERY; take advantage of any type sigs
+   recoverM (
        -- If typechecking the binds fails, then return with each
        -- signature-less binder given type (forall a.a), to minimise subsequent
        -- error messages
-       newTyVar liftedTypeKind         `thenNF_Tc` \ alpha_tv ->
+       newTyVar liftedTypeKind         `thenM` \ alpha_tv ->
        let
          forall_a_a    = mkForAllTy alpha_tv (mkTyVarTy alpha_tv)
           binder_names  = collectMonoBinders mbind
          poly_ids      = map mk_dummy binder_names
          mk_dummy name = case maybeSig tc_ty_sigs name of
-                           Just (TySigInfo _ poly_id _ _ _ _ _ _) -> poly_id   -- Signature
-                           Nothing -> mkLocalId name forall_a_a                -- No signature
+                           Just sig -> tcSigPolyId sig                 -- Signature
+                           Nothing  -> mkLocalId name forall_a_a       -- No signature
        in
-       returnTc (EmptyMonoBinds, emptyLIE, poly_ids)
+       traceTc (text "tcBindsWithSigs: error recovery" <+> ppr binder_names)   `thenM_`
+       returnM (EmptyMonoBinds, poly_ids)
     )                                          $
 
        -- TYPECHECK THE BINDINGS
-    tcMonoBinds mbind tc_ty_sigs is_rec                `thenTc` \ (mbind', lie_req, binder_names, mono_ids) ->
+    getLIE (tcMonoBinds mbind tc_ty_sigs is_rec)       `thenM` \ ((mbind', bndr_names_w_ids), lie_req) ->
     let
-       tau_tvs = varSetElems (foldr (unionVarSet . tyVarsOfType . idType) emptyVarSet mono_ids)
+       (binder_names, mono_ids) = unzip (bagToList bndr_names_w_ids)
+       tau_tvs = foldr (unionVarSet . tyVarsOfType . idType) emptyVarSet mono_ids
     in
 
        -- GENERALISE
-    generalise binder_names mbind tau_tvs lie_req tc_ty_sigs
-                               `thenTc` \ (tc_tyvars_to_gen, lie_free, dict_binds, dict_ids) ->
+       --      (it seems a bit crude to have to do getLIE twice,
+       --       but I can't see a better way just now)
+    addSrcLoc  (minimum (map getSrcLoc binder_names))          $
+    addErrCtxt (genCtxt binder_names)                          $
+    getLIE (generalise binder_names mbind tau_tvs lie_req tc_ty_sigs)
+                       `thenM` \ ((tc_tyvars_to_gen, dict_binds, dict_ids), lie_free) ->
 
 
        -- ZONK THE GENERALISED TYPE VARIABLES TO REAL TyVars
@@ -240,48 +275,45 @@ tcBindWithSigs top_lvl mbind tc_ty_sigs inline_sigs is_rec
        -- included in the forall types of the polymorphic Ids.
        -- At calls of these Ids we'll instantiate fresh type variables from
        -- them, and we use their boxity then.
-    mapNF_Tc zonkTcTyVarToTyVar tc_tyvars_to_gen       `thenNF_Tc` \ real_tyvars_to_gen ->
+    mappM zonkTcTyVarToTyVar tc_tyvars_to_gen  `thenM` \ real_tyvars_to_gen ->
 
        -- ZONK THE Ids
        -- It's important that the dict Ids are zonked, including the boxity set
        -- in the previous step, because they are later used to form the type of 
        -- the polymorphic thing, and forall-types must be zonked so far as 
        -- their bound variables are concerned
-    mapNF_Tc zonkId dict_ids                           `thenNF_Tc` \ zonked_dict_ids ->
-    mapNF_Tc zonkId mono_ids                           `thenNF_Tc` \ zonked_mono_ids ->
-
-       -- CHECK FOR BOGUS UNLIFTED BINDINGS
-    checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind zonked_mono_ids `thenTc_`
+    mappM zonkId dict_ids                              `thenM` \ zonked_dict_ids ->
+    mappM zonkId mono_ids                              `thenM` \ zonked_mono_ids ->
 
        -- BUILD THE POLYMORPHIC RESULT IDs
     let
        exports  = zipWith mk_export binder_names zonked_mono_ids
+       poly_ids = [poly_id | (_, poly_id, _) <- exports]
        dict_tys = map idType zonked_dict_ids
 
-       inlines    = mkNameSet [name | InlineSig name _ loc <- inline_sigs]
-        no_inlines = listToFM ([(name, IMustNotBeINLINEd False phase) | NoInlineSig name phase loc <- inline_sigs] ++
-                              [(name, IMustNotBeINLINEd True  phase) | InlineSig   name phase loc <- inline_sigs, maybeToBool phase])
-               -- "INLINE n foo" means inline foo, but not until at least phase n
-               -- "NOINLINE n foo" means don't inline foo until at least phase n, and even 
-               --                  then only if it is small enough etc.
-               -- "NOINLINE foo" means don't inline foo ever, which we signal with a (IMustNotBeINLINEd Nothing)
-               -- See comments in CoreUnfold.blackListed for the Authorised Version
+       inlines    = mkNameSet [name | InlineSig True name _ loc <- sigs]
+                       -- Any INLINE sig (regardless of phase control) 
+                       -- makes the RHS look small
+        inline_phases = listToFM [(name, phase) | InlineSig _ name phase _ <- sigs, 
+                                                 not (isAlwaysActive phase)]
+                       -- Set the IdInfo field to control the inline phase
+                       -- AlwaysActive is the default, so don't bother with them
 
        mk_export binder_name zonked_mono_id
          = (tyvars, 
-            attachNoInlinePrag no_inlines poly_id,
+            attachInlinePhase inline_phases poly_id,
             zonked_mono_id)
          where
            (tyvars, poly_id) = 
                case maybeSig tc_ty_sigs binder_name of
-                 Just (TySigInfo _ sig_poly_id sig_tyvars _ _ _ _ _) -> 
+                 Just (TySigInfo sig_poly_id sig_tyvars _ _ _ _ _) -> 
                        (sig_tyvars, sig_poly_id)
                  Nothing -> (real_tyvars_to_gen, new_poly_id)
 
            new_poly_id = mkLocalId binder_name poly_ty
            poly_ty = mkForAllTys real_tyvars_to_gen
-                       $ mkFunTys dict_tys 
-                       $ idType zonked_mono_id
+                   $ mkFunTys dict_tys 
+                   $ idType zonked_mono_id
                -- It's important to build a fully-zonked poly_ty, because
                -- we'll slurp out its free type variables when extending the
                -- local environment (tcExtendLocalValEnv); if it's not zonked
@@ -290,26 +322,45 @@ tcBindWithSigs top_lvl mbind tc_ty_sigs inline_sigs is_rec
     in
 
     traceTc (text "binding:" <+> ppr ((zonked_dict_ids, dict_binds),
-            exports, [idType poly_id | (_, poly_id, _) <- exports])) `thenTc_`
+                                     exports, map idType poly_ids)) `thenM_`
 
-        -- BUILD RESULTS
-    returnTc (
+       -- Check for an unlifted, non-overloaded group
+       -- In that case we must make extra checks
+    if any (isUnLiftedType . idType) zonked_mono_ids && null zonked_dict_ids 
+    then       -- Some bindings are unlifted
+       checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind      `thenM_` 
+       
+       extendLIEs lie_req                      `thenM_`
+       returnM (
+           AbsBinds [] [] exports inlines mbind',
+               -- Do not generate even any x=y bindings
+           poly_ids
+        )
+
+    else       -- The normal case
+    extendLIEs lie_free                                `thenM_`
+    returnM (
        AbsBinds real_tyvars_to_gen
                 zonked_dict_ids
                 exports
                 inlines
                 (dict_binds `andMonoBinds` mbind'),
-       lie_free,
-       [poly_id | (_, poly_id, _) <- exports]
+       poly_ids
     )
 
-attachNoInlinePrag no_inlines bndr
-  = case lookupFM no_inlines (idName bndr) of
+attachInlinePhase inline_phases bndr
+  = case lookupFM inline_phases (idName bndr) of
        Just prag -> bndr `setInlinePragma` prag
        Nothing   -> bndr
 
-checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind zonked_mono_ids
-  = ASSERT( not (any ((== unliftedTypeKind) . tyVarKind) real_tyvars_to_gen) )
+-- Check that non-overloaded unlifted bindings are
+--     a) non-recursive,
+--     b) not top level, 
+--     c) non-polymorphic
+--     d) not a multiple-binding group (more or less implied by (a))
+
+checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind
+  = ASSERT( not (any ((eqKind unliftedTypeKind) . tyVarKind) real_tyvars_to_gen) )
                -- The instCantBeGeneralised stuff in tcSimplify should have
                -- already raised an error if we're trying to generalise an 
                -- unboxed tyvar (NB: unboxed tyvars are always introduced 
@@ -317,34 +368,19 @@ checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind zonked_mono_ids
                -- because we have more precise origin information.
                -- That's why we just use an ASSERT here.
 
-       -- Check that pattern-bound variables are not unlifted
-    (if or [ (idName id `elem` pat_binders) && isUnLiftedType (idType id) 
-          | id <- zonked_mono_ids ] then
-       addErrTc (unliftedBindErr "Pattern" mbind)
-     else
-       returnTc ()
-    )                                                          `thenTc_`
-
-       -- Unlifted bindings must be non-recursive,
-       -- not top level, non-polymorphic, and not pattern bound
-    if any (isUnLiftedType . idType) zonked_mono_ids then
-       checkTc (isNotTopLevel top_lvl)
-               (unliftedBindErr "Top-level" mbind)             `thenTc_`
-       checkTc (isNonRec is_rec)
-               (unliftedBindErr "Recursive" mbind)             `thenTc_`
-       checkTc (null real_tyvars_to_gen)
-               (unliftedBindErr "Polymorphic" mbind)
-     else
-       returnTc ()
+    checkTc (isNotTopLevel top_lvl)
+           (unliftedBindErr "Top-level" mbind)         `thenM_`
+    checkTc (isNonRec is_rec)
+           (unliftedBindErr "Recursive" mbind)         `thenM_`
+    checkTc (single_bind mbind)
+           (unliftedBindErr "Multiple" mbind)          `thenM_`
+    checkTc (null real_tyvars_to_gen)
+           (unliftedBindErr "Polymorphic" mbind)
 
   where
-    pat_binders :: [Name]
-    pat_binders = collectMonoBinders (justPatBindings mbind EmptyMonoBinds)
-
-    justPatBindings bind@(PatMonoBind _ _ _) binds = bind `andMonoBinds` binds
-    justPatBindings (AndMonoBinds b1 b2) binds = 
-           justPatBindings b1 (justPatBindings b2 binds) 
-    justPatBindings other_bind binds = binds
+    single_bind (PatMonoBind _ _ _)   = True
+    single_bind (FunMonoBind _ _ _ _) = True
+    single_bind other                = False
 \end{code}
 
 
@@ -411,67 +447,48 @@ is doing.
 %************************************************************************
 
 \begin{code}
-generalise_help doc tau_tvs lie_req sigs
+generalise binder_names mbind tau_tvs lie_req sigs =
 
------------------------
-  | null sigs
-  =    -- INFERENCE CASE: Unrestricted group, no type signatures
-    tcSimplifyInfer doc
-                   tau_tvs lie_req
+  -- check for -fno-monomorphism-restriction
+  doptM Opt_NoMonomorphismRestriction          `thenM` \ no_MR ->
+  let is_unrestricted | no_MR    = True
+                     | otherwise = isUnRestrictedGroup tysig_names mbind
+  in
 
------------------------
-  | otherwise
-  =    -- CHECKING CASE: Unrestricted group, there are type signatures
-       -- Check signature contexts are empty 
-    checkSigsCtxts sigs                                `thenTc` \ (sig_avails, sig_dicts) ->
+  if not is_unrestricted then  -- RESTRICTED CASE
+       -- Check signature contexts are empty 
+    checkTc (all is_mono_sig sigs)
+           (restrictedBindCtxtErr binder_names)        `thenM_`
 
+       -- Now simplify with exactly that set of tyvars
+       -- We have to squash those Methods
+    tcSimplifyRestricted doc tau_tvs lie_req           `thenM` \ (qtvs, binds) ->
+
+       -- Check that signature type variables are OK
+    checkSigsTyVars qtvs sigs                          `thenM` \ final_qtvs ->
+
+    returnM (final_qtvs, binds, [])
+
+  else if null sigs then       -- UNRESTRICTED CASE, NO TYPE SIGS
+    tcSimplifyInfer doc tau_tvs lie_req
+
+  else                                 -- UNRESTRICTED CASE, WITH TYPE SIGS
+       -- CHECKING CASE: Unrestricted group, there are type signatures
+       -- Check signature contexts are identical
+    checkSigsCtxts sigs                        `thenM` \ (sig_avails, sig_dicts) ->
+    
        -- Check that the needed dicts can be
        -- expressed in terms of the signature ones
-    tcSimplifyInferCheck doc tau_tvs sig_avails lie_req        `thenTc` \ (forall_tvs, lie_free, dict_binds) ->
+    tcSimplifyInferCheck doc tau_tvs sig_avails lie_req        `thenM` \ (forall_tvs, dict_binds) ->
        
        -- Check that signature type variables are OK
-    checkSigsTyVars sigs                                       `thenTc_`
-
-    returnTc (forall_tvs, lie_free, dict_binds, sig_dicts)
-
-generalise binder_names mbind tau_tvs lie_req sigs
-  | is_unrestricted    -- UNRESTRICTED CASE
-  = generalise_help doc tau_tvs lie_req sigs
-
-  | otherwise          -- RESTRICTED CASE
-  =    -- Do a simplification to decide what type variables
-       -- are constrained.  We can't just take the free vars
-       -- of lie_req because that'll have methods that may
-       -- incidentally mention entirely unconstrained variables
-       --      e.g. a call to  f :: Eq a => a -> b -> b
-       -- Here, b is unconstrained.  A good example would be
-       --      foo = f (3::Int)
-       -- We want to infer the polymorphic type
-       --      foo :: forall b. b -> b
-    generalise_help doc tau_tvs lie_req sigs   `thenTc` \ (forall_tvs, lie_free, dict_binds, dict_ids) ->
-
-       -- Check signature contexts are empty 
-    checkTc (null sigs || null dict_ids)
-           (restrictedBindCtxtErr binder_names)        `thenTc_`
-
-       -- Identify constrained tyvars
-    let
-       constrained_tvs = varSetElems (tyVarsOfTypes (map idType dict_ids))
-                               -- The dict_ids are fully zonked
-       final_forall_tvs = forall_tvs `minusList` constrained_tvs
-    in
-
-       -- Now simplify with exactly that set of tyvars
-       -- We have to squash those Methods
-    tcSimplifyRestricted doc final_forall_tvs [] lie_req       `thenTc` \ (lie_free, binds) ->
+    checkSigsTyVars forall_tvs sigs                    `thenM` \ final_qtvs ->
 
-    returnTc (final_forall_tvs, lie_free, binds, [])
+    returnM (final_qtvs, dict_binds, sig_dicts)
 
   where
-    is_unrestricted | opt_NoMonomorphismRestriction = True
-                   | otherwise                     = isUnRestrictedGroup tysig_names mbind
-
-    tysig_names = [name | (TySigInfo name _ _ _ _ _ _ _) <- sigs]
+    tysig_names = map (idName . tcSigPolyId) sigs
+    is_mono_sig (TySigInfo _ _ theta _ _ _ _) = null theta
 
     doc = ptext SLIT("type signature(s) for") <+> pprBinders binder_names
 
@@ -483,38 +500,53 @@ generalise binder_names mbind tau_tvs lie_req sigs
        -- We unify them because, with polymorphic recursion, their types
        -- might not otherwise be related.  This is a rather subtle issue.
        -- ToDo: amplify
-checkSigsCtxts sigs@(TySigInfo _ id1 sig_tvs theta1 _ _ _ _ : other_sigs)
-  = mapTc_ check_one other_sigs                `thenTc_` 
+checkSigsCtxts sigs@(TySigInfo id1 sig_tvs theta1 _ _ _ src_loc : other_sigs)
+  = addSrcLoc src_loc                  $
+    mappM_ check_one other_sigs                `thenM_` 
     if null theta1 then
-       returnTc ([], [])               -- Non-overloaded type signatures
+       returnM ([], [])                -- Non-overloaded type signatures
     else
-    newDicts SignatureOrigin theta1    `thenNF_Tc` \ sig_dicts ->
+    newDicts SignatureOrigin theta1    `thenM` \ sig_dicts ->
     let
        -- The "sig_avails" is the stuff available.  We get that from
        -- the context of the type signature, BUT ALSO the lie_avail
        -- so that polymorphic recursion works right (see comments at end of fn)
        sig_avails = sig_dicts ++ sig_meths
     in
-    returnTc (sig_avails, map instToId sig_dicts)
+    returnM (sig_avails, map instToId sig_dicts)
   where
     sig1_dict_tys = map mkPredTy theta1
-    n_sig1_theta  = length theta1
-    sig_meths    = concat [insts | TySigInfo _ _ _ _ _ _ insts _ <- sigs]
+    sig_meths    = concat [insts | TySigInfo _ _ _ _ _ insts _ <- sigs]
 
-    check_one sig@(TySigInfo _ id _ theta _ _ _ src_loc)
-       = tcAddSrcLoc src_loc                                   $
-        tcAddErrCtxt (sigContextsCtxt id1 id)                  $
-        checkTc (length theta == n_sig1_theta) sigContextsErr  `thenTc_`
+    check_one sig@(TySigInfo id _ theta _ _ _ _)
+       = addErrCtxt (sigContextsCtxt id1 id)                   $
+        checkTc (equalLength theta theta1) sigContextsErr      `thenM_`
         unifyTauTyLists sig1_dict_tys (map mkPredTy theta)
 
-checkSigsTyVars sigs = mapTc_ check_one sigs
+checkSigsTyVars :: [TcTyVar] -> [TcSigInfo] -> TcM [TcTyVar]
+checkSigsTyVars qtvs sigs 
+  = mappM check_one sigs       `thenM` \ sig_tvs_s ->
+    let
+       -- Sigh.  Make sure that all the tyvars in the type sigs
+       -- appear in the returned ty var list, which is what we are
+       -- going to generalise over.  Reason: we occasionally get
+       -- silly types like
+       --      type T a = () -> ()
+       --      f :: T a
+       --      f () = ()
+       -- Here, 'a' won't appear in qtvs, so we have to add it
+
+       sig_tvs = foldr (unionVarSet . mkVarSet) emptyVarSet sig_tvs_s
+       all_tvs = mkVarSet qtvs `unionVarSet` sig_tvs
+    in
+    returnM (varSetElems all_tvs)
   where
-    check_one (TySigInfo _ id sig_tyvars sig_theta sig_tau _ _ src_loc)
-      = tcAddSrcLoc src_loc                                                    $
-       tcAddErrCtxtM (sigCtxt (sig_msg id) sig_tyvars sig_theta sig_tau)       $
-       checkSigTyVars sig_tyvars (idFreeTyVars id)
-
-    sig_msg id = ptext SLIT("When checking the type signature for") <+> quotes (ppr id)
+    check_one (TySigInfo id sig_tyvars sig_theta sig_tau _ _ src_loc)
+      = addSrcLoc src_loc                                              $
+       addErrCtxt (ptext SLIT("When checking the type signature for") 
+                     <+> quotes (ppr id))                              $
+       addErrCtxtM (sigCtxt id sig_tyvars sig_theta sig_tau)           $
+       checkSigTyVarsWrt (idFreeTyVars id) sig_tyvars
 \end{code}
 
 @getTyVarsToGen@ decides what type variables to generalise over.
@@ -565,14 +597,14 @@ is_elem v vs = isIn "isUnResMono" v vs
 
 isUnRestrictedGroup sigs (PatMonoBind other        _ _) = False
 isUnRestrictedGroup sigs (VarMonoBind v _)             = v `is_elem` sigs
-isUnRestrictedGroup sigs (FunMonoBind v _ matches _)   = any isUnRestrictedMatch matches || 
+isUnRestrictedGroup sigs (FunMonoBind v _ matches _)   = isUnRestrictedMatch matches || 
                                                          v `is_elem` sigs
 isUnRestrictedGroup sigs (AndMonoBinds mb1 mb2)                = isUnRestrictedGroup sigs mb1 &&
                                                          isUnRestrictedGroup sigs mb2
 isUnRestrictedGroup sigs EmptyMonoBinds                        = True
 
-isUnRestrictedMatch (Match _ [] Nothing _) = False     -- No args, no signature
-isUnRestrictedMatch other                 = True       -- Some args or a signature
+isUnRestrictedMatch (Match [] _ _ : _) = False -- No args => like a pattern binding
+isUnRestrictedMatch other             = True   -- Some args => a function binding
 \end{code}
 
 
@@ -587,126 +619,129 @@ The signatures have been dealt with already.
 
 \begin{code}
 tcMonoBinds :: RenamedMonoBinds 
-           -> [TcSigInfo]
-           -> RecFlag
+           -> [TcSigInfo] -> RecFlag
            -> TcM (TcMonoBinds, 
-                     LIE,              -- LIE required
-                     [Name],           -- Bound names
-                     [TcId])           -- Corresponding monomorphic bound things
+                   Bag (Name,          -- Bound names
+                        TcId))         -- Corresponding monomorphic bound things
 
 tcMonoBinds mbinds tc_ty_sigs is_rec
-  = tc_mb_pats mbinds          `thenTc` \ (complete_it, lie_req_pat, tvs, ids, lie_avail) ->
-    let
-       id_list           = bagToList ids
-       (names, mono_ids) = unzip id_list
-
-               -- This last defn is the key one:
-               -- extend the val envt with bindings for the 
-               -- things bound in this group, overriding the monomorphic
-               -- ids with the polymorphic ones from the pattern
-       extra_val_env = case is_rec of
-                         Recursive    -> map mk_bind id_list
-                         NonRecursive -> []
-    in
-       -- Don't know how to deal with pattern-bound existentials yet
-    checkTc (isEmptyBag tvs && isEmptyBag lie_avail) 
-           (existentialExplode mbinds)                 `thenTc_` 
-
-       -- *Before* checking the RHSs, but *after* checking *all* the patterns,
-       -- extend the envt with bindings for all the bound ids;
-       --   and *then* override with the polymorphic Ids from the signatures
-       -- That is the whole point of the "complete_it" stuff.
-       --
-       -- There's a further wrinkle: we have to delay extending the environment
-       -- until after we've dealt with any pattern-bound signature type variables
-       -- Consider  f (x::a) = ...f...
-       -- We're going to check that a isn't unified with anything in the envt, 
-       -- so f itself had better not be!  So we pass the envt binding f into
-       -- complete_it, which extends the actual envt in TcMatches.tcMatch, after
-       -- dealing with the signature tyvars
-
-    complete_it extra_val_env                          `thenTc` \ (mbinds', lie_req_rhss) ->
-
-    returnTc (mbinds', lie_req_pat `plusLIE` lie_req_rhss, names, mono_ids)
+       -- Three stages: 
+       -- 1. Check the patterns, building up an environment binding
+       --    the variables in this group (in the recursive case)
+       -- 2. Extend the environment
+       -- 3. Check the RHSs
+  = tc_mb_pats mbinds          `thenM` \ (complete_it, xve) ->
+    tcExtendLocalValEnv2 (bagToList xve) complete_it
   where
-
-       -- This function is used when dealing with a LHS binder; 
-       -- we make a monomorphic version of the Id.  
-       -- We check for a type signature; if there is one, we use the mono_id
-       -- from the signature.  This is how we make sure the tau part of the
-       -- signature actually maatches the type of the LHS; then tc_mb_pats
-       -- ensures the LHS and RHS have the same type
-       
-    tc_pat_bndr name pat_ty
-       = case maybeSig tc_ty_sigs name of
-           Nothing
-               -> newLocalId (getOccName name) pat_ty (getSrcLoc name)
-
-           Just (TySigInfo _ _ _ _ _ mono_id _ _)
-               -> tcAddSrcLoc (getSrcLoc name)         $
-                  unifyTauTy (idType mono_id) pat_ty   `thenTc_`
-                  returnTc mono_id
-
-    mk_bind (name, mono_id) = case maybeSig tc_ty_sigs name of
-                               Nothing                                   -> (name, mono_id)
-                               Just (TySigInfo name poly_id _ _ _ _ _ _) -> (name, poly_id)
-
-    tc_mb_pats EmptyMonoBinds
-      = returnTc (\ xve -> returnTc (EmptyMonoBinds, emptyLIE), emptyLIE, emptyBag, emptyBag, emptyLIE)
+    tc_mb_pats EmptyMonoBinds 
+      = returnM (returnM (EmptyMonoBinds, emptyBag), emptyBag)
 
     tc_mb_pats (AndMonoBinds mb1 mb2)
-      = tc_mb_pats mb1         `thenTc` \ (complete_it1, lie_req1, tvs1, ids1, lie_avail1) ->
-        tc_mb_pats mb2         `thenTc` \ (complete_it2, lie_req2, tvs2, ids2, lie_avail2) ->
+      = tc_mb_pats mb1         `thenM` \ (complete_it1, xve1) ->
+        tc_mb_pats mb2         `thenM` \ (complete_it2, xve2) ->
        let
-          complete_it xve = complete_it1 xve   `thenTc` \ (mb1', lie1) ->
-                            complete_it2 xve   `thenTc` \ (mb2', lie2) ->
-                            returnTc (AndMonoBinds mb1' mb2', lie1 `plusLIE` lie2)
+          complete_it = complete_it1   `thenM` \ (mb1', bs1) ->
+                        complete_it2   `thenM` \ (mb2', bs2) ->
+                        returnM (AndMonoBinds mb1' mb2', bs1 `unionBags` bs2)
        in
-       returnTc (complete_it,
-                 lie_req1 `plusLIE` lie_req2,
-                 tvs1 `unionBags` tvs2,
-                 ids1 `unionBags` ids2,
-                 lie_avail1 `plusLIE` lie_avail2)
+       returnM (complete_it, xve1 `unionBags` xve2)
 
     tc_mb_pats (FunMonoBind name inf matches locn)
-      = newTyVarTy kind                `thenNF_Tc` \ bndr_ty -> 
-       tc_pat_bndr name bndr_ty        `thenTc` \ bndr_id ->
+               -- Three cases:
+               --      a) Type sig supplied
+               --      b) No type sig and recursive
+               --      c) No type sig and non-recursive
+
+      | Just sig <- maybeSig tc_ty_sigs name 
+      = let    -- (a) There is a type signature
+               -- Use it for the environment extension, and check
+               -- the RHS has the appropriate type (with outer for-alls stripped off)
+          mono_id = tcSigMonoId sig
+          mono_ty = idType mono_id
+          complete_it = addSrcLoc locn                                 $
+                        tcMatchesFun name matches (Check mono_ty)      `thenM` \ matches' ->
+                        returnM (FunMonoBind mono_id inf matches' locn, 
+                                 unitBag (name, mono_id))
+       in
+       returnM (complete_it, if isRec is_rec then unitBag (name,tcSigPolyId sig) 
+                                             else emptyBag)
+
+      | isRec is_rec
+      =                -- (b) No type signature, and recursive
+               -- So we must use an ordinary H-M type variable
+               -- which means the variable gets an inferred tau-type
+       newLocalName name               `thenM` \ mono_name ->
+       newTyVarTy openTypeKind         `thenM` \ mono_ty ->
        let
-          complete_it xve = tcAddSrcLoc locn                           $
-                            tcMatchesFun xve name bndr_ty  matches     `thenTc` \ (matches', lie) ->
-                            returnTc (FunMonoBind bndr_id inf matches' locn, lie)
+          mono_id     = mkLocalId mono_name mono_ty
+          complete_it = addSrcLoc locn                                 $
+                        tcMatchesFun name matches (Check mono_ty)      `thenM` \ matches' ->
+                        returnM (FunMonoBind mono_id inf matches' locn, 
+                                 unitBag (name, mono_id))
        in
-       returnTc (complete_it, emptyLIE, emptyBag, unitBag (name, bndr_id), emptyLIE)
-
+       returnM (complete_it, unitBag (name, mono_id))
+
+      | otherwise      -- (c) No type signature, and non-recursive
+      =        let             -- So we can use a 'hole' type to infer a higher-rank type
+          complete_it 
+               = addSrcLoc locn                                $
+                 newHole                                       `thenM` \ hole -> 
+                 tcMatchesFun name matches (Infer hole)        `thenM` \ matches' ->
+                 readMutVar hole                               `thenM` \ fun_ty ->
+                 newLocalName name                             `thenM` \ mono_name ->
+                 let
+                    mono_id = mkLocalId mono_name fun_ty
+                 in
+                 returnM (FunMonoBind mono_id inf matches' locn, 
+                          unitBag (name, mono_id))
+       in
+       returnM (complete_it, emptyBag)
+       
     tc_mb_pats bind@(PatMonoBind pat grhss locn)
-      = tcAddSrcLoc locn               $
-       newTyVarTy kind                 `thenNF_Tc` \ pat_ty -> 
+      = addSrcLoc locn         $
 
                --      Now typecheck the pattern
-               -- We don't support binding fresh type variables in the
-               -- pattern of a pattern binding.  For example, this is illegal:
+               -- We do now support binding fresh (not-already-in-scope) scoped 
+               -- type variables in the pattern of a pattern binding.  
+               -- For example, this is now legal:
                --      (x::a, y::b) = e
-               -- whereas this is ok
-               --      (x::Int, y::Bool) = e
-               --
-               -- We don't check explicitly for this problem.  Instead, we simply
-               -- type check the pattern with tcPat.  If the pattern mentions any
-               -- fresh tyvars we simply get an out-of-scope type variable error
-       tcPat tc_pat_bndr pat pat_ty            `thenTc` \ (pat', lie_req, tvs, ids, lie_avail) ->
+               -- The type variables are brought into scope in tc_binds_and_then,
+               -- so we don't have to do anything here.
+
+       newHole                                 `thenM` \ hole -> 
+       tcPat tc_pat_bndr pat (Infer hole)      `thenM` \ (pat', tvs, ids, lie_avail) ->
+       readMutVar hole                         `thenM` \ pat_ty ->
+
+       -- Don't know how to deal with pattern-bound existentials yet
+        checkTc (isEmptyBag tvs && null lie_avail) 
+               (existentialExplode bind)       `thenM_` 
+
        let
-          complete_it xve = tcAddSrcLoc locn                           $
-                            tcAddErrCtxt (patMonoBindsCtxt bind)       $
-                            tcExtendLocalValEnv xve                    $
-                            tcGRHSs grhss pat_ty PatBindRhs            `thenTc` \ (grhss', lie) ->
-                            returnTc (PatMonoBind pat' grhss' locn, lie)
+          complete_it = addSrcLoc locn                                 $
+                        addErrCtxt (patMonoBindsCtxt bind)             $
+                        tcGRHSsPat grhss (Check pat_ty)        `thenM` \ grhss' ->
+                        returnM (PatMonoBind pat' grhss' locn, ids)
        in
-       returnTc (complete_it, lie_req, tvs, ids, lie_avail)
+       returnM (complete_it, if isRec is_rec then ids else emptyBag)
 
-       -- Figure out the appropriate kind for the pattern,
-       -- and generate a suitable type variable 
-    kind = case is_rec of
-               Recursive    -> liftedTypeKind  -- Recursive, so no unlifted types
-               NonRecursive -> openTypeKind    -- Non-recursive, so we permit unlifted types
+       -- tc_pat_bndr is used when dealing with a LHS binder in a pattern.
+       -- If there was a type sig for that Id, we want to make it much
+       -- as if that type signature had been on the binder as a SigPatIn.
+       -- We check for a type signature; if there is one, we use the mono_id
+       -- from the signature.  This is how we make sure the tau part of the
+       -- signature actually matches the type of the LHS; then tc_mb_pats
+       -- ensures the LHS and RHS have the same type
+       
+    tc_pat_bndr name pat_ty
+       = case maybeSig tc_ty_sigs name of
+           Nothing  -> newLocalName name                       `thenM` \ bndr_name ->
+                       tcMonoPatBndr bndr_name pat_ty
+
+           Just sig -> addSrcLoc (getSrcLoc name)              $
+                       tcSubPat (idType mono_id) pat_ty        `thenM` \ co_fn ->
+                       returnM (co_fn, mono_id)
+                    where
+                       mono_id = tcSigMonoId sig
 \end{code}
 
 
@@ -752,34 +787,37 @@ a RULE now:
        {-# SPECIALISE (f::<type) = g #-}
 
 \begin{code}
-tcSpecSigs :: [RenamedSig] -> TcM (TcMonoBinds, LIE)
+tcSpecSigs :: [RenamedSig] -> TcM TcMonoBinds
 tcSpecSigs (SpecSig name poly_ty src_loc : sigs)
   =    -- SPECIALISE f :: forall b. theta => tau  =  g
-    tcAddSrcLoc src_loc                                $
-    tcAddErrCtxt (valSpecSigCtxt name poly_ty) $
+    addSrcLoc src_loc                          $
+    addErrCtxt (valSpecSigCtxt name poly_ty)   $
 
        -- Get and instantiate its alleged specialised type
-    tcHsSigType poly_ty                                `thenTc` \ sig_ty ->
+    tcHsSigType (FunSigCtxt name) poly_ty      `thenM` \ sig_ty ->
 
        -- Check that f has a more general type, and build a RHS for
        -- the spec-pragma-id at the same time
-    tcExpr (HsVar name) sig_ty                 `thenTc` \ (spec_expr, spec_lie) ->
+    getLIE (tcCheckSigma (HsVar name) sig_ty)  `thenM` \ (spec_expr, spec_lie) ->
 
        -- Squeeze out any Methods (see comments with tcSimplifyToDicts)
-    tcSimplifyToDicts spec_lie                 `thenTc` \ (spec_dicts, spec_binds) ->
+    tcSimplifyToDicts spec_lie                 `thenM` \ spec_binds ->
 
        -- Just specialise "f" by building a SpecPragmaId binding
        -- It is the thing that makes sure we don't prematurely 
        -- dead-code-eliminate the binding we are really interested in.
-    newSpecPragmaId name sig_ty                `thenNF_Tc` \ spec_id ->
+    newLocalName name                  `thenM` \ spec_name ->
+    let
+       spec_bind = VarMonoBind (mkSpecPragmaId spec_name sig_ty)
+                               (mkHsLet spec_binds spec_expr)
+    in
 
        -- Do the rest and combine
-    tcSpecSigs sigs                    `thenTc` \ (binds_rest, lie_rest) ->
-    returnTc (binds_rest `andMonoBinds` VarMonoBind spec_id (mkHsLet spec_binds spec_expr),
-             lie_rest   `plusLIE`      mkLIE spec_dicts)
+    tcSpecSigs sigs                    `thenM` \ binds_rest ->
+    returnM (binds_rest `andMonoBinds` spec_bind)
 
 tcSpecSigs (other_sig : sigs) = tcSpecSigs sigs
-tcSpecSigs []                = returnTc (EmptyMonoBinds, emptyLIE)
+tcSpecSigs []                = returnM EmptyMonoBinds
 \end{code}
 
 
@@ -803,9 +841,10 @@ valSpecSigCtxt v ty
 sigContextsErr = ptext SLIT("Mismatched contexts")
 
 sigContextsCtxt s1 s2
-  = hang (hsep [ptext SLIT("When matching the contexts of the signatures for"), 
-               quotes (ppr s1), ptext SLIT("and"), quotes (ppr s2)])
-        4 (ptext SLIT("(the signature contexts in a mutually recursive group should all be identical)"))
+  = vcat [ptext SLIT("When matching the contexts of the signatures for"), 
+         nest 2 (vcat [ppr s1 <+> dcolon <+> ppr (idType s1),
+                       ppr s2 <+> dcolon <+> ppr (idType s2)]),
+         ptext SLIT("The signature contexts in a mutually recursive group should all be identical")]
 
 -----------------------------------------------
 unliftedBindErr flavour mbind
@@ -825,6 +864,11 @@ restrictedBindCtxtErr binder_names
        4 (vcat [ptext SLIT("in a binding group for") <+> pprBinders binder_names,
                ptext SLIT("that falls under the monomorphism restriction")])
 
+genCtxt binder_names
+  = ptext SLIT("When generalising the type(s) for") <+> pprBinders binder_names
+
 -- Used in error messages
-pprBinders bndrs = pprWithCommas ppr bndrs
+-- Use quotes for a single one; they look a bit "busy" for several
+pprBinders [bndr] = quotes (ppr bndr)
+pprBinders bndrs  = pprWithCommas ppr bndrs
 \end{code}