[project @ 1997-12-16 10:30:02 by simonm]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcBinds.lhs
index e6f78b3..30500ba 100644 (file)
@@ -6,46 +6,74 @@
 \begin{code}
 #include "HsVersions.h"
 
-module TcBinds ( tcBindsAndThen, tcPragmaSigs ) where
+module TcBinds ( tcBindsAndThen, tcPragmaSigs, checkSigTyVars, tcBindWithSigs, TcSigInfo(..) ) where
 
 IMP_Ubiq()
-
-import HsSyn           ( HsBinds(..), Bind(..), Sig(..), MonoBinds(..), 
-                         HsExpr, Match, PolyType, InPat, OutPat(..),
-                         GRHSsAndBinds, ArithSeqInfo, HsLit, Fake,
-                         collectBinders )
-import RnHsSyn         ( RenamedHsBinds(..), RenamedBind(..), RenamedSig(..), 
-                         RenamedMonoBinds(..), RnName(..)
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ <= 201
+IMPORT_DELOOPER(TcLoop)                ( tcGRHSsAndBinds )
+#else
+import {-# SOURCE #-} TcGRHSs ( tcGRHSsAndBinds )
+#endif
+
+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),
+                         SYN_IE(TcExpr), 
+                         tcIdType
                        )
-import TcHsSyn         ( TcHsBinds(..), TcBind(..), TcMonoBinds(..),
-                         TcIdOcc(..), TcIdBndr(..) )
 
-import TcMonad         hiding ( rnMtoTcM )     
-import GenSpecEtc      ( checkSigTyVars, genBinds, TcSigInfo(..) )
-import Inst            ( Inst, LIE(..), emptyLIE, plusLIE, InstOrigin(..) )
-import TcEnv           ( tcExtendLocalValEnv, tcLookupLocalValueOK, newMonoIds )
-IMPORT_DELOOPER(TcLoop)                ( tcGRHSsAndBinds )
+import TcMonad
+import Inst            ( Inst, SYN_IE(LIE), emptyLIE, plusLIE, plusLIEs, InstOrigin(..),
+                         newDicts, tyVarsOfInst, instToId, newMethodWithGivenTy
+                       )
+import TcEnv           ( tcExtendLocalValEnv, tcLookupLocalValueOK, newLocalId,
+                         tcGetGlobalTyVars, tcExtendGlobalTyVars
+                       )
+import SpecEnv         ( SpecEnv )
 import TcMatches       ( tcMatchesFun )
-import TcMonoType      ( tcPolyType )
+import TcSimplify      ( tcSimplify, tcSimplifyAndCheck )
+import TcMonoType      ( tcHsType )
 import TcPat           ( tcPat )
 import TcSimplify      ( bindInstsOfLocalFuns )
-import TcType          ( newTcTyVar, tcInstSigType )
-import Unify           ( unifyTauTy )
+import TcType          ( TcIdOcc(..), SYN_IE(TcIdBndr), 
+                         SYN_IE(TcType), SYN_IE(TcThetaType), SYN_IE(TcTauType), 
+                         SYN_IE(TcTyVarSet), SYN_IE(TcTyVar),
+                         newTyVarTy, zonkTcType, zonkTcTheta, zonkSigTyVar,
+                         newTcTyVar, tcInstSigType, newTyVarTys
+                       )
+import Unify           ( unifyTauTy, unifyTauTyLists )
 
-import Kind            ( mkBoxedTypeKind, mkTypeKind )
+import Kind            ( isUnboxedTypeKind, mkTypeKind, isTypeKind, mkBoxedTypeKind )
 import Id              ( GenId, idType, mkUserId )
 import IdInfo          ( noIdInfo )
-import Maybes          ( assocMaybe, catMaybes, Maybe(..) )
-import Name            ( pprNonSym )
+import Maybes          ( maybeToBool, assocMaybe, catMaybes )
+import Name            ( getOccName, getSrcLoc, Name )
 import PragmaInfo      ( PragmaInfo(..) )
 import Pretty
