[project @ 2001-11-30 09:32:27 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcBinds.lhs
index a590e57..76fc669 100644 (file)
@@ -1,69 +1,59 @@
 %
 %
-% (c) The GRASP/AQUA Project, Glasgow University, 1992-1996
+% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[TcBinds]{TcBinds}
 
 \begin{code}
 %
 \section[TcBinds]{TcBinds}
 
 \begin{code}
-#include "HsVersions.h"
+module TcBinds ( tcBindsAndThen, tcTopBinds,
+                tcSpecSigs, tcBindWithSigs ) where
 
 
-module TcBinds ( tcBindsAndThen, tcPragmaSigs, checkSigTyVars, tcBindWithSigs, TcSigInfo(..) ) where
+#include "HsVersions.h"
 
 
-IMP_Ubiq()
+import {-# SOURCE #-} TcMatches ( tcGRHSs, tcMatchesFun )
+import {-# SOURCE #-} TcExpr  ( tcExpr )
 
 
-import HsSyn           ( HsBinds(..), Sig(..), MonoBinds(..), 
-                         Match, HsType, InPat(..), OutPat(..), HsExpr(..),
-                         SYN_IE(RecFlag), nonRecursive,
-                         GRHSsAndBinds, ArithSeqInfo, HsLit, Fake, Stmt, DoOrListComp, Fixity, 
-                         collectMonoBinders )
-import RnHsSyn         ( SYN_IE(RenamedHsBinds), RenamedSig(..), 
-                         SYN_IE(RenamedMonoBinds)
-                       )
-import TcHsSyn         ( SYN_IE(TcHsBinds), SYN_IE(TcMonoBinds),
-                         TcIdOcc(..), SYN_IE(TcIdBndr), SYN_IE(TcExpr), 
-                         tcIdType
+import CmdLineOpts     ( opt_NoMonomorphismRestriction )
+import HsSyn           ( HsExpr(..), HsBinds(..), MonoBinds(..), Sig(..), 
+                         Match(..), HsMatchContext(..), 
+                         collectMonoBinders, andMonoBinds,
+                         collectSigTysFromMonoBinds
                        )
                        )
+import RnHsSyn         ( RenamedHsBinds, RenamedSig, RenamedMonoBinds )
+import TcHsSyn         ( TcMonoBinds, TcId, zonkId, mkHsLet )
 
 import TcMonad
 
 import TcMonad
-import Inst            ( Inst, SYN_IE(LIE), emptyLIE, plusLIE, InstOrigin(..),
-                         newDicts, tyVarsOfInst, instToId
+import Inst            ( LIE, emptyLIE, mkLIE, plusLIE, InstOrigin(..),
+                         newDicts, instToId
                        )
                        )
-import TcEnv           ( tcExtendLocalValEnv, tcLookupLocalValueOK, newMonoIds,
-                         tcGetGlobalTyVars, tcExtendGlobalTyVars
+import TcEnv           ( tcExtendLocalValEnv, newLocalName )
+import TcUnify         ( unifyTauTyLists, checkSigTyVars, sigCtxt )
+import TcSimplify      ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted, tcSimplifyToDicts )
+import TcMonoType      ( tcHsSigType, UserTypeCtxt(..), 
+                         TcSigInfo(..), tcTySig, maybeSig, tcAddScopedTyVars
                        )
                        )
-import SpecEnv         ( SpecEnv )
-IMPORT_DELOOPER(TcLoop)                ( tcGRHSsAndBinds )
-import TcMatches       ( tcMatchesFun )
-import TcSimplify      ( tcSimplify, tcSimplifyAndCheck )
-import TcMonoType      ( tcHsType )
-import TcPat           ( tcPat )
+import TcPat           ( tcPat, tcSubPat, tcMonoPatBndr )
 import TcSimplify      ( bindInstsOfLocalFuns )
 import TcSimplify      ( bindInstsOfLocalFuns )
-import TcType          ( SYN_IE(TcType), SYN_IE(TcThetaType), SYN_IE(TcTauType), 
-                         SYN_IE(TcTyVarSet), SYN_IE(TcTyVar),
-                         newTyVarTy, zonkTcType, zonkTcTyVar, zonkTcTyVars,
-                         newTcTyVar, tcInstSigType, newTyVarTys
+import TcMType         ( newTyVar, newTyVarTy, newHoleTyVarTy,
+                         zonkTcTyVarToTyVar
                        )
                        )
-import Unify           ( unifyTauTy, unifyTauTyLists )
-
-import Kind            ( isUnboxedTypeKind, mkTypeKind, isTypeKind, mkBoxedTypeKind )
-import Id              ( GenId, idType, mkUserLocal, mkUserId )
-import IdInfo          ( noIdInfo )
-import Maybes          ( maybeToBool, assocMaybe, catMaybes )
-import Name            ( getOccName, getSrcLoc, Name )
-import PragmaInfo      ( PragmaInfo(..) )
-import Pretty
-import Type            ( mkTyVarTy, mkTyVarTys, isTyVarTy, tyVarsOfTypes, eqSimpleTheta, 
-                         mkSigmaTy, splitSigmaTy, mkForAllTys, mkFunTys, getTyVar, mkDictTy,
-                         splitRhoTy, mkForAllTy, splitForAllTy )
-import TyVar           ( GenTyVar, SYN_IE(TyVar), tyVarKind, minusTyVarSet, emptyTyVarSet,
-                         elementOfTyVarSet, unionTyVarSets, tyVarSetToList )
-import Bag             ( bagToList, foldrBag, isEmptyBag )
-import Util            ( isIn, zipEqual, zipWithEqual, zipWith3Equal, hasNoDups, assoc,
-                         assertPanic, panic, pprTrace )
-import PprType         ( GenClass, GenType, GenTyVar )
-import Unique          ( Unique )
-import SrcLoc           ( SrcLoc )
-
-import Outputable      --( interppSP, interpp'SP )
+import TcType          ( mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType, 
+                         mkPredTy, mkForAllTy, isUnLiftedType, 
+                         unliftedTypeKind, liftedTypeKind, openTypeKind, eqKind
+                       )
+
+import CoreFVs         ( idFreeTyVars )
+import Id              ( mkLocalId, mkSpecPragmaId, setInlinePragma )
+import Var             ( idType, idName )
+import Name            ( Name, getSrcLoc )
+import NameSet
+import Var             ( tyVarKind )
+import VarSet
+import Bag
+import Util            ( isIn, equalLength )
+import BasicTypes      ( TopLevelFlag(..), RecFlag(..), isNonRec, isNotTopLevel,
+                         isAlwaysActive )
+import FiniteMap       ( listToFM, lookupFM )
+import Outputable
 \end{code}
 
 
 \end{code}
 
 
@@ -99,85 +89,99 @@ At the top-level the LIE is sure to contain nothing but constant
 dictionaries, which we resolve at the module level.
 
 \begin{code}
 dictionaries, which we resolve at the module level.
 
 \begin{code}
-tcBindsAndThen
-       :: (TcHsBinds s -> thing -> thing)              -- Combinator
-       -> RenamedHsBinds
-       -> TcM s (thing, LIE s)
-       -> TcM s (thing, LIE s)
-
-tcBindsAndThen combiner EmptyBinds do_next
-  = do_next    `thenTc` \ (thing, lie) ->
-    returnTc (combiner EmptyBinds thing, lie)
-
-tcBindsAndThen combiner (ThenBinds binds1 binds2) do_next
-  = tcBindsAndThen combiner binds1 (tcBindsAndThen combiner binds2 do_next)
-
-tcBindsAndThen combiner (MonoBind bind sigs is_rec) do_next
-  = fixTc (\ ~(prag_info_fn, _) ->
-       -- This is the usual prag_info fix; the PragmaInfo field of an Id
-       -- is not inspected till ages later in the compiler, so there
-       -- should be no black-hole problems here.
-
-       -- TYPECHECK THE SIGNATURES
-    mapTc (tcTySig prag_info_fn) ty_sigs               `thenTc` \ tc_ty_sigs ->
-
-    tcBindWithSigs binder_names bind 
-                  tc_ty_sigs is_rec prag_info_fn       `thenTc` \ (poly_binds, poly_lie, poly_ids) ->
+tcTopBinds :: RenamedHsBinds -> TcM ((TcMonoBinds, TcEnv), LIE)
+tcTopBinds binds
+  = tc_binds_and_then TopLevel glue binds      $
+    tcGetEnv                                   `thenNF_Tc` \ env ->
+    returnTc ((EmptyMonoBinds, env), emptyLIE)
+  where
+    glue is_rec binds1 (binds2, thing) = (binds1 `AndMonoBinds` binds2, thing)
 
 
-       -- Extend the environment to bind the new polymorphic Ids
-    tcExtendLocalValEnv binder_names poly_ids $
 
 
-       -- Build bindings and IdInfos corresponding to user pragmas
-    tcPragmaSigs sigs                  `thenTc` \ (prag_info_fn, prag_binds, prag_lie) ->
+tcBindsAndThen
+       :: (RecFlag -> TcMonoBinds -> thing -> thing)           -- Combinator
+       -> RenamedHsBinds
+       -> TcM (thing, LIE)
+       -> TcM (thing, LIE)
+
+tcBindsAndThen = tc_binds_and_then NotTopLevel
+
+tc_binds_and_then top_lvl combiner EmptyBinds do_next
+  = do_next
+tc_binds_and_then top_lvl combiner (MonoBind EmptyMonoBinds sigs is_rec) do_next
+  = do_next
+
+tc_binds_and_then top_lvl combiner (ThenBinds b1 b2) do_next
+  = tc_binds_and_then top_lvl combiner b1      $
+    tc_binds_and_then top_lvl combiner b2      $
+    do_next
+
+tc_binds_and_then top_lvl combiner (MonoBind bind sigs is_rec) do_next
+  =    -- 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)      $
+
+       -- 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] $
+  
+         -- Build bindings and IdInfos corresponding to user pragmas
+      tcSpecSigs sigs          `thenTc` \ (prag_binds, prag_lie) ->
 
        -- Now do whatever happens next, in the augmented envt
 
        -- Now do whatever happens next, in the augmented envt
-    do_next                            `thenTc` \ (thing, thing_lie) ->
+      do_next                  `thenTc` \ (thing, thing_lie) ->
 
        -- Create specialisations of functions bound here
 
        -- Create specialisations of functions bound here
-    bindInstsOfLocalFuns (prag_lie `plusLIE` thing_lie)
-                         poly_ids      `thenTc` \ (lie2, inst_mbinds) ->
-
-       -- All done
-    let
-       final_lie   = lie2 `plusLIE` poly_lie
-       final_binds = MonoBind poly_binds  [] is_rec            `ThenBinds`
-                     MonoBind inst_mbinds [] nonRecursive      `ThenBinds`
-                     prag_binds
-    in
-    returnTc (prag_info_fn, (combiner final_binds thing, final_lie))
-    )                                  `thenTc` \ (_, result) ->
-    returnTc result
-  where
-    binder_names = map fst (bagToList (collectMonoBinders bind))
-    ty_sigs      = [sig  | sig@(Sig name _ _) <- sigs]
+       -- 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  $
+                               -- 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
+                  )
+
+       (NotTopLevel, Recursive)
+               -> bindInstsOfLocalFuns 
+                               (thing_lie `plusLIE` poly_lie `plusLIE` prag_lie) 
+                               poly_ids                        `thenTc` \ (final_lie, lie_binds) ->
+
+                  returnTc (
+                       combiner Recursive (
+                               poly_binds `andMonoBinds`
+                               lie_binds  `andMonoBinds`
+                               prag_binds) thing,
+                       final_lie
+                  )
 \end{code}
 
 \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 s (thing, LIE s, thing_ty))
