[project @ 2005-03-09 14:26:56 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index db7e183..0a433ec 100644 (file)
@@ -10,6 +10,7 @@ module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,
        tcSimplifyToDicts, tcSimplifyIPs, 
+       tcSimplifySuperClasses,
        tcSimplifyTop, tcSimplifyInteractive,
        tcSimplifyBracket,
 
@@ -21,42 +22,43 @@ module TcSimplify (
 
 import {-# SOURCE #-} TcUnify( unifyTauTy )
 import TcEnv           -- temp
-import HsSyn           ( HsBind(..), LHsBinds, HsExpr(..), LHsExpr )
+import HsSyn           ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
 import TcHsSyn         ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp )
 
 import TcRnMonad
 import Inst            ( lookupInst, LookupInstResult(..),
-                         tyVarsOfInst, fdPredsOfInsts, fdPredsOfInst, newDicts,
+                         tyVarsOfInst, fdPredsOfInsts, newDicts, 
                          isDict, isClassDict, isLinearInst, linearInstType,
                          isStdClassTyVarDict, isMethodFor, isMethod,
                          instToId, tyVarsOfInsts,  cloneDict,
                          ipNamesOfInsts, ipNamesOfInst, dictPred,
-                         instBindingRequired,
-                         newDictsFromOld, tcInstClassOp,
-                         getDictClassTys, isTyVarDict,
-                         instLoc, zonkInst, tidyInsts, tidyMoreInsts,
-                         Inst, pprInsts, pprInstsInFull, tcGetInstEnvs,
-                         isIPDict, isInheritableInst, pprDFuns
+                         instBindingRequired, fdPredsOfInst,
+                         newDictsAtLoc, tcInstClassOp,
+                         getDictClassTys, isTyVarDict, instLoc,
+                         zonkInst, tidyInsts, tidyMoreInsts,
+                         Inst, pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
+                         isInheritableInst, pprDFuns, pprDictsTheta
                        )
-import TcEnv           ( tcGetGlobalTyVars, tcLookupId, findGlobals )
-import InstEnv         ( lookupInstEnv, classInstEnv )
+import TcEnv           ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders )
+import InstEnv         ( lookupInstEnv, classInstances )
 import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
-import TcType          ( TcTyVar, TcTyVarSet, ThetaType, TyVarDetails(VanillaTv),
-                         mkClassPred, isOverloadedTy, mkTyConApp,
+import TcType          ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, 
+                          mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
                          mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
-                         tyVarsOfPred, tcEqType )
+                         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, classKey )
 import FunDeps         ( oclose, grow, improve, pprEquationDoc )
 import PrelInfo                ( isNumericClass ) 
 import PrelNames       ( splitName, fstName, sndName, integerTyConName,
                          showClassKey, eqClassKey, ordClassKey )
-import Subst           ( mkTopTyVarSubst, substTheta, substTy )
+import Type            ( zipTopTvSubst, substTheta, substTy )
 import TysWiredIn      ( pairTyCon, doubleTy )
 import ErrUtils                ( Message )
+import BasicTypes      ( TopLevelFlag, isNotTopLevel )
 import VarSet
 import VarEnv          ( TidyEnv )
 import FiniteMap
@@ -508,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
 ~~~~~~~~~~~~~~~~
