[project @ 1996-03-19 08:58:34 by partain]
[ghc-hetmet.git] / ghc / compiler / typecheck / GenSpecEtc.lhs
index c607157..f0008df 100644 (file)
@@ -1,5 +1,5 @@
 %
-% (c) The GRASP/AQUA Project, Glasgow University, 1992-1995
+% (c) The GRASP/AQUA Project, Glasgow University, 1992-1996
 %
 \section[GenSpecEtc]{Code for GEN, SPEC, PRED, and REL}
 
@@ -7,73 +7,60 @@
 #include "HsVersions.h"
 
 module GenSpecEtc (
-       genBinds, SignatureInfo(..),
-       checkSigTyVars,
-
-       -- and to make the interface self-sufficient...
-       Bag, E, Bind, Binds, TypecheckedPat, Id, Inst,
-       LIE, TcResult, Name, SrcLoc, Subst, TyVar, UniType,
-       UniqueSupply, Error(..), Pretty(..), PprStyle,
-       PrettyRep
+       TcSigInfo(..), 
+       genBinds, 
+       checkSigTyVars, checkSigTyVarsGivenGlobals,
+       specTy
     ) where
 
-import TcMonad         -- typechecker monadery
-import TcMonadFns      ( applyTcSubstAndCollectTyVars,
-                         mkIdsWithGivenTys
-                       )
-import AbsSyn
-
-import AbsUniType
-import E               ( tvOfE, E, LVE(..), TCE(..), UniqFM, CE(..) )
-                       -- TCE and CE for pragmas only
-import Errors
-import Id              ( getIdUniType, mkInstId, Id, DictVar(..) )
-import IdInfo
-import Inst
-import LIE             ( mkLIE, unMkLIE, LIE )
+import Ubiq
+
+import TcMonad
+import Inst            ( Inst, InstOrigin(..), LIE(..), plusLIE, 
+                         newDicts, tyVarsOfInst, instToId )
+import TcEnv           ( tcGetGlobalTyVars, newMonoIds )
+import TcSimplify      ( tcSimplify, tcSimplifyAndCheck, tcSimplifyWithExtraGlobals )
+import TcType          ( TcType(..), TcThetaType(..), TcTauType(..), 
+                         TcTyVarSet(..), TcTyVar(..), tcInstType, zonkTcType )
+
+import HsSyn           ( HsBinds(..), Bind(..), MonoBinds(..), HsExpr, OutPat(..), 
+                         Sig, HsLit, ArithSeqInfo, InPat, GRHSsAndBinds, Match, Fake,
+                         collectBinders )
+import TcHsSyn         ( TcIdOcc(..), TcIdBndr(..), TcHsBinds(..), TcBind(..), TcExpr(..) )
+
+import Bag             ( Bag, foldBag, bagToList, listToBag, isEmptyBag )
+import Class           ( GenClass )
+import Id              ( GenId, Id(..), mkUserId, idType )
 import ListSetOps      ( minusList, unionLists, intersectLists )
