[project @ 2003-06-20 11:14:18 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index 98e5b70..999d390 100644 (file)
@@ -10,6 +10,7 @@ module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,
        tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
+       tcSimplifyBracket,
 
        tcSimplifyDeriv, tcSimplifyDefault,
        bindInstsOfLocalFuns
@@ -18,49 +19,51 @@ module TcSimplify (
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TcUnify( unifyTauTy )
-
+import TcEnv           -- temp
 import HsSyn           ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
 import TcHsSyn         ( TcExpr, TcId,
                          TcMonoBinds, TcDictBinds
                        )
 
-import TcMonad
+import TcRnMonad
 import Inst            ( lookupInst, LookupInstResult(..),
-                         tyVarsOfInst, predsOfInsts, predsOfInst, newDicts,
+                         tyVarsOfInst, fdPredsOfInsts, fdPredsOfInst, newDicts,
                          isDict, isClassDict, isLinearInst, linearInstType,
                          isStdClassTyVarDict, isMethodFor, isMethod,
                          instToId, tyVarsOfInsts,  cloneDict,
                          ipNamesOfInsts, ipNamesOfInst, dictPred,
                          instBindingRequired, instCanBeGeneralised,
-                         newDictsFromOld, newMethodAtLoc,
+                         newDictsFromOld, tcInstClassOp,
                          getDictClassTys, isTyVarDict,
-                         instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
-                         Inst, LIE, pprInsts, pprInstsInFull,
-                         mkLIE, lieToList
+                         instLoc, zonkInst, tidyInsts, tidyMoreInsts,
+                         Inst, pprInsts, pprInstsInFull,
+                         isIPDict, isInheritableInst
                        )
-import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv, tcLookupGlobalId )
+import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv, tcLookupId, findGlobals )
 import InstEnv         ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
 import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
 import TcType          ( TcTyVar, TcTyVarSet, ThetaType, TyVarDetails(VanillaTv),
                          mkClassPred, isOverloadedTy, mkTyConApp,
                          mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
-                         tyVarsOfPred, isIPPred, isInheritablePred, predHasFDs )
+                         tyVarsOfPred )
 import Id              ( idType, mkUserLocal )
 import Var             ( TyVar )
 import Name            ( getOccName, getSrcLoc )
 import NameSet         ( NameSet, mkNameSet, elemNameSet )
 import Class           ( classBigSig )
 import FunDeps         ( oclose, grow, improve, pprEquationDoc )
-import PrelInfo                ( isNumericClass, isCreturnableClass, isCcallishClass, 
-                         splitName, fstName, sndName )
+import PrelInfo                ( isNumericClass, isCreturnableClass, isCcallishClass ) 
+import PrelNames       ( splitName, fstName, sndName )
 
 import Subst           ( mkTopTyVarSubst, substTheta, substTy )
 import TysWiredIn      ( unitTy, pairTyCon )
+import ErrUtils                ( Message )
 import VarSet
+import VarEnv          ( TidyEnv )
 import FiniteMap
 import Outputable
 import ListSetOps      ( equivClasses )
-import Util            ( zipEqual )
+import Util            ( zipEqual, isSingleton )
 import List            ( partition )
 import CmdLineOpts
 \end{code}
@@ -533,31 +536,32 @@ again.
 tcSimplifyInfer
        :: SDoc
        -> TcTyVarSet           -- fv(T); type vars
-       -> LIE                  -- Wanted
+       -> [Inst]               -- Wanted
        -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
-               LIE,            -- Free
                TcDictBinds,    -- Bindings
                [TcId])         -- Dict Ids that must be bound here (zonked)
+       -- Any free (escaping) Insts are tossed into the environment
 \end{code}
 
 
 \begin{code}
 tcSimplifyInfer doc tau_tvs wanted_lie
   = inferLoop doc (varSetElems tau_tvs)
-             (lieToList wanted_lie)    `thenTc` \ (qtvs, frees, binds, irreds) ->
+             wanted_lie                `thenM` \ (qtvs, frees, binds, irreds) ->
 
        -- Check for non-generalisable insts
-    mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds)  `thenTc_`
+    mappM_ addCantGenErr (filter (not . instCanBeGeneralised) irreds)  `thenM_`
 
-    returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
+    extendLIEs frees                                                   `thenM_`
+    returnM (qtvs, binds, map instToId irreds)
 
 inferLoop doc tau_tvs wanteds
   =    -- Step 1
-    zonkTcTyVarsAndFV tau_tvs          `thenNF_Tc` \ tau_tvs' ->
-    mapNF_Tc zonkInst wanteds          `thenNF_Tc` \ wanteds' ->
-    tcGetGlobalTyVars                  `thenNF_Tc` \ gbl_tvs ->
+    zonkTcTyVarsAndFV tau_tvs          `thenM` \ tau_tvs' ->
+    mappM zonkInst wanteds             `thenM` \ wanteds' ->
+    tcGetGlobalTyVars                  `thenM` \ gbl_tvs ->
     let
-       preds = predsOfInsts wanteds'
+       preds = fdPredsOfInsts wanteds'
        qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
 
        try_me inst
@@ -565,12 +569,13 @@ inferLoop doc tau_tvs wanteds
          | isClassDict inst              = DontReduceUnlessConstant    -- Dicts
          | otherwise                     = ReduceMe                    -- Lits and Methods
     in