@@ -649,9 +666,10 @@ inferLoop doc tau_tvs wanteds
        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_`
+    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'    `thenM` \ (no_improvement, frees, binds, irreds) ->
 
@@ -761,11 +779,13 @@ tcSimplifyCheck
 --     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      `thenM` \ (qtvs', binds) ->
-    returnM 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
@@ -780,7 +800,9 @@ tcSimplifyInferCheck
                 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,
@@ -807,17 +829,16 @@ tcSimplifyInferCheck doc tau_tvs givens wanted_lie
 Here is the workhorse function for all three wrappers.
 
 \begin{code}
-tcSimplCheck doc get_qtvs givens wanted_lie
-  = check_loop givens wanted_lie       `thenM` \ (qtvs, frees, binds, irreds) ->
-
-       -- Complain about any irreducible ones
-    mappM zonkInst given_dicts_and_ips                         `thenM` \ givens' ->
-    groupErrs (addNoInstanceErrs (Just doc) givens') irreds    `thenM_`
+tcSimplCheck doc get_qtvs want_scs givens wanted_lie
+  = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
 
-       -- Done
-    extendLIEs frees           `thenM_`
-    returnM (qtvs, 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 
@@ -836,7 +857,7 @@ tcSimplCheck doc get_qtvs givens wanted_lie
            -- 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'       `thenM` \ (no_improvement, frees, binds, irreds) ->
 
@@ -851,51 +872,203 @@ tcSimplCheck doc get_qtvs givens wanted_lie
 
 %************************************************************************
 %*                                                                     *
+               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}
+
+
+%************************************************************************
+%*                                                                     *
 \subsection{tcSimplifyRestricted}
 %*                                                                     *
 %************************************************************************
 
+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
        -> [Inst]               -- Free in the RHSs
        -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
                TcDictBinds)    -- Bindings
+       -- tcSimpifyRestricted returns no constraints to
+       -- quantify over; by definition there are none.
+       -- They are all thrown back in the LIE
 
-tcSimplifyRestricted doc tau_tvs wanteds
-  =    -- First squash out all methods, to find the constrained tyvars
-       -- We can't just take the free vars of wanted_lie because that'll
-       -- have methods that may incidentally mention entirely unconstrained variables
-       --      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
-
-       -- 'reduceMe': Reduce as far as we can.  Don't stop at
+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.
-    simpleReduceLoop doc reduceMe wanteds      `thenM` \ (foo_frees, foo_binds, constrained_dicts) ->
+       --
+       -- 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)    `thenM` \ tau_tvs' ->
-    tcGetGlobalTyVars                          `thenM` \ gbl_tvs ->
     let
        constrained_tvs = tyVarsOfInsts constrained_dicts
-       qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs)
+       qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
                         `minusVarSet` constrained_tvs
     in
     traceTc (text "tcSimplifyRestricted" <+> vcat [
-               pprInsts wanteds, pprInsts foo_frees, pprInsts constrained_dicts,
-               ppr foo_binds,
+               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;
@@ -907,28 +1080,30 @@ tcSimplifyRestricted doc tau_tvs wanteds
        -- 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
-    restrict_loop doc qtvs wanteds
-       -- We still need a loop because improvement can take place
-       -- E.g. if we have (C (T a)) and the instance decl
-       --      instance D Int b => C (T a) where ...
-       -- and there's a functional dependency for D.   Then we may improve
-       -- the tyep variable 'b'.
-
-restrict_loop doc qtvs wanteds
-  = mappM zonkInst wanteds                     `thenM` \ wanteds' ->
-    zonkTcTyVarsAndFV (varSetElems qtvs)       `thenM` \ qtvs' ->
+       --
+       -- 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'       `thenM` \ (no_improvement, frees, binds, irreds) ->
-    if no_improvement then
-       ASSERT( null irreds )
-       extendLIEs frees                        `thenM_`
-       returnM (varSetElems qtvs', binds)
+    reduceContextWithoutImprovement 
+       doc try_me wanteds'             `thenM` \ (frees, binds, irreds) ->
+    ASSERT( null irreds )
+
+       -- See "Notes on implicit parameters, Question 4: top level"
+    if is_nested_group then
+       extendLIEs frees        `thenM_`
+        returnM (varSetElems qtvs, binds)
     else
-       restrict_loop doc qtvs' (irreds ++ frees)       `thenM` \ (qtvs1, binds1) ->
-       returnM (qtvs1, binds `unionBags` binds1)
+       let
+           (non_ips, bad_ips) = partition isClassDict frees
+       in    
+       addTopIPErrs bndrs bad_ips      `thenM_`
+       extendLIEs non_ips              `thenM_`
+        returnM (varSetElems qtvs, binds)
 \end{code}
 
 
@@ -970,12 +1145,12 @@ 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 :: [Inst] -> TcM (TcDictBinds)
@@ -991,8 +1166,8 @@ tcSimplifyToDicts wanteds
     doc = text "tcSimplifyToDicts"
 
        -- Reduce methods and lits only; stop as soon as we get a dictionary
-    try_me inst        | isDict inst = DontReduce NoSCs        -- See notes above for why NoSCs
-               | otherwise   = ReduceMe
+    try_me inst        | isDict inst = KeepDictWithoutSCs      -- See notes above re "WithoutSCs"
+               | otherwise   = ReduceMe NoSCs
 \end{code}
 
 
@@ -1048,7 +1223,7 @@ tcSimplifyIPs given_ips wanteds
 
        -- 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
       = mappM zonkInst givens          `thenM` \ givens' ->
@@ -1091,30 +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 ::        [Inst] -> [TcId] -> TcM (LHsBinds TcId)
+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
   = extendLIEs wanteds         `thenM_`
-    returnM emptyBag
+    returnM emptyLHsBinds
 
   | otherwise
-  = simpleReduceLoop doc try_me wanteds                `thenM` \ (frees, binds, irreds) ->
+  = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
     ASSERT( null irreds )
+    extendLIEs not_for_me      `thenM_`
     extendLIEs frees           `thenM_`
     returnM binds
   where
     doc                     = text "bindInsts" <+> ppr local_ids
     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}
 
 
@@ -1128,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
@@ -1143,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
@@ -1153,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
@@ -1393,7 +1577,7 @@ reduceContext doc try_me givens wanteds
             ]))                                        `thenM_`
 
         -- Build the Avail mapping from "givens"
-    foldlM addGiven emptyFM givens                     `thenM` \ init_state ->
+    foldlM addGiven emptyAvails givens                 `thenM` \ init_state ->
 
         -- Do the real work
     reduceList (0,[]) try_me wanteds init_state                `thenM` \ avails ->
@@ -1418,23 +1602,60 @@ reduceContext doc try_me givens wanteds
 
     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_`