-import Maybes          ( assocMaybe, Maybe(..) )
-import Name            ( Name(..) )    -- ToDo: a HACK
-import TcSimplify      ( tcSimplify, tcSimplifyAndCheck )
+import Maybes          ( Maybe(..), allMaybes )
+import Outputable      ( interppSP, interpp'SP )
+import Pretty
+import PprType         ( GenClass, GenType, GenTyVar )
+import Type            ( mkTyVarTy, splitSigmaTy, mkForAllTys, mkFunTys,
+                         getTyVar_maybe, tyVarsOfTypes, eqSimpleTheta )
+import TyVar           ( GenTyVar, TyVar(..), minusTyVarSet, emptyTyVarSet,
+                         elementOfTyVarSet, unionTyVarSets, tyVarSetToList )
+import Usage           ( UVar(..) )
+import Unique          ( Unique )
 import Util
-
-IMPORT_Trace           -- ToDo: rm (debugging)
-import Pretty          -- 
 \end{code}
 
 %************************************************************************
 %*                                                                     *
-\subsection[Gen-SignatureInfo]{The @SignatureInfo@ type}
+\subsection[Gen-SignatureInfo]{The @TcSigInfo@ type}
 %*                                                                     *
 %************************************************************************
 
 A type signature (or user-pragma) is typechecked to produce a
-@SignatureInfo@.
+@TcSigInfo@.  It contains @TcTypes@ because they are unified with
+the variable's type, and after that checked to see whether they've
+been instantiated.
 
 \begin{code}
-data SignatureInfo
-  = TySigInfo      Id  -- for this value...
-                   [TyVar] [Inst] TauType
-                   SrcLoc
-
-  | ValSpecInfo            Name        -- we'd rather have the Name than Id...
-                   UniType
-                   (Maybe Name)
-                   SrcLoc
-
-  | ValInlineInfo   Name
-                   UnfoldingGuidance
-                   SrcLoc
-
-  | ValDeforestInfo Name
-                    SrcLoc
-
-  | ValMagicUnfoldingInfo
-                   Name
-                   FAST_STRING
+data TcSigInfo s
+  = TySigInfo      (TcIdBndr s)        -- for this value...
+                   [TcTyVar s] (TcThetaType s) (TcTauType s)
                    SrcLoc
-
-  -- ToDo: perhaps add more (for other user pragmas)
 \end{code}
 
 
@@ -84,16 +71,13 @@ data SignatureInfo
 %************************************************************************
 
 \begin{code}
-genBinds :: Bool                               -- True <=> top level
-        -> E 
-        -> TypecheckedBind 
-        -> LIE                                 -- LIE from typecheck of binds
-        -> LVE                                 -- Local types
-        -> [SignatureInfo]                     -- Signatures, if any
-        -> TcM (TypecheckedBinds, LIE, LVE)    -- Generalised binds, reduced LIE,
-                                               --      polymorphic LVE
-                                               -- The LVE and LIE are fixed points
-                                               -- of the substitution
+genBinds :: [Name]                             -- Binders
+        -> [TcIdBndr s]                        -- Monomorphic binders
+        -> TcBind s                            -- Type-checked monobind
+        -> LIE s                               -- LIE from typecheck of binds
+        -> [TcSigInfo s]                       -- Signatures, if any
+        -> (Name -> PragmaInfo)                -- Gives pragma info for binder
+        -> TcM s (TcHsBinds s, LIE s, [TcIdBndr s])
 \end{code}
 
 In the call $(@genBinds@~env~bind~lie~lve)$, $(bind,lie,lve)$
@@ -143,128 +127,70 @@ generate a suitable AbsBinds to enclose the bindings.
 \end{itemize}
 
 \begin{code}
-genBinds top_level e bind lie lve sigs
-  = getSrcLocTc                                        `thenNF_Tc` \ locn ->
-
-       -- GET TYPE VARIABLES FREE IN ENV
-    applyTcSubstAndCollectTyVars (tvOfE e)     `thenNF_Tc` \ free_tyvars ->
-
-       -- CHECK THAT THE SIGNATURES MATCH
+genBinds binder_names mono_ids bind lie sig_infos prag_info_fn
+  =    -- CHECK THAT THE SIGNATURES MATCH
        -- Doesn't affect substitution
-    mapTc (checkSigMatch free_tyvars) sigs     `thenTc_`
-
-        -- UNPACK THE LVE
-    let
-       (bound_var_names, bound_var_locals) = unzip lve
-       bound_var_types = map getIdUniType bound_var_locals
-    in
-    applyTcSubstToTys bound_var_types `thenNF_Tc`      \ bound_var_types' ->
+    mapTc checkSigMatch sig_infos      `thenTc_`
+
+       -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE IDENTICAL
+       -- The type signatures on a mutually-recursive group of definitions
+       -- must all have the same context (or none).
+       -- We have to zonk them first to make their type variables line up
+    mapNF_Tc get_zonked_theta sig_infos                `thenNF_Tc` \ thetas ->
+    checkTc (null thetas || all (eqSimpleTheta (head thetas)) (tail thetas)) 
+           (sigContextsErr sig_infos)          `thenTc_`
+
+       -- COMPUTE VARIABLES OVER WHICH TO QUANTIFY, namely tyvars_to_gen
+    mapNF_Tc (zonkTcType . idType) mono_ids    `thenNF_Tc` \ mono_id_types ->
+    tcGetGlobalTyVars                          `thenNF_Tc` \ free_tyvars ->
     let
-       mentioned_tyvars' = extractTyVarsFromTys bound_var_types'
-
-        -- COMPUTE VARIABLES OVER WHICH TO QUANTIFY, namely tyvars_to_gen
-       tyvars_to_gen = mentioned_tyvars' `minusList` free_tyvars
-
-       -- UNSCRAMBLE "sigs" INTO VARIOUS FLAVOURS
-       -- AND SNAFFLE ANY "IdInfos" FOR VARS HERE
-
-       (ty_sigs, upragmas) = partition is_tysig_info sigs
-       inline_sigs         = filter is_inline_info   upragmas
-       deforest_sigs       = filter is_deforest_info upragmas
-       magic_uf_sigs       = filter is_magic_uf_info upragmas
-       spec_sigs           = filter is_spec_info     upragmas
-
-       unfold_me_fn n
-         = case [ x | x@(ValInlineInfo v _ _) <- inline_sigs, v == n ] of
-             (ValInlineInfo _ guide _ :_) -> iWantToBeINLINEd guide
-             [] ->
-               case [ x | x@(ValMagicUnfoldingInfo v _ _) <- magic_uf_sigs, v == n ] of
-                 (ValMagicUnfoldingInfo _ str _:_) -> mkMagicUnfolding str
-                 []                            -> noInfo_UF
-
-        deforest_me_fn n
-          = case [ x | x@(ValDeforestInfo v _) <- deforest_sigs, v == n ] of
-            (ValDeforestInfo _ _ : _) -> DoDeforest
-            [] -> Don'tDeforest
-
-       id_info_for n
-         = noIdInfo
-             `addInfo_UF` (unfold_me_fn   n)
-              `addInfo`    (deforest_me_fn n)
-
-       id_infos = [ id_info_for n | n <- bound_var_names ]
+       mentioned_tyvars = tyVarsOfTypes mono_id_types
+       tyvars_to_gen    = mentioned_tyvars `minusTyVarSet` free_tyvars
     in
-    resolveOverloading top_level e free_tyvars tyvars_to_gen lie bind ty_sigs
+
+       -- DEAL WITH OVERLOADING
+    resolveOverloading tyvars_to_gen lie bind sig_infos
                 `thenTc` \ (lie', reduced_tyvars_to_gen, dict_binds, dicts_bound) ->
 
         -- BUILD THE NEW LOCALS
     let
-       dict_tys = map getInstUniType dicts_bound
-
-       envs_and_new_locals_types
-         = map (quantifyTy reduced_tyvars_to_gen . glueTyArgs dict_tys) bound_var_types'
-
-       (_, new_locals_types) = unzip envs_and_new_locals_types
-    in
-        -- The new_locals function is passed into genBinds
-        -- so it can generate top-level or non-top-level locals
-    let
-       lve_of_new_ids = mkIdsWithGivenTys bound_var_names new_locals_types id_infos
-       new_ids = map snd lve_of_new_ids
+       tyvars      = tyVarSetToList reduced_tyvars_to_gen      -- Commit to a particular order
+       dict_tys    = [idType d | TcId d <- dicts_bound]        -- Slightly ugh-ish
+       poly_tys    = map (mkForAllTys tyvars . mkFunTys dict_tys) mono_id_types
+       poly_ids    = zipWithEqual mk_poly binder_names poly_tys
+       mk_poly name ty = mkUserId name ty (prag_info_fn name)
     in
         -- BUILD RESULTS
     returnTc (
---     pprTrace "Gen: " (ppSep [ppr PprDebug new_ids, 
---                              ppStr "; to gen ", ppr PprDebug tyvars_to_gen,
---                              ppStr "; reduced ", ppr PprDebug reduced_tyvars_to_gen
---             ]) $
-        AbsBinds reduced_tyvars_to_gen (map mkInstId dicts_bound)
-                (bound_var_locals `zip` new_ids)
-                dict_binds bind,
+        AbsBinds tyvars
+                 dicts_bound
+                 (map TcId mono_ids `zip` map TcId poly_ids)
+                 dict_binds
+                 bind,
         lie',
-        lve_of_new_ids
+        poly_ids
     )
-  where
-    is_tysig_info (TySigInfo _ _ _ _ _) = True
-    is_tysig_info _                    = False
 
-    is_inline_info (ValInlineInfo _ _ _) = True
-    is_inline_info _ = False
-
-    is_deforest_info (ValDeforestInfo _ _) = True
-    is_deforest_info _ = False
-    is_magic_uf_info (ValMagicUnfoldingInfo _ _ _) = True
-    is_magic_uf_info _ = False
-
-    is_spec_info (ValSpecInfo _ _ _ _) = True
-    is_spec_info _ = False
+get_zonked_theta (TySigInfo _ _ theta _ _)
+  = mapNF_Tc (\ (c,t) -> zonkTcType t `thenNF_Tc` \ t' -> returnNF_Tc (c,t')) theta
 \end{code}
 
 
 \begin{code}
-resolveOverloading 
-       :: Bool                 -- True <=> top level
-       -> E
-       -> [TyVar]              -- Tyvars free in E
-       -> [TyVar]              -- Tyvars over which we are going to generalise
-       -> LIE                  -- The LIE to deal with
-       -> TypecheckedBind      -- The binding group
-       -> [SignatureInfo]      -- And its real type-signature information
-       -> TcM (LIE,                    -- LIE to pass up the way; a fixed point of
-                                       -- the current substitution
-               [TyVar],                -- Revised tyvars to generalise
-               [(Inst, TypecheckedExpr)],-- Dict bindings
-               [Inst])                 -- List of dicts to bind here
-                      
-resolveOverloading top_level e free_tyvars tyvars_to_gen lie bind ty_sigs
-  = let
-       dicts = unMkLIE lie
-    in
-        -- DEAL WITH MONOMORPHISM RESTRICTION
-    if (not (isUnRestrictedGroup tysig_vars bind)) then 
-
-       -- Restricted group, so bind no dictionaries, and
+resolveOverloading
+       :: TcTyVarSet s         -- Tyvars over which we are going to generalise
+       -> LIE s                -- The LIE to deal with
+       -> TcBind s             -- The binding group
+       -> [TcSigInfo s]        -- And its real type-signature information
+       -> TcM s (LIE s,                        -- LIE to pass up the way; a fixed point of
+                                               -- the current substitution
+                 TcTyVarSet s,                 -- Revised tyvars to generalise
+                 [(TcIdOcc s, TcExpr s)],      -- Dict bindings
+                 [TcIdOcc s])                  -- List of dicts to bind here
+
+resolveOverloading tyvars_to_gen dicts bind ty_sigs
+  | not (isUnRestrictedGroup tysig_vars bind)
+  =    -- Restricted group, so bind no dictionaries, and
        -- remove from tyvars_to_gen any constrained type variables
 
        -- *Don't* simplify dicts at this point, because we aren't going
@@ -277,11 +203,11 @@ resolveOverloading top_level e free_tyvars tyvars_to_gen lie bind ty_sigs
        -- we'll know that the literals are all Ints, and we can just produce
        -- Int literals!
 
-       -- Find all the type variables involved in overloading 
+       -- 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 
+       --      constrained, then it will never, ever get bound, and lands
        --      up printed out in interface files!  Notorious example:
        --              instance Eq a => Eq (Foo a b) where ..
        --      Here, b is not constrained, even though it looks as if it is.
@@ -289,94 +215,62 @@ resolveOverloading top_level e free_tyvars tyvars_to_gen lie bind ty_sigs
        --      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 
+       --      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.
        --
        -- So we are careful, and do a complete simplification just to find the
        -- constrained tyvars. We don't use any of the results, except to
        -- find which tyvars are constrained.
 
-       tcSimplify top_level free_tyvars tyvars_to_gen dicts
-                                   `thenTc` \ (_, _, dicts_sig) ->
-
--- ASSERT: tcSimplify has already applied subst to its results
--- (WDP/SLPJ 95/07)
---     applyTcSubstToInsts dicts_sig   `thenNF_Tc`     \ dicts_sig' ->
+       tcSimplify tyvars_to_gen dicts      `thenTc` \ (_, _, dicts_sig) ->
        let
-         constrained_tyvars
-           = foldr (unionLists . extractTyVarsFromInst) [] dicts_sig
-
-         reduced_tyvars_to_gen = tyvars_to_gen `minusList` constrained_tyvars
-
-         increased_free_tyvars = free_tyvars `unionLists` constrained_tyvars
+         -- ASSERT: dicts_sig is already zonked!
+         constrained_tyvars    = foldBag unionTyVarSets tyVarsOfInst emptyTyVarSet dicts_sig
+         reduced_tyvars_to_gen = tyvars_to_gen `minusTyVarSet` constrained_tyvars
        in
 
-       -- Do it again, but with increased_free_tyvars/reduced_tyvars_to_gen:
-
-       tcSimplify top_level increased_free_tyvars reduced_tyvars_to_gen dicts
+       -- Do it again, but with increased free_tyvars/reduced_tyvars_to_gen:
+       -- We still need to do this simplification, because some dictionaries 
+       -- may gratuitouslyconstrain some tyvars over which we *are* going 
+       -- to generalise. 
+       -- For example d::Eq (Foo a b), where Foo is instanced as above.
+       tcSimplifyWithExtraGlobals constrained_tyvars reduced_tyvars_to_gen dicts
                                    `thenTc` \ (dicts_free, dicts_binds, dicts_sig2) ->
---NB: still no applyTcSubstToInsts
+       ASSERT(isEmptyBag dicts_sig2)
 
---     pprTrace "resolve:" (ppCat [ppr PprDebug free_tyvars, ppr PprDebug tyvars_to_gen, ppr PprDebug constrained_tyvars, ppr PprDebug reduced_tyvars_to_gen, ppr PprDebug bind]) $
-       returnTc (mkLIE (dicts_free++dicts_sig2), -- All these are left unbound
-                 reduced_tyvars_to_gen, 
+       returnTc (dicts_free,                   -- All these are left unbound
+                 reduced_tyvars_to_gen,
                  dicts_binds,                  -- Local dict binds
                  [])                           -- No lambda-bound dicts
 
                -- The returned LIE should be a fixed point of the substitution
 
-    else -- Unrestricted group
-       case ty_sigs of
-        [] ->  -- NO TYPE SIGNATURES
+  | otherwise  -- An unrestricted group
+  = case ty_sigs of
+       [] ->   -- NO TYPE SIGNATURES
 
-           tcSimplify top_level free_tyvars tyvars_to_gen dicts
-                                   `thenTc` \ (dicts_free, dict_binds, dicts_sig) ->
-           returnTc (mkLIE dicts_free, tyvars_to_gen, dict_binds, dicts_sig)
+           tcSimplify tyvars_to_gen dicts  `thenTc` \ (dicts_free, dict_binds, dicts_sig) ->
+           returnTc (dicts_free, tyvars_to_gen, dict_binds, 
+                     map instToId (bagToList dicts_sig))
 
-        other -> -- TYPE SIGNATURES PRESENT!
+       (TySigInfo _ _ theta _ _ : other) -> -- TYPE SIGNATURES PRESENT!
 
-               -- Check that all the signature contexts are identical
-               -- "tysig_dicts_s" is a list (one for each id declared
-               -- in this group) of lists of dicts (the list
-               -- corresponds to the context in the sig).
-               -- "dicts_sig" is just the first such list; we match
-               -- it against all the others.
+           tcAddErrCtxt (sigsCtxt tysig_vars) $
 
-           mapNF_Tc applyTcSubstToInsts tysig_dicts_s
-                               `thenNF_Tc` \ (dicts_sig : other_dicts_s) ->
-
-           checkTc (not (all (same_dicts dicts_sig) other_dicts_s))
-               -- The type signatures on a mutually-recursive group of definitions
-               -- must all have the same context (or none).  See Errors.lhs.
-               (sigContextsErr ty_sigs) `thenTc_`
+           newDicts SignatureOrigin theta      `thenNF_Tc` \ (dicts_sig, dict_ids) ->
 
                    -- Check that the needed dicts can be expressed in
                    -- terms of the signature ones
            tcSimplifyAndCheck
-               top_level
-               free_tyvars     -- Vars free in the environment
                tyvars_to_gen   -- Type vars over which we will quantify
                dicts_sig       -- Available dicts
                dicts           -- Want bindings for these dicts
-               (BindSigCtxt tysig_vars)
 
                                    `thenTc` \ (dicts_free, dict_binds) ->
 
-           returnTc (mkLIE dicts_free, tyvars_to_gen, dict_binds, dicts_sig)
+           returnTc (dicts_free, tyvars_to_gen, dict_binds, dict_ids)
   where
-    tysig_dicts_s = [dicts   | (TySigInfo _       _ dicts _ _) <- ty_sigs]
-    tysig_vars    = [sig_var | (TySigInfo sig_var _ _     _ _) <- ty_sigs] 
-
-       -- same_dicts checks that (post substitution) all the type signatures
-       -- constrain the same type variables in the same way
-    same_dicts []      []       = True
-    same_dicts []      _        = False
-    same_dicts _       []       = False
-    same_dicts (d1:d1s) (d2:d2s) = matchesInst d1 d2 && same_dicts d1s d2s
-
-    -- don't use the old version, because zipWith will truncate
-    -- the longer one!
-    --OLD: same_dicts dicts1 dicts2 = and (zipWith matchesInst dicts1 dicts2)
+    tysig_vars   = [sig_var | (TySigInfo sig_var _ _ _ _) <- ty_sigs]
 \end{code}
 
 @checkSigMatch@ does the next step in checking signature matching.
@@ -388,20 +282,12 @@ The error message here is somewhat unsatisfactory, but it'll do for
 now (ToDo).
 
 \begin{code}
-checkSigMatch :: [TyVar]       -- Free in environment
-             -> SignatureInfo
-             -> TcM [TyVar]
-
-checkSigMatch env_tyvars (TySigInfo name sig_tyvars _ tau_ty src_loc)
-  = let
-       inferred_ty = getIdUniType name
-    in
-    addSrcLocTc src_loc        (
-    checkSigTyVars env_tyvars sig_tyvars tau_ty inferred_ty
-                  (SigCtxt name tau_ty)
-    )
+checkSigMatch :: TcSigInfo s -> TcM s [TcTyVar s]
 
-checkSigMatch _ other_not_really_a_sig = returnTc []
+checkSigMatch (TySigInfo id sig_tyvars _ tau_ty src_loc)
+  = tcAddSrcLoc src_loc        $
+    tcAddErrCtxt (sigCtxt id) $
+    checkSigTyVars sig_tyvars tau_ty (idType id)
 \end{code}
 
 
@@ -414,22 +300,23 @@ checkSigMatch _ other_not_really_a_sig = returnTc []
 Not exported:
 
 \begin{code}
-isUnRestrictedGroup :: [Id]            -- Signatures given for these
-                    -> TypecheckedBind
-                    -> Bool
+isUnRestrictedGroup :: [TcIdBndr s]            -- Signatures given for these
+                   -> TcBind s
+                   -> Bool
 
 isUnRestrictedGroup sigs EmptyBind              = True
 isUnRestrictedGroup sigs (NonRecBind monobinds) = isUnResMono sigs monobinds
 isUnRestrictedGroup sigs (RecBind monobinds)    = isUnResMono sigs monobinds
 
-is_elem = isIn "isUnResMono"
+is_elem v vs = isIn "isUnResMono" v vs
 
-isUnResMono sigs EmptyMonoBinds = True
-isUnResMono sigs (AndMonoBinds mb1 mb2) = isUnResMono sigs mb1 && isUnResMono sigs mb2
-isUnResMono sigs (PatMonoBind (VarPat v) _ _)  = v `is_elem` sigs
-isUnResMono sigs (PatMonoBind other      _ _)  = False
-isUnResMono sigs (VarMonoBind v _)             = v `is_elem` sigs
-isUnResMono sigs (FunMonoBind _ _ _)           = True
+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}
 
 
@@ -441,7 +328,7 @@ isUnResMono sigs (FunMonoBind _ _ _)                = True
 
 @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 
+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]
@@ -456,51 +343,119 @@ are
                        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.
 
