[project @ 2005-03-09 14:26:56 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index 5ef2132..0a433ec 100644 (file)
@@ -9,7 +9,10 @@
 module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,
-       tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
+       tcSimplifyToDicts, tcSimplifyIPs, 
+       tcSimplifySuperClasses,
+       tcSimplifyTop, tcSimplifyInteractive,
+       tcSimplifyBracket,
 
        tcSimplifyDeriv, tcSimplifyDefault,
        bindInstsOfLocalFuns
@@ -18,50 +21,53 @@ module TcSimplify (
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TcUnify( unifyTauTy )
+import TcEnv           -- temp
+import HsSyn           ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
+import TcHsSyn         ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp )
 
-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, newDicts, 
                          isDict, isClassDict, isLinearInst, linearInstType,
                          isStdClassTyVarDict, isMethodFor, isMethod,
                          instToId, tyVarsOfInsts,  cloneDict,
                          ipNamesOfInsts, ipNamesOfInst, dictPred,
-                         instBindingRequired, instCanBeGeneralised,
-                         newDictsFromOld, newMethodAtLoc,
-                         getDictClassTys, isTyVarDict,
-                         instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
-                         Inst, LIE, pprInsts, pprInstsInFull,
-                         mkLIE, lieToList
+                         instBindingRequired, fdPredsOfInst,
+                         newDictsAtLoc, tcInstClassOp,
+                         getDictClassTys, isTyVarDict, instLoc,
+                         zonkInst, tidyInsts, tidyMoreInsts,
+                         Inst, pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
+                         isInheritableInst, pprDFuns, pprDictsTheta
                        )
-import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv, tcLookupGlobalId )
-import InstEnv         ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
+import TcEnv           ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders )
+import InstEnv         ( lookupInstEnv, classInstances )
 import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
-import TcType          ( TcTyVar, TcTyVarSet, ThetaType, 
-                         mkClassPred, isOverloadedTy, mkTyConApp,
+import TcType          ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, 
+                          mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
                          mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
-                         tyVarsOfPred, isIPPred, isInheritablePred, predHasFDs )
+                         tyVarsOfPred, tcEqType, pprPred, mkPredTy )
 import Id              ( idType, mkUserLocal )
 import Var             ( TyVar )
-import Name            ( getOccName, getSrcLoc )
+import Name            ( Name, getOccName, getSrcLoc )
 import NameSet         ( NameSet, mkNameSet, elemNameSet )
-import Class           ( classBigSig )
+import Class           ( classBigSig, classKey )
 import FunDeps         ( oclose, grow, improve, pprEquationDoc )
-import PrelInfo                ( isNumericClass, isCreturnableClass, isCcallishClass, 
-                         splitName, fstName, sndName )
-
-import Subst           ( mkTopTyVarSubst, substTheta, substTy )
-import TysWiredIn      ( unitTy, pairTyCon )
+import PrelInfo                ( isNumericClass ) 
+import PrelNames       ( splitName, fstName, sndName, integerTyConName,
+                         showClassKey, eqClassKey, ordClassKey )
+import Type            ( zipTopTvSubst, substTheta, substTy )
+import TysWiredIn      ( pairTyCon, doubleTy )
+import ErrUtils                ( Message )
+import BasicTypes      ( TopLevelFlag, isNotTopLevel )
 import VarSet
+import VarEnv          ( TidyEnv )
 import FiniteMap
+import Bag
 import Outputable
 import ListSetOps      ( equivClasses )
-import Util            ( zipEqual )
+import Util            ( zipEqual, isSingleton )
 import List            ( partition )
+import SrcLoc          ( Located(..) )
 import CmdLineOpts
 \end{code}
 
@@ -73,6 +79,60 @@ import CmdLineOpts
 %************************************************************************
 
        --------------------------------------