+
+        -- 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
- =  tcGetInstEnvs                      `thenM` \ (home_ie, pkg_ie) ->
+ =  tcGetInstEnvs                      `thenM` \ inst_envs -> 
     let
        preds = [ (pred, pp_loc)
-               | inst <- keysFM avails,
-                 let pp_loc = pprInstLoc (instLoc inst),
-                 pred <- fdPredsOfInst inst
+               | (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
+
+       -- 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 = classInstEnv home_ie clas ++ classInstEnv pkg_ie clas
+       get_insts clas = classInstances inst_envs clas
      in
      if null eqns then
        returnM True
@@ -1443,10 +1664,11 @@ tcImprove avails
         mappM_ unify eqns      `thenM_`
        returnM False
   where
-    unify ((qtvs, t1, t2), doc)
-        = addErrCtxt doc                               $
-          tcInstTyVars VanillaTv (varSetElems qtvs)    `thenM` \ (_, _, 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.
@@ -1486,7 +1708,8 @@ 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
@@ -1508,7 +1731,7 @@ reduce stack try_me wanted avails
   | otherwise
   = case try_me wanted of {
 
-      DontReduce want_scs -> addIrred want_scs avails 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
@@ -1518,12 +1741,12 @@ reduce stack try_me wanted avails
                -- First, see if the inst can be reduced to a constant in one step
        try_simple addFree
 
-    ; ReduceMe ->              -- It should be reduced
+    ; ReduceMe want_scs ->     -- It should be reduced
        lookupInst wanted             `thenM` \ lookup_result ->
        case lookup_result of
            GenInst wanteds' rhs -> addIrred NoSCs avails wanted                `thenM` \ avails1 ->
                                    reduceList stack try_me wanteds' avails1    `thenM` \ avails2 ->
-                                   addWanted avails2 wanted rhs wanteds'
+                                   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
@@ -1533,17 +1756,17 @@ reduce stack try_me wanted avails
                --     the examples in [SUPERCLASS-LOOP]
                -- So we do an addIrred before, and then overwrite it afterwards with addWanted
 
-           SimpleInst rhs       -> addWanted avails wanted rhs []
+           SimpleInst rhs -> addWanted want_scs avails wanted rhs []
 
            NoInstance ->    -- No such instance!
                             -- Add it and its superclasses
-                            addIrred AddSCs avails wanted
+                            addIrred want_scs avails wanted
     }
   where
     try_simple do_this_otherwise
       = lookupInst wanted        `thenM` \ lookup_result ->
        case lookup_result of
-           SimpleInst rhs -> addWanted avails wanted rhs []
+           SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
            other          -> do_this_otherwise avails wanted
 \end{code}
 
@@ -1598,34 +1821,37 @@ addFree :: Avails -> Inst -> TcM Avails
        --
 addFree avails free = returnM (addToFM avails free IsFree)
 
-addWanted :: Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
-addWanted avails wanted rhs_expr wanteds
-  = addAvailAndSCs avails wanted avail
+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 -> TcM Avails
-addGiven avails given = addAvailAndSCs avails given (Given (instToId given) False)
+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 NoSCs  avails irred = returnM (addToFM avails irred Irred)
-addIrred AddSCs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
-                              addAvailAndSCs avails irred Irred
-
-addAvailAndSCs :: Avails -> Inst -> Avail -> TcM Avails
-addAvailAndSCs avails inst avail
-  | not (isClassDict inst) = returnM avails1
-  | otherwise             = traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps]) `thenM_`
-                            addSCs is_loop avails1 inst 
+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
-    avails1     = addToFM avails inst avail
-    is_loop inst = any (`tcEqType` idType (instToId inst)) dep_tys
+    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 emptyVarSet avail
+    deps         = findAllDeps (unitVarSet (instToId inst)) avail
     dep_tys     = map idType (varSetElems deps)
 
     findAllDeps :: IdSet -> Avail -> IdSet
@@ -1633,53 +1859,57 @@ addAvailAndSCs avails inst avail
     -- 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 findAllDeps
-             (extendVarSetList so_far (map instToId kids))     -- Add the kids to so_far
-              [a | Just a <- map (lookupFM avails) kids]       -- Find the kids' Avail
-    findAllDeps so_far other = 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
 
-addSCs :: (Inst -> Bool) -> Avails -> Inst -> 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.
 
 addSCs is_loop avails dict
-  = newDictsFromOld dict sc_theta'     `thenM` \ sc_dicts ->
-    foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
+  = 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
-      | add_me sc_dict = addSCs is_loop avails' sc_dict
-      | otherwise      = returnM avails
+    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 = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
        avails'    = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
 
-    add_me :: Inst -> Bool
-    add_me sc_dict
-       | is_loop sc_dict = False       -- See Note [SUPERCLASS-LOOP]
-       | otherwise       = case lookupFM avails sc_dict of
-                               Just (Given _ _) -> False       -- Given is cheaper than superclass selection
-                               other            -> True        
+    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 [SUPERCLASS-LOOP]: Checking for loops
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-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
+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
@@ -1769,66 +1999,77 @@ It's OK: the final zonking stage should zap y to (), which is fine.
 
 \begin{code}
 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
-tcSimplifyTop         wanteds = tc_simplify_top False {- Not interactive loop -} wanteds
-tcSimplifyInteractive wanteds = tc_simplify_top True  {- Interactive loop -}     wanteds
+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 is_interactive wanteds
-  = getLclEnv                                                  `thenM` \ lcl_env ->
-    traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))        `thenM_`
-    simpleReduceLoop (text "tcSimplTop") reduceMe wanteds      `thenM` \ (frees, binds, irreds) ->
-    ASSERT( null frees )
+tc_simplify_top doc is_interactive want_scs wanteds
+  = do { lcl_env <- getLclEnv
+       ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
 
-    let
+       ; 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
-               -- namely, the onese whose type variable isn't bound
-               -- up with one of the non-standard classes
-       (std_oks, std_bads)     = partition worth_a_try std_groups
-       worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
-       non_std_tyvars          = unionVarSets (map tyVarsOfInst non_stds)
-
-               -- Collect together all the bad guys
-       bad_guys               = non_stds ++ concat std_bads
-       (bad_ips, non_ips)     = partition isIPDict bad_guys
-       (no_insts, ambigs)     = partition no_inst non_ips
-       no_inst d              = not (isTyVarDict d) 
-       -- Previously, there was a more elaborate no_inst definition:
-       --      no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
-       --      fixed_tvs = oclose (fdPredsOfInsts tidy_dicts) emptyVarSet
-       -- But that seems over-elaborate to me; it only bites for class decls with
-       -- fundeps like this:           class C a b | -> b where ...
-    in
+           (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
-    groupErrs (addNoInstanceErrs Nothing []) no_insts  `thenM_`
-    addTopIPErrs bad_ips                               `thenM_`
+       ; 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
-    ifErrsM (returnM []) (
-       
-       -- Complain about the ones that don't fall under
-       -- the Haskell rules for disambiguation
-       -- This group includes both non-existent instances
-       --      e.g. Num (IO a) and Eq (Int -> Int)
-       -- and ambiguous dictionaries
-       --      e.g. Num a
-       addTopAmbigErrs ambigs          `thenM_`
-
-       -- Disambiguate the ones that look feasible
-        mappM (disambigGroup is_interactive) std_oks
-    )                                  `thenM` \ binds_ambig ->
-
-    returnM (binds `unionBags` unionManyBags binds_ambig)
+       -- 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
@@ -1923,7 +2164,7 @@ disambigGroup is_interactive dicts
        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) ->
+                        reduceMe dicts                 `thenM` \ (frees, binds, ambigs) ->
        WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
        warnDefault dicts default_ty                    `thenM_`
        returnM binds
@@ -1996,11 +2237,11 @@ tcSimplifyDeriv :: [TyVar]
                -> TcM ThetaType        -- Needed
 
 tcSimplifyDeriv tyvars theta
-  = tcInstTyVars VanillaTv tyvars                      `thenM` \ (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)    `thenM` \ wanteds ->
+    newDicts DerivOrigin (substTheta tenv theta)       `thenM` \ wanteds ->
     simpleReduceLoop doc reduceMe wanteds              `thenM` \ (frees, _, irreds) ->
     ASSERT( null frees )                       -- reduceMe never returns Free
 
@@ -2032,7 +2273,7 @@ tcSimplifyDeriv tyvars theta
          -- of problems; in particular, it's hard to compare solutions for
          -- equality when finding the fixpoint.  So I just rule it out for now.
   
-       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
@@ -2054,7 +2295,7 @@ tcSimplifyDefault :: ThetaType    -- Wanted; has no type variables in it
                  -> TcM ()
 
 tcSimplifyDefault theta
-  = newDicts DataDeclOrigin theta              `thenM` \ wanteds ->
+  = newDicts DefaultOrigin theta               `thenM` \ wanteds ->
     simpleReduceLoop doc reduceMe wanteds      `thenM` \ (frees, _, irreds) ->
     ASSERT( null frees )       -- try_me never returns Free
     addNoInstanceErrs Nothing []  irreds       `thenM_`
@@ -2107,13 +2348,27 @@ addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
 plural [x] = empty
 plural xs  = char 's'
 
-addTopIPErrs 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 <+> pprInsts tidy_dicts)
+                                    plural tidy_dicts <+> pprDictsTheta tidy_dicts)
 
 addNoInstanceErrs :: Maybe SDoc        -- Nothing => top level
                                -- Just d => d describes the construct