-It's {\em assumed} that the substitution has already been applied to the 
-environment type variables.
-
 \begin{code}
-checkSigTyVars :: [TyVar]      -- Tyvars free in environment; 
-                               -- fixed points of substitution
-              -> [TyVar]       -- The original signature type variables
-              -> UniType       -- signature type (for err msg)
-              -> UniType       -- inferred type (for err msg)
-              -> UnifyErrContext -- also for error msg
-              -> TcM [TyVar]   -- Post-substitution signature type variables
-
-checkSigTyVars env_tyvars sig_tyvars sig_tau inferred_tau err_ctxt
-  = getSrcLocTc                                        `thenNF_Tc` \ locn ->
-    applyTcSubstToTy inferred_tau              `thenNF_Tc` \ inferred_tau' ->
-    let
-       match_err = badMatchErr sig_tau inferred_tau' err_ctxt locn
-    in
-    applyTcSubstToTyVars sig_tyvars    `thenNF_Tc` \ sig_tys ->
-
-        -- Check point (a) above
-    checkMaybesTc (map getTyVarMaybe sig_tys) match_err        `thenTc` \ sig_tyvars' ->
+checkSigTyVars :: [TcTyVar s]          -- The original signature type variables
+              -> TcType s              -- signature type (for err msg)
+              -> TcType s              -- inferred type (for err msg)
+              -> TcM s [TcTyVar s]     -- Post-substitution signature type variables
+
+checkSigTyVars sig_tyvars sig_tau inferred_tau
+  = tcGetGlobalTyVars                  `thenNF_Tc` \ env_tyvars ->
+    checkSigTyVarsGivenGlobals env_tyvars sig_tyvars sig_tau inferred_tau
+
+checkSigTyVarsGivenGlobals
+        :: TcTyVarSet s        -- Consider these fully-zonked tyvars as global
+        -> [TcTyVar s]         -- The original signature type variables
+        -> TcType s            -- signature type (for err msg)
+        -> TcType s            -- inferred type (for err msg)
+        -> TcM s [TcTyVar s]   -- Post-substitution signature type variables
+
+checkSigTyVarsGivenGlobals globals sig_tyvars sig_tau inferred_tau
+  =     -- Check point (a) above
+    mapNF_Tc (zonkTcType.mkTyVarTy) sig_tyvars                         `thenNF_Tc` \ sig_tys ->
+    checkMaybeTcM (allMaybes (map getTyVar_maybe sig_tys)) match_err   `thenTc` \ sig_tyvars' ->
 
         -- Check point (b)