-import RnHsSyn         ( RnName )      -- instances
-import Type            ( mkTyVarTy, mkTyVarTys, isTyVarTy,
-                         mkSigmaTy, splitSigmaTy,
+import Type            ( mkTyVarTy, mkTyVarTys, isTyVarTy, tyVarsOfTypes, eqSimpleTheta, 
+                         mkSigmaTy, splitSigmaTy, mkForAllTys, mkFunTys, getTyVar, mkDictTy,
                          splitRhoTy, mkForAllTy, splitForAllTy )
-import Util            ( isIn, zipEqual, panic )
+import TyVar           ( GenTyVar, SYN_IE(TyVar), tyVarKind, mkTyVarSet, 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 )
+
+
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \subsection{Type-checking bindings}
@@ -63,7 +91,7 @@ specialising the things bound.
 @tcBindsAndThen@ also takes a "combiner" which glues together the
 bindings and the "thing" to make a new "thing".
 
-The real work is done by @tcBindAndThen@.
+The real work is done by @tcBindWithSigsAndThen@.
 
 Recursive and non-recursive binds are handled in essentially the same
 way: because of uniques there are no scoping issues left.  The only
@@ -79,23 +107,57 @@ dictionaries, which we resolve at the module level.
 
 \begin{code}
 tcBindsAndThen
-       :: (TcHsBinds s -> thing -> thing)              -- Combinator
+       :: (RecFlag -> TcMonoBinds s -> thing -> thing)         -- Combinator
        -> RenamedHsBinds
-       -> TcM s (thing, LIE s, thing_ty)
-       -> TcM s (thing, LIE s, thing_ty)
+       -> TcM s (thing, LIE s)
+       -> TcM s (thing, LIE s)
 
 tcBindsAndThen combiner EmptyBinds do_next
-  = do_next    `thenTc` \ (thing, lie, thing_ty) ->
-    returnTc (combiner EmptyBinds thing, lie, thing_ty)
-
-tcBindsAndThen combiner (SingleBind bind) do_next
-  = tcBindAndThen combiner bind [] do_next
-
-tcBindsAndThen combiner (BindWith bind sigs) do_next
-  = tcBindAndThen combiner bind sigs do_next
+  = do_next    `thenTc` \ (thing, lie) ->
+    returnTc (combiner nonRecursive EmptyMonoBinds 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) ->
+
+       -- 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) ->
+
+       -- Now do whatever happens next, in the augmented envt
+    do_next                            `thenTc` \ (thing, thing_lie) ->
+
+       -- 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_thing = combiner is_rec poly_binds $
+                     combiner nonRecursive inst_mbinds $
+                     combiner nonRecursive prag_binds 
+                     thing
+    in
+    returnTc (prag_info_fn, (final_thing, final_lie))
+    )                                  `thenTc` \ (_, result) ->
+    returnTc result
+  where
+    binder_names = map fst (bagToList (collectMonoBinders bind))
+    ty_sigs      = [sig  | sig@(Sig name _ _) <- sigs]
 \end{code}
 
 An aside.  The original version of @tcBindsAndThen@ which lacks a
@@ -114,209 +176,248 @@ tcBindsAndThen EmptyBinds do_next
   = do_next            `thenTc` \ (thing, lie, thing_ty) ->
     returnTc ((EmptyBinds, thing), lie, thing_ty)
 
-tcBindsAndThen (SingleBind bind) do_next
-  = tcBindAndThen bind [] do_next
-
-tcBindsAndThen (BindWith bind sigs) do_next
-  = tcBindAndThen bind sigs do_next
-
 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}
 
+
 %************************************************************************
 %*                                                                     *
-\subsection{Bind}
+\subsection{tcBindWithSigs}
 %*                                                                     *
 %************************************************************************
 
-\begin{code}
-tcBindAndThen
-       :: (TcHsBinds s -> thing -> thing)                -- Combinator
-       -> RenamedBind                                    -- The Bind to typecheck
-       -> [RenamedSig]                                   -- ...and its signatures
-       -> TcM s (thing, LIE s, thing_ty)                 -- Thing to type check in
-                                                         -- augmented envt
-       -> TcM s (thing, LIE s, thing_ty)                 -- Results, incl the
-
-tcBindAndThen combiner bind sigs 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.
-    
-    tcBindAndSigs binder_names bind 
-                 sigs prag_info_fn     `thenTc` \ (poly_binds, poly_lie, poly_ids) ->
-
-       -- 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) ->
+@tcBindWithSigs@ deals with a single binding group.  It does generalisation,
+so all the clever stuff is in here.
 
-       -- Now do whatever happens next, in the augmented envt
-    do_next                            `thenTc` \ (thing, thing_lie, thing_ty) ->
+* binder_names and mbind must define the same set of Names
 
-       -- 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 = poly_binds `ThenBinds`
-                     SingleBind (NonRecBind inst_mbinds) `ThenBinds`
-                     prag_binds
-    in
-    returnTc (prag_info_fn, (combiner final_binds thing, final_lie, thing_ty))
-    )                                  `thenTc` \ (_, result) ->
-    returnTc result
-  where
-    binder_names = collectBinders bind
+* The Names in tc_ty_sigs must be a subset of binder_names
 
+* The Ids in tc_ty_sigs don't necessarily have to have the same name
+  as the Name in the tc_ty_sig
 