+    traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds, ppr (grow preds tau_tvs'), ppr qtvs])     `thenM_`
                -- Step 2
-    reduceContext doc try_me [] wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
+    reduceContext doc try_me [] wanteds'    `thenM` \ (no_improvement, frees, binds, irreds) ->
 
                -- Step 3
     if no_improvement then
-       returnTc (varSetElems qtvs, frees, binds, irreds)
+       returnM (varSetElems qtvs, frees, binds, irreds)
     else
        -- If improvement did some unification, we go round again.  There
        -- are two subtleties:
@@ -587,8 +592,8 @@ inferLoop doc tau_tvs wanteds
        -- However, NOTICE that when we are done, we might have some bindings, but
        -- the final qtvs might be empty.  See [NO TYVARS] below.
                                
-       inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
-       returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
+       inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
+       returnM (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
 \end{code}
 
 Example [LOOP]
@@ -634,9 +639,9 @@ The net effect of [NO TYVARS]
 \begin{code}
 isFreeWhenInferring :: TyVarSet -> Inst        -> Bool
 isFreeWhenInferring qtvs inst
-  =  isFreeWrtTyVars qtvs inst                 -- Constrains no quantified vars
-  && all isInheritablePred (predsOfInst inst)  -- And no implicit parameter involved
-                                               -- (see "Notes on implicit parameters")
+  =  isFreeWrtTyVars qtvs inst         -- Constrains no quantified vars
+  && isInheritableInst inst            -- And no implicit parameter involved
+                                       -- (see "Notes on implicit parameters")
 
 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
                   -> NameSet   -- Quantified implicit parameters
@@ -664,24 +669,19 @@ tcSimplifyCheck
         :: SDoc
         -> [TcTyVar]           -- Quantify over these
         -> [Inst]              -- Given
-        -> LIE                 -- Wanted
-        -> TcM (LIE,           -- Free
-                TcDictBinds)   -- Bindings
+        -> [Inst]              -- Wanted
+        -> TcM TcDictBinds     -- Bindings
 
 -- tcSimplifyCheck is used when checking expression type signatures,
 -- class decls, instance decls etc.
 --
--- NB: we psss isFree (not isFreeAndInheritable) to tcSimplCheck
--- It's important that we can float out non-inheritable predicates
--- Example:            (?x :: Int) is ok!
---
 -- NB: tcSimplifyCheck does not consult the
 --     global type variables in the environment; so you don't
 --     need to worry about setting them before calling tcSimplifyCheck
 tcSimplifyCheck doc qtvs givens wanted_lie
   = tcSimplCheck doc get_qtvs
-                givens wanted_lie      `thenTc` \ (qtvs', frees, binds) ->
-    returnTc (frees, binds)
+                givens wanted_lie      `thenM` \ (qtvs', binds) ->
+    returnM binds
   where
     get_qtvs = zonkTcTyVarsAndFV qtvs
 
@@ -693,9 +693,8 @@ tcSimplifyInferCheck
         :: SDoc
         -> TcTyVarSet          -- fv(T)
         -> [Inst]              -- Given
-        -> LIE                 -- Wanted
+        -> [Inst]              -- Wanted
         -> TcM ([TcTyVar],     -- Variables over which to quantify
-                LIE,           -- Free
                 TcDictBinds)   -- Bindings
 
 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
@@ -712,37 +711,38 @@ tcSimplifyInferCheck doc tau_tvs givens wanted_lie
        -- f isn't quantified over b.
     all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
 
-    get_qtvs = zonkTcTyVarsAndFV all_tvs       `thenNF_Tc` \ all_tvs' ->
-              tcGetGlobalTyVars                `thenNF_Tc` \ gbl_tvs ->
+    get_qtvs = zonkTcTyVarsAndFV all_tvs       `thenM` \ all_tvs' ->
+              tcGetGlobalTyVars                `thenM` \ gbl_tvs ->
               let
                  qtvs = all_tvs' `minusVarSet` gbl_tvs
                        -- We could close gbl_tvs, but its not necessary for
                        -- soundness, and it'll only affect which tyvars, not which
                        -- dictionaries, we quantify over
               in
-              returnNF_Tc qtvs
+              returnM qtvs
 \end{code}
 
 Here is the workhorse function for all three wrappers.
 
 \begin{code}
 tcSimplCheck doc get_qtvs givens wanted_lie
-  = check_loop givens (lieToList wanted_lie)   `thenTc` \ (qtvs, frees, binds, irreds) ->
+  = check_loop givens wanted_lie       `thenM` \ (qtvs, frees, binds, irreds) ->
 
        -- Complain about any irreducible ones
-    complainCheck doc givens irreds            `thenNF_Tc_`
+    complainCheck doc givens irreds            `thenM_`
 
        -- Done
-    returnTc (qtvs, mkLIE frees, binds)
+    extendLIEs frees                           `thenM_`
+    returnM (qtvs, binds)
 
   where
     ip_set = mkNameSet (ipNamesOfInsts givens)
 
     check_loop givens wanteds
       =                -- Step 1
-       mapNF_Tc zonkInst givens        `thenNF_Tc` \ givens' ->
-       mapNF_Tc zonkInst wanteds       `thenNF_Tc` \ wanteds' ->
-       get_qtvs                        `thenNF_Tc` \ qtvs' ->
+       mappM zonkInst givens   `thenM` \ givens' ->
+       mappM zonkInst wanteds  `thenM` \ wanteds' ->
+       get_qtvs                `thenM` \ qtvs' ->
 
                    -- Step 2
        let
@@ -751,14 +751,14 @@ tcSimplCheck doc get_qtvs givens wanted_lie
            try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
                        | otherwise                            = ReduceMe
        in
-       reduceContext doc try_me givens' wanteds'       `thenTc` \ (no_improvement, frees, binds, irreds) ->
+       reduceContext doc try_me givens' wanteds'       `thenM` \ (no_improvement, frees, binds, irreds) ->
 
                    -- Step 3
        if no_improvement then
-           returnTc (varSetElems qtvs', frees, binds, irreds)
+           returnM (varSetElems qtvs', frees, binds, irreds)
        else
-           check_loop givens' (irreds ++ frees)        `thenTc` \ (qtvs', frees1, binds1, irreds1) ->
-           returnTc (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
+           check_loop givens' (irreds ++ frees)        `thenM` \ (qtvs', frees1, binds1, irreds1) ->
+           returnM (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
 \end{code}
 
 
@@ -773,12 +773,11 @@ tcSimplifyRestricted      -- Used for restricted binding groups
                        -- i.e. ones subject to the monomorphism restriction
        :: SDoc
        -> TcTyVarSet           -- Free in the type of the RHSs
-       -> LIE                  -- Free in the RHSs
+       -> [Inst]               -- Free in the RHSs
        -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
-               LIE,            -- Free
                TcDictBinds)    -- Bindings
 
-tcSimplifyRestricted doc tau_tvs wanted_lie
+tcSimplifyRestricted doc tau_tvs wanteds
   =    -- First squash out all methods, to find the constrained tyvars
        -- We can't just take the free vars of wanted_lie because that'll
        -- have methods that may incidentally mention entirely unconstrained variables
@@ -787,24 +786,26 @@ tcSimplifyRestricted doc tau_tvs wanted_lie
        --      foo = f (3::Int)
        -- We want to infer the polymorphic type
        --      foo :: forall b. b -> b
-    let
-       wanteds = lieToList wanted_lie
-       try_me inst = ReduceMe          -- Reduce as far as we can.  Don't stop at
-                                       -- dicts; the idea is to get rid of as many type
-                                       -- variables as possible, and we don't want to stop
-                                       -- at (say) Monad (ST s), because that reduces
-                                       -- immediately, with no constraint on s.
-    in
-    simpleReduceLoop doc try_me wanteds                `thenTc` \ (_, _, constrained_dicts) ->
+
+       -- 'reduceMe': Reduce as far as we can.  Don't stop at
+       -- dicts; the idea is to get rid of as many type
+       -- variables as possible, and we don't want to stop
+       -- at (say) Monad (ST s), because that reduces
+       -- immediately, with no constraint on s.
+    simpleReduceLoop doc reduceMe wanteds      `thenM` \ (foo_frees, foo_binds, constrained_dicts) ->
 
        -- Next, figure out the tyvars we will quantify over
-    zonkTcTyVarsAndFV (varSetElems tau_tvs)    `thenNF_Tc` \ tau_tvs' ->
-    tcGetGlobalTyVars                          `thenNF_Tc` \ gbl_tvs ->
+    zonkTcTyVarsAndFV (varSetElems tau_tvs)    `thenM` \ tau_tvs' ->
+    tcGetGlobalTyVars                          `thenM` \ gbl_tvs ->
     let
        constrained_tvs = tyVarsOfInsts constrained_dicts
-       qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts constrained_dicts) gbl_tvs)
+       qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs)
                         `minusVarSet` constrained_tvs
     in
+    traceTc (text "tcSimplifyRestricted" <+> vcat [
+               pprInsts wanteds, pprInsts foo_frees, pprInsts constrained_dicts,
+               ppr foo_binds,
+               ppr constrained_tvs, ppr tau_tvs', ppr qtvs ])  `thenM_`
 
        -- The first step may have squashed more methods than
        -- necessary, so try again, this time knowing the exact
@@ -819,18 +820,28 @@ tcSimplifyRestricted doc tau_tvs wanted_lie
        -- Remember that we may need to do *some* simplification, to
        -- (for example) squash {Monad (ST s)} into {}.  It's not enough
        -- just to float all constraints
-    mapNF_Tc zonkInst (lieToList wanted_lie)   `thenNF_Tc` \ wanteds' ->
+    restrict_loop doc qtvs wanteds
+       -- We still need a loop because improvement can take place
+       -- E.g. if we have (C (T a)) and the instance decl
+       --      instance D Int b => C (T a) where ...
+       -- and there's a functional dependency for D.   Then we may improve
+       -- the tyep variable 'b'.
+
+restrict_loop doc qtvs wanteds
+  = mappM zonkInst wanteds                     `thenM` \ wanteds' ->
+    zonkTcTyVarsAndFV (varSetElems qtvs)       `thenM` \ qtvs' ->
     let
-        try_me inst | isFreeWrtTyVars qtvs inst = Free
-                   | otherwise                 = ReduceMe
+        try_me inst | isFreeWrtTyVars qtvs' inst = Free
+                   | otherwise                  = ReduceMe
     in
-    reduceContext doc try_me [] wanteds'       `thenTc` \ (no_improvement, frees, binds, irreds) ->
-    ASSERT( no_improvement )
-    ASSERT( null irreds )
-       -- No need to loop because simpleReduceLoop will have
-       -- already done any improvement necessary
-
-    returnTc (varSetElems qtvs, mkLIE frees, binds)
+    reduceContext doc try_me [] wanteds'       `thenM` \ (no_improvement, frees, binds, irreds) ->
+    if no_improvement then
+       ASSERT( null irreds )
+       extendLIEs frees                        `thenM_`
+       returnM (varSetElems qtvs', binds)
+    else
+       restrict_loop doc qtvs' (irreds ++ frees)       `thenM` \ (qtvs1, binds1) ->
+       returnM (qtvs1, binds `AndMonoBinds` binds1)
 \end{code}
 
 
@@ -880,17 +891,17 @@ because the scsel will mess up matching.  Instead we want
 Hence "DontReduce NoSCs"
 
 \begin{code}
-tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
-tcSimplifyToDicts wanted_lie
-  = simpleReduceLoop doc try_me wanteds                `thenTc` \ (frees, binds, irreds) ->
+tcSimplifyToDicts :: [Inst] -> TcM (TcDictBinds)
+tcSimplifyToDicts wanteds
+  = simpleReduceLoop doc try_me wanteds                `thenM` \ (frees, binds, irreds) ->
        -- Since try_me doesn't look at types, we don't need to
        -- do any zonking, so it's safe to call reduceContext directly
     ASSERT( null frees )
-    returnTc (irreds, binds)
+    extendLIEs irreds          `thenM_`
+    returnM binds
 
   where
     doc = text "tcSimplifyToDicts"
-    wanteds = lieToList wanted_lie
 
        -- Reduce methods and lits only; stop as soon as we get a dictionary
     try_me inst        | isDict inst = DontReduce NoSCs
@@ -898,6 +909,24 @@ tcSimplifyToDicts wanted_lie
 \end{code}
 
 
+
+tcSimplifyBracket is used when simplifying the constraints arising from
+a Template Haskell bracket [| ... |].  We want to check that there aren't
+any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
+Show instance), but we aren't otherwise interested in the results.
+Nor do we care about ambiguous dictionaries etc.  We will type check
+this bracket again at its usage site.
+
+\begin{code}
+tcSimplifyBracket :: [Inst] -> TcM ()
+tcSimplifyBracket wanteds
+  = simpleReduceLoop doc reduceMe wanteds      `thenM_`
+    returnM ()
+  where
+    doc = text "tcSimplifyBracket"
+\end{code}
+
+
 %************************************************************************
 %*                                                                     *
 \subsection{Filtering at a dynamic binding}
@@ -920,14 +949,14 @@ force the binding for ?x to be of type Int.
 
 \begin{code}
 tcSimplifyIPs :: [Inst]                -- The implicit parameters bound here
-             -> LIE
-             -> TcM (LIE, TcDictBinds)
-tcSimplifyIPs given_ips wanted_lie
-  = simpl_loop given_ips wanteds       `thenTc` \ (frees, binds) ->
-    returnTc (mkLIE frees, binds)
+             -> [Inst]         -- Wanted
+             -> TcM TcDictBinds
+tcSimplifyIPs given_ips wanteds
+  = simpl_loop given_ips wanteds       `thenM` \ (frees, binds) ->
+    extendLIEs frees                   `thenM_`
+    returnM binds
   where
     doc             = text "tcSimplifyIPs" <+> ppr given_ips
-    wanteds  = lieToList wanted_lie
     ip_set   = mkNameSet (ipNamesOfInsts given_ips)
 
        -- Simplify any methods that mention the implicit parameter
@@ -935,17 +964,17 @@ tcSimplifyIPs given_ips wanted_lie
                | otherwise                = ReduceMe
 
     simpl_loop givens wanteds
-      = mapNF_Tc zonkInst givens               `thenNF_Tc` \ givens' ->
-        mapNF_Tc zonkInst wanteds              `thenNF_Tc` \ wanteds' ->
+      = mappM zonkInst givens          `thenM` \ givens' ->
+        mappM zonkInst wanteds         `thenM` \ wanteds' ->
 
-        reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
+        reduceContext doc try_me givens' wanteds'    `thenM` \ (no_improvement, frees, binds, irreds) ->
 
         if no_improvement then
            ASSERT( null irreds )
-           returnTc (frees, binds)
+           returnM (frees, binds)
        else
-           simpl_loop givens' (irreds ++ frees)        `thenTc` \ (frees1, binds1) ->
-           returnTc (frees1, binds `AndMonoBinds` binds1)
+           simpl_loop givens' (irreds ++ frees)        `thenM` \ (frees1, binds1) ->
+           returnM (frees1, binds `AndMonoBinds` binds1)
 \end{code}
 
 
@@ -975,20 +1004,21 @@ For each method @Inst@ in the @init_lie@ that mentions one of the
 @LIE@), as well as the @HsBinds@ generated.
 
 \begin{code}
-bindInstsOfLocalFuns ::        LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
+bindInstsOfLocalFuns ::        [Inst] -> [TcId] -> TcM TcMonoBinds
 
-bindInstsOfLocalFuns init_lie local_ids
+bindInstsOfLocalFuns wanteds local_ids
   | null overloaded_ids
        -- Common case
-  = returnTc (init_lie, EmptyMonoBinds)
+  = extendLIEs wanteds         `thenM_`
+    returnM EmptyMonoBinds
 
   | otherwise
-  = simpleReduceLoop doc try_me wanteds                `thenTc` \ (frees, binds, irreds) ->
+  = simpleReduceLoop doc try_me wanteds                `thenM` \ (frees, binds, irreds) ->
     ASSERT( null irreds )
-    returnTc (mkLIE frees, binds)
+    extendLIEs frees           `thenM_`
+    returnM binds
   where
     doc                     = text "bindInsts" <+> ppr local_ids
-    wanteds         = lieToList init_lie
     overloaded_ids   = filter is_overloaded local_ids
     is_overloaded id = isOverloadedTy (idType id)
 
@@ -1089,7 +1119,7 @@ The loop startes
 \begin{code}
 extractResults :: Avails
               -> [Inst]                -- Wanted
-              -> NF_TcM (TcDictBinds,  -- Bindings
+              -> TcM (TcDictBinds,     -- Bindings
                          [Inst],       -- Irreducible ones
                          [Inst])       -- Free ones
 
@@ -1097,7 +1127,7 @@ extractResults avails wanteds
   = go avails EmptyMonoBinds [] [] wanteds
   where
     go avails binds irreds frees [] 
-      = returnNF_Tc (binds, irreds, frees)
+      = returnM (binds, irreds, frees)
 
     go avails binds irreds frees (w:ws)
       = case lookupFM avails w of
@@ -1120,8 +1150,8 @@ extractResults avails wanteds
                                new_binds = addBind binds w rhs
 
          Just (Linear n split_inst avail)      -- Transform Linear --> LinRhss
-           -> get_root irreds frees avail w            `thenNF_Tc` \ (irreds', frees', root_id) ->
-              split n (instToId split_inst) root_id w  `thenNF_Tc` \ (binds', rhss) ->
+           -> get_root irreds frees avail w            `thenM` \ (irreds', frees', root_id) ->
+              split n (instToId split_inst) root_id w  `thenM` \ (binds', rhss) ->
               go (addToFM avails w (LinRhss rhss))
                  (binds `AndMonoBinds` binds')
                  irreds' frees' (split_inst : w : ws)
@@ -1132,11 +1162,11 @@ extractResults avails wanteds
                   new_binds  = addBind binds w rhs
                   new_avails = addToFM avails w (LinRhss rhss)
 
-    get_root irreds frees (Given id _) w = returnNF_Tc (irreds, frees, id)
-    get_root irreds frees Irred               w = cloneDict w  `thenNF_Tc` \ w' ->
-                                          returnNF_Tc (w':irreds, frees, instToId w')
-    get_root irreds frees IsFree       w = cloneDict w `thenNF_Tc` \ w' ->
-                                          returnNF_Tc (irreds, w':frees, instToId w')
+    get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
+    get_root irreds frees Irred               w = cloneDict w  `thenM` \ w' ->
+                                          returnM (w':irreds, frees, instToId w')
+    get_root irreds frees IsFree       w = cloneDict w `thenM` \ w' ->
+                                          returnM (irreds, w':frees, instToId w')
 
     add_given avails w 
        | instBindingRequired w = addToFM avails w (Given (instToId w) True)
@@ -1165,7 +1195,7 @@ extractResults avails wanteds
 
 
 split :: Int -> TcId -> TcId -> Inst 
-      -> NF_TcM (TcDictBinds, [TcExpr])
+      -> TcM (TcDictBinds, [TcExpr])
 -- (split n split_id root_id wanted) returns
 --     * a list of 'n' expressions, all of which witness 'avail'
 --     * a bunch of auxiliary bindings to support these expressions
@@ -1183,11 +1213,11 @@ split n split_id root_id wanted
     occ     = getOccName id
     loc     = getSrcLoc id
 
-    go 1 = returnNF_Tc (EmptyMonoBinds, [HsVar root_id])
+    go 1 = returnM (EmptyMonoBinds, [HsVar root_id])
 
-    go n = go ((n+1) `div` 2)          `thenNF_Tc` \ (binds1, rhss) ->
-          expand n rhss                `thenNF_Tc` \ (binds2, rhss') ->
-          returnNF_Tc (binds1 `AndMonoBinds` binds2, rhss')
+    go n = go ((n+1) `div` 2)          `thenM` \ (binds1, rhss) ->
+          expand n rhss                `thenM` \ (binds2, rhss') ->
+          returnM (binds1 `AndMonoBinds` binds2, rhss')
 
        -- (expand n rhss) 
        -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
@@ -1196,19 +1226,19 @@ split n split_id root_id wanted
        --            [fst x, snd x, rhs2] )
     expand n rhss
        | n `rem` 2 == 0 = go rhss      -- n is even
-       | otherwise      = go (tail rhss)       `thenNF_Tc` \ (binds', rhss') ->
-                          returnNF_Tc (binds', head rhss : rhss')
+       | otherwise      = go (tail rhss)       `thenM` \ (binds', rhss') ->
+                          returnM (binds', head rhss : rhss')
        where
-         go rhss = mapAndUnzipNF_Tc do_one rhss        `thenNF_Tc` \ (binds', rhss') ->
-                   returnNF_Tc (andMonoBindList binds', concat rhss')
+         go rhss = mapAndUnzipM do_one rhss    `thenM` \ (binds', rhss') ->
+                   returnM (andMonoBindList binds', concat rhss')
 
-         do_one rhs = tcGetUnique                      `thenNF_Tc` \ uniq -> 
-                      tcLookupGlobalId fstName         `thenNF_Tc` \ fst_id ->
-                      tcLookupGlobalId sndName         `thenNF_Tc` \ snd_id ->
+         do_one rhs = newUnique                        `thenM` \ uniq -> 
+                      tcLookupId fstName               `thenM` \ fst_id ->
+                      tcLookupId sndName               `thenM` \ snd_id ->
                       let 
                          x = mkUserLocal occ uniq pair_ty loc
                       in
-                      returnNF_Tc (VarMonoBind x (mk_app split_id rhs),
+                      returnM (VarMonoBind x (mk_app split_id rhs),
                                    [mk_fs_app fst_id ty x, mk_fs_app snd_id ty x])
 
 mk_fs_app id ty var = HsVar id `TyApp` [ty,ty] `HsApp` HsVar var
@@ -1240,13 +1270,13 @@ simpleReduceLoop :: SDoc
                         [Inst])                -- Irreducible
 
 simpleReduceLoop doc try_me wanteds
-  = mapNF_Tc zonkInst wanteds                  `thenNF_Tc` \ wanteds' ->
-    reduceContext doc try_me [] wanteds'       `thenTc` \ (no_improvement, frees, binds, irreds) ->
+  = mappM zonkInst wanteds                     `thenM` \ wanteds' ->
+    reduceContext doc try_me [] wanteds'       `thenM` \ (no_improvement, frees, binds, irreds) ->
     if no_improvement then
-       returnTc (frees, binds, irreds)
+       returnM (frees, binds, irreds)
     else
-       simpleReduceLoop doc try_me (irreds ++ frees)   `thenTc` \ (frees1, binds1, irreds1) ->
-       returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
+       simpleReduceLoop doc try_me (irreds ++ frees)   `thenM` \ (frees1, binds1, irreds1) ->
+       returnM (frees1, binds `AndMonoBinds` binds1, irreds1)
 \end{code}
 
 
@@ -1256,7 +1286,7 @@ reduceContext :: SDoc
              -> (Inst -> WhatToDo)
              -> [Inst]                 -- Given
              -> [Inst]                 -- Wanted
-             -> NF_TcM (Bool,          -- True <=> improve step did no unification
+             -> TcM (Bool,             -- True <=> improve step did no unification
                         [Inst],        -- Free
                         TcDictBinds,   -- Dictionary bindings
                         [Inst])        -- Irreducible
@@ -1269,19 +1299,19 @@ reduceContext doc try_me givens wanteds
             text "given" <+> ppr givens,
             text "wanted" <+> ppr wanteds,
             text "----------------------"
-            ]))                                        `thenNF_Tc_`
+            ]))                                        `thenM_`
 
         -- Build the Avail mapping from "givens"
-    foldlNF_Tc addGiven emptyFM givens                 `thenNF_Tc` \ init_state ->
+    foldlM addGiven emptyFM givens                     `thenM` \ init_state ->
 
         -- Do the real work
-    reduceList (0,[]) try_me wanteds init_state                `thenNF_Tc` \ avails ->
+    reduceList (0,[]) try_me wanteds init_state                `thenM` \ avails ->
 
        -- Do improvement, using everything in avails
        -- In particular, avails includes all superclasses of everything
-    tcImprove avails                                   `thenTc` \ no_improvement ->
+    tcImprove avails                                   `thenM` \ no_improvement ->
 
-    extractResults avails wanteds                      `thenNF_Tc` \ (binds, irreds, frees) ->
+    extractResults avails wanteds                      `thenM` \ (binds, irreds, frees) ->
 
     traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
@@ -1293,18 +1323,17 @@ reduceContext doc try_me givens wanteds
             text "frees" <+> ppr frees,
             text "no_improvement =" <+> ppr no_improvement,
             text "----------------------"
-            ]))                                        `thenNF_Tc_`
+            ]))                                        `thenM_`
 
