[project @ 2003-09-20 17:26:46 by ross]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcBinds.lhs
index a33e7f4..b5d2cb7 100644 (file)
@@ -4,61 +4,51 @@
 \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 HsSyn           ( HsExpr(..), HsBinds(..), MonoBinds(..), Sig(..), StmtCtxt(..),
-                         Match(..), collectMonoBinders, andMonoBinds
+import CmdLineOpts     ( DynFlag(Opt_NoMonomorphismRestriction) )
+import HsSyn           ( HsExpr(..), HsBinds(..), MonoBinds(..), Sig(..), 
+                         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, tyVarsOfInst, instToId,
-                         getAllFunDepsOfLIE, getIPsOfLIE, zonkFunDeps
-                       )
-import TcEnv           ( tcExtendLocalValEnv,
-                         newSpecPragmaId, newLocalId,
-                         tcLookupTyCon, 
-                         tcGetGlobalTyVars, tcExtendGlobalTyVars
-                       )
-import TcSimplify      ( tcSimplify, tcSimplifyAndCheck, tcSimplifyToDicts )
-import TcImprove       ( tcImprove )
-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          ( TcThetaType, newTyVarTy, newTyVar, 
-                         zonkTcTypes, zonkTcThetaType, 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 Id              ( mkVanillaId, setInlinePragma, idFreeTyVars )
+import CoreFVs         ( idFreeTyVars )
+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, mkTyConApp,
-                         mkForAllTys, mkFunTys, 
-                         mkPredTy, mkForAllTy, isUnLiftedType, 
-                         isUnboxedType, unboxedTypeKind, boxedTypeKind, openTypeKind
-                       )
-import FunDeps         ( tyVarFunDep, oclose )
 import Var             ( tyVarKind )
 import VarSet
 import Bag
-import Util            ( isIn )
-import Maybes          ( maybeToBool )
-import BasicTypes      ( TopLevelFlag(..), RecFlag(..), isNotTopLevel )
+import Util            ( isIn, equalLength )
+import BasicTypes      ( TopLevelFlag(..), RecFlag(..), isNonRec, isRec, 
+                         isNotTopLevel, isAlwaysActive )
 import FiniteMap       ( listToFM, lookupFM )
-import PrelNames       ( ioTyConName, mainKey, hasKey )
 import Outputable
 \end{code}
 
@@ -95,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
 
@@ -122,91 +121,88 @@ 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 ->
-  
-      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] $
+  =    -- 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) ->
   
-         -- 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 unboxed 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}
 