-    checkTc (not (hasNoDups sig_tyvars')) match_err    `thenTc_`
+    checkTcM (hasNoDups sig_tyvars') match_err         `thenTc_`
 
        -- Check point (c)
-       -- We want to report errors in terms of the original signature tyvars, 
+       -- 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.
     let
-       is_elem = isIn "checkSigTyVars"
-
-       mono_tyvars = [ sig_tyvar 
+       mono_tyvars = [ sig_tyvar
                      | (sig_tyvar,sig_tyvar') <- zipEqual sig_tyvars sig_tyvars',
-                       sig_tyvar' `is_elem` env_tyvars
+                       sig_tyvar' `elementOfTyVarSet` globals
                      ]
     in
-    checkTc (not (null mono_tyvars))
-           (notAsPolyAsSigErr sig_tau mono_tyvars err_ctxt locn) `thenTc_`
+    checkTc (null mono_tyvars)
+           (notAsPolyAsSigErr sig_tau mono_tyvars)     `thenTc_`
 
     returnTc sig_tyvars'
+  where
+    match_err = zonkTcType inferred_tau        `thenNF_Tc` \ inferred_tau' ->
+               failTc (badMatchErr sig_tau inferred_tau')
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+\subsection[GenEtc-SpecTy]{Instantiate a type and create new dicts for it}
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+specTy :: InstOrigin s
+       -> Type
+       -> NF_TcM s ([TcTyVar s], LIE s, TcType s, [TcIdOcc s])
+
+specTy origin sigma_ty
+  = tcInstType [] sigma_ty             `thenNF_Tc` \ tc_sigma_ty ->
+    let
+       (tyvars, theta, tau) = splitSigmaTy tc_sigma_ty
+    in
+        -- Instantiate the dictionary types
+    newDicts origin theta              `thenNF_Tc` \ (dicts, dict_ids) ->
+
+        -- Return the list of tyvars, the list of dicts and the tau type
+    returnNF_Tc (tyvars, dicts, tau, dict_ids)
+\end{code}
+
+
+
+Contexts and errors
+~~~~~~~~~~~~~~~~~~~
+\begin{code}
+notAsPolyAsSigErr sig_tau mono_tyvars sty
+  = ppHang (ppStr "A type signature is more polymorphic than the inferred type")
+       4  (ppAboves [ppStr "(That is, one or more type variables in the inferred type can't be forall'd.)",
+                     ppHang (ppStr "Monomorphic type variable(s):")
+                          4 (interpp'SP sty mono_tyvars),
+                     ppStr "Possible cause: the RHS mentions something subject to the monomorphism restriction"
+                    ])
+\end{code}
+
+
+\begin{code}
+badMatchErr sig_ty inferred_ty sty
+  = ppHang (ppStr "Type signature doesn't match inferred type") 
+        4 (ppAboves [ppHang (ppStr "Signature:") 4 (ppr sty sig_ty),
+                     ppHang (ppStr "Inferred :") 4 (ppr sty inferred_ty)
+          ])
+
+sigCtxt id sty 
+  = ppSep [ppStr "When checking signature for", ppr sty id]
+sigsCtxt ids sty 
+  = ppSep [ppStr "When checking signature(s) for:", interpp'SP sty ids]
+\end{code}
+
+
+\begin{code}
+sigContextsErr ty_sigs sty
+  = ppHang (ppStr "A group of type signatures have mismatched contexts")
+        4 (ppAboves (map ppr_sig_info ty_sigs))
+  where
+    ppr_sig_info (TySigInfo val tyvars theta tau_ty _)
+      = ppHang (ppBeside (ppr sty val) (ppStr " :: "))
+            4 (if null theta
+               then ppNil
+               else ppBesides [ppStr "(", 
+                               ppIntersperse (ppStr ", ") (map (ppr_inst sty) theta), 
+                               ppStr ") => ..."])
+    ppr_inst sty (clas, ty) = ppCat [ppr sty clas, ppr sty ty]
 \end{code}