+       Notes on functional dependencies (a bug)
+       --------------------------------------
+
+| > class Foo a b | a->b
+| >
+| > class Bar a b | a->b
+| >
+| > data Obj = Obj
+| >
+| > instance Bar Obj Obj
+| >
+| > instance (Bar a b) => Foo a b
+| >
+| > foo:: (Foo a b) => a -> String
+| > foo _ = "works"
+| >
+| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
+| > runFoo f = f Obj
+| 
+| *Test> runFoo foo
+| 
+| <interactive>:1:
+|     Could not deduce (Bar a b) from the context (Foo a b)
+|       arising from use of `foo' at <interactive>:1
+|     Probable fix:
+|         Add (Bar a b) to the expected type of an expression
+|     In the first argument of `runFoo', namely `foo'
+|     In the definition of `it': it = runFoo foo
+| 
+| Why all of the sudden does GHC need the constraint Bar a b? The
+| function foo didn't ask for that... 
+
+The trouble is that to type (runFoo foo), GHC has to solve the problem:
+
+       Given constraint        Foo a b
+       Solve constraint        Foo a b'
+
+Notice that b and b' aren't the same.  To solve this, just do
+improvement and then they are the same.  But GHC currently does
+       simplify constraints
+       apply improvement
+       and loop
+
+That is usually fine, but it isn't here, because it sees that Foo a b is
+not the same as Foo a b', and so instead applies the instance decl for
+instance Bar a b => Foo a b.  And that's where the Bar constraint comes
+from.
+
+The Right Thing is to improve whenever the constraint set changes at
+all.  Not hard in principle, but it'll take a bit of fiddling to do.  
+
+
+
+       --------------------------------------
                Notes on quantification
        --------------------------------------
 
@@ -302,6 +362,36 @@ but we'll produce the non-principal type
 
 
        --------------------------------------
+       The need for forall's in constraints
+       --------------------------------------
+
+[Exchange on Haskell Cafe 5/6 Dec 2000]
+
+  class C t where op :: t -> Bool
+  instance C [t] where op x = True
+
+  p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
+  q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
+
+The definitions of p and q differ only in the order of the components in
+the pair on their right-hand sides.  And yet:
+
+  ghc and "Typing Haskell in Haskell" reject p, but accept q;
+  Hugs rejects q, but accepts p;
+  hbc rejects both p and q;
+  nhc98 ... (Malcolm, can you fill in the blank for us!).
+
+The type signature for f forces context reduction to take place, and
+the results of this depend on whether or not the type of y is known,
+which in turn depends on which component of the pair the type checker
+analyzes first.  
+
+Solution: if y::m a, float out the constraints
+       Monad m, forall c. C (m c)
+When m is later unified with [], we can solve both constraints.
+
+
+       --------------------------------------
                Notes on implicit parameters
        --------------------------------------
 
@@ -420,6 +510,21 @@ you might not expect the addition to be done twice --- but it will if
 we follow the argument of Question 2 and generalise over ?y.
 
 
+Question 4: top level
+~~~~~~~~~~~~~~~~~~~~~
+At the top level, monomorhism makes no sense at all.
+
+    module Main where
+       main = let ?x = 5 in print foo
+
+       foo = woggle 3
+
+       woggle :: (?x :: Int) => Int -> Int
+       woggle y = ?x + y
+
+We definitely don't want (foo :: Int) with a top-level implicit parameter
+(?x::Int) becuase there is no way to bind it.  
+
 
 Possible choices
 ~~~~~~~~~~~~~~~~
@@ -533,44 +638,44 @@ 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) ->
-
-       -- Check for non-generalisable insts
-    mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds)  `thenTc_`
+             wanted_lie                `thenM` \ (qtvs, frees, binds, irreds) ->
 
-    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
          | isFreeWhenInferring qtvs inst = Free
          | isClassDict inst              = DontReduceUnlessConstant    -- Dicts
-         | otherwise                     = ReduceMe                    -- Lits and Methods
+         | otherwise                     = ReduceMe NoSCs              -- 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 +692,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 `unionBags` binds1, irreds1)
 \end{code}
 
 Example [LOOP]
@@ -634,9 +739,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,21 +769,23 @@ 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.
--- Note that 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)
+  = ASSERT( all isSkolemTyVar qtvs )
+    do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
+       ; extendLIEs frees
+       ; return binds }
   where
-    get_qtvs = zonkTcTyVarsAndFV qtvs
+--  get_qtvs = zonkTcTyVarsAndFV qtvs
+    get_qtvs = return (mkVarSet qtvs)  -- All skolems
 
 
 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
@@ -688,13 +795,14 @@ 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
-  = tcSimplCheck doc get_qtvs givens wanted_lie
+  = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
+       ; extendLIEs frees
+       ; return (qtvs', binds) }
   where
        -- Figure out which type variables to quantify over
        -- You might think it should just be the signature tyvars,
@@ -707,53 +815,114 @@ 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) ->
-
-       -- Complain about any irreducible ones
-    complainCheck doc givens irreds            `thenNF_Tc_`
+tcSimplCheck doc get_qtvs want_scs givens wanted_lie
+  = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
 
-       -- Done
-    returnTc (qtvs, mkLIE frees, binds)
+               -- Complain about any irreducible ones
+       ; if not (null irreds)
+         then do { givens' <- mappM zonkInst given_dicts_and_ips
+                 ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds }
+         else return ()
 
+       ; returnM (qtvs, frees, binds) }
   where
+    given_dicts_and_ips = filter (not . isMethod) givens
+       -- For error reporting, filter out methods, which are 
+       -- only added to the given set as an optimisation
+
     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
            -- When checking against a given signature we always reduce
            -- until we find a match against something given, or can't reduce
            try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
-                       | otherwise                            = ReduceMe
+                       | otherwise                            = ReduceMe want_scs
        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 `unionBags` binds1, irreds1)
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+               tcSimplifySuperClasses
+%*                                                                     *
+%************************************************************************
+
+Note [SUPERCLASS-LOOP 1]
+~~~~~~~~~~~~~~~~~~~~~~~~
+We have to be very, very careful when generating superclasses, lest we
+accidentally build a loop. Here's an example:
+
+  class S a
+
+  class S a => C a where { opc :: a -> a }
+  class S b => D b where { opd :: b -> b }
+  
+  instance C Int where
+     opc = opd
+  
+  instance D Int where
+     opd = opc
+
+From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
+Simplifying, we may well get:
+       $dfCInt = :C ds1 (opd dd)
+       dd  = $dfDInt
+       ds1 = $p1 dd
+Notice that we spot that we can extract ds1 from dd.  
+
+Alas!  Alack! We can do the same for (instance D Int):
+
+       $dfDInt = :D ds2 (opc dc)
+       dc  = $dfCInt
+       ds2 = $p1 dc
+
+And now we've defined the superclass in terms of itself.
+
+Solution: never generate a superclass selectors at all when
+satisfying the superclass context of an instance declaration.
+
+Two more nasty cases are in
+       tcrun021
+       tcrun033
+
+\begin{code}
+tcSimplifySuperClasses qtvs givens sc_wanteds
+  = ASSERT( all isSkolemTyVar qtvs )
+    do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
+       ; binds2             <- tc_simplify_top doc False NoSCs frees
+       ; return (binds1 `unionBags` binds2) }
+  where
+    get_qtvs = return (mkVarSet qtvs)
+    doc = ptext SLIT("instance declaration superclass context")
 \end{code}
 
 
@@ -763,46 +932,143 @@ tcSimplCheck doc get_qtvs givens wanted_lie
 %*                                                                     *
 %************************************************************************
 
+tcSimplifyRestricted infers which type variables to quantify for a 
+group of restricted bindings.  This isn't trivial.
+
+Eg1:   id = \x -> x
+       We want to quantify over a to get id :: forall a. a->a
+       
+Eg2:   eq = (==)
+       We do not want to quantify over a, because there's an Eq a 
+       constraint, so we get eq :: a->a->Bool  (notice no forall)
+
+So, assume:
+       RHS has type 'tau', whose free tyvars are tau_tvs
+       RHS has constraints 'wanteds'
+
+Plan A (simple)
+  Quantify over (tau_tvs \ ftvs(wanteds))
+  This is bad. The constraints may contain (Monad (ST s))
+  where we have        instance Monad (ST s) where...
+  so there's no need to be monomorphic in s!
+
+  Also the constraint might be a method constraint,
+  whose type mentions a perfectly innocent tyvar:
+         op :: Num a => a -> b -> a
+  Here, b is unconstrained.  A good example would be
+       foo = op (3::Int)
+  We want to infer the polymorphic type
+       foo :: forall b. b -> b
+
+
+Plan B (cunning, used for a long time up to and including GHC 6.2)
+  Step 1: Simplify the constraints as much as possible (to deal 
+  with Plan A's problem).  Then set
+       qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
+
+  Step 2: Now simplify again, treating the constraint as 'free' if 
+  it does not mention qtvs, and trying to reduce it otherwise.
+  The reasons for this is to maximise sharing.
+
+  This fails for a very subtle reason.  Suppose that in the Step 2
+  a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
+  In the Step 1 this constraint might have been simplified, perhaps to
+  (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
+  This won't happen in Step 2... but that in turn might prevent some other
+  constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..}) 
+  and that in turn breaks the invariant that no constraints are quantified over.
+
+  Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
+  the problem.
+
+
+Plan C (brutal)
+  Step 1: Simplify the constraints as much as possible (to deal 
+  with Plan A's problem).  Then set
+       qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
+  Return the bindings from Step 1.
+  
+
+A note about Plan C (arising from "bug" reported by George Russel March 2004)
+Consider this:
+
+      instance (HasBinary ty IO) => HasCodedValue ty
+
+      foo :: HasCodedValue a => String -> IO a
+
+      doDecodeIO :: HasCodedValue a => () -> () -> IO a
+      doDecodeIO codedValue view  
+        = let { act = foo "foo" } in  act
+
+You might think this should work becuase the call to foo gives rise to a constraint
+(HasCodedValue t), which can be satisfied by the type sig for doDecodeIO.  But the
+restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
+constraint using the (rather bogus) instance declaration, and now we are stuffed.
+
+I claim this is not really a bug -- but it bit Sergey as well as George.  So here's
+plan D
+
+
+Plan D (a variant of plan B)
+  Step 1: Simplify the constraints as much as possible (to deal 
+  with Plan A's problem), BUT DO NO IMPROVEMENT.  Then set
+       qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
+
+  Step 2: Now simplify again, treating the constraint as 'free' if 
+  it does not mention qtvs, and trying to reduce it otherwise.
+
+  The point here is that it's generally OK to have too few qtvs; that is,
+  to make the thing more monomorphic than it could be.  We don't want to
+  do that in the common cases, but in wierd cases it's ok: the programmer
+  can always add a signature.  
+
+  Too few qtvs => too many wanteds, which is what happens if you do less
+  improvement.
+
+
 \begin{code}
 tcSimplifyRestricted   -- Used for restricted binding groups
                        -- i.e. ones subject to the monomorphism restriction
        :: SDoc
+       -> TopLevelFlag
+       -> [Name]               -- Things bound in this group
        -> 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
-  =    -- 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
-       --      e.g. a call to  f :: Eq a => a -> b -> b
-       -- Here, b is unconstrained.  A good example would be
-       --      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) ->
+       -- tcSimpifyRestricted returns no constraints to
+       -- quantify over; by definition there are none.
+       -- They are all thrown back in the LIE
+
+tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
+       -- Zonk everything in sight
+  = mappM zonkInst wanteds                     `thenM` \ wanteds' ->
+    zonkTcTyVarsAndFV (varSetElems tau_tvs)    `thenM` \ tau_tvs' ->
+    tcGetGlobalTyVars                          `thenM` \ gbl_tvs' ->
+
+       -- '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.
+       --
+       -- BUT do no improvement!  See Plan D above
+    reduceContextWithoutImprovement 
+       doc reduceMe wanteds'           `thenM` \ (_frees, _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 ->
     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 _frees, pprInsts constrained_dicts,
+               ppr _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
+       -- necessary, so try again, this time more gently, knowing the exact
        -- set of type variables to quantify over.
        --
        -- We quantify only over constraints that are captured by qtvs;
@@ -814,18 +1080,30 @@ 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' ->
+       --
+       -- At top level, we *do* squash methods becuase we want to 
+       -- expose implicit parameters to the test that follows
     let
-        try_me inst | isFreeWrtTyVars qtvs inst = Free
-                   | otherwise                 = ReduceMe
+       is_nested_group = isNotTopLevel top_lvl
+        try_me inst | isFreeWrtTyVars qtvs inst,
+                     (is_nested_group || isDict inst) = Free
+                   | otherwise                        = ReduceMe AddSCs
     in
-    reduceContext doc try_me [] wanteds'       `thenTc` \ (no_improvement, frees, binds, irreds) ->
-    ASSERT( no_improvement )
+    reduceContextWithoutImprovement 
+       doc try_me wanteds'             `thenM` \ (frees, binds, irreds) ->
     ASSERT( null irreds )
-       -- No need to loop because simpleReduceLoop will have
-       -- already done any improvement necessary
 
-    returnTc (varSetElems qtvs, mkLIE frees, binds)
+       -- See "Notes on implicit parameters, Question 4: top level"
+    if is_nested_group then
+       extendLIEs frees        `thenM_`
+        returnM (varSetElems qtvs, binds)
+    else
+       let
+           (non_ips, bad_ips) = partition isClassDict frees
+       in    
+       addTopIPErrs bndrs bad_ips      `thenM_`
+       extendLIEs non_ips              `thenM_`
+        returnM (varSetElems qtvs, binds)
 \end{code}
 
 
@@ -867,29 +1145,47 @@ want to get
        forall dIntegralInt.
        fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
 
-because the scsel will mess up matching.  Instead we want
+because the scsel will mess up RULE matching.  Instead we want
 
        forall dIntegralInt, dNumInt.
        fromIntegral Int Int dIntegralInt dNumInt = id Int
 
-Hence "DontReduce NoSCs"
+Hence "WithoutSCs"
 
 \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
-               | otherwise   = ReduceMe
+    try_me inst        | isDict inst = KeepDictWithoutSCs      -- See notes above re "WithoutSCs"
+               | otherwise   = ReduceMe NoSCs
+\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}
 
 
@@ -915,32 +1211,32 @@ 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
     try_me inst | isFreeWrtIPs ip_set inst = Free
-               | otherwise                = ReduceMe
+               | otherwise                = ReduceMe NoSCs
 
     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 `unionBags` binds1)
 \end{code}
 
 
@@ -970,29 +1266,37 @@ 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 init_lie local_ids
+bindInstsOfLocalFuns ::        [Inst] -> [TcId] -> TcM TcDictBinds
+-- Simlifies only MethodInsts, and generate only bindings of form 
+--     fm = f tys dicts
+-- We're careful not to even generate bindings of the form
+--     d1 = d2
+-- You'd think that'd be fine, but it interacts with what is
+-- arguably a bug in Match.tidyEqnInfo (see notes there)
+
+bindInstsOfLocalFuns wanteds local_ids
   | null overloaded_ids
        -- Common case
-  = returnTc (init_lie, EmptyMonoBinds)
+  = extendLIEs wanteds         `thenM_`
+    returnM emptyLHsBinds
 
   | otherwise
-  = simpleReduceLoop doc try_me wanteds                `thenTc` \ (frees, binds, irreds) ->
+  = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
     ASSERT( null irreds )
-    returnTc (mkLIE frees, binds)
+    extendLIEs not_for_me      `thenM_`
+    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)
+    (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
 
     overloaded_set = mkVarSet overloaded_ids   -- There can occasionally be a lot of them
                                                -- so it's worth building a set, so that
                                                -- lookup (in isMethodFor) is faster
-
-    try_me inst | isMethodFor overloaded_set inst = ReduceMe
-               | otherwise                       = Free
+    try_me inst | isMethod inst = ReduceMe NoSCs
+               | otherwise     = Free
 \end{code}
 
 
@@ -1006,14 +1310,15 @@ The main control over context reduction is here
 
 \begin{code}
 data WhatToDo
- = ReduceMe            -- Try to reduce this
+ = ReduceMe WantSCs    -- Try to reduce this
                        -- If there's no instance, behave exactly like
                        -- DontReduce: add the inst to
                        -- the irreductible ones, but don't
                        -- produce an error message of any kind.
                        -- It might be quite legitimate such as (Eq a)!
 
- | DontReduce WantSCs          -- Return as irreducible
+ | KeepDictWithoutSCs  -- Return as irreducible; don't add its superclasses
+                       -- Rather specialised: see notes with tcSimplifyToDicts
 
  | DontReduceUnlessConstant    -- Return as irreducible unless it can
                                -- be reduced to a constant in one step
@@ -1021,7 +1326,7 @@ data WhatToDo
  | Free                          -- Return as free
 
 reduceMe :: Inst -> WhatToDo
-reduceMe inst = ReduceMe
+reduceMe inst = ReduceMe AddSCs
 
 data WantSCs = NoSCs | AddSCs  -- Tells whether we should add the superclasses
                                -- of a predicate when adding it to the avails
@@ -1031,6 +1336,7 @@ data WantSCs = NoSCs | AddSCs     -- Tells whether we should add the superclasses
 
 \begin{code}
 type Avails = FiniteMap Inst Avail
+emptyAvails = emptyFM
 
 data Avail
   = IsFree             -- Used for free Insts
@@ -1043,9 +1349,10 @@ data Avail
 
   | NoRhs              -- Used for Insts like (CCallable f)
                        -- where no witness is required.
+                       -- ToDo: remove?
 
   | Rhs                -- Used when there is a RHS
-       TcExpr          -- The RHS
+       (LHsExpr TcId)  -- The RHS
        [Inst]          -- Insts free in the RHS; we need these too
 
   | Linear             -- Splittable Insts only.
@@ -1057,7 +1364,7 @@ data Avail
   | LinRhss            -- Splittable Insts only; this is used only internally
                        --      by extractResults, where a Linear 
                        --      is turned into an LinRhss
-       [TcExpr]        -- A supply of suitable RHSs
+       [LHsExpr TcId]  -- A supply of suitable RHSs
 
 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
                        | (inst,avail) <- fmToList avails ]
@@ -1084,15 +1391,15 @@ The loop startes
 \begin{code}
 extractResults :: Avails
               -> [Inst]                -- Wanted
-              -> NF_TcM (TcDictBinds,  -- Bindings
-                         [Inst],       -- Irreducible ones
-                         [Inst])       -- Free ones
+              -> TcM (TcDictBinds,     -- Bindings
+                       [Inst],         -- Irreducible ones
+                       [Inst])         -- Free ones
 
 extractResults avails wanteds
-  = go avails EmptyMonoBinds [] [] wanteds
+  = go avails emptyBag [] [] 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
@@ -1106,7 +1413,7 @@ extractResults avails wanteds
          Just (Given id _) -> go avails new_binds irreds frees ws
                            where
                               new_binds | id == instToId w = binds
-                                        | otherwise        = addBind binds w (HsVar id)
+                                        | otherwise        = addBind binds w (L (instSpan w) (HsVar id))
                -- The sought Id can be one of the givens, via a superclass chain
                -- and then we definitely don't want to generate an x=x binding!
 
@@ -1114,18 +1421,24 @@ extractResults avails wanteds
                             where
                                new_binds = addBind binds w rhs
 
-         Just (LinRhss (rhs:rhss))     -- Consume one of the Rhss
+         Just (Linear n split_inst avail)      -- Transform Linear --> LinRhss
+           -> 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 `unionBags` binds')
+                 irreds' frees' (split_inst : w : ws)
+
+         Just (LinRhss (rhs:rhss))             -- Consume one of the Rhss
                -> go new_avails new_binds irreds frees ws
                where           
                   new_binds  = addBind binds w rhs
                   new_avails = addToFM avails w (LinRhss rhss)
 
-         Just (Linear n split_inst avail)
-           -> split n (instToId split_inst) avail w    `thenNF_Tc` \ (binds', (rhs:rhss), irreds') ->
-              go (addToFM avails w (LinRhss rhss))
-                 (binds `AndMonoBinds` addBind binds' w rhs)
-                 (irreds' ++ irreds) frees (split_inst:ws)
-
+    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)
@@ -1153,30 +1466,31 @@ extractResults avails wanteds
        --                        1 or 0 insts to add to irreds
 
 
-split :: Int -> TcId -> Avail -> Inst 
-      -> NF_TcM (TcDictBinds, [TcExpr], [Inst])
--- (split n split_id avail wanted) returns
+split :: Int -> TcId -> TcId -> Inst 
+      -> TcM (TcDictBinds, [LHsExpr TcId])
+-- (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
 --     * one or zero insts needed to witness the whole lot
 --       (maybe be zero if the initial Inst is a Given)
-split n split_id avail wanted
+--
+-- NB: 'wanted' is just a template
+
+split n split_id root_id wanted
   = go n
   where
-    ty  = linearInstType wanted
+    ty      = linearInstType wanted
     pair_ty = mkTyConApp pairTyCon [ty,ty]
-    id  = instToId wanted
-    occ = getOccName id
-    loc = getSrcLoc id
+    id      = instToId wanted
+    occ     = getOccName id
+    loc     = getSrcLoc id
+    span    = instSpan wanted
 
-    go 1 = case avail of
-            Given id _ -> returnNF_Tc (EmptyMonoBinds, [HsVar id], [])
-            Irred      -> cloneDict wanted             `thenNF_Tc` \ w' ->
-                          returnNF_Tc (EmptyMonoBinds, [HsVar (instToId w')], [w'])
+    go 1 = returnM (emptyBag, [L span $ HsVar root_id])
 
-    go n = go ((n+1) `div` 2)          `thenNF_Tc` \ (binds1, rhss, irred) ->
-          expand n rhss                `thenNF_Tc` \ (binds2, rhss') ->
-          returnNF_Tc (binds1 `AndMonoBinds` binds2, rhss', irred)
+    go n = go ((n+1) `div` 2)          `thenM` \ (binds1, rhss) ->
+          expand n rhss                `thenM` \ (binds2, rhss') ->
+          returnM (binds1 `unionBags` binds2, rhss')
 
        -- (expand n rhss) 
        -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
@@ -1185,26 +1499,28 @@ split n split_id avail 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 (listToBag 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),
-                                   [mk_fs_app fst_id ty x, mk_fs_app snd_id ty x])
+                      returnM (L span (VarBind x (mk_app span split_id rhs)),
+                               [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
 
-mk_fs_app id ty var = HsVar id `TyApp` [ty,ty] `HsApp` HsVar var
+mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
 
-mk_app id rhs = HsApp (HsVar id) rhs
+mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
 
-addBind binds inst rhs = binds `AndMonoBinds` VarMonoBind (instToId inst) rhs
+addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst)) 
+                                                     (VarBind (instToId inst) rhs))
+instSpan wanted = instLocSrcSpan (instLoc wanted)
 \end{code}
 
 
@@ -1229,13 +1545,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 `unionBags` binds1, irreds1)
 \end{code}
 
 
@@ -1245,7 +1561,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
@@ -1258,19 +1574,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 emptyAvails 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 "----------------------",
@@ -1282,37 +1598,77 @@ reduceContext doc try_me givens wanteds
             text "frees" <+> ppr frees,
             text "no_improvement =" <+> ppr no_improvement,
             text "----------------------"
-            ]))                                        `thenNF_Tc_`
+            ]))                                        `thenM_`
+
+    returnM (no_improvement, frees, binds, irreds)
+
+-- reduceContextWithoutImprovement differs from reduceContext
+--     (a) no improvement
+--     (b) 'givens' is assumed empty
+reduceContextWithoutImprovement doc try_me wanteds
+  =
+    traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
+            text "----------------------",
+            doc,
+            text "wanted" <+> ppr wanteds,
+            text "----------------------"
+            ]))                                        `thenM_`
 
-    returnTc (no_improvement, frees, binds, irreds)
+        -- Do the real work
+    reduceList (0,[]) try_me wanteds emptyAvails       `thenM` \ avails ->
+    extractResults avails wanteds                      `thenM` \ (binds, irreds, frees) ->
 
+    traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
+            text "----------------------",
+            doc,
+            text "wanted" <+> ppr wanteds,
+            text "----",
+            text "avails" <+> pprAvails avails,
+            text "frees" <+> ppr frees,
+            text "----------------------"
+            ]))                                        `thenM_`
+
+    returnM (frees, binds, irreds)
+
+tcImprove :: Avails -> TcM Bool                -- False <=> no change
+-- Perform improvement using all the predicates in Avails
 tcImprove avails
- =  tcGetInstEnv                               `thenTc` \ inst_env ->
+ =  tcGetInstEnvs                      `thenM` \ inst_envs -> 
     let
        preds = [ (pred, pp_loc)
-               | inst <- keysFM avails,
-                 let pp_loc = pprInstLoc (instLoc inst),
-                 pred <- predsOfInst inst,
-                 predHasFDs pred
+               | (inst, avail) <- fmToList avails,
+                 pred <- get_preds inst avail,
+                 let pp_loc = pprInstLoc (instLoc inst)
                ]
                -- Avails has all the superclasses etc (good)
                -- It also has all the intermediates of the deduction (good)
                -- It does not have duplicates (good)
                -- NB that (?x::t1) and (?x::t2) will be held separately in avails
                --    so that improve will see them separate
-       eqns  = improve (classInstEnv inst_env) preds
+
+       -- For free Methods, we want to take predicates from their context,
+       -- but for Methods that have been squished their context will already
+       -- be in Avails, and we don't want duplicates.  Hence this rather
+       -- horrid get_preds function
+       get_preds inst IsFree = fdPredsOfInst inst
+       get_preds inst other | isDict inst = [dictPred inst]
+                            | otherwise   = []
+
+       eqns = improve get_insts preds
+       get_insts clas = classInstances inst_envs clas
      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 (varSetElems qtvs)      `thenNF_Tc` \ (_, _, tenv) ->
-          unifyTauTy (substTy tenv t1) (substTy tenv t2)
+    unify ((qtvs, pairs), doc)
+        = addErrCtxt doc                       $
+          tcInstTyVars (varSetElems qtvs)      `thenM` \ (_, _, tenv) ->
+          mapM_ (unif_pr tenv) pairs
+    unif_pr tenv (ty1,ty2) =  unifyTauTy (substTy tenv ty1) (substTy tenv ty2)
 \end{code}
 
 The main context-reduction function is @reduce@.  Here's its game plan.
@@ -1352,29 +1708,30 @@ reduceList (n,stack) try_me wanteds state
   =
 #ifdef DEBUG
    (if n > 8 then
-       pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
+       pprTrace "Interesting! Context reduction stack deeper than 8:" 
+                (nest 2 (pprStack stack))
     else (\x->x))
 #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!
-reduce stack try_me wanted state
+reduce stack try_me wanted avails
     -- It's the same as an existing inst, or a superclass thereof
-  | Just avail <- isAvailable state wanted
+  | Just avail <- isAvailable avails wanted
   = if isLinearInst wanted then
-       addLinearAvailable state avail wanted   `thenNF_Tc` \ (state', wanteds') ->
-       reduceList stack try_me wanteds' state'
+       addLinearAvailable avails avail wanted  `thenM` \ (avails', wanteds') ->
+       reduceList stack try_me wanteds' avails'
     else
-       returnTc state          -- No op for non-linear things
+       returnM avails          -- No op for non-linear things
 
   | otherwise
   = case try_me wanted of {
 
-      DontReduce want_scs -> addIrred want_scs state wanted
+      KeepDictWithoutSCs -> addIrred NoSCs avails wanted
 
     ; DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
                                     -- First, see if the inst can be reduced to a constant in one step
@@ -1384,24 +1741,33 @@ reduce stack try_me wanted state
                -- First, see if the inst can be reduced to a constant in one step
        try_simple addFree
 
-    ; ReduceMe ->              -- It should be reduced
-       lookupInst wanted             `thenNF_Tc` \ lookup_result ->
+    ; ReduceMe want_scs ->     -- It should be reduced
+       lookupInst wanted             `thenM` \ lookup_result ->
        case lookup_result of
-           GenInst wanteds' rhs -> reduceList stack try_me wanteds' state      `thenTc` \ state' ->
-                                   addWanted state' wanted rhs wanteds'
-           SimpleInst rhs       -> addWanted state wanted rhs []
+           GenInst wanteds' rhs -> addIrred NoSCs avails wanted                `thenM` \ avails1 ->
+                                   reduceList stack try_me wanteds' avails1    `thenM` \ avails2 ->
+                                   addWanted want_scs avails2 wanted rhs wanteds'
+               -- Experiment with temporarily doing addIrred *before* the reduceList, 
+               -- which has the effect of adding the thing we are trying
+               -- to prove to the database before trying to prove the things it
+               -- needs.  See note [RECURSIVE DICTIONARIES]
+               -- NB: we must not do an addWanted before, because that adds the
+               --     superclasses too, and thaat can lead to a spurious loop; see
+               --     the examples in [SUPERCLASS-LOOP]
+               -- So we do an addIrred before, and then overwrite it afterwards with addWanted
+
+           SimpleInst rhs -> addWanted want_scs avails wanted rhs []
 
            NoInstance ->    -- No such instance!
                             -- Add it and its superclasses
-                            addIrred AddSCs state wanted
-
+                            addIrred want_scs avails wanted
     }
   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
+           SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
+           other          -> do_this_otherwise avails wanted
 \end{code}
 
 
@@ -1413,107 +1779,203 @@ 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
-  | need_split avail
-  = 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])
+       -- avails currently maps [wanted -> avail]
+       -- Extend avails to reflect a neeed for an extra copy of avail
 
-  | otherwise
-  = returnNF_Tc (addToFM avails wanted avail', [])
-  where
-    avail' = case avail of
-               Given id _   -> Given id True
-               Linear n i a -> Linear (n+1) i a 
+  | Just avail' <- split_avail avail
+  = returnM (addToFM avails wanted avail', [])
 
-    need_split Irred         = True
-    need_split (Given _ used) = used
-    need_split (Linear _ _ _) = False
+  | otherwise
+  = 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
+       -- (Just av) if there's a modified version of avail that
+       --           we can use to replace avail in avails
+       -- Nothing   if there isn't, so we need to create a Linear
+    split_avail (Linear n i a)             = Just (Linear (n+1) i a)
+    split_avail (Given id used) | not used  = Just (Given id True)
+                               | otherwise = Nothing
+    split_avail Irred                      = Nothing
+    split_avail IsFree                     = Nothing
+    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)
-
-addWanted :: Avails -> Inst -> TcExpr -> [Inst] -> NF_TcM Avails
-addWanted avails wanted rhs_expr wanteds
--- Do *not* add superclasses as well.  Here's an example of why not
---     class Eq a => 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 unsatisfactory, because
---           we may also lose some entirely-legitimate sharing this way
-
-  = ASSERT( not (wanted `elemFM` avails) )
-    returnNF_Tc (addToFM avails wanted avail)
+addFree avails free = returnM (addToFM avails free IsFree)
+
+addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
+addWanted want_scs avails wanted rhs_expr wanteds
+  = addAvailAndSCs want_scs avails wanted avail
   where
     avail | instBindingRequired wanted = Rhs rhs_expr wanteds
          | otherwise                  = ASSERT( null wanteds ) NoRhs
 
-addGiven :: Avails -> Inst -> NF_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
+addGiven :: Avails -> Inst -> TcM Avails
+addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
+       -- Always add superclasses for 'givens'
+       --
+       -- 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 want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
+                                addAvailAndSCs want_scs avails irred Irred
+
+addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
+addAvailAndSCs want_scs avails inst avail
+  | not (isClassDict inst) = return avails_with_inst
+  | NoSCs <- want_scs     = return avails_with_inst
+  | otherwise             = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
+                               ; addSCs is_loop avails_with_inst inst }
+  where
+    avails_with_inst = addToFM avails inst avail
+
+    is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
+                       -- Note: this compares by *type*, not by Unique
+    deps         = findAllDeps (unitVarSet (instToId inst)) avail
+    dep_tys     = map idType (varSetElems deps)
+
+    findAllDeps :: IdSet -> Avail -> IdSet
+    -- Find all the Insts that this one depends on
+    -- See Note [SUPERCLASS-LOOP]
+    -- Watch out, though.  Since the avails may contain loops 
+    -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
+    findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
+    findAllDeps so_far other       = so_far
+
+    find_all :: IdSet -> Inst -> IdSet
+    find_all so_far kid
+      | kid_id `elemVarSet` so_far       = so_far
+      | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
+      | otherwise                        = so_far'
+      where
+       so_far' = extendVarSet so_far kid_id    -- Add the new kid to so_far
+       kid_id = instToId kid
 
-add_scs :: Avails -> Inst -> NF_TcM Avails
+addSCs :: (TcPredType -> 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
+  = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
+       ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
   where
     (clas, tys) = getDictClassTys dict
     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
-    sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
+    sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
 
-    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
+    add_sc avails (sc_dict, sc_sel)
+      | is_loop (dictPred sc_dict) = return avails     -- See Note [SUPERCLASS-LOOP 2]
+      | is_given sc_dict          = return avails
+      | otherwise                 = addSCs is_loop avails' sc_dict
       where
-       sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
-       avail      = Rhs sc_sel_rhs [dict]
+       sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
+       avails'    = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
+
+    is_given :: Inst -> Bool
+    is_given sc_dict = case lookupFM avails sc_dict of
+                         Just (Given _ _) -> True      -- Given is cheaper than superclass selection
+                         other            -> False     
 \end{code}
 
-Note [SUPER].  We have to be careful here.  If we are *given* d1:Ord a,
+Note [SUPERCLASS-LOOP 2]
+~~~~~~~~~~~~~~~~~~~~~~~~
+But the above isn't enough.  Suppose we are *given* d1:Ord a,
 and want to deduce (d2:C [a]) where
 
        class Ord a => C a where
-       instance Ord a => C [a] where ...
+       instance Ord [a] => C [a] where ...
 
-Then we'll use the instance decl to deduce C [a] and then add the
+Then we'll use the instance decl to deduce C [a] from Ord [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.
-
+for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
+build a loop! 
+
+Here's another variant, immortalised in tcrun020
+       class Monad m => C1 m
+       class C1 m => C2 m x
+       instance C2 Maybe Bool
+For the instance decl we need to build (C1 Maybe), and it's no good if
+we run around and add (C2 Maybe Bool) and its superclasses to the avails 
+before we search for C1 Maybe.
+
+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.
+
+
+Note [RECURSIVE DICTIONARIES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider 
+    data D r = ZeroD | SuccD (r (D r));
+    
+    instance (Eq (r (D r))) => Eq (D r) where
+        ZeroD     == ZeroD     = True
+        (SuccD a) == (SuccD b) = a == b
+        _         == _         = False;
+    
+    equalDC :: D [] -> D [] -> Bool;
+    equalDC = (==);
+
+We need to prove (Eq (D [])).  Here's how we go:
+
+       d1 : Eq (D [])
+
+by instance decl, holds if
+       d2 : Eq [D []]
+       where   d1 = dfEqD d2
+
+by instance decl of Eq, holds if
+       d3 : D []
+       where   d2 = dfEqList d3
+               d1 = dfEqD d2
+
+But now we can "tie the knot" to give
+
+       d3 = d1
+       d2 = dfEqList d3
+       d1 = dfEqD d2
+
+and it'll even run!  The trick is to put the thing we are trying to prove
+(in this case Eq (D []) into the database before trying to prove its
+contributing clauses.
+       
 
 %************************************************************************
 %*                                                                     *
@@ -1536,45 +1998,81 @@ 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) ->
-    ASSERT( null frees )
-
-    let
+tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
+tcSimplifyTop wanteds
+  = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
+  where 
+    doc = text "tcSimplifyTop"
+
+tcSimplifyInteractive wanteds
+  = tc_simplify_top doc True  {- Interactive loop -}     AddSCs wanteds
+  where 
+    doc = text "tcSimplifyTop"
+
+-- The TcLclEnv should be valid here, solely to improve
+-- error message generation for the monomorphism restriction
+tc_simplify_top doc is_interactive want_scs wanteds
+  = do { lcl_env <- getLclEnv
+       ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
+
+       ; let try_me inst = ReduceMe want_scs
+       ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
+
+       ; let
                -- All the non-std ones are definite errors
-       (stds, non_stds) = partition isStdClassTyVarDict irreds
-
-               -- Group by type variable
-       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
-               -- up with one of the non-standard classes
-       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
-    in
-       -- Disambiguate the ones that look feasible
-    mapTc disambigGroup std_oks                `thenTc` \ binds_ambig ->
-
-       -- And complain about the ones that don't
-       -- 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_`
-
-    returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
-  where
-    wanteds    = lieToList wanted_lie
-
-    d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
+           (stds, non_stds) = partition isStdClassTyVarDict irreds
+    
+                   -- Group by type variable
+           std_groups = equivClasses cmp_by_tyvar stds
+    
+                   -- Pick the ones which its worth trying to disambiguate
+                   -- 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
+           (non_ips, bad_ips) = partition isClassDict bad_guys
+           (ambigs, no_insts) = partition isTyVarDict non_ips
+           -- If the dict has no type constructors involved, it must be ambiguous,
+           -- except I suppose that another error with fundeps maybe should have
+           -- constrained those type variables
+
+       -- Report definite errors
+       ; ASSERT( null frees )
+         groupErrs (addNoInstanceErrs Nothing []) no_insts
+       ; strangeTopIPErrs bad_ips
+
+       -- Deal with ambiguity errors, but only if
+       -- if there has not been an error so far:
+       -- errors often give rise to spurious ambiguous Insts.
+       -- For example:
+       --   f = (*)    -- Monomorphic
+       --   g :: Num a => a -> a
+       --   g x = f x x
+       -- Here, we get a complaint when checking the type signature for g,
+       -- that g isn't polymorphic enough; but then we get another one when
+       -- dealing with the (Num a) context arising from f's definition;
+       -- we try to unify a with Int (to default it), but find that it's
+       -- already been unified with the rigid variable from g's type sig
+       ; binds_ambig <- ifErrsM (returnM []) $
+           do  { -- 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 ambigs
+
+                 -- Disambiguate the ones that look feasible
+               ; mappM (disambigGroup is_interactive) std_oks }
+
+       ; return (binds `unionBags` unionManyBags binds_ambig) }
+
+----------------------------------
+d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
 
 get_tv d   = case getDictClassTys d of
                   (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
@@ -1615,15 +2113,12 @@ Since we're not using the result of @foo@, the result if (presumably)
 @void@.
 
 \begin{code}
-disambigGroup :: [Inst]        -- All standard classes of form (C a)
+disambigGroup :: Bool  -- True <=> simplifying at top-level interactive loop
+             -> [Inst] -- All standard classes of form (C a)
              -> TcM TcDictBinds
 
-disambigGroup dicts
-  |   any isNumericClass classes       -- Guaranteed all standard classes
-         -- see comment at the end of function for reasons as to
-         -- why the defaulting mechanism doesn't apply to groups that
-         -- include CCallable or CReturnable dicts.
-   && not (any isCcallishClass classes)
+disambigGroup is_interactive dicts
+  |   any std_default_class classes    -- Guaranteed all standard classes
   =    -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
        -- SO, TRY DEFAULT TYPES IN ORDER
 
@@ -1631,47 +2126,60 @@ 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 ->
+    get_default_tys                    `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_`
-    simpleReduceLoop (text "disambig" <+> ppr dicts)
-                    reduceMe dicts                     `thenTc` \ (frees, binds, ambigs) ->
-    WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
-    warnDefault dicts chosen_default_ty                        `thenTc_`
-    returnTc 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
-
-  | otherwise -- No defaults
-  = addAmbigErrs dicts `thenNF_Tc_`
-    returnTc EmptyMonoBinds
+       -- See if any default works
+    tryM (try_default default_tys)     `thenM` \ mb_ty ->
+    case mb_ty of
+       Left  _                 -> bomb_out
+       Right chosen_default_ty -> choose_default chosen_default_ty
+
+  | otherwise                          -- No defaults
+  = bomb_out
 
   where
-    tyvar       = get_tv (head dicts)          -- Should be non-empty
-    classes     = map get_clas dicts
+    tyvar   = get_tv (head dicts)      -- Should be non-empty
+    classes = map get_clas dicts
+
+    std_default_class cls
+      =  isNumericClass cls
+      || (is_interactive && 
+         classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
+               -- In interactive mode, we default Show a to Show ()
+               -- to avoid graututious errors on "show []"
+
+    choose_default default_ty  -- Commit to tyvar = default_ty
+      =        -- Bind the type variable 
+       unifyTauTy default_ty (mkTyVarTy tyvar) `thenM_`
+       -- and reduce the context, for real this time
+       simpleReduceLoop (text "disambig" <+> ppr dicts)
+                        reduceMe dicts                 `thenM` \ (frees, binds, ambigs) ->
+       WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
+       warnDefault dicts default_ty                    `thenM_`
+       returnM binds
+
+    bomb_out = addTopAmbigErrs dicts   `thenM_`
+              returnM emptyBag
+
+get_default_tys
+  = do         { mb_defaults <- getDefaultTys
+       ; case mb_defaults of
+               Just tys -> return tys
+               Nothing  ->     -- No use-supplied default;
+                               -- use [Integer, Double]
+                           do { integer_ty <- tcMetaTy integerTyConName
+                              ; return [integer_ty, doubleTy] } }
 \end{code}
 
 [Aside - why the defaulting mechanism is turned off when
@@ -1729,55 +2237,51 @@ tcSimplifyDeriv :: [TyVar]
                -> TcM ThetaType        -- Needed
 
 tcSimplifyDeriv tyvars theta
-  = tcInstTyVars tyvars                                        `thenNF_Tc` \ (tvs, _, tenv) ->
+  = tcInstTyVars 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 DerivOrigin (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
-
-       check_pred pred
-         | isEmptyVarSet pred_tyvars   -- Things like (Eq T) should be rejected
-         = addErrTc (noInstErr pred)
-
-         | not undecidable_ok && not (isTyVarClassPred pred)
-         -- Check that the returned dictionaries are all of form (C a b)
-         --    (where a, b are type variables).  
-         -- We allow this if we had -fallow-undecidable-instances,
-         -- but note that risks non-termination in the 'deriving' context-inference
-         -- fixpoint loop.   It is useful for situations like
-         --    data Min h a = E | M a (h a)
-         -- which gives the instance decl
-         --    instance (Eq a, Eq (h a)) => Eq (Min h a)
-          = addErrTc (noInstErr pred)
+
+       (bad_insts, ok_insts) = partition is_bad_inst irreds
+       is_bad_inst dict 
+          = let pred = dictPred dict   -- reduceMe squashes all non-dicts
+            in isEmptyVarSet (tyVarsOfPred pred)
+                 -- Things like (Eq T) are bad
+            || (not undecidable_ok && not (isTyVarClassPred pred))
+                 -- The returned dictionaries should be of form (C a b)
+                 --    (where a, b are type variables).  
+                 -- We allow non-tyvar dicts if we had -fallow-undecidable-instances,
+                 -- but note that risks non-termination in the 'deriving' context-inference
+                 -- fixpoint loop.   It is useful for situations like
+                 --    data Min h a = E | M a (h a)
+                 -- which gives the instance decl
+                 --    instance (Eq a, Eq (h a)) => Eq (Min h a)
   
-         | not (pred_tyvars `subVarSet` tv_set) 
+       simpl_theta = map dictPred ok_insts
+       weird_preds = [pred | pred <- simpl_theta
+                           , not (tyVarsOfPred pred `subVarSet` tv_set)]  
          -- Check for a bizarre corner case, when the derived instance decl should
          -- have form  instance C a b => D (T a) where ...
          -- Note that 'b' isn't a parameter of T.  This gives rise to all sorts
          -- of problems; in particular, it's hard to compare solutions for
          -- equality when finding the fixpoint.  So I just rule it out for now.
-         = addErrTc (badDerivedPred pred)
   
-         | otherwise
-         = returnNF_Tc ()
-         where
-           pred_tyvars = tyVarsOfPred pred
-
-       rev_env = mkTopTyVarSubst tvs (mkTyVarTys tyvars)
+       rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
                -- This reverse-mapping is a Royal Pain, 
                -- 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)
+    addNoInstanceErrs Nothing [] bad_insts             `thenM_`
+    mapM_ (addErrTc . badDerivedPred) weird_preds      `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}
@@ -1791,14 +2295,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 DefaultOrigin 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_`
+    addNoInstanceErrs Nothing []  irreds       `thenM_`
     if null irreds then
-       returnTc ()
+       returnM ()
     else
-       failTc
+       failM
   where
     doc = ptext SLIT("default declaration")
 \end{code}
@@ -1815,140 +2319,202 @@ 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
 
+groupErrs report_err [] 
+  = returnM ()
+groupErrs report_err (inst:insts) 
+  = do_one (inst:friends)              `thenM_`
+    groupErrs report_err others
 
-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 ()
   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)
+addTopIPErrs :: [Name] -> [Inst] -> TcM ()
+addTopIPErrs bndrs [] 
+  = return ()
+addTopIPErrs bndrs ips
+  = addErrTcM (tidy_env, mk_msg tidy_ips)
+  where
+    (tidy_env, tidy_ips) = tidyInsts ips
+    mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from the monomorphic top-level binding(s) of"),
+                           pprBinders bndrs <> colon],
+                      nest 2 (vcat (map ppr_ip ips)),
+                      monomorphism_fix]
+    ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
+
+strangeTopIPErrs :: [Inst] -> TcM ()
+strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
+  = groupErrs report tidy_dicts
+  where
+    (tidy_env, tidy_dicts) = tidyInsts dicts
+    report dicts = addErrTcM (tidy_env, mk_msg dicts)
+    mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <> 
+                                    plural tidy_dicts <+> pprDictsTheta tidy_dicts)
+
+addNoInstanceErrs :: Maybe SDoc        -- Nothing => top level
+                               -- Just d => d describes the construct
+                 -> [Inst]     -- What is given by the context or type sig
+                 -> [Inst]     -- What is wanted
+                 -> TcM ()     
+addNoInstanceErrs mb_what givens [] 
+  = returnM ()
+addNoInstanceErrs mb_what givens dicts
+  =    -- Some of the dicts are here because there is no instances
+       -- and some because there are too many instances (overlap)
+    getDOpts           `thenM` \ dflags ->
+    tcGetInstEnvs      `thenM` \ inst_envs ->
+    let
+       (tidy_env1, tidy_givens) = tidyInsts givens
+       (tidy_env2, tidy_dicts)  = tidyMoreInsts tidy_env1 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)
+       -- Run through the dicts, generating a message for each
+       -- overlapping one, but simply accumulating all the 
+       -- no-instance ones so they can be reported as a group
+       (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
+       check_overlap (overlap_doc, no_inst_dicts) dict 
+         | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
+         | otherwise
+         = case lookupInstEnv dflags inst_envs clas tys of
+               -- The case of exactly one match and no unifiers means
+               -- a successful lookup.  That can't happen here, becuase
+               -- dicts only end up here if they didn't match in Inst.lookupInst
+#ifdef DEBUG
+               ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
+#endif
+               ([], _)  -> (overlap_doc, dict : no_inst_dicts)         -- No match
+               res      -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
+         where
+           (clas,tys) = getDictClassTys dict
+    in
+       
+       -- Now generate a good message for the no-instance bunch
+    mk_probable_fix tidy_env2 no_inst_dicts    `thenM` \ (tidy_env3, probable_fix) ->
+    let
+       no_inst_doc | null no_inst_dicts = empty
+                   | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
+       heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+> 
+                               ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
+               | otherwise   = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
+                                    nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
+    in
+       -- And emit both the non-instance and overlap messages
+    addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
+  where
+    mk_overlap_msg dict (matches, unifiers)
+      = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") 
+                                       <+> pprPred (dictPred dict))),
+               sep [ptext SLIT("Matching instances") <> colon,
+                    nest 2 (vcat [pprDFuns dfuns, pprDFuns unifiers])],
+               ASSERT( not (null matches) )
+               if not (isSingleton matches)
+               then    -- Two or more matches
+                    empty
+               else    -- One match, plus some unifiers
+               ASSERT( not (null unifiers) )
+               parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
+                                quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
+                             ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
+      where
+       dfuns = [df | (_, (_,_,df)) <- matches]
 