@@ -2125,7 +2380,6 @@ addNoInstanceErrs mb_what givens []
 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)
-       -- The first thing we do is separate them
     getDOpts           `thenM` \ dflags ->
     tcGetInstEnvs      `thenM` \ inst_envs ->
     let
@@ -2140,56 +2394,69 @@ addNoInstanceErrs mb_what givens dicts
          | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
          | otherwise
          = case lookupInstEnv dflags inst_envs clas tys of
-               res@(ms, _) 
-                 | length ms > 1 -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
-                 | otherwise     -> (overlap_doc, dict : no_inst_dicts)        -- No match
-               -- NB: there can be exactly one match, in the case where we have
-               --      instance C a where ...
-               -- (In this case, lookupInst doesn't bother to look up, 
-               --  unless -fallow-undecidable-instances is set.)
-               -- So we report this as "no instance" rather than "overlap"; the fix is
-               -- to specify -fallow-undecidable-instances, but we leave that to the programmer!
+               -- 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
-    mk_probable_fix tidy_env2 mb_what no_inst_dicts    `thenM` \ (tidy_env3, probable_fix) ->
+       
+       -- 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") <+> pprInsts no_inst_dicts
-               | otherwise   = sep [ptext SLIT("Could not deduce") <+> pprInsts no_inst_dicts,
-                                    nest 2 $ ptext SLIT("from the context") <+> pprInsts tidy_givens]
+                               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") <+> ppr dict)),
+      = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") 
+                                       <+> pprPred (dictPred dict))),
                sep [ptext SLIT("Matching instances") <> colon,
-                    nest 2 (pprDFuns (dfuns ++ unifiers))],
-               if null unifiers 
-               then empty
-               else parens (ptext SLIT("The choice depends on the instantiation of") <+>
-                            quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))))]
+                    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]
 