-tcBindAndSigs binder_rn_names bind sigs prag_info_fn
-  = let
-       binder_names = map de_rn binder_rn_names
-       de_rn (RnName n) = n
-    in
-    recoverTc (
+\begin{code}
+tcBindWithSigs 
+       :: [Name]
+       -> RenamedMonoBinds
+       -> [TcSigInfo s]
+       -> RecFlag
+       -> (Name -> PragmaInfo)
+       -> TcM s (TcMonoBinds s, LIE s, [TcIdBndr s])
+
+tcBindWithSigs binder_names mbind tc_ty_sigs is_rec prag_info_fn
+  = recoverTc (
        -- If typechecking the binds fails, then return with each
-       -- binder given type (forall a.a), to minimise subsequent
+       -- signature-less binder given type (forall a.a), to minimise subsequent
        -- error messages
        newTcTyVar mkBoxedTypeKind              `thenNF_Tc` \ alpha_tv ->
        let
          forall_a_a = mkForAllTy alpha_tv (mkTyVarTy alpha_tv)
-         poly_ids   = [ mkUserId name forall_a_a (prag_info_fn name)
-                      | name <- binder_names]
+         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 -> mkUserId name forall_a_a NoPragmaInfo    -- No signature
        in
-       returnTc (EmptyBinds, emptyLIE, poly_ids)
+       returnTc (EmptyMonoBinds, emptyLIE, poly_ids)
     ) $
 
-       -- Create a new identifier for each binder, with each being given
-       -- a type-variable type.
-    newMonoIds binder_rn_names kind (\ mono_ids ->
-           tcTySigs sigs               `thenTc` \ sig_info ->
-           tc_bind bind                `thenTc` \ (bind', lie) ->
-           returnTc (mono_ids, bind', lie, sig_info)
-    )
-           `thenTc` \ (mono_ids, bind', lie, sig_info) ->
-
-           -- Notice that genBinds gets the old (non-extended) environment
-    genBinds binder_names mono_ids bind' lie sig_info prag_info_fn
-  where
-    kind = case bind of
-               NonRecBind _ -> mkTypeKind      -- Recursive, so no unboxed types
-               RecBind _    -> mkBoxedTypeKind -- Non-recursive, so we permit unboxed types
-\end{code}
-
+       -- Create a new identifier for each binder, with each being given
+       -- a fresh unique, and a type-variable type.
+       -- For "mono_lies" see comments about polymorphic recursion at the 
+       -- end of the function.
+    mapAndUnzipNF_Tc mk_mono_id binder_names   `thenNF_Tc` \ (mono_lies, mono_ids) ->
+    let
+       mono_lie = plusLIEs mono_lies
+       mono_id_tys = map idType mono_ids
+    in
 
-===========
-\begin{code}
-{-
+       -- 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_tys lie     `thenTc` \ (tyvars_not_to_gen, tyvars_to_gen) ->
+
+       -- DEAL WITH TYPE VARIABLE KINDS
+    mapTc defaultUncommittedTyVar 
+         (tyVarSetToList tyvars_to_gen)        `thenTc` \ real_tyvars_to_gen_list ->
+    let
+       real_tyvars_to_gen = mkTyVarSet 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
+               --
+               -- **** This step can do unification => keep other zonking after this ****
+    in
 
-data SigInfo
-  = SigInfo    RnName
-               (TcIdBndr s)            -- Polymorpic version
-               (TcIdBndr s)            -- Monomorphic verstion
-               [TcType s] [TcIdOcc s]  -- Instance information for the monomorphic version
+       -- SIMPLIFY THE LIE
+    tcExtendGlobalTyVars tyvars_not_to_gen (
+       if null tc_ty_sigs then
+               -- No signatures, so just simplify the lie
+               -- NB: no signatures => no polymorphic recursion, so no
+               -- need to use mono_lies (which will be empty anyway)
+           tcSimplify real_tyvars_to_gen lie           `thenTc` \ (lie_free, dict_binds, lie_bound) ->
+           returnTc (lie_free, dict_binds, map instToId (bagToList lie_bound))
+
+       else
+           zonkTcTheta 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 mono_lie
+               -- so that polymorphic recursion works right (see comments at end of fn)
+               givens = dicts_sig `plusLIE` mono_lie
+           in
+
+               -- Check that the needed dicts can be expressed in
+               -- terms of the signature ones
+           tcAddErrCtxt (sigsCtxt tysig_names) $
+           tcSimplifyAndCheck real_tyvars_to_gen givens 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) 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 zonkTcType mono_id_tys                    `thenNF_Tc` \ zonked_mono_id_types ->
+    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             = (real_tyvars_to_gen_list, TcId poly_id,     TcId mono_id)
+         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 real_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.
+    in
 
+        -- BUILD RESULTS
+    returnTc (
+        AbsBinds real_tyvars_to_gen_list
+                 dicts_bound
+                 exports
+                 (dict_binds `AndMonoBinds` mbind'),
+        lie_free,
+        [poly_id | (_, TcId poly_id, _) <- exports]
+    )
+  where
+    no_of_binders = length binder_names
+
+    mk_mono_id binder_name
+      |  theres_a_signature    -- There's a signature; and it's overloaded, 
+      && not (null sig_theta)  -- so make a Method
+      = tcAddSrcLoc sig_loc $
+       newMethodWithGivenTy SignatureOrigin 
+               (TcId poly_id) (mkTyVarTys sig_tyvars) 
+               sig_theta sig_tau                       `thenNF_Tc` \ (mono_lie, TcId mono_id) ->
+                                                       -- A bit turgid to have to strip the TcId
+       returnNF_Tc (mono_lie, mono_id)
+
+      | otherwise              -- No signature or not overloaded; 
+      = tcAddSrcLoc (getSrcLoc binder_name) $
+       (if theres_a_signature then
+               returnNF_Tc sig_tau     -- Non-overloaded signature; use its type
+        else
+               newTyVarTy kind         -- No signature; use a new type variable
+       )                                       `thenNF_Tc` \ mono_id_ty ->
+
+       newLocalId (getOccName binder_name) mono_id_ty  `thenNF_Tc` \ mono_id ->
+       returnNF_Tc (emptyLIE, mono_id)
+      where
+       maybe_sig          = maybeSig tc_ty_sigs binder_name
+       theres_a_signature = maybeToBool maybe_sig
+       Just (TySigInfo name poly_id sig_tyvars sig_theta sig_tau sig_loc) = maybe_sig
+
+    tysig_names     = [name | (TySigInfo name _ _ _ _ _) <- tc_ty_sigs]
+    is_unrestricted = isUnRestrictedGroup tysig_names mbind
+
+    kind | is_rec    = mkBoxedTypeKind -- Recursive, so no unboxed types
+        | otherwise = mkTypeKind               -- Non-recursive, so we permit unboxed types
+\end{code}
 
+Polymorphic recursion
+~~~~~~~~~~~~~~~~~~~~~
+The game plan for polymorphic recursion in the code above is 
 
-       -- Deal with type signatures
-    tcTySigs sigs              `thenTc` \ sig_infos ->
-    let
-       sig_binders   = [binder      | SigInfo binder _ _ _ _  <- sig_infos]
-       poly_sigs     = [(name,poly) | SigInfo name poly _ _ _ <- sig_infos]
-       mono_sigs     = [(name,mono) | SigInfo name _ mono _ _ <- sig_infos]
-       nosig_binders = binders `minusList` sig_binders
-    in
+       * 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:
 
-       -- Typecheck the binding group
-    tcExtendLocalEnv poly_sigs         (
-    newMonoIds nosig_binders kind      (\ nosig_local_ids ->
-           tcMonoBinds mono_sigs mono_binds    `thenTc` \ binds_w_lies ->
-           returnTc (nosig_local_ids, binds_w_lies)
-    ))                                 `thenTc` \ (nosig_local_ids, binds_w_lies) ->
+       f :: Eq a => [a] -> [a]
+       f xs = ...f...
 
+If we don't take care, after typechecking we get
 
-       -- Decide what to generalise over
-    getImplicitStuffToGen sig_ids binds_w_lies 
-                       `thenTc` \ (tyvars_not_to_gen, tyvars_to_gen, lie_to_gen) ->
+       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 ins't being used (but that's a very common case).
 
-       *** CHECK FOR UNBOXED TYVARS HERE! ***
+This can lead to a massive space leak, from the following top-level defn:
 
+       ff :: [Int] -> [Int]
+       ff = f 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.
 
-       -- Make poly_ids for all the binders that don't have type signatures
-    let
-       tys_to_gen   = mkTyVarTys tyvars_to_gen
-       dicts_to_gen = map instToId (bagToList lie_to_gen)
-       dict_tys     = map tcIdType dicts_to_gen
-
-       mk_poly binder local_id = mkUserId (getName binder) ty noPragmaInfo
-                      where
-                         ty = mkForAllTys tyvars_to_gen $
-                              mkFunTys dict_tys $
-                              tcIdType local_id
-
-       more_sig_infos = [ SigInfo binder (mk_poly binder local_id) 
-                                  local_id tys_to_gen dicts_to_gen lie_to_gen
-                        | (binder, local_id) <- zipEqual "???" nosig_binders nosig_local_ids
-                        ]
-
-       all_sig_infos = sig_infos ++ more_sig_infos     -- Contains a "signature" for each binder
-    in
+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.  Thats' what the "mono_lies"
+is doing.
 
 
-       -- Now generalise the bindings
-    let
-       -- local_binds is a bunch of bindings of the form
-       --      f_mono = f_poly tyvars dicts
-       -- one for each binder, f, that lacks a type signature.
-       -- This bunch of bindings is put at the top of the RHS of every
-       -- binding in the group, so as to bind all the f_monos.
-               
-       local_binds = [ (local_id, mkHsDictApp (mkHsTyApp (HsVar local_id) tys_to_gen) dicts_to_gen)
-                     | local_id <- nosig_local_ids
-                     ]
-
-        find_sig lid = head [ (pid, tvs, ds, lie) 
-                         | SigInfo _ pid lid' tvs ds lie, 
-                           lid==lid'
-                         ]
-
-      gen_bind (bind, lie)
-       = tcSimplifyWithExtraGlobals tyvars_not_to_gen tyvars_to_gen avail lie
-                                   `thenTc` \ (lie_free, dict_binds) ->
-         returnTc (AbsBind tyvars_to_gen_here
-                           dicts
-                           (zipEqual "gen_bind" local_ids poly_ids)
-                           (dict_binds ++ local_binds)
-                           bind,
-                   lie_free)
-       where
-         local_ids  = bindersOf bind
-         local_sigs = [sig | sig@(SigInfo _ _ local_id _ _) <- all_sig_infos,
-                             local_id `elem` local_ids
-                      ]
-
-         (tyvars_to_gen_here, dicts, avail) 
-               = case (local_ids, sigs) of
-
-                   ([local_id], [SigInfo _ _ _ tyvars_to_gen dicts lie])
-                         -> (tyvars_to_gen, dicts, lie)
-
-                   other -> (tyvars_to_gen, dicts, avail)
-\end{code}
+%************************************************************************
+%*                                                                     *
+\subsection{getTyVarsToGen}
+%*                                                                     *
+%************************************************************************
 
-@getImplicitStuffToGen@ decides what type variables
-and LIE to generalise over.
+@getTyVarsToGen@ decides what type variables generalise over.
 
 For a "restricted group" -- see the monomorphism restriction
 for a definition -- we bind no dictionaries, and
@@ -332,9 +433,10 @@ stuff.  If we simplify only at the f-binding (not the xs-binding)
 we'll know that the literals are all Ints, and we can just produce
 Int literals!
 
-Find all the type variables involved in overloading, the "constrained_tyvars"
-These are the ones we *aren't* going to generalise.
-We must be careful about doing this:
+Find all the type variables involved in overloading, the
+"constrained_tyvars".  These are the ones we *aren't* going to
+generalise.  We must be careful about doing this:
+
  (a) If we fail to generalise a tyvar which is not actually
        constrained, then it will never, ever get bound, and lands
        up printed out in interface files!  Notorious example:
@@ -343,6 +445,7 @@ 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.
+
  (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
        tyvars in it.  They won't be in scope if we've generalised them.
@@ -352,86 +455,109 @@ constrained tyvars. We don't use any of the results, except to
 find which tyvars are constrained.
 
 \begin{code}
-getImplicitStuffToGen is_restricted sig_ids binds_w_lies
-  | isUnRestrictedGroup tysig_vars bind
-  = tcSimplify tyvars_to_gen lie       `thenTc` \ (_, _, dicts_to_gen) ->
-    returnNF_Tc (emptyTyVarSet, tyvars_to_gen, dicts_to_gen)
-
-  | otherwise
-  = tcSimplify tyvars_to_gen lie           `thenTc` \ (_, _, constrained_dicts) ->
-     let
+getTyVarsToGen is_unrestricted mono_id_tys lie
+  = tcGetGlobalTyVars                          `thenNF_Tc` \ free_tyvars ->
+    mapNF_Tc zonkTcType mono_id_tys            `thenNF_Tc` \ zonked_mono_id_tys ->
+    let
+       tyvars_to_gen = tyVarsOfTypes zonked_mono_id_tys `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    = foldBag unionTyVarSets tyVarsOfInst emptyTyVarSet constrained_dicts
-         reduced_tyvars_to_gen = tyvars_to_gen `minusTyVarSet` constrained_tyvars
-     in
-     returnTc (constrained_tyvars, reduced_tyvars_to_gen, emptyLIE)
-
-  where
-    sig_vars   = [sig_var | (TySigInfo sig_var _ _ _ _) <- ty_sigs]
-
-    (tyvars_to_gen, lie) = foldBag (\(tv1,lie2) (tv2,lie2) -> (tv1 `unionTyVarSets` tv2,
-                                                              lie1 `plusLIE` lie2))
-                                   get
-                                   (emptyTyVarSet, emptyLIE)
-                                   binds_w_lies
-    get (bind, lie)
-      = case bindersOf bind of
-         [local_id] | local_id `in` sig_ids ->         -- A simple binding with
-                                                       -- a type signature
-                       (emptyTyVarSet, emptyLIE)
-
-         local_ids ->                                  -- Complex binding or no type sig
-                       (foldr (unionTyVarSets . tcIdType) emptyTyVarSet local_ids, 
-                        lie)
--}
+           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}
-tc_bind :: RenamedBind -> TcM s (TcBind s, LIE s)
+isUnRestrictedGroup :: [Name]          -- Signatures given for these
+                   -> RenamedMonoBinds
+                   -> Bool
 
-tc_bind (NonRecBind mono_binds)
-  = tcMonoBinds mono_binds     `thenTc` \ (mono_binds2, lie) ->
-    returnTc  (NonRecBind mono_binds2, lie)
+is_elem v vs = isIn "isUnResMono" v vs
 
-tc_bind (RecBind mono_binds)
-  = tcMonoBinds mono_binds     `thenTc` \ (mono_binds2, lie) ->
-    returnTc  (RecBind mono_binds2, lie)
+isUnRestrictedGroup sigs (PatMonoBind (VarPatIn v) _ _) = v `is_elem` sigs
+isUnRestrictedGroup sigs (PatMonoBind other      _ _)  = False
+isUnRestrictedGroup sigs (VarMonoBind v _)             = v `is_elem` sigs
+isUnRestrictedGroup sigs (FunMonoBind _ _ _ _)         = True
+isUnRestrictedGroup sigs (AndMonoBinds mb1 mb2)                = isUnRestrictedGroup sigs mb1 &&
+                                                         isUnRestrictedGroup sigs mb2
+isUnRestrictedGroup sigs EmptyMonoBinds                        = True
 \end{code}
 
-\begin{code}
-tcMonoBinds :: RenamedMonoBinds -> TcM s (TcMonoBinds s, LIE s)
-
-tcMonoBinds EmptyMonoBinds = returnTc (EmptyMonoBinds, emptyLIE)
-
-tcMonoBinds (AndMonoBinds mb1 mb2)
-  = tcMonoBinds mb1            `thenTc` \ (mb1a, lie1) ->
-    tcMonoBinds mb2            `thenTc` \ (mb2a, lie2) ->
-    returnTc (AndMonoBinds mb1a mb2a, lie1 `plusLIE` lie2)
+@defaultUncommittedTyVar@ checks for generalisation over unboxed
+types, and defaults any TypeKind TyVars to BoxedTypeKind.
 
-tcMonoBinds bind@(PatMonoBind pat grhss_and_binds locn)
-  = tcAddSrcLoc locn            $
+\begin{code}
+defaultUncommittedTyVar tyvar
+  | isTypeKind (tyVarKind tyvar)
+  = newTcTyVar mkBoxedTypeKind                                 `thenNF_Tc` \ boxed_tyvar ->
+    unifyTauTy (mkTyVarTy boxed_tyvar) (mkTyVarTy tyvar)       `thenTc_`
+    returnTc boxed_tyvar
 
-       -- LEFT HAND SIDE
-    tcPat pat                          `thenTc` \ (pat2, lie_pat, pat_ty) ->
+  | otherwise
+  = returnTc tyvar
+\end{code}
 
-       -- BINDINGS AND GRHSS
-    tcGRHSsAndBinds grhss_and_binds    `thenTc` \ (grhss_and_binds2, lie, grhss_ty) ->
 
-       -- Unify the two sides
-    tcAddErrCtxt (patMonoBindsCtxt bind) $
-       unifyTauTy pat_ty grhss_ty                      `thenTc_`
+%************************************************************************
+%*                                                                     *
+\subsection{tcMonoBind}
+%*                                                                     *
+%************************************************************************
 
-       -- RETURN
-    returnTc (PatMonoBind pat2 grhss_and_binds2 locn,
-             plusLIE lie_pat lie)
+@tcMonoBinds@ deals with a single @MonoBind@.  
+The signatures have been dealt with already.
 
-tcMonoBinds (FunMonoBind name inf matches locn)
-  = tcAddSrcLoc locn                           $
-    tcLookupLocalValueOK "tcMonoBinds" name    `thenNF_Tc` \ id ->
-    tcMatchesFun name (idType id) matches      `thenTc` \ (matches', lie) ->
-    returnTc (FunMonoBind (TcId id) inf matches' locn, lie)
+\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                       $
+       tcAddErrCtxt (patMonoBindsCtxt bind)    $
+       tcPat pat                               `thenTc` \ (pat2, lie_pat, pat_ty) ->
+
+               -- Before checking the RHS, but after the pattern, extend the envt with
+               -- bindings for the *polymorphic* Ids from any type signatures
+       tcExtendLocalValEnv sig_names sig_ids   $
+       tcGRHSsAndBinds pat_ty grhss_and_binds  `thenTc` \ (grhss_and_binds2, lie) ->
+       returnTc (PatMonoBind pat2 grhss_and_binds2 locn,
+                 plusLIE lie_pat lie)
 \end{code}
 
 %************************************************************************
@@ -445,28 +571,157 @@ tcMonoBinds (FunMonoBind name inf matches locn)
 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}
-tcTySigs :: [RenamedSig] -> TcM s [TcSigInfo s]
+data TcSigInfo s
+  = TySigInfo      
+       Name                    -- N, the Name in corresponding binding
+       (TcIdBndr s)            -- *Polymorphic* binder for this value...
+                               -- Usually has name = N, but doesn't have to.
+       [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}
 
-tcTySigs (Sig v ty _ src_loc : other_sigs)
- = tcAddSrcLoc src_loc (
-       tcPolyType ty                   `thenTc` \ sigma_ty ->
-       tcInstSigType sigma_ty          `thenNF_Tc` \ sigma_ty' ->
-       let
-           (tyvars', theta', tau') = splitSigmaTy sigma_ty'
-       in
 
-       tcLookupLocalValueOK "tcSig1" v `thenNF_Tc` \ val ->
-       unifyTauTy (idType val) tau'    `thenTc_`
+\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@( sig1@(TySigInfo _ id1 _ theta1 _ _) : all_sigs_but_first )
+  =    -- CHECK THAT THE SIGNATURE TYVARS AND TAU_TYPES ARE OK
+       -- Doesn't affect substitution
+    mapTc check_one_sig tc_ty_sigs     `thenTc_`
+
+       -- 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
+    mapTc check_one_cxt all_sigs_but_first             `thenTc_`
+
+    returnTc theta1
+  where
+    sig1_dict_tys      = mk_dict_tys theta1
+    n_sig1_dict_tys    = length sig1_dict_tys
+
+    check_one_cxt 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_one_sig (TySigInfo name id sig_tyvars _ sig_tau src_loc)
+      = tcAddSrcLoc src_loc    $
+       tcAddErrCtxt (sigCtxt id) $
+       checkSigTyVars sig_tyvars sig_tau
+
+    mk_dict_tys theta = [mkDictTy c t | (c,t) <- theta]
+\end{code}
+
+
+@checkSigTyVars@ is used after the type in a type signature has been unified with
+the actual type found.  It then checks that the type variables of the type signature
+are
+       (a) still all type variables
+               eg matching signature [a] against inferred type [(p,q)]
+               [then a will be unified to a non-type variable]
+
+       (b) still all distinct
+               eg matching signature [(a,b)] against inferred type [(p,p)]
+               [then a and b will be unified together]
 
-       returnTc (TySigInfo val tyvars' theta' tau' src_loc)
-   )           `thenTc` \ sig_info1 ->
+BUT ACTUALLY THESE FIRST TWO ARE FORCED BY USING DontBind TYVARS
 
-   tcTySigs other_sigs `thenTc` \ sig_infos ->
-   returnTc (sig_info1 : sig_infos)
+       (c) not mentioned in the environment
+               eg the signature for f in this:
 
-tcTySigs (other : sigs) = tcTySigs sigs
-tcTySigs []            = returnTc []
+                       g x = ... where
+                                       f :: a->[a]
+                                       f y = [x,y]
+
+               Here, f is forced to be monorphic by the free occurence of x.
+
+Before doing this, the substitution is applied to the signature type variable.
+
+\begin{code}
+checkSigTyVars :: [TcTyVar s]          -- The original signature type variables
+              -> TcType s              -- signature type (for err msg)
+              -> TcM s ()
+
+checkSigTyVars sig_tyvars sig_tau
+  =    -- Several type signatures in the same bindings group can 
+       -- cause the signature type variable from the different
+       -- signatures to be unified.  So we need to zonk them.
+    mapNF_Tc zonkSigTyVar sig_tyvars   `thenNF_Tc` \ sig_tyvars' ->
+
+       -- Point (a) is forced by the fact that they are signature type
+       -- variables, so the unifer won't bind them to a type.
+
+       -- Check point (b)
+    checkTcM (hasNoDups sig_tyvars')
+            (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_tyvars' correspond
+       -- 1-1 with sig_tyvars, so we can just map back.
+    tcGetGlobalTyVars                  `thenNF_Tc` \ globals ->
+    let
+--     mono_tyvars = [sig_tv | (sig_tv, sig_tv') <- sig_tyvars `zip` sig_tyvars',
+--                              sig_tv' `elementOfTyVarSet` globals
+--                   ]
+       mono_tyvars' = [sig_tv' | sig_tv' <- sig_tyvars', 
+                                 sig_tv' `elementOfTyVarSet` globals]
+    in
+    checkTcM (null mono_tyvars')
+            (zonkTcType sig_tau        `thenNF_Tc` \ sig_tau' ->
+             failTc (notAsPolyAsSigErr sig_tau' mono_tyvars'))
 \end{code}
 
 
@@ -485,10 +740,18 @@ 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,
+                      TcMonoBinds s,
                       LIE s)
 
-tcPragmaSigs sigs = returnTc ( \name -> NoPragmaInfo, EmptyBinds, emptyLIE )
+-- For now we just deal with INLINE pragmas
+tcPragmaSigs sigs = returnTc (prag_fn, EmptyMonoBinds, emptyLIE )
+  where
+    prag_fn name | any has_inline sigs = IWantToBeINLINEd
+                | otherwise           = NoPragmaInfo
+                where
+                   has_inline (InlineSig n _) = (n == name)
+                   has_inline other           = False
+               
 
 {- 
 tcPragmaSigs sigs
@@ -505,12 +768,10 @@ tcPragmaSigs sigs
 Here are the easy cases for tcPragmaSigs
 
 \begin{code}
-tcPragmaSig (DeforestSig name loc)
-  = returnTc ((name, addInfo DoDeforest),EmptyBinds,emptyLIE)
 tcPragmaSig (InlineSig name loc)
-  = returnTc ((name, addInfo_UF (iWantToBeINLINEd UnfoldAlways)), EmptyBinds, emptyLIE)
+  = returnTc ((name, addUnfoldInfo (iWantToBeINLINEd UnfoldAlways)), EmptyBinds, emptyLIE)
 tcPragmaSig (MagicUnfoldingSig name string loc)
-  = returnTc ((name, addInfo_UF (mkMagicUnfolding string)), EmptyBinds, emptyLIE)
+  = returnTc ((name, addUnfoldInfo (mkMagicUnfolding string)), EmptyBinds, emptyLIE)
 \end{code}
 
 The interesting case is for SPECIALISE pragmas.  There are two forms.
@@ -567,7 +828,7 @@ tcPragmaSig (SpecSig name poly_ty maybe_spec_name src_loc)
     tcAddErrCtxt (valSpecSigCtxt name spec_ty) $
 
        -- Get and instantiate its alleged specialised type
-    tcPolyType poly_ty                         `thenTc` \ sig_sigma ->
+    tcHsType poly_ty                           `thenTc` \ sig_sigma ->
     tcInstSigType  sig_sigma                   `thenNF_Tc` \ sig_ty ->
     let
        (sig_tyvars, sig_theta, sig_tau) = splitSigmaTy sig_ty
@@ -642,80 +903,84 @@ tcPragmaSig (SpecSig name poly_ty maybe_spec_name src_loc)
                         VarMonoBind spec_pragma_id (HsVar (TcId local_spec_id))
            spec_info  = SpecInfo spec_tys (length main_theta) local_spec_id
        in
-       returnTc ((name, addInfo spec_info), spec_binds, spec_lie)
+       returnTc ((name, addSpecInfo spec_info), spec_binds, spec_lie)
 -}
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection[TcBinds-monomorphism]{The monomorphism restriction}
+\subsection[TcBinds-errors]{Error contexts and messages}
 %*                                                                     *
 %************************************************************************
 
-Not exported:
 
 \begin{code}
-isUnRestrictedGroup :: [TcIdBndr s]            -- Signatures given for these
-                   -> TcBind s
-                   -> Bool
+patMonoBindsCtxt bind sty
+  = hang (ptext SLIT("In a pattern binding:")) 4 (ppr sty bind)
 
-isUnRestrictedGroup sigs EmptyBind              = True
-isUnRestrictedGroup sigs (NonRecBind monobinds) = isUnResMono sigs monobinds
-isUnRestrictedGroup sigs (RecBind monobinds)    = isUnResMono sigs monobinds
+-----------------------------------------------
+valSpecSigCtxt v ty sty
+  = hang (ptext SLIT("In a SPECIALIZE pragma for a value:"))
+        4 (sep [(<>) (ppr sty v) (ptext SLIT(" ::")),
+                 ppr sty ty])
 
-is_elem v vs = isIn "isUnResMono" v vs
 
-isUnResMono sigs (PatMonoBind (VarPat (TcId v)) _ _)   = v `is_elem` sigs
-isUnResMono sigs (PatMonoBind other      _ _)          = False
-isUnResMono sigs (VarMonoBind (TcId v) _)              = v `is_elem` sigs
-isUnResMono sigs (FunMonoBind _ _ _ _)                 = True
-isUnResMono sigs (AndMonoBinds mb1 mb2)                        = isUnResMono sigs mb1 &&
-                                                         isUnResMono sigs mb2
-isUnResMono sigs EmptyMonoBinds                                = True
-\end{code}
 
+-----------------------------------------------
+notAsPolyAsSigErr sig_tau mono_tyvars sty
+  = hang (ptext SLIT("A type signature is more polymorphic than the inferred type"))
+       4  (vcat [text "Can't for-all the type variable(s)" <+> interpp'SP sty mono_tyvars,
+                 text "in the inferred type" <+> ppr sty sig_tau
+          ])
 
-%************************************************************************
-%*                                                                     *
-\subsection[TcBinds-errors]{Error contexts and messages}
-%*                                                                     *
-%************************************************************************
+-----------------------------------------------
+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)
+          ])
 
+-----------------------------------------------
+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]
 
-\begin{code}
-patMonoBindsCtxt bind sty
-  = ppHang (ppPStr SLIT("In a pattern binding:")) 4 (ppr sty bind)
+-----------------------------------------------
+sigContextsErr sty
+  = ptext SLIT("Mismatched contexts")
+sigContextsCtxt s1 s2 sty
+  = hang (hsep [ptext SLIT("When matching the contexts of the signatures for"), 
+               ppr sty s1, ptext SLIT("and"), ppr sty s2])
+        4 (ptext SLIT("(the signature contexts in a mutually recursive group should all be identical)"))
+
+-----------------------------------------------
+specGroundnessCtxt
+  = panic "specGroundnessCtxt"
 
 --------------------------------------------
 specContextGroundnessCtxt -- err_ctxt dicts sty
   = panic "specContextGroundnessCtxt"
 {-
-  = ppHang (
-       ppSep [ppBesides [ppStr "In the SPECIALIZE pragma for `", ppr sty name, ppStr "'"],
-              ppBesides [ppStr " specialised to the type `", ppr sty spec_ty,  ppStr "'"],
-              pp_spec_id sty,
-              ppStr "... not all overloaded type variables were instantiated",
-              ppStr "to ground types:"])
-      4 (ppAboves [ppCat [ppr sty c, ppr sty t]
+  = 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 -> ppNil)
+         ValSpecSigCtxt    n ty loc      -> (n, ty, loc, \ x -> empty)
          ValSpecSpecIdCtxt n ty spec loc ->
            (n, ty, loc,
-            \ sty -> ppBesides [ppStr "... type of explicit id `", ppr sty spec, ppStr "'"])
+            \ sty -> hsep [ptext SLIT("... type of explicit id"), ppr sty spec])
 -}
+\end{code}
 
------------------------------------------------
-specGroundnessCtxt
-  = panic "specGroundnessCtxt"
 
 
-valSpecSigCtxt v ty sty
-  = ppHang (ppPStr SLIT("In a SPECIALIZE pragma for a value:"))
-        4 (ppSep [ppBeside (pprNonSym sty v) (ppPStr SLIT(" ::")),
-                 ppr sty ty])
-\end{code}