-    returnTc (no_improvement, frees, binds, irreds)
+    returnM (no_improvement, frees, binds, irreds)
 
 tcImprove avails
- =  tcGetInstEnv                               `thenTc` \ inst_env ->
+ =  tcGetInstEnv                               `thenM` \ inst_env ->
     let
        preds = [ (pred, pp_loc)
                | inst <- keysFM avails,
                  let pp_loc = pprInstLoc (instLoc inst),
-                 pred <- predsOfInst inst,
-                 predHasFDs pred
+                 pred <- fdPredsOfInst inst
                ]
                -- Avails has all the superclasses etc (good)
                -- It also has all the intermediates of the deduction (good)
@@ -1314,15 +1343,15 @@ tcImprove avails
        eqns  = improve (classInstEnv inst_env) preds
      in
      if null eqns then
-       returnTc True
+       returnM True
      else
-       traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))     `thenNF_Tc_`
-        mapTc_ unify eqns      `thenTc_`
-       returnTc False
+       traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))     `thenM_`
+        mappM_ unify eqns      `thenM_`
+       returnM False
   where
     unify ((qtvs, t1, t2), doc)
-        = tcAddErrCtxt doc                             $
-          tcInstTyVars VanillaTv (varSetElems qtvs)    `thenNF_Tc` \ (_, _, tenv) ->
+        = addErrCtxt doc                               $
+          tcInstTyVars VanillaTv (varSetElems qtvs)    `thenM` \ (_, _, tenv) ->
           unifyTauTy (substTy tenv t1) (substTy tenv t2)
 \end{code}
 