-       -> TcM s ((TcHsBinds s, thing), LIE s, 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}
-
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
@@ -197,139 +201,300 @@ so all the clever stuff is in here.
 
 \begin{code}
 tcBindWithSigs 
 
 \begin{code}
 tcBindWithSigs 
-       :: [Name]
+       :: TopLevelFlag
        -> RenamedMonoBinds
        -> RenamedMonoBinds
-       -> [TcSigInfo s]
+       -> [TcSigInfo]
+       -> [RenamedSig]         -- Used solely to get INLINE, NOINLINE sigs
        -> RecFlag
        -> RecFlag
-       -> (Name -> PragmaInfo)
-       -> TcM s (TcMonoBinds s, LIE s, [TcIdBndr s])
+       -> TcM (TcMonoBinds, LIE, [TcId])
 
 
-tcBindWithSigs binder_names mbind tc_ty_sigs is_rec prag_info_fn
+tcBindWithSigs top_lvl mbind tc_ty_sigs inline_sigs is_rec
   = recoverTc (
        -- If typechecking the binds fails, then return with each
        -- signature-less binder given type (forall a.a), to minimise subsequent
        -- error messages
   = recoverTc (
        -- If typechecking the binds fails, then return with each
        -- signature-less binder given type (forall a.a), to minimise subsequent
        -- error messages
-       newTcTyVar mkBoxedTypeKind              `thenNF_Tc` \ alpha_tv ->
+       newTyVar liftedTypeKind         `thenNF_Tc` \ alpha_tv ->
        let
        let
-         forall_a_a = mkForAllTy alpha_tv (mkTyVarTy alpha_tv)
-         poly_ids   = map mk_dummy binder_names
+         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
          mk_dummy name = case maybeSig tc_ty_sigs name of
-                           Just (TySigInfo _ poly_id _ _ _ _) -> poly_id       -- Signature
-                           Nothing -> mkUserId name forall_a_a NoPragmaInfo    -- No signature
+                           Just (TySigInfo _ poly_id _ _ _ _ _ _) -> poly_id   -- Signature
+                           Nothing -> mkLocalId name forall_a_a                -- No signature
        in
        returnTc (EmptyMonoBinds, emptyLIE, poly_ids)
        in
        returnTc (EmptyMonoBinds, emptyLIE, poly_ids)
-    ) $
+    )                                          $
 
 
-       -- Create a new identifier for each binder, with each being given
-       -- a fresh unique, and a type-variable type.
-    tcGetUniques no_of_binders                 `thenNF_Tc` \ uniqs ->
-    mapNF_Tc mk_mono_id_ty binder_names        `thenNF_Tc` \ mono_id_tys ->
+       -- TYPECHECK THE BINDINGS
+    tcMonoBinds mbind tc_ty_sigs is_rec                `thenTc` \ (mbind', lie_req, binder_names, mono_ids) ->
     let
     let
-       mono_id_tyvars     = tyVarsOfTypes mono_id_tys
-       mono_ids           = zipWith3Equal "tcBindAndSigs" mk_id binder_names uniqs mono_id_tys
-       mk_id name uniq ty = mkUserLocal (getOccName name) uniq ty (getSrcLoc name)
+       tau_tvs = foldr (unionVarSet . tyVarsOfType . idType) emptyVarSet mono_ids
     in
 
     in
 
-       -- TYPECHECK THE BINDINGS
-    tcMonoBinds mbind binder_names mono_ids tc_ty_sigs `thenTc` \ (mbind', lie) ->
-
-       -- CHECK THAT THE SIGNATURES MATCH
-       -- (must do this before getTyVarsToGen)
-    checkSigMatch tc_ty_sigs                           `thenTc` \ sig_theta ->
-       
-       -- 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
-    getTyVarsToGen is_unrestricted mono_id_tyvars lie  `thenTc` \ (tyvars_not_to_gen, tyvars_to_gen) ->
-
-       -- DEAL WITH TYPE VARIABLE KINDS
-    mapTc defaultUncommittedTyVar (tyVarSetToList tyvars_to_gen)       `thenTc` \ tyvars_to_gen_list ->
-               -- It's important that the final list (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.
-               --
-               -- This step can do unification => keep other zonking after this
-
-       -- SIMPLIFY THE LIE
-    tcExtendGlobalTyVars tyvars_not_to_gen (
-       if null tc_ty_sigs then
-               -- No signatures, so just simplify the lie
-           tcSimplify tyvars_to_gen lie                `thenTc` \ (lie_free, dict_binds, lie_bound) ->
-           returnTc (lie_free, dict_binds, map instToId (bagToList lie_bound))
-
-       else
-           zonk_theta 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
-
-               -- Check that the needed dicts can be expressed in
-               -- terms of the signature ones
-           tcAddErrCtxt (sigsCtxt tysig_names) $
-           tcSimplifyAndCheck tyvars_to_gen dicts_sig lie      `thenTc` \ (lie_free, dict_binds) ->
-           returnTc (lie_free, dict_binds, dict_ids)
-
-    )                                          `thenTc` \ (lie_free, dict_binds, dicts_bound) ->
-
-    ASSERT( not (any (isUnboxedTypeKind . tyVarKind) 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 zonkTcType mono_id_tys                    `thenNF_Tc` \ zonked_mono_id_types ->
+       -- GENERALISE
+    tcAddSrcLoc  (minimum (map getSrcLoc binder_names))                $
+    tcAddErrCtxt (genCtxt binder_names)                                $
+    generalise binder_names mbind tau_tvs lie_req tc_ty_sigs
+                               `thenTc` \ (tc_tyvars_to_gen, lie_free, dict_binds, dict_ids) ->
+
+
+       -- 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.
+    mapNF_Tc zonkTcTyVarToTyVar tc_tyvars_to_gen       `thenNF_Tc` \ 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_`
+
+       -- BUILD THE POLYMORPHIC RESULT IDs
     let
     let
-       exports  = zipWith3 mk_export binder_names mono_ids zonked_mono_id_types
-       dict_tys = map tcIdType dicts_bound
-
-       mk_export binder_name mono_id zonked_mono_id_ty
-         | maybeToBool maybe_sig = (sig_tyvars,         TcId sig_poly_id, TcId mono_id)
-         | otherwise             = (tyvars_to_gen_list, TcId poly_id,     TcId mono_id)
+       exports  = zipWith mk_export binder_names zonked_mono_ids
+       dict_tys = map idType zonked_dict_ids
+
+       inlines    = mkNameSet [name | InlineSig True name _ loc <- inline_sigs]
+        no_inlines = listToFM [(name, phase) | InlineSig _ name phase _ <- inline_sigs, 
+                                              not (isAlwaysActive phase)]
+                       -- AlwaysActive is the default, so don't bother with them
+
+       mk_export binder_name zonked_mono_id
+         = (tyvars, 
+            attachNoInlinePrag no_inlines poly_id,
+            zonked_mono_id)
          where
          where
-           maybe_sig = maybeSig tc_ty_sigs binder_name
-           Just (TySigInfo _ sig_poly_id sig_tyvars _ _ _) = maybe_sig
-           poly_id = mkUserId binder_name poly_ty (prag_info_fn binder_name)
-           poly_ty = mkForAllTys tyvars_to_gen_list $ mkFunTys dict_tys $ zonked_mono_id_ty
-                               -- 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.
+           (tyvars, poly_id) = 
+               case maybeSig tc_ty_sigs binder_name of
+                 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
+               -- 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.
     in
 
     in
 
+    traceTc (text "binding:" <+> ppr ((zonked_dict_ids, dict_binds),
+            exports, [idType poly_id | (_, poly_id, _) <- exports])) `thenTc_`
+
         -- BUILD RESULTS
     returnTc (
         -- BUILD RESULTS
     returnTc (
-        AbsBinds tyvars_to_gen_list
-                 dicts_bound
-                 exports
-                 (dict_binds `AndMonoBinds` mbind'),
-        lie_free,
-        [poly_id | (_, TcId poly_id, _) <- exports]
+       AbsBinds real_tyvars_to_gen
+                zonked_dict_ids
+                exports
+                inlines
+                (dict_binds `andMonoBinds` mbind'),
+       lie_free,
+       [poly_id | (_, poly_id, _) <- exports]
     )
     )
+
+attachNoInlinePrag no_inlines bndr
+  = case lookupFM no_inlines (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 ((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.
+
+       -- 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 ()
+
+  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
+\end{code}
+
+
+Polymorphic recursion
+~~~~~~~~~~~~~~~~~~~~~
+The game plan for polymorphic recursion in the code above is 
+
+       * Bind any variable for which we have a type signature
+         to an Id with a polymorphic type.  Then when type-checking 
+         the RHSs we'll make a full polymorphic call.
+
+This fine, but if you aren't a bit careful you end up with a horrendous
+amount of partial application and (worse) a huge space leak. For example:
+
+       f :: Eq a => [a] -> [a]
+       f xs = ...f...
+
+If we don't take care, after typechecking we get
+
+       f = /\a -> \d::Eq a -> let f' = f a d
+                              in
+                              \ys:[a] -> ...f'...
+
+Notice the the stupid construction of (f a d), which is of course
+identical to the function we're executing.  In this case, the
+polymorphic recursion isn't being used (but that's a very common case).
+We'd prefer
+
+       f = /\a -> \d::Eq a -> letrec
+                                fm = \ys:[a] -> ...fm...
+                              in
+                              fm
+
+This can lead to a massive space leak, from the following top-level defn
+(post-typechecking)
+
+       ff :: [Int] -> [Int]
+       ff = f Int dEqInt
+
+Now (f dEqInt) evaluates to a lambda that has f' as a free variable; but
+f' is another thunk which evaluates to the same thing... and you end
+up with a chain of identical values all hung onto by the CAF ff.
+
+       ff = f Int dEqInt
+
+          = let f' = f Int dEqInt in \ys. ...f'...
+
+          = let f' = let f' = f Int dEqInt in \ys. ...f'...
+                     in \ys. ...f'...
+
+Etc.
+Solution: when typechecking the RHSs we always have in hand the
+*monomorphic* Ids for each binding.  So we just need to make sure that
+if (Method f a d) shows up in the constraints emerging from (...f...)
+we just use the monomorphic Id.  We achieve this by adding monomorphic Ids
+to the "givens" when simplifying constraints.  That's what the "lies_avail"
+is doing.
+
+
+%************************************************************************
+%*                                                                     *
+\subsection{getTyVarsToGen}
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+generalise binder_names mbind tau_tvs lie_req sigs
+  | not is_unrestricted        -- RESTRICTED CASE
+  =    -- Check signature contexts are empty 
+    checkTc (all is_mono_sig sigs)
+           (restrictedBindCtxtErr binder_names)        `thenTc_`
+
+       -- Now simplify with exactly that set of tyvars
+       -- We have to squash those Methods
+    tcSimplifyRestricted doc tau_tvs lie_req           `thenTc` \ (qtvs, lie_free, binds) ->
+
+       -- Check that signature type variables are OK
+    checkSigsTyVars sigs                               `thenTc_`
+
+    returnTc (qtvs, lie_free, binds, [])
+
+  | null sigs                  -- UNRESTRICTED CASE, NO TYPE SIGS
+  = tcSimplifyInfer doc tau_tvs lie_req
+
+  | otherwise                  -- UNRESTRICTED CASE, WITH TYPE SIGS
+  =    -- CHECKING CASE: Unrestricted group, there are type signatures
+       -- Check signature contexts are empty 
+    checkSigsCtxts sigs                                `thenTc` \ (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) ->
+       
+       -- Check that signature type variables are OK
+    checkSigsTyVars sigs                                       `thenTc_`
+
+    returnTc (forall_tvs, lie_free, dict_binds, sig_dicts)
+
   where
   where
-    no_of_binders = length binder_names
+    is_unrestricted | opt_NoMonomorphismRestriction = True
+                   | otherwise                     = isUnRestrictedGroup tysig_names mbind
 
 
-    mk_mono_id_ty binder_name = case maybeSig tc_ty_sigs binder_name of
-                                 Just (TySigInfo name _ _ _ tau_ty _) -> returnNF_Tc tau_ty -- There's a signature
-                                 otherwise                            -> newTyVarTy kind    -- No signature
+    tysig_names = [name | (TySigInfo name _ _ _ _ _ _ _) <- sigs]
+    is_mono_sig (TySigInfo _ _ _ theta _ _ _ _) = null theta
 
 
-    tysig_names     = [name | (TySigInfo name _ _ _ _ _) <- tc_ty_sigs]
-    is_unrestricted = isUnRestrictedGroup tysig_names mbind
+    doc = ptext SLIT("type signature(s) for") <+> pprBinders binder_names
 
 
-    kind | is_rec    = mkBoxedTypeKind -- Recursive, so no unboxed types
-        | otherwise = mkTypeKind               -- Non-recursive, so we permit unboxed types
+-----------------------
+       -- 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)
+  = tcAddSrcLoc src_loc                        $
+    mapTc_ check_one other_sigs                `thenTc_` 
+    if null theta1 then
+       returnTc ([], [])               -- Non-overloaded type signatures
+    else
+    newDicts SignatureOrigin theta1    `thenNF_Tc` \ 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)
+  where
+    sig1_dict_tys = map mkPredTy theta1
+    sig_meths    = concat [insts | TySigInfo _ _ _ _ _ _ insts _ <- sigs]
+
+    check_one sig@(TySigInfo _ id _ theta _ _ _ src_loc)
+       = tcAddErrCtxt (sigContextsCtxt id1 id)                 $
+        checkTc (equalLength theta theta1) sigContextsErr      `thenTc_`
+        unifyTauTyLists sig1_dict_tys (map mkPredTy theta)
 
 
-zonk_theta theta = mapNF_Tc zonk theta
-       where
-         zonk (c,t) = zonkTcType t     `thenNF_Tc` \ t' ->
-                      returnNF_Tc (c,t')
+checkSigsTyVars sigs = mapTc_ check_one sigs
+  where
+    check_one (TySigInfo _ id sig_tyvars sig_theta sig_tau _ _ src_loc)
+      = tcAddSrcLoc src_loc                                            $
+       tcAddErrCtxt (ptext SLIT("When checking the type signature for") 
+                     <+> quotes (ppr id))                              $
+       tcAddErrCtxtM (sigCtxt sig_tyvars sig_theta sig_tau)            $
+       checkSigTyVars sig_tyvars (idFreeTyVars id)
 \end{code}
 
 \end{code}
 
-@getImplicitStuffToGen@ decides what type variables generalise over.
+@getTyVarsToGen@ decides what type variables to generalise over.
 
 For a "restricted group" -- see the monomorphism restriction
 for a definition -- we bind no dictionaries, and
 
 For a "restricted group" -- see the monomorphism restriction
 for a definition -- we bind no dictionaries, and
@@ -357,6 +522,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.
        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
 
  (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
@@ -367,54 +534,22 @@ constrained tyvars. We don't use any of the results, except to
 find which tyvars are constrained.
 
 \begin{code}
 find which tyvars are constrained.
 
 \begin{code}
-getTyVarsToGen is_unrestricted mono_tyvars lie
-  = tcGetGlobalTyVars                          `thenNF_Tc` \ free_tyvars ->
-    zonkTcTyVars mono_tyvars                   `thenNF_Tc` \ mentioned_tyvars ->
-    let
-       tyvars_to_gen    = mentioned_tyvars `minusTyVarSet` free_tyvars
-    in
-    if is_unrestricted
-    then
-       returnTc (emptyTyVarSet, tyvars_to_gen)
-    else
-       tcSimplify tyvars_to_gen lie        `thenTc` \ (_, _, constrained_dicts) ->
-       let
-         -- ASSERT: dicts_sig is already zonked!
-           constrained_tyvars    = foldrBag (unionTyVarSets . tyVarsOfInst) emptyTyVarSet constrained_dicts
-           reduced_tyvars_to_gen = tyvars_to_gen `minusTyVarSet` constrained_tyvars
-        in
-        returnTc (constrained_tyvars, reduced_tyvars_to_gen)
-\end{code}
-
-
-\begin{code}
 isUnRestrictedGroup :: [Name]          -- Signatures given for these
                    -> RenamedMonoBinds
                    -> Bool
 
 is_elem v vs = isIn "isUnResMono" v vs
 
 isUnRestrictedGroup :: [Name]          -- Signatures given for these
                    -> RenamedMonoBinds
                    -> Bool
 
 is_elem v vs = isIn "isUnResMono" v vs
 
-isUnRestrictedGroup sigs (PatMonoBind (VarPatIn v) _ _) = v `is_elem` sigs
-isUnRestrictedGroup sigs (PatMonoBind other      _ _)  = False
+isUnRestrictedGroup sigs (PatMonoBind other        _ _) = False
 isUnRestrictedGroup sigs (VarMonoBind v _)             = v `is_elem` sigs
 isUnRestrictedGroup sigs (VarMonoBind v _)             = v `is_elem` sigs
-isUnRestrictedGroup sigs (FunMonoBind _ _ _ _)         = True
+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
 isUnRestrictedGroup sigs (AndMonoBinds mb1 mb2)                = isUnRestrictedGroup sigs mb1 &&
                                                          isUnRestrictedGroup sigs mb2
 isUnRestrictedGroup sigs EmptyMonoBinds                        = True
-\end{code}
-
-@defaultUncommittedTyVar@ checks for generalisation over unboxed
-types, and defaults any TypeKind TyVars to BoxedTypeKind.
 
 
-\begin{code}
-defaultUncommittedTyVar tyvar
-  | isTypeKind (tyVarKind tyvar)
-  = newTcTyVar mkBoxedTypeKind                                 `thenNF_Tc` \ boxed_tyvar ->
-    unifyTauTy (mkTyVarTy boxed_tyvar) (mkTyVarTy tyvar)       `thenTc_`
-    returnTc boxed_tyvar
-
-  | otherwise
-  = returnTc tyvar
+isUnRestrictedMatch (Match [] _ _ : _) = False -- No args => like a pattern binding
+isUnRestrictedMatch other             = True   -- Some args => a function binding
 \end{code}
 
 
 \end{code}
 
 
@@ -429,190 +564,129 @@ The signatures have been dealt with already.
 
 \begin{code}
 tcMonoBinds :: RenamedMonoBinds 
 
 \begin{code}
 tcMonoBinds :: RenamedMonoBinds 
-           -> [Name] -> [TcIdBndr s]
-           -> [TcSigInfo s]
-           -> TcM s (TcMonoBinds s, LIE s)
-
-tcMonoBinds mbind binder_names mono_ids tc_ty_sigs
-  = tcExtendLocalValEnv binder_names mono_ids (
-       tc_mono_binds mbind
-    )
-  where
-    sig_names = [name | (TySigInfo name _ _ _ _ _) <- tc_ty_sigs]
-    sig_ids   = [id   | (TySigInfo _   id _ _ _ _) <- tc_ty_sigs]
-
-    tc_mono_binds EmptyMonoBinds = returnTc (EmptyMonoBinds, emptyLIE)
-
-    tc_mono_binds (AndMonoBinds mb1 mb2)
-      = tc_mono_binds mb1              `thenTc` \ (mb1a, lie1) ->
-        tc_mono_binds mb2              `thenTc` \ (mb2a, lie2) ->
-        returnTc (AndMonoBinds mb1a mb2a, lie1 `plusLIE` lie2)
-
-    tc_mono_binds (FunMonoBind name inf matches locn)
-      = tcAddSrcLoc locn                               $
-       tcLookupLocalValueOK "tc_mono_binds" name       `thenNF_Tc` \ id ->
-
-               -- Before checking the RHS, extend the envt with
-               -- bindings for the *polymorphic* Ids from any type signatures
-       tcExtendLocalValEnv sig_names sig_ids           $
-       tcMatchesFun name (idType id) matches           `thenTc` \ (matches', lie) ->
-
-       returnTc (FunMonoBind (TcId id) inf matches' locn, lie)
-
-    tc_mono_binds bind@(PatMonoBind pat grhss_and_binds locn)
-      = tcAddSrcLoc locn                       $
-       tcPat pat                               `thenTc` \ (pat2, lie_pat, pat_ty) ->
-       tcExtendLocalValEnv sig_names sig_ids   $
-       tcGRHSsAndBinds grhss_and_binds         `thenTc` \ (grhss_and_binds2, lie, grhss_ty) ->
-       tcAddErrCtxt (patMonoBindsCtxt bind)    $
-       unifyTauTy pat_ty grhss_ty              `thenTc_`
-       returnTc (PatMonoBind pat2 grhss_and_binds2 locn,
-                 plusLIE lie_pat lie)
-\end{code}
-
-%************************************************************************
-%*                                                                     *
-\subsection{Signatures}
-%*                                                                     *
-%************************************************************************
-
-@tcSigs@ checks the signatures for validity, and returns a list of
-{\em freshly-instantiated} signatures.  That is, the types are already
-split up, and have fresh type variables installed.  All non-type-signature
-"RenamedSigs" are ignored.
-
-The @TcSigInfo@ contains @TcTypes@ because they are unified with
-the variable's type, and after that checked to see whether they've
-been instantiated.
-
-\begin{code}
-data TcSigInfo s
-  = TySigInfo      Name
-                   (TcIdBndr s)        -- *Polymorphic* binder for this value...
-                   [TcTyVar s] (TcThetaType s) (TcTauType s)
-                   SrcLoc
-
-
-maybeSig :: [TcSigInfo s] -> Name -> Maybe (TcSigInfo s)
-       -- Search for a particular signature
-maybeSig [] name = Nothing
-maybeSig (sig@(TySigInfo sig_name _ _ _ _ _) : sigs) name
-  | name == sig_name = Just sig
-  | otherwise       = maybeSig sigs name
-\end{code}
-
-
-\begin{code}
-tcTySig :: (Name -> PragmaInfo)
-       -> RenamedSig
-       -> TcM s (TcSigInfo s)
-
-tcTySig prag_info_fn (Sig v ty src_loc)
- = tcAddSrcLoc src_loc $
-   tcHsType ty                 `thenTc` \ sigma_ty ->
-   tcInstSigType sigma_ty      `thenNF_Tc` \ sigma_ty' ->
-   let
-     poly_id = mkUserId v sigma_ty' (prag_info_fn v)
-     (tyvars', theta', tau') = splitSigmaTy sigma_ty'
-       -- This splitSigmaTy tries hard to make sure that tau' is a type synonym
-       -- wherever possible, which can improve interface files.
-   in
-   returnTc (TySigInfo v poly_id tyvars' theta' tau' src_loc)
-\end{code}
-
-@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 []
-  = returnTc (error "checkSigMatch")
-
-checkSigMatch tc_ty_sigs
-  =    -- 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).
+           -> [TcSigInfo]
+           -> RecFlag
+           -> TcM (TcMonoBinds, 
+                     LIE,              -- LIE required
+                     [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.
        --
        --
-       -- We unify them because, with polymorphic recursion, their types
-       -- might not otherwise be related.  This is a rather subtle issue.
-       -- ToDo: amplify
-    tcAddErrCtxt (sigContextsCtxt tc_ty_sigs) (
-       mapTc (unifyTauTyLists dict_tys1) dict_tys_s
-    )                                          `thenTc_`
-    
-       -- CHECK THAT THE SIGNATURE TYVARS AND TAU_TYPES ARE OK
-       -- Doesn't affect substitution
-    mapTc check_one_sig tc_ty_sigs     `thenTc_`
-
-    returnTc theta1
-  where
-    (theta1:thetas)          = [theta | TySigInfo _ _ _ theta _ _ <- tc_ty_sigs]
-    (dict_tys1 : dict_tys_s) = map mk_dict_tys (theta1 : thetas)
-    mk_dict_tys theta       = [mkDictTy c t | (c,t) <- theta]
-
-    check_one_sig (TySigInfo name id sig_tyvars _ sig_tau src_loc)
-      = tcAddSrcLoc src_loc    $
-       tcAddErrCtxt (sigCtxt id) $
-       checkSigTyVars sig_tyvars sig_tau
-\end{code}
-
+       -- 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
 
 
-@checkSigTyVars@ is used after the type in a type signature has been unified with
-the actual type found.  It then checks that the type variables of the type signature
-are
-       (a) still all type variables
-               eg matching signature [a] against inferred type [(p,q)]
-               [then a will be unified to a non-type variable]
+    complete_it extra_val_env                          `thenTc` \ (mbinds', lie_req_rhss) ->
 
 
-       (b) still all distinct
-               eg matching signature [(a,b)] against inferred type [(p,p)]
-               [then a and b will be unified together]
+    returnTc (mbinds', lie_req_pat `plusLIE` lie_req_rhss, names, mono_ids)
+  where
 
 
-BUT ACTUALLY THESE FIRST TWO ARE FORCED BY USING DontBind TYVARS
+    mk_bind (name, mono_id) = case maybeSig tc_ty_sigs name of
+                               Nothing                                   -> (name, mono_id)
+                               Just (TySigInfo name poly_id _ _ _ _ _ _) -> (name, poly_id)
 
 
-       (c) not mentioned in the environment
-               eg the signature for f in this:
+    tc_mb_pats EmptyMonoBinds
+      = returnTc (\ xve -> returnTc (EmptyMonoBinds, emptyLIE), emptyLIE, emptyBag, emptyBag, emptyLIE)
 
 
-                       g x = ... where
-                                       f :: a->[a]
-                                       f y = [x,y]
+    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) ->
+       let
+          complete_it xve = complete_it1 xve   `thenTc` \ (mb1', lie1) ->
+                            complete_it2 xve   `thenTc` \ (mb2', lie2) ->
+                            returnTc (AndMonoBinds mb1' mb2', lie1 `plusLIE` lie2)
+       in
+       returnTc (complete_it,
+                 lie_req1 `plusLIE` lie_req2,
+                 tvs1 `unionBags` tvs2,
+                 ids1 `unionBags` ids2,
+                 lie_avail1 `plusLIE` lie_avail2)
+
+    tc_mb_pats (FunMonoBind name inf matches locn)
+      = (case maybeSig tc_ty_sigs name of
+           Just (TySigInfo _ _ _ _ _ mono_id _ _) 
+                   -> returnNF_Tc mono_id
+           Nothing -> newLocalName name        `thenNF_Tc` \ bndr_name ->
+                      newTyVarTy openTypeKind  `thenNF_Tc` \ bndr_ty -> 
+                       -- NB: not a 'hole' tyvar; since there is no type 
+                       -- signature, we revert to ordinary H-M typechecking
+                       -- which means the variable gets an inferred tau-type
+                      returnNF_Tc (mkLocalId bndr_name bndr_ty)
+       )                                       `thenNF_Tc` \ bndr_id ->
+       let
+          bndr_ty         = idType bndr_id
+          complete_it xve = tcAddSrcLoc locn                           $
+                            tcMatchesFun xve name bndr_ty  matches     `thenTc` \ (matches', lie) ->
+                            returnTc (FunMonoBind bndr_id inf matches' locn, lie)
+       in
+       returnTc (complete_it, emptyLIE, emptyBag, unitBag (name, bndr_id), emptyLIE)
 
 
-               Here, f is forced to be monorphic by the free occurence of x.
+    tc_mb_pats bind@(PatMonoBind pat grhss locn)
+      = tcAddSrcLoc locn               $
+       newHoleTyVarTy                  `thenNF_Tc` \ pat_ty -> 
 
 
-Before doing this, the substitution is applied to the signature type variable.
+               --      Now typecheck the pattern
+               -- 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
+               -- The type variables are brought into scope in tc_binds_and_then,
+               -- so we don't have to do anything here.
 
 
-\begin{code}
-checkSigTyVars :: [TcTyVar s]          -- The original signature type variables
-              -> TcType s              -- signature type (for err msg)
-              -> TcM s ()
-
-checkSigTyVars sig_tyvars sig_tau
-  = tcGetGlobalTyVars                  `thenNF_Tc` \ globals ->
-    let
-       mono_tyvars = filter (`elementOfTyVarSet` globals) sig_tyvars
-    in
-       -- TEMPORARY FIX
-       -- Until the final Bind-handling stuff is in, several type signatures in the same
-       -- bindings group can cause the signature type variable from the different
-       -- signatures to be unified.  So we still need to zonk and check point (b).
-       -- Remove when activating the new binding code
-    mapNF_Tc zonkTcTyVar sig_tyvars    `thenNF_Tc` \ sig_tys ->
-    checkTcM (hasNoDups (map (getTyVar "checkSigTyVars") sig_tys))
-            (zonkTcType sig_tau        `thenNF_Tc` \ sig_tau' ->
-             failTc (badMatchErr sig_tau sig_tau')
-            )                          `thenTc_`
-
-
-       -- Check point (c)
-       -- We want to report errors in terms of the original signature tyvars,
-       -- ie sig_tyvars, NOT sig_tyvars'.  sig_tys and sig_tyvars' correspond
-       -- 1-1 with sig_tyvars, so we can just map back.
-    checkTc (null mono_tyvars)
-           (notAsPolyAsSigErr sig_tau mono_tyvars)
+       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 PatBindRhs grhss pat_ty            `thenTc` \ (grhss', lie) ->
+                            returnTc (PatMonoBind pat' grhss' locn, lie)
+       in
+       returnTc (complete_it, lie_req, tvs, ids, lie_avail)
+
+       -- 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    `thenNF_Tc` \ bndr_name ->
+                  tcMonoPatBndr bndr_name pat_ty
+
+           Just (TySigInfo _ _ _ _ _ mono_id _ _)
+               -> tcAddSrcLoc (getSrcLoc name)         $
+                  tcSubPat pat_ty (idType mono_id)     `thenTc` \ (co_fn, lie) ->
+                  returnTc (co_fn, lie, mono_id)
 \end{code}
 
 
 \end{code}
 
 
@@ -622,45 +696,13 @@ checkSigTyVars sig_tyvars sig_tau
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 
-
-@tcPragmaSigs@ munches up the "signatures" that arise through *user*
+@tcSpecSigs@ munches up the specialisation "signatures" that arise through *user*
 pragmas.  It is convenient for them to appear in the @[RenamedSig]@
 part of a binding because then the same machinery can be used for
 moving them into place as is done for type signatures.
 
 pragmas.  It is convenient for them to appear in the @[RenamedSig]@
 part of a binding because then the same machinery can be used for
 moving them into place as is done for type signatures.
 
-\begin{code}
-tcPragmaSigs :: [RenamedSig]                   -- The pragma signatures
-            -> TcM s (Name -> PragmaInfo,      -- Maps name to the appropriate PragmaInfo
-                      TcHsBinds s,
-                      LIE s)
-
-tcPragmaSigs sigs = returnTc ( \name -> NoPragmaInfo, EmptyBinds, emptyLIE )
+They look like this:
 
 
-{- 
-tcPragmaSigs sigs
-  = mapAndUnzip3Tc tcPragmaSig sigs    `thenTc` \ (names_w_id_infos, binds, lies) ->
-    let
-       name_to_info name = foldr ($) noIdInfo
-                                 [info_fn | (n,info_fn) <- names_w_id_infos, n==name]
-    in
-    returnTc (name_to_info,
-             foldr ThenBinds EmptyBinds binds,
-             foldr plusLIE emptyLIE lies)
-\end{code}
-
-Here are the easy cases for tcPragmaSigs
-
-\begin{code}
-tcPragmaSig (DeforestSig name loc)
-  = returnTc ((name, addDeforestInfo DoDeforest),EmptyBinds,emptyLIE)
-tcPragmaSig (InlineSig name loc)
-  = returnTc ((name, addUnfoldInfo (iWantToBeINLINEd UnfoldAlways)), EmptyBinds, emptyLIE)
-tcPragmaSig (MagicUnfoldingSig name string loc)
-  = returnTc ((name, addUnfoldInfo (mkMagicUnfolding string)), EmptyBinds, emptyLIE)
-\end{code}
-
-The interesting case is for SPECIALISE pragmas.  There are two forms.
-Here's the first form:
 \begin{verbatim}
        f :: Ord a => [a] -> b -> b
        {-# SPECIALIZE f :: [Int] -> b -> b #-}
 \begin{verbatim}
        f :: Ord a => [a] -> b -> b
        {-# SPECIALIZE f :: [Int] -> b -> b #-}
@@ -683,113 +725,45 @@ specialiser will subsequently discover that there's a call of @f@ at
 Int, and will create a specialisation for @f@.  After that, the
 binding for @f*@ can be discarded.
 
 Int, and will create a specialisation for @f@.  After that, the
 binding for @f*@ can be discarded.
 
-The second form is this:
-\begin{verbatim}
-       f :: Ord a => [a] -> b -> b
-       {-# SPECIALIZE f :: [Int] -> b -> b = g #-}
-\end{verbatim}
-
-Here @g@ is specified as a function that implements the specialised
-version of @f@.  Suppose that g has type (a->b->b); that is, g's type
-is more general than that required.  For this we generate
-\begin{verbatim}
-       f@Int = /\b -> g Int b
-       f* = f@Int
-\end{verbatim}
-
-Here @f@@Int@ is a SpecId, the specialised version of @f@.  It inherits
-f's export status etc.  @f*@ is a SpecPragmaId, as before, which just serves
-to prevent @f@@Int@ from being discarded prematurely.  After specialisation,
-if @f@@Int@ is going to be used at all it will be used explicitly, so the simplifier can
-discard the f* binding.
-
-Actually, there is really only point in giving a SPECIALISE pragma on exported things,
-and the simplifer won't discard SpecIds for exporte things anyway, so maybe this is
-a bit of overkill.
+We used to have a form
+       {-# SPECIALISE f :: <type> = g #-}
+which promised that g implemented f at <type>, but we do that with 
+a RULE now:
+       {-# SPECIALISE (f::<type) = g #-}
 
 \begin{code}
 
 \begin{code}
-tcPragmaSig (SpecSig name poly_ty maybe_spec_name src_loc)
-  = tcAddSrcLoc src_loc                                $
-    tcAddErrCtxt (valSpecSigCtxt name spec_ty) $
+tcSpecSigs :: [RenamedSig] -> TcM (TcMonoBinds, LIE)
+tcSpecSigs (SpecSig name poly_ty src_loc : sigs)
+  =    -- SPECIALISE f :: forall b. theta => tau  =  g
+    tcAddSrcLoc src_loc                                $
+    tcAddErrCtxt (valSpecSigCtxt name poly_ty) $
 
        -- Get and instantiate its alleged specialised type
 
        -- Get and instantiate its alleged specialised type
-    tcHsType poly_ty                           `thenTc` \ sig_sigma ->
-    tcInstSigType  sig_sigma                   `thenNF_Tc` \ sig_ty ->
-    let
-       (sig_tyvars, sig_theta, sig_tau) = splitSigmaTy sig_ty
-       origin = ValSpecOrigin name
-    in
+    tcHsSigType (FunSigCtxt name) poly_ty      `thenTc` \ 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) ->
 
 
-       -- Check that the SPECIALIZE pragma had an empty context
-    checkTc (null sig_theta)
-           (panic "SPECIALIZE non-empty context (ToDo: msg)") `thenTc_`
+       -- Squeeze out any Methods (see comments with tcSimplifyToDicts)
+    tcSimplifyToDicts spec_lie                 `thenTc` \ (spec_dicts, spec_binds) ->
 
 
-       -- Get and instantiate the type of the id mentioned
-    tcLookupLocalValueOK "tcPragmaSig" name    `thenNF_Tc` \ main_id ->
-    tcInstSigType [] (idType main_id)          `thenNF_Tc` \ main_ty ->
+       -- 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.
+    newLocalName name                  `thenNF_Tc` \ spec_name ->
     let
     let
-       (main_tyvars, main_rho) = splitForAllTy main_ty
-       (main_theta,main_tau)   = splitRhoTy main_rho
-       main_arg_tys            = mkTyVarTys main_tyvars
+       spec_bind = VarMonoBind (mkSpecPragmaId spec_name sig_ty)
+                               (mkHsLet spec_binds spec_expr)
     in
 
     in
 
-       -- Check that the specialised type is indeed an instance of
-       -- the type of the main function.
-    unifyTauTy sig_tau main_tau                `thenTc_`
-    checkSigTyVars sig_tyvars sig_tau  `thenTc_`
-
-       -- Check that the type variables of the polymorphic function are
-       -- either left polymorphic, or instantiate to ground type.
-       -- Also check that the overloaded type variables are instantiated to
-       -- ground type; or equivalently that all dictionaries have ground type
-    mapTc zonkTcType main_arg_tys      `thenNF_Tc` \ main_arg_tys' ->
-    zonkTcThetaType main_theta         `thenNF_Tc` \ main_theta' ->
-    tcAddErrCtxt (specGroundnessCtxt main_arg_tys')
-             (checkTc (all isGroundOrTyVarTy main_arg_tys'))           `thenTc_`
-    tcAddErrCtxt (specContextGroundnessCtxt main_theta')
-             (checkTc (and [isGroundTy ty | (_,ty) <- theta']))        `thenTc_`
-
-       -- Build the SpecPragmaId; 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_pragma_id ->
-
-       -- Build a suitable binding; depending on whether we were given
-       -- a value (Maybe Name) to be used as the specialisation.
-    case using of
-      Nothing ->               -- No implementation function specified
-
-               -- Make a Method inst for the occurrence of the overloaded function
-       newMethodWithGivenTy (OccurrenceOf name)
-                 (TcId main_id) main_arg_tys main_rho  `thenNF_Tc` \ (lie, meth_id) ->
-
-       let
-           pseudo_bind = VarMonoBind spec_pragma_id pseudo_rhs
-           pseudo_rhs  = mkHsTyLam sig_tyvars (HsVar (TcId meth_id))
-       in
-       returnTc (pseudo_bind, lie, \ info -> info)
-
-      Just spec_name ->                -- Use spec_name as the specialisation value ...
-
-               -- Type check a simple occurrence of the specialised Id
-       tcId spec_name          `thenTc` \ (spec_body, spec_lie, spec_tau) ->
-
-               -- Check that it has the correct type, and doesn't constrain the
-               -- signature variables at all
-       unifyTauTy sig_tau spec_tau             `thenTc_`
-       checkSigTyVars sig_tyvars sig_tau       `thenTc_`
-
-           -- Make a local SpecId to bind to applied spec_id
-       newSpecId main_id main_arg_tys sig_ty   `thenNF_Tc` \ local_spec_id ->
+       -- Do the rest and combine
+    tcSpecSigs sigs                    `thenTc` \ (binds_rest, lie_rest) ->
+    returnTc (binds_rest `andMonoBinds` spec_bind,
+             lie_rest   `plusLIE`      mkLIE spec_dicts)
 
 
-       let
-           spec_rhs   = mkHsTyLam sig_tyvars spec_body
-           spec_binds = VarMonoBind local_spec_id spec_rhs
-                          `AndMonoBinds`
-                        VarMonoBind spec_pragma_id (HsVar (TcId local_spec_id))
-           spec_info  = SpecInfo spec_tys (length main_theta) local_spec_id
-       in
-       returnTc ((name, addSpecInfo spec_info), spec_binds, spec_lie)
--}
+tcSpecSigs (other_sig : sigs) = tcSpecSigs sigs
+tcSpecSigs []                = returnTc (EmptyMonoBinds, emptyLIE)
 \end{code}
 
 
 \end{code}
 
 
@@ -801,77 +775,46 @@ tcPragmaSig (SpecSig name poly_ty maybe_spec_name src_loc)
 
 
 \begin{code}
 
 
 \begin{code}
-patMonoBindsCtxt bind sty
-  = hang (ptext SLIT("In a pattern binding:")) 4 (ppr sty bind)
+patMonoBindsCtxt bind
+  = hang (ptext SLIT("In a pattern binding:")) 4 (ppr bind)
 
 -----------------------------------------------
 
 -----------------------------------------------
-valSpecSigCtxt v ty sty
-  = hang (ptext SLIT("In a SPECIALIZE pragma for a value:"))
-        4 (sep [(<>) (ppr sty v) (ptext SLIT(" ::")),
-                 ppr sty ty])
-
-
+valSpecSigCtxt v ty
+  = sep [ptext SLIT("In a SPECIALIZE pragma for a value:"),
+        nest 4 (ppr v <+> dcolon <+> ppr ty)]
 
 -----------------------------------------------
 
 -----------------------------------------------
-notAsPolyAsSigErr sig_tau mono_tyvars sty
-  = hang (ptext SLIT("A type signature is more polymorphic than the inferred type"))
-       4  (vcat [text "Some type variables in the inferred type can't be forall'd, namely:",
-                     interpp'SP sty mono_tyvars,
-                     ptext SLIT("Possible cause: the RHS mentions something subject to the monomorphism restriction")
-                    ])
+sigContextsErr = ptext SLIT("Mismatched contexts")
 
 
------------------------------------------------
-badMatchErr sig_ty inferred_ty sty
-  = hang (ptext SLIT("Type signature doesn't match inferred type"))
-        4 (vcat [hang (ptext SLIT("Signature:")) 4 (ppr sty sig_ty),
-                     hang (ptext SLIT("Inferred :")) 4 (ppr sty inferred_ty)
-          ])
+sigContextsCtxt s1 s2
+  = 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")]
 
 -----------------------------------------------
 
 -----------------------------------------------
-sigCtxt id sty 
-  = sep [ptext SLIT("When checking signature for"), ppr sty id]
-sigsCtxt ids sty 
-  = sep [ptext SLIT("When checking signature(s) for:"), interpp'SP sty ids]
+unliftedBindErr flavour mbind
+  = hang (text flavour <+> ptext SLIT("bindings for unlifted types aren't allowed:"))
+        4 (ppr mbind)
 
 -----------------------------------------------
 
 -----------------------------------------------
-sigContextsCtxt ty_sigs sty
-  = hang (ptext SLIT("When matching the contexts of the signatures of a recursive group"))
-        4 (vcat (map ppr_tc_ty_sig ty_sigs))
-  where
-    ppr_tc_ty_sig (TySigInfo val _ tyvars theta tau_ty _)
-      = hang ((<>) (ppr sty val) (ptext SLIT(" :: ")))
-            4 (if null theta
-               then empty
-               else hcat [parens (hsep (punctuate comma (map (ppr_inst sty) theta))), 
-                          text " => ..."])
-    ppr_inst sty (clas, ty) = hsep [ppr sty clas, ppr sty ty]
+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)
 
 -----------------------------------------------
 
 -----------------------------------------------
-specGroundnessCtxt
-  = panic "specGroundnessCtxt"
-
---------------------------------------------
-specContextGroundnessCtxt -- err_ctxt dicts sty
-  = panic "specContextGroundnessCtxt"
-{-
-  = hang (
-       sep [hsep [ptext SLIT("In the SPECIALIZE pragma for"), ppr sty name],
-            hcat [ptext SLIT(" specialised to the type"), ppr sty spec_ty],
-            pp_spec_id sty,
-            ptext SLIT("... not all overloaded type variables were instantiated"),
-            ptext SLIT("to ground types:")])
-      4 (vcat [hsep [ppr sty c, ppr sty t]
-                 | (c,t) <- map getDictClassAndType dicts])
-  where
-    (name, spec_ty, locn, pp_spec_id)
-      = case err_ctxt of
-         ValSpecSigCtxt    n ty loc      -> (n, ty, loc, \ x -> empty)
-         ValSpecSpecIdCtxt n ty spec loc ->
-           (n, ty, loc,
-            \ sty -> hsep [ptext SLIT("... type of explicit id"), ppr sty spec])
--}
+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}
 \end{code}
-
-
-
-