[project @ 1997-07-26 03:27:26 by sof]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcBinds.lhs
index 21be195..2417160 100644 (file)
@@ -6,46 +6,74 @@
 \begin{code}
 #include "HsVersions.h"
 
-module TcBinds ( tcBindsAndThen, tcPragmaSigs ) where
-
-import Ubiq
+module TcBinds ( tcBindsAndThen, tcPragmaSigs, checkSigTyVars, tcBindWithSigs, TcSigInfo(..) ) where
+
+IMP_Ubiq()
+#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 HsSyn           ( HsBinds(..), Bind(..), Sig(..), MonoBinds(..), 
-                         HsExpr, Match, PolyType, InPat, OutPat(..),
-                         GRHSsAndBinds, ArithSeqInfo, HsLit, Fake,
-                         collectBinders )
-import RnHsSyn         ( RenamedHsBinds(..), RenamedBind(..), RenamedSig(..), 
-                         RenamedMonoBinds(..), RnName(..)
+import TcMonad
+import Inst            ( Inst, SYN_IE(LIE), emptyLIE, plusLIE, InstOrigin(..),
+                         newDicts, tyVarsOfInst, instToId
                        )
-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 TcLoop          ( tcGRHSsAndBinds )
+import TcEnv           ( tcExtendLocalValEnv, tcLookupLocalValueOK, newMonoIds,
+                         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, tcInstType )
-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, zonkTcTyVar, zonkTcTyVars,
+                         newTcTyVar, tcInstSigType, newTyVarTys
+                       )
+import Unify           ( unifyTauTy, unifyTauTyLists )
 
-import Kind            ( mkBoxedTypeKind, mkTypeKind )
-import Id              ( GenId, idType, mkUserId )
+import Kind            ( isUnboxedTypeKind, mkTypeKind, isTypeKind, mkBoxedTypeKind )
+import Id              ( GenId, idType, mkUserLocal, 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, 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,173 @@ 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) ->
-
-       -- Create specialisations of functions bound here
-    bindInstsOfLocalFuns (prag_lie `plusLIE` thing_lie)
-                         poly_ids      `thenTc` \ (lie2, inst_mbinds) ->
+* binder_names and mbind must define the same set of Names
 
-       -- 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 _ -> mkBoxedTypeKind -- Recursive, so no unboxed types
-               RecBind _    -> mkTypeKind      -- Non-recursive, so we permit unboxed types
-\end{code}
-
-
-===========
-\begin{code}
-{-
-
-data SigInfo
-  = SigInfo    RnName
-               (TcIdBndr s)            -- Polymorpic version
-               (TcIdBndr s)            -- Monomorphic verstion
-               [TcType s] [TcIdOcc s]  -- Instance information for the monomorphic version
-
-
-
-       -- Deal with type signatures
-    tcTySigs sigs              `thenTc` \ sig_infos ->
+       -- 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 ->
     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
+       mono_ids           = zipWith3Equal "tcBindAndSigs" mk_id binder_names uniqs mono_id_tys
+       mk_id name uniq ty = mkUserLocal (getOccName name) uniq ty (getSrcLoc name)
     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_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
 
-       -- 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) ->
-
-
-       -- Decide what to generalise over
-    getImplicitStuffToGen sig_ids binds_w_lies 
-                       `thenTc` \ (tyvars_not_to_gen, tyvars_to_gen, lie_to_gen) ->
-
-
-       *** CHECK FOR UNBOXED TYVARS HERE! ***
-
-
-
-       -- Make poly_ids for all the binders that don't have type signatures
+       -- SIMPLIFY THE LIE
+    tcExtendGlobalTyVars tyvars_not_to_gen (
+       if null tc_ty_sigs then
+               -- No signatures, so just simplify the lie
+           tcSimplify real_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 real_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) 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
-       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) <- nosig_binders `zipEqual` nosig_local_ids
-                        ]
-
-       all_sig_infos = sig_infos ++ more_sig_infos     -- Contains a "signature" for each binder
+       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
 