-addAmbigErrs dicts
-  = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
+    mk_probable_fix tidy_env dicts     
+      = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 (vcat fixes)])
+      where
+       fixes = add_ors (fix1 ++ fix2)
+
+       fix1 = case mb_what of
+                Nothing   -> []        -- Top level
+                Just what -> -- Nested (type signatures, instance decls)
+                             [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
+                               ptext SLIT("to the") <+> what] ]
+
+       fix2 | null instance_dicts = []
+            | otherwise           = [ ptext SLIT("add an instance declaration for")
+                                      <+> pprDictsTheta instance_dicts ]
+       instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
+               -- Insts for which it is worth suggesting an adding an instance declaration
+               -- Exclude implicit parameters, and tyvar dicts
+
+       add_ors :: [SDoc] -> [SDoc]     -- The empty case should not happen
+       add_ors []      = [ptext SLIT("[No suggested fixes]")]  -- Strange
+       add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
+
+addTopAmbigErrs dicts
+-- Divide into groups that share a common set of ambiguous tyvars
+  = mapM report (equivClasses cmp [(d, tvs_of d) | d <- 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))])
+    tvs_of :: Inst -> [TcTyVar]
+    tvs_of d = varSetElems (tyVarsOfInst d)
+    cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
+    
+    report :: [(Inst,[TcTyVar])] -> TcM ()
+    report pairs@((inst,tvs) : _)      -- The pairs share a common set of ambiguous tyvars
+       = mkMonomorphismMsg tidy_env tvs        `thenM` \ (tidy_env, mono_msg) ->
+         setSrcSpan (instLocSrcSpan (instLoc inst)) $
+               -- the location of the first one will do for the err message
+         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 (pprDictsInFull dicts)]
+         in_msg = text "in the constraint" <> plural dicts <> colon
+
+
+mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> 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 inst_tvs
+  = findGlobals (mkVarSet inst_tvs) tidy_env   `thenM` \ (tidy_env, docs) ->
+    returnM (tidy_env, mk_msg docs)
   where