@@ -1368,8 +1397,8 @@ reduceList (n,stack) try_me wanteds state
 #endif
     go wanteds state
   where
-    go []     state = returnTc state
-    go (w:ws) state = reduce (n+1, w:stack) try_me w state     `thenTc` \ state' ->
+    go []     state = returnM state
+    go (w:ws) state = reduce (n+1, w:stack) try_me w state     `thenM` \ state' ->
                      go ws state'
 
     -- Base case: we're done!
@@ -1377,10 +1406,10 @@ reduce stack try_me wanted state
     -- It's the same as an existing inst, or a superclass thereof
   | Just avail <- isAvailable state wanted
   = if isLinearInst wanted then
-       addLinearAvailable state avail wanted   `thenNF_Tc` \ (state', wanteds') ->
+       addLinearAvailable state avail wanted   `thenM` \ (state', wanteds') ->
        reduceList stack try_me wanteds' state'
     else
-       returnTc state          -- No op for non-linear things
+       returnM state           -- No op for non-linear things
 
   | otherwise
   = case try_me wanted of {
@@ -1396,9 +1425,9 @@ reduce stack try_me wanted state
        try_simple addFree
 
     ; ReduceMe ->              -- It should be reduced
-       lookupInst wanted             `thenNF_Tc` \ lookup_result ->
+       lookupInst wanted             `thenM` \ lookup_result ->
        case lookup_result of
-           GenInst wanteds' rhs -> reduceList stack try_me wanteds' state      `thenTc` \ state' ->
+           GenInst wanteds' rhs -> reduceList stack try_me wanteds' state      `thenM` \ state' ->
                                    addWanted state' wanted rhs wanteds'
            SimpleInst rhs       -> addWanted state wanted rhs []
 
@@ -1409,7 +1438,7 @@ reduce stack try_me wanted state
     }
   where
     try_simple do_this_otherwise