-       -- 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
-                           (local_ids `zipEqual` 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
-                      ]
+    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
 
-         (tyvars_to_gen_here, dicts, avail) 
-               = case (local_ids, sigs) of
+    tysig_names     = [name | (TySigInfo name _ _ _ _ _) <- tc_ty_sigs]
+    is_unrestricted = isUnRestrictedGroup tysig_names mbind
 
-                   ([local_id], [SigInfo _ _ _ tyvars_to_gen dicts lie])
-                         -> (tyvars_to_gen, dicts, lie)
+    kind | is_rec    = mkBoxedTypeKind -- Recursive, so no unboxed types
+        | otherwise = mkTypeKind               -- Non-recursive, so we permit unboxed types
 
-                   other -> (tyvars_to_gen, dicts, avail)
+zonk_theta theta = mapNF_Tc zonk theta
+       where
+         zonk (c,t) = zonkTcType t     `thenNF_Tc` \ t' ->
+                      returnNF_Tc (c,t')
 \end{code}
 
-@getImplicitStuffToGen@ decides what type variables
-and LIE to generalise over.
+@getImplicitStuffToGen@ decides what type variables generalise over.
 
 For a "restricted group" -- see the monomorphism restriction
 for a definition -- we bind no dictionaries, and
@@ -332,9 +358,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 +370,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 +380,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)
+@defaultUncommittedTyVar@ checks for generalisation over unboxed
+types, and defaults any TypeKind TyVars to BoxedTypeKind.
 
-tcMonoBinds (AndMonoBinds mb1 mb2)
-  = tcMonoBinds mb1            `thenTc` \ (mb1a, lie1) ->
-    tcMonoBinds mb2            `thenTc` \ (mb2a, lie2) ->
-    returnTc (AndMonoBinds mb1a mb2a, lie1 `plusLIE` lie2)
-
-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 +496,150 @@ 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 ->
-       tcInstType [] 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}
 
-       returnTc (TySigInfo val tyvars' theta' tau' src_loc)
-   )           `thenTc` \ sig_info1 ->
+@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.
 
-   tcTySigs other_sigs `thenTc` \ sig_infos ->
-   returnTc (sig_info1 : sig_infos)
+The error message here is somewhat unsatisfactory, but it'll do for
+now (ToDo).
 
-tcTySigs (other : sigs) = tcTySigs sigs
-tcTySigs []            = returnTc []
+\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]
+
+BUT ACTUALLY THESE FIRST TWO ARE FORCED BY USING DontBind TYVARS
+
+       (c) not mentioned in the environment
+               eg the signature for f in this:
+
+                       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
+  = 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)
 \end{code}
 
 
@@ -485,10 +658,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
@@ -506,11 +687,11 @@ Here are the easy cases for tcPragmaSigs
 
 \begin{code}
 tcPragmaSig (DeforestSig name loc)
-  = returnTc ((name, addInfo DoDeforest),EmptyBinds,emptyLIE)
+  = returnTc ((name, addDeforestInfo 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,8 +748,8 @@ 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 ->
-    tcInstType [] sig_sigma                    `thenNF_Tc` \ sig_ty ->
+    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
@@ -580,7 +761,7 @@ tcPragmaSig (SpecSig name poly_ty maybe_spec_name src_loc)
 
        -- Get and instantiate the type of the id mentioned
     tcLookupLocalValueOK "tcPragmaSig" name    `thenNF_Tc` \ main_id ->
-    tcInstType [] (idType main_id)             `thenNF_Tc` \ main_ty ->
+    tcInstSigType [] (idType main_id)          `thenNF_Tc` \ main_ty ->
     let
        (main_tyvars, main_rho) = splitForAllTy main_ty
        (main_theta,main_tau)   = splitRhoTy main_rho
@@ -642,80 +823,85 @@ 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 "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")
+                    ])
 
-%************************************************************************
-%*                                                                     *
-\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}