-    mk_probable_fix tidy_env Nothing dicts     -- Top level
-      = mkMonomorphismMsg tidy_env dicts
-    mk_probable_fix tidy_env (Just what) dicts -- Nested (type signatures, instance decls)
-      = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 fix1, nest 2 fix2])
+    mk_probable_fix tidy_env dicts     
+      = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 (vcat fixes)])
       where
-       fix1 = sep [ptext SLIT("Add") <+> pprInsts dicts,
-                   ptext SLIT("to the") <+> what]
+       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 = empty
-            | otherwise           = ptext SLIT("Or add an instance declaration for")
-                                    <+> pprInsts instance_dicts
+       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
@@ -2203,40 +2470,39 @@ addTopAmbigErrs dicts
     
     report :: [(Inst,[TcTyVar])] -> TcM ()
     report pairs@((inst,tvs) : _)      -- The pairs share a common set of ambiguous tyvars
-       = mkMonomorphismMsg tidy_env dicts      `thenM` \ (tidy_env, mono_msg) ->
-         addSrcSpan (instLocSrcSpan (instLoc inst)) $
+       = 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 (pprInstsInFull dicts)]
-         in_msg | isSingleton dicts = text "in the top-level constraint:"
-                | otherwise         = text "in these top-level constraints:"
+                         pprQuotedList tvs <+> in_msg,
+                    nest 2 (pprDictsInFull dicts)]
+         in_msg = text "in the constraint" <> plural dicts <> colon
 
 
-mkMonomorphismMsg :: TidyEnv -> [Inst] -> TcM (TidyEnv, Message)
+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 insts
-  | isEmptyVarSet inst_tvs
-  = returnM (tidy_env, empty)
-  | otherwise
-  = findGlobals inst_tvs tidy_env      `thenM` \ (tidy_env, docs) ->
+mkMonomorphismMsg tidy_env inst_tvs
+  = findGlobals (mkVarSet inst_tvs) tidy_env   `thenM` \ (tidy_env, docs) ->
     returnM (tidy_env, mk_msg docs)
-
   where
-    inst_tvs = tyVarsOfInsts insts
-
-    mk_msg []   = empty                -- This happens in things like
-                               --      f x = show (read "foo")
-                               -- whre monomorphism doesn't play any role
+    mk_msg []   = 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),
-                       ptext SLIT("Probable fix: give these definition(s) an explicit type signature")]
+                       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
   = doptM Opt_WarnTypeDefaults  `thenM` \ warn_flag ->
@@ -2246,7 +2512,7 @@ warnDefault dicts default_ty
     (_, tidy_dicts) = tidyInsts dicts
     warn_msg  = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
                                quotes (ppr default_ty),
-                     pprInstsInFull tidy_dicts]
+                     pprDictsInFull tidy_dicts]
 
 -- Used for the ...Thetas variants; all top level
 badDerivedPred pred
@@ -2257,7 +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)]
+         nest 4 (pprStack stack)]
 
-reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
+pprStack stack = vcat (map pprInstInFull stack)
 \end{code}