-      = lookupInst wanted        `thenNF_Tc` \ lookup_result ->
+      = lookupInst wanted        `thenM` \ lookup_result ->
        case lookup_result of
            SimpleInst rhs -> addWanted state wanted rhs []
            other          -> do_this_otherwise state wanted
@@ -1424,19 +1453,19 @@ isAvailable avails wanted = lookupFM avails wanted
        -- *not* by unique.  So
        --      d1::C Int ==  d2::C Int
 
-addLinearAvailable :: Avails -> Avail -> Inst -> NF_TcM (Avails, [Inst])
+addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
 addLinearAvailable avails avail wanted
        -- avails currently maps [wanted -> avail]
        -- Extend avails to reflect a neeed for an extra copy of avail
 
   | Just avail' <- split_avail avail
-  = returnNF_Tc (addToFM avails wanted avail', [])
+  = returnM (addToFM avails wanted avail', [])
 
   | otherwise
-  = tcLookupGlobalId splitName                 `thenNF_Tc` \ split_id ->
-    newMethodAtLoc (instLoc wanted) split_id 
-                  [linearInstType wanted]      `thenNF_Tc` \ (split_inst,_) ->
-    returnNF_Tc (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
+  = tcLookupId splitName                       `thenM` \ split_id ->
+    tcInstClassOp (instLoc wanted) split_id 
+                 [linearInstType wanted]       `thenM` \ split_inst ->
+    returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
 
   where
     split_avail :: Avail -> Maybe Avail
@@ -1451,61 +1480,70 @@ addLinearAvailable avails avail wanted
     split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
                  
 -------------------------
-addFree :: Avails -> Inst -> NF_TcM Avails
+addFree :: Avails -> Inst -> TcM Avails
        -- When an Inst is tossed upstairs as 'free' we nevertheless add it
        -- to avails, so that any other equal Insts will be commoned up right
        -- here rather than also being tossed upstairs.  This is really just
        -- an optimisation, and perhaps it is more trouble that it is worth,
        -- as the following comments show!
        --
-       -- NB1: do *not* add superclasses.  If we have
+       -- NB: do *not* add superclasses.  If we have
        --      df::Floating a
        --      dn::Num a
        -- but a is not bound here, then we *don't* want to derive
        -- dn from df here lest we lose sharing.
        --
-addFree avails free = returnNF_Tc (addToFM avails free IsFree)
+addFree avails free = returnM (addToFM avails free IsFree)
 
-addWanted :: Avails -> Inst -> TcExpr -> [Inst] -> NF_TcM Avails
+addWanted :: Avails -> Inst -> TcExpr -> [Inst] -> TcM Avails
 addWanted avails wanted rhs_expr wanteds
--- Do *not* add superclasses as well.  Here's an example of why not
---     class Eq b => Foo a b
---     instance Eq a => Foo [a] a
--- If we are reducing
---     (Foo [t] t)
--- we'll first deduce that it holds (via the instance decl).  We
--- must not then overwrite the Eq t constraint with a superclass selection!
---     ToDo: this isn't entirely satisfactory, because
---           we may also lose some entirely-legitimate sharing this way
-
-  = ASSERT( not (wanted `elemFM` avails) )
-    returnNF_Tc (addToFM avails wanted avail)
+  = ASSERT2( not (wanted `elemFM` avails), ppr wanted $$ ppr avails )
+    addAvailAndSCs avails wanted avail
   where
     avail | instBindingRequired wanted = Rhs rhs_expr wanteds
          | otherwise                  = ASSERT( null wanteds ) NoRhs
 
-addGiven :: Avails -> Inst -> NF_TcM Avails
+addGiven :: Avails -> Inst -> TcM Avails
 addGiven state given = addAvailAndSCs state given (Given (instToId given) False)
-
-addIrred :: WantSCs -> Avails -> Inst -> NF_TcM Avails
-addIrred NoSCs  state irred = returnNF_Tc (addToFM state irred Irred)
-addIrred AddSCs state irred = addAvailAndSCs state irred Irred
-
-addAvailAndSCs :: Avails -> Inst -> Avail -> NF_TcM Avails
-addAvailAndSCs avails wanted avail
-  = add_scs (addToFM avails wanted avail) wanted
-
-add_scs :: Avails -> Inst -> NF_TcM Avails
+       -- No ASSERT( not (given `elemFM` avails) ) because in an instance
+       -- decl for Ord t we can add both Ord t and Eq t as 'givens', 
+       -- so the assert isn't true
+
+addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
+addIrred NoSCs  avails irred = returnM (addToFM avails irred Irred)
+addIrred AddSCs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
+                              addAvailAndSCs avails irred Irred
+
+addAvailAndSCs :: Avails -> Inst -> Avail -> TcM Avails
+addAvailAndSCs avails inst avail
+  | not (isClassDict inst) = returnM avails1
+  | otherwise             = addSCs is_loop avails1 inst 
+  where
+    avails1 = addToFM avails inst avail
+    is_loop inst = inst `elem` deps    -- Note: this compares by *type*, not by Unique
+    deps         = findAllDeps avails avail
+
+findAllDeps :: Avails -> Avail -> [Inst]
+-- Find all the Insts that this one depends on
+-- See Note [SUPERCLASS-LOOP]
+findAllDeps avails (Rhs _ kids) = kids ++ concat (map (find_all_deps_help avails) kids)
+findAllDeps avails other       = []
+
+find_all_deps_help :: Avails -> Inst -> [Inst]
+find_all_deps_help avails inst
+  = case lookupFM avails inst of
+       Just avail -> findAllDeps avails avail
+       Nothing    -> []
+
+addSCs :: (Inst -> Bool) -> Avails -> Inst -> TcM Avails
        -- Add all the superclasses of the Inst to Avails
+       -- The first param says "dont do this because the original thing
+       --      depends on this one, so you'd build a loop"
        -- Invariant: the Inst is already in Avails.
 
-add_scs avails dict
-  | not (isClassDict dict)
-  = returnNF_Tc avails
-
-  | otherwise  -- It is a dictionary
-  = newDictsFromOld dict sc_theta'     `thenNF_Tc` \ sc_dicts ->
-    foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
+addSCs is_loop avails dict
+  = newDictsFromOld dict sc_theta'     `thenM` \ sc_dicts ->
+    foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
   where
     (clas, tys) = getDictClassTys dict
     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
@@ -1513,14 +1551,21 @@ add_scs avails dict
 
     add_sc avails (sc_dict, sc_sel)    -- Add it, and its superclasses
       = case lookupFM avails sc_dict of
-         Just (Given _ _) -> returnNF_Tc avails        -- See Note [SUPER] below
-         other            -> addAvailAndSCs avails sc_dict avail
+         Just (Given _ _) -> returnM avails    -- Given is cheaper than
+                                                       --   a superclass selection
+         Just other | is_loop sc_dict -> returnM avails        -- See Note [SUPERCLASS-LOOP]
+                    | otherwise       -> returnM avails'       -- SCs already added
+
+         Nothing -> addSCs is_loop avails' sc_dict
       where
        sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
        avail      = Rhs sc_sel_rhs [dict]
+       avails'    = addToFM avails sc_dict avail
 \end{code}
 
-Note [SUPER].  We have to be careful here.  If we are *given* d1:Ord a,
+Note [SUPERCLASS-LOOP]: Checking for loops
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have to be careful here.  If we are *given* d1:Ord a,
 and want to deduce (d2:C [a]) where
 
        class Ord a => C a where
@@ -1529,8 +1574,27 @@ and want to deduce (d2:C [a]) where
 Then we'll use the instance decl to deduce C [a] and then add the
 superclasses of C [a] to avails.  But we must not overwrite the binding
 for d1:Ord a (which is given) with a superclass selection or we'll just
-build a loop!  Hence looking for Given.  Crudely, Given is cheaper
-than a selection.
+build a loop! 
+
+Here's another example 
+       class Eq b => Foo a b
+       instance Eq a => Foo [a] a
+If we are reducing
+       (Foo [t] t)
+
+we'll first deduce that it holds (via the instance decl).  We must not
+then overwrite the Eq t constraint with a superclass selection!
+
+At first I had a gross hack, whereby I simply did not add superclass constraints
+in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
+becuase it lost legitimate superclass sharing, and it still didn't do the job:
+I found a very obscure program (now tcrun021) in which improvement meant the
+simplifier got two bites a the cherry... so something seemed to be an Irred
+first time, but reducible next time.
+
+Now we implement the Right Solution, which is to check for loops directly 
+when adding superclasses.  It's a bit like the occurs check in unification.
+
 
 
 %************************************************************************
@@ -1554,9 +1618,13 @@ It's OK: the final zonking stage should zap y to (), which is fine.
 
 
 \begin{code}
-tcSimplifyTop :: LIE -> TcM TcDictBinds
-tcSimplifyTop wanted_lie
-  = simpleReduceLoop (text "tcSimplTop") reduceMe wanteds      `thenTc` \ (frees, binds, irreds) ->
+tcSimplifyTop :: [Inst] -> TcM TcDictBinds
+-- The TcLclEnv should be valid here, solely to improve
+-- error message generation for the monomorphism restriction
+tcSimplifyTop wanteds
+  = getLclEnv                                                  `thenM` \ lcl_env ->
+    traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))        `thenM_`
+    simpleReduceLoop (text "tcSimplTop") reduceMe wanteds      `thenM` \ (frees, binds, irreds) ->
     ASSERT( null frees )
 
     let
@@ -1567,32 +1635,46 @@ tcSimplifyTop wanted_lie
        std_groups = equivClasses cmp_by_tyvar stds
 
                -- Pick the ones which its worth trying to disambiguate
-       (std_oks, std_bads) = partition worth_a_try std_groups
-
-               -- Have a try at disambiguation
-               -- if the type variable isn't bound
+               -- namely, the onese whose type variable isn't bound
                -- up with one of the non-standard classes
+       (std_oks, std_bads)     = partition worth_a_try std_groups
        worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
        non_std_tyvars          = unionVarSets (map tyVarsOfInst non_stds)
 
                -- Collect together all the bad guys
-       bad_guys = non_stds ++ concat std_bads
+       bad_guys               = non_stds ++ concat std_bads
+       (tidy_env, tidy_dicts) = tidyInsts bad_guys
+       (bad_ips, non_ips)     = partition isIPDict tidy_dicts
+       (no_insts, ambigs)     = partition no_inst non_ips
+       no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
+       fixed_tvs = oclose (fdPredsOfInsts tidy_dicts) emptyVarSet
     in
-       -- Disambiguate the ones that look feasible
-    mapTc disambigGroup std_oks                `thenTc` \ binds_ambig ->
 
-       -- And complain about the ones that don't
+       -- Report definite errors
+    addTopInstanceErrs tidy_env no_insts       `thenM_`
+    addTopIPErrs tidy_env bad_ips              `thenM_`
+
+       -- Deal with ambiguity errors, but only if
+       -- if there has not been an error so far; errors often
+       -- give rise to spurious ambiguous Insts
+    ifErrsM (returnM []) (
+       
+       -- Complain about the ones that don't fall under
+       -- the Haskell rules for disambiguation
        -- This group includes both non-existent instances
        --      e.g. Num (IO a) and Eq (Int -> Int)
        -- and ambiguous dictionaries
        --      e.g. Num a
-    addTopAmbigErrs bad_guys           `thenNF_Tc_`
+       addTopAmbigErrs (tidy_env, ambigs)      `thenM_`
 
-    returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
-  where
-    wanteds    = lieToList wanted_lie
+       -- Disambiguate the ones that look feasible
+        mappM disambigGroup std_oks
+    )                                  `thenM` \ binds_ambig ->
+
+    returnM (binds `andMonoBinds` andMonoBindList binds_ambig)
 
-    d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
+----------------------------------
+d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
 
 get_tv d   = case getDictClassTys d of
                   (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
@@ -1649,43 +1731,46 @@ disambigGroup dicts
        -- default list which can satisfy all the ambiguous classes.
        -- For example, if Real a is reqd, but the only type in the
        -- default list is Int.
-    tcGetDefaultTys                    `thenNF_Tc` \ default_tys ->
+    getDefaultTys                      `thenM` \ default_tys ->
     let
       try_default []   -- No defaults work, so fail
-       = failTc
+       = failM
 
       try_default (default_ty : default_tys)
-       = tryTc_ (try_default default_tys) $    -- If default_ty fails, we try
+       = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
                                                -- default_tys instead
-         tcSimplifyDefault theta               `thenTc` \ _ ->
-         returnTc default_ty
+         tcSimplifyDefault theta               `thenM` \ _ ->
+         returnM default_ty
         where
          theta = [mkClassPred clas [default_ty] | clas <- classes]
     in
-       -- See if any default works, and if so bind the type variable to it
-       -- If not, add an AmbigErr
-    recoverTc (addAmbigErrs dicts                      `thenNF_Tc_`
-              returnTc EmptyMonoBinds) $
-
-    try_default default_tys                    `thenTc` \ chosen_default_ty ->
-
-       -- Bind the type variable and reduce the context, for real this time
-    unifyTauTy chosen_default_ty (mkTyVarTy tyvar)     `thenTc_`
+       -- See if any default works
+    tryM (try_default default_tys)     `thenM` \ mb_ty ->
+    case mb_ty of {
+       Left _ ->       -- If not, add an AmbigErr
+                 addTopAmbigErrs (tidyInsts dicts)     `thenM_`
+                 returnM EmptyMonoBinds ;
+
+       Right chosen_default_ty ->
+
+       -- If so, bind the type variable 
+       -- and reduce the context, for real this time
+    unifyTauTy chosen_default_ty (mkTyVarTy tyvar)     `thenM_`
     simpleReduceLoop (text "disambig" <+> ppr dicts)
-                    reduceMe dicts                     `thenTc` \ (frees, binds, ambigs) ->
+                    reduceMe dicts                     `thenM` \ (frees, binds, ambigs) ->
     WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
-    warnDefault dicts chosen_default_ty                        `thenTc_`
-    returnTc binds
+    warnDefault dicts chosen_default_ty                        `thenM_`
+    returnM binds }
 
   | all isCreturnableClass classes
   =    -- Default CCall stuff to (); we don't even both to check that () is an
        -- instance of CReturnable, because we know it is.
-    unifyTauTy (mkTyVarTy tyvar) unitTy    `thenTc_`
-    returnTc EmptyMonoBinds
+    unifyTauTy (mkTyVarTy tyvar) unitTy        `thenM_`
+    returnM EmptyMonoBinds
 
   | otherwise -- No defaults
-  = addAmbigErrs dicts `thenNF_Tc_`
-    returnTc EmptyMonoBinds
+  = addTopAmbigErrs (tidyInsts dicts)  `thenM_`
+    returnM EmptyMonoBinds
 
   where
     tyvar       = get_tv (head dicts)          -- Should be non-empty
@@ -1747,15 +1832,15 @@ tcSimplifyDeriv :: [TyVar]
                -> TcM ThetaType        -- Needed
 
 tcSimplifyDeriv tyvars theta
-  = tcInstTyVars VanillaTv tyvars                      `thenNF_Tc` \ (tvs, _, tenv) ->
+  = tcInstTyVars VanillaTv tyvars                      `thenM` \ (tvs, _, tenv) ->
        -- The main loop may do unification, and that may crash if 
        -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
        -- ToDo: what if two of them do get unified?
-    newDicts DataDeclOrigin (substTheta tenv theta)    `thenNF_Tc` \ wanteds ->
-    simpleReduceLoop doc reduceMe wanteds              `thenTc` \ (frees, _, irreds) ->
+    newDicts DataDeclOrigin (substTheta tenv theta)    `thenM` \ wanteds ->
+    simpleReduceLoop doc reduceMe wanteds              `thenM` \ (frees, _, irreds) ->
     ASSERT( null frees )                       -- reduceMe never returns Free
 
-    doptsTc Opt_AllowUndecidableInstances              `thenNF_Tc` \ undecidable_ok ->
+    doptM Opt_AllowUndecidableInstances                `thenM` \ undecidable_ok ->
     let
        tv_set      = mkVarSet tvs
        simpl_theta = map dictPred irreds       -- reduceMe squashes all non-dicts
@@ -1784,7 +1869,7 @@ tcSimplifyDeriv tyvars theta
          = addErrTc (badDerivedPred pred)
   
          | otherwise
-         = returnNF_Tc ()
+         = returnM ()
          where
            pred_tyvars = tyVarsOfPred pred
 
@@ -1793,9 +1878,9 @@ tcSimplifyDeriv tyvars theta
                -- but the result should mention TyVars not TcTyVars
     in
    
-    mapNF_Tc check_pred simpl_theta            `thenNF_Tc_`
-    checkAmbiguity tvs simpl_theta tv_set      `thenTc_`
-    returnTc (substTheta rev_env simpl_theta)
+    mappM check_pred simpl_theta               `thenM_`
+    checkAmbiguity tvs simpl_theta tv_set      `thenM_`
+    returnM (substTheta rev_env simpl_theta)
   where
     doc    = ptext SLIT("deriving classes for a data type")
 \end{code}
@@ -1809,14 +1894,14 @@ tcSimplifyDefault :: ThetaType  -- Wanted; has no type variables in it
                  -> TcM ()
 
 tcSimplifyDefault theta
-  = newDicts DataDeclOrigin theta              `thenNF_Tc` \ wanteds ->
-    simpleReduceLoop doc reduceMe wanteds      `thenTc` \ (frees, _, irreds) ->
+  = newDicts DataDeclOrigin theta              `thenM` \ wanteds ->
+    simpleReduceLoop doc reduceMe wanteds      `thenM` \ (frees, _, irreds) ->
     ASSERT( null frees )       -- try_me never returns Free
-    mapNF_Tc (addErrTc . noInstErr) irreds     `thenNF_Tc_`
+    mappM (addErrTc . noInstErr) irreds        `thenM_`
     if null irreds then
-       returnTc ()
+       returnM ()
     else
-       failTc
+       failM
   where
     doc = ptext SLIT("default declaration")
 \end{code}
@@ -1833,89 +1918,124 @@ from the insts, or just whatever seems to be around in the monad just
 now?
 
 \begin{code}
-groupInsts :: [Inst] -> [[Inst]]
+groupErrs :: ([Inst] -> TcM ())        -- Deal with one group
+         -> [Inst]             -- The offending Insts
+          -> TcM ()
 -- Group together insts with the same origin
 -- We want to report them together in error messages
-groupInsts []          = []
-groupInsts (inst:insts) = (inst:friends) : groupInsts others
-                       where
-                               -- (It may seem a bit crude to compare the error messages,
-                               --  but it makes sure that we combine just what the user sees,
-                               --  and it avoids need equality on InstLocs.)
-                         (friends, others) = partition is_friend insts
-                         loc_msg           = showSDoc (pprInstLoc (instLoc inst))
-                         is_friend friend  = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
-
-
-addTopAmbigErrs dicts
-  = mapNF_Tc (addTopInstanceErrs tidy_env) (groupInsts no_insts)       `thenNF_Tc_`
-    mapNF_Tc (addTopIPErrs tidy_env)       (groupInsts bad_ips)                `thenNF_Tc_`
-    mapNF_Tc (addAmbigErr tidy_env)       ambigs                       `thenNF_Tc_`
-    returnNF_Tc ()
+
+groupErrs report_err [] 
+  = returnM ()
+groupErrs report_err (inst:insts) 
+  = do_one (inst:friends)              `thenM_`
+    groupErrs report_err others
+
   where
-    fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
-    (tidy_env, tidy_dicts) = tidyInsts dicts
-    (bad_ips, non_ips)     = partition is_ip tidy_dicts
-    (no_insts, ambigs)     = partition no_inst non_ips
-    is_ip d   = any isIPPred (predsOfInst d)
-    no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
+       -- (It may seem a bit crude to compare the error messages,
+       --  but it makes sure that we combine just what the user sees,
+       --  and it avoids need equality on InstLocs.)
+   (friends, others) = partition is_friend insts
+   loc_msg          = showSDoc (pprInstLoc (instLoc inst))
+   is_friend friend  = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
+   do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
+               -- Add location and context information derived from the Insts
+
+-- Add the "arising from..." part to a message about bunch of dicts
+addInstLoc :: [Inst] -> Message -> Message
+addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
 
 plural [x] = empty
 plural xs  = char 's'
 
+
 addTopIPErrs tidy_env tidy_dicts
-  = addInstErrTcM (instLoc (head tidy_dicts))
-       (tidy_env,
-        ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprInsts tidy_dicts)
+  = groupErrs report tidy_dicts
+  where
+    report dicts = addErrTcM (tidy_env, mk_msg dicts)
+    mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <> 
+                                    plural tidy_dicts <+> pprInsts tidy_dicts)
 
 -- Used for top-level irreducibles
 addTopInstanceErrs tidy_env tidy_dicts
-  = addInstErrTcM (instLoc (head tidy_dicts))
-       (tidy_env,
-        ptext SLIT("No instance") <> plural tidy_dicts <+> 
-               ptext SLIT("for") <+> pprInsts tidy_dicts)
-
-addAmbigErrs dicts
-  = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
+  = groupErrs report tidy_dicts
   where
-    (tidy_env, tidy_dicts) = tidyInsts dicts
-
-addAmbigErr tidy_env tidy_dict
-  = addInstErrTcM (instLoc tidy_dict)
-       (tidy_env,
-        sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
-             nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
+    report dicts = mkMonomorphismMsg tidy_env dicts    `thenM` \ (tidy_env, mono_msg) ->
+                  addErrTcM (tidy_env, mk_msg dicts $$ mono_msg)
+    mk_msg dicts = addInstLoc dicts (ptext SLIT("No instance") <> plural tidy_dicts <+> 
+                                    ptext SLIT("for") <+> pprInsts tidy_dicts)
+                  
+
+addTopAmbigErrs (tidy_env, tidy_dicts)
+-- Divide into groups that share a common set of ambiguous tyvars
+  = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
   where
-    ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
+    tvs_of :: Inst -> [TcTyVar]
+    tvs_of d = varSetElems (tyVarsOfInst d)
+    cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
+    
+    report :: [(Inst,[TcTyVar])] -> TcM ()
+    report pairs@((_,tvs) : _) -- The pairs share a common set of ambiguous tyvars
+       = mkMonomorphismMsg tidy_env dicts      `thenM` \ (tidy_env, mono_msg) ->
+         addErrTcM (tidy_env, msg $$ mono_msg)
+       where
+         dicts = map fst pairs
+         msg = sep [text "Ambiguous type variable" <> plural tvs <+> 
+                            pprQuotedList tvs <+> in_msg,
+                    nest 2 (pprInstsInFull dicts)]
+         in_msg | isSingleton dicts = text "in the top-level constraint:"
+                | otherwise         = text "in these top-level constraints:"
+
+
+mkMonomorphismMsg :: TidyEnv -> [Inst] -> TcM (TidyEnv, Message)
+-- There's an error with these Insts; if they have free type variables
+-- it's probably caused by the monomorphism restriction. 
+-- Try to identify the offending variable
+-- ASSUMPTION: the Insts are fully zonked
+mkMonomorphismMsg tidy_env insts
+  | isEmptyVarSet inst_tvs
+  = returnM (tidy_env, empty)
+  | otherwise
+  = findGlobals inst_tvs tidy_env      `thenM` \ (tidy_env, docs) ->
+    returnM (tidy_env, mk_msg docs)
 
+  where
+    inst_tvs = tyVarsOfInsts insts
+
+    mk_msg []   = empty                -- This happens in things like
+                               --      f x = show (read "foo")
+                               -- whre monomorphism doesn't play any role
+    mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
+                       nest 2 (vcat docs),
+                       ptext SLIT("Probable fix: give these definition(s) an explicit type signature")]
+    
 warnDefault dicts default_ty
-  = doptsTc Opt_WarnTypeDefaults  `thenTc` \ warn_flag ->
-    tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
+  = doptM Opt_WarnTypeDefaults  `thenM` \ warn_flag ->
+    addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
   where
        -- Tidy them first
     (_, tidy_dicts) = tidyInsts dicts
-    get_loc i = case instLoc i of { (_,loc,_) -> loc }
     warn_msg  = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
                                quotes (ppr default_ty),
                      pprInstsInFull tidy_dicts]
 
 complainCheck doc givens irreds