-    ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
-
+    mk_msg []   = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
+                       -- 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),
+                       monomorphism_fix
+                      ]
+monomorphism_fix :: SDoc
+monomorphism_fix = ptext SLIT("Probable fix:") <+> 
+                  (ptext SLIT("give these definition(s) an explicit type signature")
+                   $$ ptext SLIT("or use -fno-monomorphism-restriction"))
+    
 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 ()
-  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 ->
-    let
-       (tidy_env1, tidy_givens) = tidyInsts givens
-       (tidy_env2, tidy_dicts)  = tidyMoreInsts tidy_env1 dicts
-
-       doc = vcat [sep [herald <+> pprInsts tidy_dicts,
-                        nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
-                   ambig_doc,
-                   ptext SLIT("Probable fix:"),
-                   nest 4 fix1,
-                   nest 4 fix2]
-
-       herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
-       unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
-                   | otherwise     = empty
-
-               -- The error message when we don't find a suitable instance
-               -- is complicated by the fact that sometimes this is because
-               -- there is no instance, and sometimes it's because there are
-               -- too many instances (overlap).  See the comments in TcEnv.lhs
-               -- with the InstEnv stuff.
-
-       ambig_doc
-           | not ambig_overlap = empty
-           | otherwise
-           = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
-                   nest 4 (ptext SLIT("depends on the instantiation of") <+>
-                           quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
-
-       fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
-                   ptext SLIT("to the") <+> what_doc]
-
-       fix2 | null instance_dicts 
-            = empty
-            | otherwise
-            = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
-
-       instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
-               -- Insts for which it is worth suggesting an adding an instance declaration
-               -- Exclude implicit parameters, and tyvar dicts
-
-           -- Checks for the ambiguous case when we have overlapping instances
-       ambig_overlap = any ambig_overlap1 dicts
-       ambig_overlap1 dict 
-               | isClassDict dict
-               = case lookupInstEnv dflags inst_env clas tys of
-                           NoMatch ambig -> ambig
-                           other         -> False
-               | otherwise = False
-               where
-                 (clas,tys) = getDictClassTys dict
-    in
-    addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
+                     pprDictsInFull tidy_dicts]
 
 -- Used for the ...Thetas variants; all top level
-noInstErr pred = ptext SLIT("No instance for") <+> quotes (ppr pred)
-
 badDerivedPred pred
   = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
          ptext SLIT("type variables that are not data type parameters"),
@@ -1957,12 +2523,7 @@ badDerivedPred pred
 reduceDepthErr n stack
   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
          ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
-         nest 4 (pprInstsInFull stack)]
-
-reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
+         nest 4 (pprStack stack)]
 
------------------------------------------------
-addCantGenErr inst
-  = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
-                  nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])
+pprStack stack = vcat (map pprInstInFull stack)
 \end{code}