-An aside.  The original version of @tcBindsAndThen@ which lacks a
-combiner function, appears below.  Though it is perfectly well
-behaved, it cannot be typed by Haskell, because the recursive call is
-at a different type to the definition itself.  There aren't too many
-examples of this, which is why I thought it worth preserving! [SLPJ]
-
-\begin{pseudocode}
-% tcBindsAndThen
-%      :: RenamedHsBinds
-%      -> TcM (thing, LIE, thing_ty))
-%      -> TcM ((TcHsBinds, thing), LIE, thing_ty)
-% 
-% tcBindsAndThen EmptyBinds do_next
-%   = do_next          `thenTc` \ (thing, lie, thing_ty) ->
-%     returnTc ((EmptyBinds, thing), lie, thing_ty)
-% 
-% tcBindsAndThen (ThenBinds binds1 binds2) do_next
-%   = tcBindsAndThen binds1 (tcBindsAndThen binds2 do_next)
-%      `thenTc` \ ((binds1', (binds2', thing')), lie1, thing_ty) ->
-% 
-%     returnTc ((binds1' `ThenBinds` binds2', thing'), lie1, thing_ty)
-% 
-% tcBindsAndThen (MonoBind bind sigs is_rec) do_next
-%   = tcBindAndThen bind sigs do_next
-\end{pseudocode}
-
 
 %************************************************************************
 %*                                                                     *
@@ -228,218 +224,166 @@ 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 boxedTypeKind          `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 -> mkVanillaId 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) ->
-
-       -- CHECK THAT THE SIGNATURES MATCH
-       -- (must do this before getTyVarsToGen)
-    checkSigMatch top_lvl binder_names mono_ids tc_ty_sigs     `thenTc` \ maybe_sig_theta ->   
-
-       -- IMPROVE the LIE
-       -- Force any unifications dictated by functional dependencies.
-       -- Because unification may happen, it's important that this step
-       -- come before:
-       --   - computing vars over which to quantify
-       --   - zonking the generalized type vars
-    let lie_avail = case maybe_sig_theta of
-                     Nothing      -> emptyLIE
-                     Just (_, la) -> la
-       lie_avail_req = lie_avail `plusLIE` lie_req in
-    tcImprove lie_avail_req                            `thenTc_`
-
-       -- COMPUTE VARIABLES OVER WHICH TO QUANTIFY, namely tyvars_to_gen
-       -- The tyvars_not_to_gen are free in the environment, and hence
-       -- candidates for generalisation, but sometimes the monomorphism
-       -- restriction means we can't generalise them nevertheless
+    getLIE (tcMonoBinds mbind tc_ty_sigs is_rec)       `thenM` \ ((mbind', bndr_names_w_ids), lie_req) ->
     let
-       mono_id_tys = map idType mono_ids
+       (binder_names, mono_ids) = unzip (bagToList bndr_names_w_ids)
+       tau_tvs = foldr (unionVarSet . tyVarsOfType . idType) emptyVarSet mono_ids
     in
-    getTyVarsToGen is_unrestricted mono_id_tys lie_req `thenNF_Tc` \ (tyvars_not_to_gen, tyvars_to_gen) ->
-
-       -- Finally, zonk the generalised type variables to real TyVars
-       -- This commits any unbound kind variables to boxed kind
-       -- I'm a little worried that such a kind variable might be
-       -- free in the environment, but I don't think it's possible for
-       -- this to happen when the type variable is not free in the envt
-       -- (which it isn't).            SLPJ Nov 98
-    mapTc zonkTcTyVarToTyVar (varSetElems tyvars_to_gen)       `thenTc` \ real_tyvars_to_gen_list ->
-    let
-       real_tyvars_to_gen = mkVarSet real_tyvars_to_gen_list
-               -- It's important that the final list 
-               -- (real_tyvars_to_gen and real_tyvars_to_gen_list) is fully
-               -- zonked, *including boxity*, because they'll be included in the forall types of
-               -- the polymorphic Ids, and instances of these Ids will be generated from them.
-               -- 
-               -- Also NB that tcSimplify takes zonked tyvars as its arg, hence we pass
-               -- real_tyvars_to_gen
-    in
-
-       -- SIMPLIFY THE LIE
-    tcExtendGlobalTyVars tyvars_not_to_gen (
-       let ips = getIPsOfLIE lie_avail_req in
-       if null real_tyvars_to_gen_list && (null ips || not is_unrestricted) then
-               -- No polymorphism, and no IPs, so no need to simplify context
-           returnTc (lie_req, EmptyMonoBinds, [])
-       else
-       case maybe_sig_theta of
-         Nothing ->
-               -- No signatures, so just simplify the lie
-               -- NB: no signatures => no polymorphic recursion, so no
-               -- need to use lie_avail (which will be empty anyway)
-           tcSimplify (text "tcBinds1" <+> ppr binder_names)
-                      real_tyvars_to_gen lie_req       `thenTc` \ (lie_free, dict_binds, lie_bound) ->
-           returnTc (lie_free, dict_binds, map instToId (bagToList lie_bound))
-
-         Just (sig_theta, lie_avail) ->
-               -- There are signatures, and their context is sig_theta
-               -- Furthermore, lie_avail is an LIE containing the 'method insts'
-               -- for the things bound here
-
-           zonkTcThetaType sig_theta                   `thenNF_Tc` \ sig_theta' ->
-           newDicts SignatureOrigin sig_theta'         `thenNF_Tc` \ (dicts_sig, dict_ids) ->
-               -- It's important that sig_theta is zonked, because
-               -- dict_id is later used to form the type of the polymorphic thing,
-               -- and forall-types must be zonked so far as their bound variables
-               -- are concerned
-
-           let
-               -- The "givens" 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)
-               givens = dicts_sig `plusLIE` lie_avail
-           in
-
-               -- Check that the needed dicts can be expressed in
-               -- terms of the signature ones
-           tcAddErrCtxt  (bindSigsCtxt tysig_names) $
-           tcSimplifyAndCheck
-               (ptext SLIT("type signature for") <+> pprQuotedList binder_names)
-               real_tyvars_to_gen givens lie_req       `thenTc` \ (lie_free, dict_binds) ->
-
-           returnTc (lie_free, dict_binds, dict_ids)
-
-    )                                          `thenTc` \ (lie_free, dict_binds, dicts_bound) ->
-
-       -- GET THE FINAL MONO_ID_TYS
-    zonkTcTypes mono_id_tys                    `thenNF_Tc` \ zonked_mono_id_types ->
-
-
-       -- CHECK FOR BOGUS UNPOINTED BINDINGS
-    (if any isUnLiftedType zonked_mono_id_types then
-               -- Unlifted bindings must be non-recursive,
-               -- not top level, and non-polymorphic
-       checkTc (isNotTopLevel top_lvl)
-               (unliftedBindErr "Top-level" mbind)             `thenTc_`
-       checkTc (case is_rec of {Recursive -> False; NonRecursive -> True})
-               (unliftedBindErr "Recursive" mbind)             `thenTc_`
-       checkTc (null real_tyvars_to_gen_list)
-               (unliftedBindErr "Polymorphic" mbind)
-     else
-       returnTc ()
-    )                                                  `thenTc_`
-
-    ASSERT( not (any ((== unboxedTypeKind) . tyVarKind) real_tyvars_to_gen_list) )
-               -- 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 
-               -- along with a class constraint) and it's better done there 
-               -- because we have more precise origin information.
-               -- That's why we just use an ASSERT here.
 
-
-        -- BUILD THE POLYMORPHIC RESULT IDs
-    mapNF_Tc zonkId mono_ids           `thenNF_Tc` \ zonked_mono_ids ->
+       -- GENERALISE
+       --      (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
+       -- This commits any unbound kind variables to boxed kind, by unification
+       -- It's important that the final quanfified type variables
+       -- are fully zonked, *including boxity*, because they'll be 
+       -- 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.
+    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
+    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
-       dict_tys = map idType dicts_bound
+       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_list, new_poly_id)
+                 Nothing -> (real_tyvars_to_gen, new_poly_id)
 
-           new_poly_id = mkVanillaId binder_name poly_ty
-           poly_ty = mkForAllTys real_tyvars_to_gen_list 
-                       $ mkFunTys dict_tys 
-                       $ idType (zonked_mono_id)
+           new_poly_id = mkLocalId binder_name poly_ty
+           poly_ty = mkForAllTys real_tyvars_to_gen
+                   $ 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
                -- it appears to have free tyvars that aren't actually free 
                -- at all.
-       
-       pat_binders :: [Name]
-       pat_binders = collectMonoBinders (justPatBindings mbind EmptyMonoBinds)
     in
-       -- CHECK FOR UNBOXED BINDERS IN PATTERN BINDINGS
-    mapTc (\id -> checkTc (not (idName id `elem` pat_binders
-                               && isUnboxedType (idType id)))
-                         (unboxedPatBindErr id)) zonked_mono_ids
-                               `thenTc_`
-
-        -- BUILD RESULTS
-    returnTc (
-        -- pprTrace "binding.." (ppr ((dicts_bound, dict_binds), exports, [idType poly_id | (_, poly_id, _) <- exports])) $
-        AbsBinds real_tyvars_to_gen_list
-                 dicts_bound
-                 exports
-                 inlines
-                 (dict_binds `andMonoBinds` mbind'),
-        lie_free,
-        [poly_id | (_, poly_id, _) <- exports]
-    )
-  where
-    tysig_names     = [name | (TySigInfo name _ _ _ _ _ _ _) <- tc_ty_sigs]
-    is_unrestricted = isUnRestrictedGroup tysig_names mbind
 
-justPatBindings bind@(PatMonoBind _ _ _) binds = bind `andMonoBinds` binds
-justPatBindings (AndMonoBinds b1 b2) binds = 
-       justPatBindings b1 (justPatBindings b2 binds) 
-justPatBindings other_bind binds = binds
+    traceTc (text "binding:" <+> ppr ((zonked_dict_ids, dict_binds),
+                                     exports, map idType poly_ids)) `thenM_`
 
-attachNoInlinePrag no_inlines bndr
-  = case lookupFM no_inlines (idName bndr) of
+       -- 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'),
+       poly_ids
+    )
+
+attachInlinePhase inline_phases bndr
+  = case lookupFM inline_phases (idName bndr) of
        Just prag -> bndr `setInlinePragma` prag
        Nothing   -> bndr
+
+-- 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 
+               -- along with a class constraint) and it's better done there 
+               -- because we have more precise origin information.
+               -- That's why we just use an ASSERT here.
+
+    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
+    single_bind (PatMonoBind _ _ _)   = True
+    single_bind (FunMonoBind _ _ _ _) = True
+    single_bind other                = False
 \end{code}
 
+
 Polymorphic recursion
 ~~~~~~~~~~~~~~~~~~~~~
 The game plan for polymorphic recursion in the code above is 
@@ -502,6 +446,109 @@ is doing.
 %*                                                                     *
 %************************************************************************
 
+\begin{code}
+generalise binder_names mbind tau_tvs lie_req sigs =
+
+  -- check for -fno-monomorphism-restriction
+  doptM Opt_NoMonomorphismRestriction          `thenM` \ no_MR ->
+  let is_unrestricted | no_MR    = True
+                     | otherwise = isUnRestrictedGroup tysig_names mbind
+  in
+
+  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        `thenM` \ (forall_tvs, dict_binds) ->
+       
+       -- Check that signature type variables are OK
+    checkSigsTyVars forall_tvs sigs                    `thenM` \ final_qtvs ->
+
+    returnM (final_qtvs, dict_binds, sig_dicts)
+
+  where
+    tysig_names = map (idName . tcSigPolyId) sigs
+    is_mono_sig (TySigInfo _ _ theta _ _ _ _) = null theta
+
+    doc = ptext SLIT("type signature(s) for") <+> pprBinders binder_names
+
+-----------------------
+       -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE UNIFIABLE
+       -- The type signatures on a mutually-recursive group of definitions
+       -- must all have the same context (or none).
+       --
+       -- 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 _ _ _ src_loc : other_sigs)
+  = addSrcLoc src_loc                  $
+    mappM_ check_one other_sigs                `thenM_` 
+    if null theta1 then
+       returnM ([], [])                -- Non-overloaded type signatures
+    else
+    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
+    returnM (sig_avails, map instToId sig_dicts)
+  where
+    sig1_dict_tys = map mkPredTy theta1
+    sig_meths    = concat [insts | TySigInfo _ _ _ _ _ insts _ <- sigs]
+
+    check_one sig@(TySigInfo id _ theta _ _ _ _)
+       = addErrCtxt (sigContextsCtxt id1 id)                   $
+        checkTc (equalLength theta theta1) sigContextsErr      `thenM_`
+        unifyTauTyLists sig1_dict_tys (map mkPredTy theta)
+
+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)
+      = 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.
 
 For a "restricted group" -- see the monomorphism restriction
@@ -530,6 +577,8 @@ generalise.  We must be careful about doing this:
        Another, more common, example is when there's a Method inst in
        the LIE, whose type might very well involve non-overloaded
        type variables.
+  [NOTE: Jan 2001: I don't understand the problem here so I'm doing 
+       the simple thing instead]
 
  (b) On the other hand, we mustn't generalise tyvars which are constrained,
        because we are going to pass on out the unmodified LIE, with those
@@ -540,43 +589,6 @@ constrained tyvars. We don't use any of the results, except to
 find which tyvars are constrained.
 
 \begin{code}
-getTyVarsToGen is_unrestricted mono_id_tys lie
-  = tcGetGlobalTyVars                  `thenNF_Tc` \ free_tyvars ->
-    zonkTcTypes mono_id_tys            `thenNF_Tc` \ zonked_mono_id_tys ->
-    let
-       body_tyvars = tyVarsOfTypes zonked_mono_id_tys `minusVarSet` free_tyvars
-       fds         = getAllFunDepsOfLIE lie
-    in
-    if is_unrestricted
-    then
-         -- We need to augment the type variables that appear explicitly in
-         -- the type by those that are determined by the functional dependencies.
-         -- e.g. suppose our type is   C a b => a -> a
-         --    with the fun-dep  a->b
-         -- Then we should generalise over b too; otherwise it will be
-         -- reported as ambiguous.
-       zonkFunDeps fds         `thenNF_Tc` \ fds' ->
-       let tvFundep        = tyVarFunDep fds'
-           extended_tyvars = oclose tvFundep body_tyvars
-       in
-       returnNF_Tc (emptyVarSet, extended_tyvars)
-    else
-       -- This recover and discard-errs is to avoid duplicate error
-       -- messages; this, after all, is an "extra" call to tcSimplify
-       recoverNF_Tc (returnNF_Tc (emptyVarSet, body_tyvars))           $
-       discardErrsTc                                                   $
-
-       tcSimplify (text "getTVG") body_tyvars lie    `thenTc` \ (_, _, constrained_dicts) ->
-       let
-         -- ASSERT: dicts_sig is already zonked!
-           constrained_tyvars    = foldrBag (unionVarSet . tyVarsOfInst) emptyVarSet constrained_dicts
-           reduced_tyvars_to_gen = body_tyvars `minusVarSet` constrained_tyvars
-        in
-        returnTc (constrained_tyvars, reduced_tyvars_to_gen)
-\end{code}
-
-
-\begin{code}
 isUnRestrictedGroup :: [Name]          -- Signatures given for these
                    -> RenamedMonoBinds
                    -> Bool
@@ -585,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}
 
 
@@ -607,219 +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 type signatures
-    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) ->
-       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)
-       in
-       returnTc (complete_it, 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.
 
-       -- Figure out the appropriate kind for the pattern,
-       -- and generate a suitable type variable 
-    kind = case is_rec of
-               Recursive    -> boxedTypeKind   -- Recursive, so no unboxed types
-               NonRecursive -> openTypeKind    -- Non-recursive, so we permit unboxed types
-\end{code}
-
-%************************************************************************
-%*                                                                     *
-\subsection{Signatures}
-%*                                                                     *
-%************************************************************************
-
-@checkSigMatch@ does the next step in checking signature matching.
-The tau-type part has already been unified.  What we do here is to
-check that this unification has not over-constrained the (polymorphic)
-type variables of the original signature type.
-
-The error message here is somewhat unsatisfactory, but it'll do for
-now (ToDo).
-
-\begin{code}
-checkSigMatch :: TopLevelFlag -> [Name] -> [TcId] -> [TcSigInfo] -> TcM (Maybe (TcThetaType, LIE))
-checkSigMatch top_lvl binder_names mono_ids sigs
-  | main_bound_here
-  =    -- First unify the main_id with IO t, for any old t
-    tcSetErrCtxt mainTyCheckCtxt (
-       tcLookupTyCon ioTyConName               `thenTc`    \ ioTyCon ->
-       newTyVarTy boxedTypeKind                `thenNF_Tc` \ t_tv ->
-       unifyTauTy ((mkTyConApp ioTyCon [t_tv]))
-                  (idType main_mono_id)
-    )                                          `thenTc_`
-
-       -- Now check the signatures
-       -- Must do this after the unification with IO t, 
-       -- in case of a silly signature like
-       --      main :: forall a. a
-       -- The unification to IO t will bind the type variable 'a',
-       -- which is just waht check_one_sig looks for
-    mapTc check_one_sig sigs                   `thenTc_`
-    mapTc check_main_ctxt sigs                 `thenTc_` 
-
-           returnTc (Just ([], emptyLIE))
-
-  | not (null sigs)
-  = mapTc check_one_sig sigs                   `thenTc_`
-    mapTc check_one_ctxt all_sigs_but_first    `thenTc_`
-    returnTc (Just (theta1, sig_lie))
-
-  | otherwise
-  = returnTc Nothing           -- No constraints from type sigs
-
-  where
-    (TySigInfo _ id1 _ theta1 _ _ _ _ : all_sigs_but_first) = sigs
-
-    sig1_dict_tys      = mk_dict_tys theta1
-    n_sig1_dict_tys    = length sig1_dict_tys
-    sig_lie            = mkLIE (concat [insts | TySigInfo _ _ _ _ _ _ insts _ <- sigs])
-
-    maybe_main        = find_main top_lvl binder_names mono_ids
-    main_bound_here   = maybeToBool maybe_main
-    Just main_mono_id = maybe_main
-                     
-       -- CHECK THAT THE SIGNATURE TYVARS AND TAU_TYPES ARE OK
-       -- Doesn't affect substitution
-    check_one_sig (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)
+       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_` 
 
-       -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE UNIFIABLE
-       -- The type signatures on a mutually-recursive group of definitions
-       -- must all have the same context (or none).
-       --
-       -- We unify them because, with polymorphic recursion, their types
-       -- might not otherwise be related.  This is a rather subtle issue.
-       -- ToDo: amplify
-    check_one_ctxt sig@(TySigInfo _ id _ theta _ _ _ src_loc)
-       = tcAddSrcLoc src_loc   $
-        tcAddErrCtxt (sigContextsCtxt id1 id) $
-        checkTc (length this_sig_dict_tys == n_sig1_dict_tys)
-                               sigContextsErr          `thenTc_`
-        unifyTauTyLists sig1_dict_tys this_sig_dict_tys
-      where
-        this_sig_dict_tys = mk_dict_tys theta
-
-       -- CHECK THAT FOR A GROUP INVOLVING Main.main, all 
-       -- the signature contexts are empty (what a bore)
-    check_main_ctxt sig@(TySigInfo _ id _ theta _ _ _ src_loc)
-       = tcAddSrcLoc src_loc   $
-         checkTc (null theta) (mainContextsErr id)
-
-    mk_dict_tys theta = map mkPredTy theta
-
-    sig_msg id = ptext SLIT("When checking the type signature for") <+> quotes (ppr id)
-
-       -- Search for Main.main in the binder_names, return corresponding mono_id
-    find_main NotTopLevel binder_names mono_ids = Nothing
-    find_main TopLevel    binder_names mono_ids = go binder_names mono_ids
-    go [] [] = Nothing
-    go (n:ns) (m:ms) | n `hasKey` mainKey = Just m
-                    | otherwise          = go ns ms
+       let
+          complete_it = addSrcLoc locn                                 $
+                        addErrCtxt (patMonoBindsCtxt bind)             $
+                        tcGRHSsPat grhss (Check pat_ty)        `thenM` \ grhss' ->
+                        returnM (PatMonoBind pat' grhss' locn, ids)
+       in
+       returnM (complete_it, if isRec is_rec then ids else emptyBag)
+
+       -- 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}
 
 
@@ -865,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_lie1, 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`      spec_lie1)
+    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}
 
 
@@ -913,41 +838,37 @@ valSpecSigCtxt v ty
         nest 4 (ppr v <+> dcolon <+> ppr ty)]
 
 -----------------------------------------------
-unboxedPatBindErr id
-  = ptext SLIT("variable in a lazy pattern binding has unboxed type: ")
-        <+> quotes (ppr id)
-
------------------------------------------------
-bindSigsCtxt ids
-  = ptext SLIT("When checking the type signature(s) for") <+> pprQuotedList ids
-
------------------------------------------------
-sigContextsErr
-  = ptext SLIT("Mismatched contexts")
+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)"))
-
-mainContextsErr id
-  | id `hasKey` mainKey = ptext SLIT("Main.main cannot be overloaded")
-  | otherwise
-  = quotes (ppr id) <+> ptext SLIT("cannot be overloaded") <> char ',' <> -- sigh; workaround for cpp's inability to deal
-    ptext SLIT("because it is mutually recursive with Main.main")         -- with commas inside SLIT strings.
-
-mainTyCheckCtxt
-  = hsep [ptext SLIT("When checking that"), quotes (ptext SLIT("main")),
-         ptext SLIT("has the required type")]
+  = 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
-  = hang (text flavour <+> ptext SLIT("bindings for unlifted types aren't allowed"))
+  = hang (text flavour <+> ptext SLIT("bindings for unlifted types aren't allowed:"))
         4 (ppr mbind)
 
+-----------------------------------------------
 existentialExplode mbinds
   = hang (vcat [text "My brain just exploded.",
                text "I can't handle pattern bindings for existentially-quantified constructors.",
                text "In the binding group"])
        4 (ppr mbinds)
+
+-----------------------------------------------
+restrictedBindCtxtErr binder_names
+  = hang (ptext SLIT("Illegal overloaded type signature(s)"))
+       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
+-- 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}