-  = mapNF_Tc zonkInst given_dicts_and_ips                        `thenNF_Tc` \ givens' ->
-    mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds)  `thenNF_Tc_`
-    returnNF_Tc ()
+  = mappM zonkInst given_dicts_and_ips                 `thenM` \ givens' ->
+    groupErrs (addNoInstanceErrs doc givens') irreds   `thenM_`
+    returnM ()
   where
     given_dicts_and_ips = filter (not . isMethod) givens
        -- Filter out methods, which are only added to
        -- the given set as an optimisation
 
 addNoInstanceErrs what_doc givens dicts
-  = getDOptsTc         `thenNF_Tc` \ dflags ->
-    tcGetInstEnv       `thenNF_Tc` \ inst_env ->
+  = getDOpts           `thenM` \ dflags ->
+    tcGetInstEnv       `thenM` \ inst_env ->
     let
        (tidy_env1, tidy_givens) = tidyInsts givens
        (tidy_env2, tidy_dicts)  = tidyMoreInsts tidy_env1 dicts
 
-       doc = vcat [sep [herald <+> pprInsts tidy_dicts,
+       doc = vcat [addInstLoc dicts $
+                   sep [herald <+> pprInsts tidy_dicts,
                         nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
                    ambig_doc,
                    ptext SLIT("Probable fix:"),
@@ -1962,7 +2082,7 @@ addNoInstanceErrs what_doc givens dicts
                where
                  (clas,tys) = getDictClassTys dict
     in
-    addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
+    addErrTcM (tidy_env2, doc)
 
 -- Used for the ...Thetas variants; all top level
 noInstErr pred = ptext SLIT("No instance for") <+> quotes (ppr pred)