Properly ppr InstEqs in wanteds of implication constraints
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index d481146..aff019e 100644 (file)
@@ -6,6 +6,13 @@
 TcSimplify
 
 \begin{code}
 TcSimplify
 
 \begin{code}
+{-# OPTIONS -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
 module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,
 module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,
@@ -15,7 +22,9 @@ module TcSimplify (
        tcSimplifyBracket, tcSimplifyCheckPat,
 
        tcSimplifyDeriv, tcSimplifyDefault,
        tcSimplifyBracket, tcSimplifyCheckPat,
 
        tcSimplifyDeriv, tcSimplifyDefault,
-       bindInstsOfLocalFuns, bindIrreds,
+       bindInstsOfLocalFuns, 
+
+        misMatchMsg
     ) where
 
 #include "HsVersions.h"
     ) where
 
 #include "HsVersions.h"
@@ -31,6 +40,8 @@ import TcGadt
 import TcType
 import TcMType
 import TcIface
 import TcType
 import TcMType
 import TcIface
+import TcTyFuns
+import TypeRep
 import Var
 import Name
 import NameSet
 import Var
 import Name
 import NameSet
@@ -44,12 +55,14 @@ import ErrUtils
 import BasicTypes
 import VarSet
 import VarEnv
 import BasicTypes
 import VarSet
 import VarEnv
+import Module
 import FiniteMap
 import Bag
 import Outputable
 import Maybes
 import ListSetOps
 import Util
 import FiniteMap
 import Bag
 import Outputable
 import Maybes
 import ListSetOps
 import Util
+import UniqSet
 import SrcLoc
 import DynFlags
 
 import SrcLoc
 import DynFlags
 
@@ -398,14 +411,19 @@ over implicit parameters. See the predicate isFreeWhenInferring.
 
 Note [Implicit parameters and ambiguity] 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Note [Implicit parameters and ambiguity] 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What type should we infer for this?
-       f x = (show ?y, x::Int)
-Since we must quantify over the ?y, the most plausible type is
-       f :: (Show a, ?y::a) => Int -> (String, Int)
-But notice that the type of the RHS is (String,Int), with no type 
-varibables mentioned at all!  The type of f looks ambiguous.  But
-it isn't, because at a call site we might have
-       let ?y = 5::Int in f 7
+Only a *class* predicate can give rise to ambiguity
+An *implicit parameter* cannot.  For example:
+       foo :: (?x :: [a]) => Int
+       foo = length ?x
+is fine.  The call site will suppply a particular 'x'
+
+Furthermore, the type variables fixed by an implicit parameter
+propagate to the others.  E.g.
+       foo :: (Show a, ?x::[a]) => Int
+       foo = show (?x++?x)
+The type of foo looks ambiguous.  But it isn't, because at a call site
+we might have
+       let ?x = 5::Int in foo
 and all is well.  In effect, implicit parameters are, well, parameters,
 so we can take their type variables into account as part of the
 "tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
 and all is well.  In effect, implicit parameters are, well, parameters,
 so we can take their type variables into account as part of the
 "tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
@@ -638,54 +656,79 @@ tcSimplifyInfer
 
 \begin{code}
 tcSimplifyInfer doc tau_tvs wanted
 
 \begin{code}
 tcSimplifyInfer doc tau_tvs wanted
-  = do { tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
-       ; wanted' <- mappM zonkInst wanted      -- Zonk before deciding quantified tyvars
+  = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+       ; wanted'  <- mappM zonkInst wanted     -- Zonk before deciding quantified tyvars
        ; gbl_tvs  <- tcGetGlobalTyVars
        ; gbl_tvs  <- tcGetGlobalTyVars
-       ; let preds = fdPredsOfInsts wanted'
-             qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
+       ; let preds1   = fdPredsOfInsts wanted'
+             gbl_tvs1 = oclose preds1 gbl_tvs
+             qtvs     = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1
                        -- See Note [Choosing which variables to quantify]
 
                -- To maximise sharing, remove from consideration any 
                -- constraints that don't mention qtvs at all
                        -- See Note [Choosing which variables to quantify]
 
                -- To maximise sharing, remove from consideration any 
                -- constraints that don't mention qtvs at all
-       ; let (free1, bound) = partition (isFreeWhenInferring qtvs) wanted'
-       ; extendLIEs free1
+       ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
+       ; extendLIEs free
 
                -- To make types simple, reduce as much as possible
 
                -- To make types simple, reduce as much as possible
-       ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ 
-                  ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound))
+       ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$ 
+                  ppr gbl_tvs1 $$ ppr free $$ ppr bound))
        ; (irreds1, binds1) <- tryHardCheckLoop doc bound
 
                -- Note [Inference and implication constraints]
        ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
        ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
 
        ; (irreds1, binds1) <- tryHardCheckLoop doc bound
 
                -- Note [Inference and implication constraints]
        ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
        ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
 
-               -- By now improvment may have taken place, and we must *not*
-               -- quantify over any variable free in the environment
-               -- tc137 (function h inside g) is an example
-       ; gbl_tvs <- tcGetGlobalTyVars
-       ; qtvs1 <- zonkTcTyVarsAndFV (varSetElems qtvs)
-       ; qtvs2 <- zonkQuantifiedTyVars (varSetElems (qtvs1 `minusVarSet` gbl_tvs))
-
-               -- Do not quantify over constraints that *now* do not
-               -- mention quantified type variables, because they are
-               -- simply ambiguous (or might be bound further out).  Example:
-               --      f :: Eq b => a -> (a, b)
-               --      g x = fst (f x)
-               -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
-               -- We decide to quantify over 'alpha' alone, but free1 does not include f77
-               -- because f77 mentions 'alpha'.  Then reducing leaves only the (ambiguous)
-               -- constraint (Eq beta), which we dump back into the free set
-               -- See test tcfail181
-       ; let (free3, irreds3) = partition (isFreeWhenInferring (mkVarSet qtvs2)) irreds2
-       ; extendLIEs free3
-       
+               -- Now work out all over again which type variables to quantify,
+               -- exactly in the same way as before, but starting from irreds2.  Why?
+               -- a) By now improvment may have taken place, and we must *not*
+               --    quantify over any variable free in the environment
+               --    tc137 (function h inside g) is an example
+               --
+               -- b) Do not quantify over constraints that *now* do not
+               --    mention quantified type variables, because they are
+               --    simply ambiguous (or might be bound further out).  Example:
+               --      f :: Eq b => a -> (a, b)
+               --      g x = fst (f x)
+               --    From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
+               --    We decide to quantify over 'alpha' alone, but free1 does not include f77
+               --    because f77 mentions 'alpha'.  Then reducing leaves only the (ambiguous)
+               --    constraint (Eq beta), which we dump back into the free set
+               --    See test tcfail181
+               --
+               -- c) irreds may contain type variables not previously mentioned,
+               --    e.g.  instance D a x => Foo [a] 
+               --          wanteds = Foo [a]
+               --       Then after simplifying we'll get (D a x), and x is fresh
+               --       We must quantify over x else it'll be totally unbound
+       ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)
+       ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1)
+               -- Note that we start from gbl_tvs1
+               -- We use tcGetGlobalTyVars, then oclose wrt preds2, because
+               -- we've already put some of the original preds1 into frees
+               -- E.g.         wanteds = C a b   (where a->b)
+               --              gbl_tvs = {a}
+               --              tau_tvs = {b}
+               -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
+               -- irreds2 will be empty.  But we don't want to generalise over b!
+       ; let preds2 = fdPredsOfInsts irreds2   -- irreds2 is zonked
+             qtvs   = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
+       ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
+       ; extendLIEs free
+
+               -- Turn the quantified meta-type variables into real type variables
+       ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
+
                -- We can't abstract over any remaining unsolved 
                -- implications so instead just float them outwards. Ugh.
                -- We can't abstract over any remaining unsolved 
                -- implications so instead just float them outwards. Ugh.
-       ; let (q_dicts, implics) = partition isDict irreds3
+       ; let (q_dicts0, implics) = partition isAbstractableInst irreds3
        ; loc <- getInstLoc (ImplicOrigin doc)
        ; loc <- getInstLoc (ImplicOrigin doc)
-       ; implic_bind <- bindIrreds loc qtvs2 q_dicts implics
+       ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics
+
+               -- Prepare equality instances for quantification
+       ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
+       ; q_eqs <- mappM finalizeEqInst q_eqs0
 
 
-       ; return (qtvs2, q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
+       ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
        -- NB: when we are done, we might have some bindings, but
        -- the final qtvs might be empty.  See Note [NO TYVARS] below.
 
        -- NB: when we are done, we might have some bindings, but
        -- the final qtvs might be empty.  See Note [NO TYVARS] below.
 
@@ -718,6 +761,8 @@ approximateImplications doc want_dict irreds
        = [ d | let tv_set = mkVarSet tvs
              , d <- get_dicts wanteds 
              , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
        = [ d | let tv_set = mkVarSet tvs
              , d <- get_dicts wanteds 
              , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
+    get_dict i@(EqInst {}) | want_dict i = [i]
+                          | otherwise   = [] 
     get_dict other = pprPanic "approximateImplications" (ppr other)
 \end{code}
 
     get_dict other = pprPanic "approximateImplications" (ppr other)
 \end{code}
 
@@ -736,7 +781,7 @@ with 'given' implications.
 
 So our best approximation is to make (D [a]) part of the inferred
 context, so we can use that to discharge the implication. Hence
 
 So our best approximation is to make (D [a]) part of the inferred
 context, so we can use that to discharge the implication. Hence
-the strange function get_dictsin approximateImplications.
+the strange function get_dicts in approximateImplications.
 
 The common cases are more clear-cut, when we have things like
        forall a. C a => C b
 
 The common cases are more clear-cut, when we have things like
        forall a. C a => C b
@@ -760,7 +805,8 @@ tcSimplifyInferCheck
                 TcDictBinds)   -- Bindings
 
 tcSimplifyInferCheck loc tau_tvs givens wanteds
                 TcDictBinds)   -- Bindings
 
 tcSimplifyInferCheck loc tau_tvs givens wanteds
-  = do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
+  = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
+       ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
 
        -- Figure out which type variables to quantify over
        -- You might think it should just be the signature tyvars,
 
        -- Figure out which type variables to quantify over
        -- You might think it should just be the signature tyvars,
@@ -784,6 +830,7 @@ tcSimplifyInferCheck loc tau_tvs givens wanteds
                -- Now we are back to normal (c.f. tcSimplCheck)
        ; implic_bind <- bindIrreds loc qtvs' givens irreds
 
                -- Now we are back to normal (c.f. tcSimplCheck)
        ; implic_bind <- bindIrreds loc qtvs' givens irreds
 
+       ; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind))
        ; return (qtvs', binds `unionBags` implic_bind) }
 \end{code}
 
        ; return (qtvs', binds `unionBags` implic_bind) }
 \end{code}
 
@@ -866,7 +913,8 @@ tcSimplifyCheck     :: InstLoc
                -> TcM TcDictBinds      -- Bindings
 tcSimplifyCheck loc qtvs givens wanteds 
   = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
                -> TcM TcDictBinds      -- Bindings
 tcSimplifyCheck loc qtvs givens wanteds 
   = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
-    do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
+    do { traceTc (text "tcSimplifyCheck")
+       ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
        ; implic_bind <- bindIrreds loc qtvs givens irreds
        ; return (binds `unionBags` implic_bind) }
 
        ; implic_bind <- bindIrreds loc qtvs givens irreds
        ; return (binds `unionBags` implic_bind) }
 
@@ -880,7 +928,8 @@ tcSimplifyCheckPat :: InstLoc
                   -> TcM TcDictBinds   -- Bindings
 tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
   = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
                   -> TcM TcDictBinds   -- Bindings
 tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
   = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
-    do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
+    do { traceTc (text "tcSimplifyCheckPat")
+       ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
        ; implic_bind <- bindIrredsR loc qtvs co_vars reft 
                                    givens irreds
        ; return (binds `unionBags` implic_bind) }
        ; implic_bind <- bindIrredsR loc qtvs co_vars reft 
                                    givens irreds
        ; return (binds `unionBags` implic_bind) }
@@ -901,8 +950,10 @@ bindIrredsR loc qtvs co_vars reft givens irreds
   | null irreds
   = return emptyBag
   | otherwise
   | null irreds
   = return emptyBag
   | otherwise
-  = do { let givens' = filter isDict givens
-               -- The givens can include methods
+  = do { let givens' = filter isAbstractableInst givens
+               -- The givens can (redundantly) include methods
+               -- We want to retain both EqInsts and Dicts
+               -- There should be no implicadtion constraints
                -- See Note [Pruning the givens in an implication constraint]
 
           -- If there are no 'givens' *and* the refinement is empty
                -- See Note [Pruning the givens in an implication constraint]
 
           -- If there are no 'givens' *and* the refinement is empty
@@ -939,31 +990,41 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
 -- This binding must line up the 'rhs' in reduceImplication
 makeImplicationBind loc all_tvs reft
                    givens      -- Guaranteed all Dicts
 -- This binding must line up the 'rhs' in reduceImplication
 makeImplicationBind loc all_tvs reft
                    givens      -- Guaranteed all Dicts
+                               -- or EqInsts
                    irreds
  | null irreds                 -- If there are no irreds, we are done
  = return ([], emptyBag)
  | otherwise                   -- Otherwise we must generate a binding
  = do  { uniq <- newUnique 
        ; span <- getSrcSpanM
                    irreds
  | null irreds                 -- If there are no irreds, we are done
  = return ([], emptyBag)
  | otherwise                   -- Otherwise we must generate a binding
  = do  { uniq <- newUnique 
        ; span <- getSrcSpanM
+       ; let (eq_givens, dict_givens) = partition isEqInst givens
+             eq_tyvar_cos = mkTyVarTys (varSetElems $ tyVarsOfTypes $ map eqInstType eq_givens)
+               -- Urgh! See line 2187 or thereabouts.  I believe that all these
+               -- 'givens' must be a simple CoVar.  This MUST be cleaned up.
+
        ; let name = mkInternalName uniq (mkVarOcc "ic") span
              implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
                                         tci_tyvars = all_tvs, 
        ; let name = mkInternalName uniq (mkVarOcc "ic") span
              implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
                                         tci_tyvars = all_tvs, 
-                                        tci_given = givens,
+                                        tci_given = (eq_givens ++ dict_givens),
                                         tci_wanted = irreds, tci_loc = loc }
                                         tci_wanted = irreds, tci_loc = loc }
-
-       ; let n_irreds = length irreds
-             irred_ids = map instToId irreds
-             tup_ty = mkTupleTy Boxed n_irreds (map idType irred_ids)
-             pat = TuplePat (map nlVarPat irred_ids) Boxed tup_ty
+       ; let   -- only create binder for dict_irreds
+             (eq_irreds, dict_irreds) = partition isEqInst irreds
+              n_dict_irreds = length dict_irreds
+             dict_irred_ids = map instToId dict_irreds
+             tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
+             pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty
              rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
              rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
-             co  = mkWpApps (map instToId givens) <.> mkWpTyApps (mkTyVarTys all_tvs)
-             bind | n_irreds==1 = VarBind (head irred_ids) rhs
-                  | otherwise   = PatBind { pat_lhs = L span pat, 
-                                            pat_rhs = unguardedGRHSs rhs, 
-                                            pat_rhs_ty = tup_ty,
-                                            bind_fvs = placeHolderNames }
-       ; -- pprTrace "Make implic inst" (ppr implic_inst) $
-         return ([implic_inst], unitBag (L span bind)) }
+             co  = mkWpApps (map instToId dict_givens)
+                   <.> mkWpTyApps eq_tyvar_cos
+                   <.> mkWpTyApps (mkTyVarTys all_tvs)
+             bind | [dict_irred_id] <- dict_irred_ids  = VarBind dict_irred_id rhs
+                  | otherwise        = PatBind { pat_lhs = L span pat, 
+                                                 pat_rhs = unguardedGRHSs rhs, 
+                                                 pat_rhs_ty = tup_ty,
+                                                 bind_fvs = placeHolderNames }
+       ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
+       ; return ([implic_inst], unitBag (L span bind)) 
+        }
 
 -----------------------------------------------------------
 tryHardCheckLoop :: SDoc
 
 -----------------------------------------------------------
 tryHardCheckLoop :: SDoc
@@ -971,7 +1032,9 @@ tryHardCheckLoop :: SDoc
             -> TcM ([Inst], TcDictBinds)
 
 tryHardCheckLoop doc wanteds
             -> TcM ([Inst], TcDictBinds)
 
 tryHardCheckLoop doc wanteds
-  = checkLoop (mkRedEnv doc try_me []) wanteds
+  = do { (irreds,binds,_) <- checkLoop (mkRedEnv doc try_me []) wanteds
+       ; return (irreds,binds)
+       }
   where
     try_me inst = ReduceMe AddSCs
        -- Here's the try-hard bit
   where
     try_me inst = ReduceMe AddSCs
        -- Here's the try-hard bit
@@ -983,7 +1046,9 @@ gentleCheckLoop :: InstLoc
               -> TcM ([Inst], TcDictBinds)
 
 gentleCheckLoop inst_loc givens wanteds
               -> TcM ([Inst], TcDictBinds)
 
 gentleCheckLoop inst_loc givens wanteds
-  = checkLoop env wanteds
+  = do { (irreds,binds,_) <- checkLoop env wanteds
+       ; return (irreds,binds)
+       }
   where
     env = mkRedEnv (pprInstLoc inst_loc) try_me givens
 
   where
     env = mkRedEnv (pprInstLoc inst_loc) try_me givens
 
@@ -991,6 +1056,16 @@ gentleCheckLoop inst_loc givens wanteds
                | otherwise          = Stop
        -- When checking against a given signature 
        -- we MUST be very gentle: Note [Check gently]
                | otherwise          = Stop
        -- When checking against a given signature 
        -- we MUST be very gentle: Note [Check gently]
+
+gentleInferLoop :: SDoc -> [Inst]
+               -> TcM ([Inst], TcDictBinds)
+gentleInferLoop doc wanteds
+  = do         { (irreds, binds, _) <- checkLoop env wanteds
+       ; return (irreds, binds) }
+  where
+    env = mkRedEnv doc try_me []
+    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+               | otherwise          = Stop
 \end{code}
 
 Note [Check gently]
 \end{code}
 
 Note [Check gently]
@@ -1008,7 +1083,7 @@ Inside the pattern match, which binds (a:*, x:a), we know that
 Hence we have a dictionary for Show [a] available; and indeed we 
 need it.  We are going to build an implication contraint
        forall a. (b~[a]) => Show [a]
 Hence we have a dictionary for Show [a] available; and indeed we 
 need it.  We are going to build an implication contraint
        forall a. (b~[a]) => Show [a]
-Later, we will solve this constraint using the knowledg e(Show b)
+Later, we will solve this constraint using the knowledge (Show b)
        
 But we MUST NOT reduce (Show [a]) to (Show a), else the whole
 thing becomes insoluble.  So we simplify gently (get rid of literals
        
 But we MUST NOT reduce (Show [a]) to (Show a), else the whole
 thing becomes insoluble.  So we simplify gently (get rid of literals
@@ -1021,28 +1096,68 @@ with tryHardCheckLooop.
 -----------------------------------------------------------
 checkLoop :: RedEnv
          -> [Inst]                     -- Wanted
 -----------------------------------------------------------
 checkLoop :: RedEnv
          -> [Inst]                     -- Wanted
-         -> TcM ([Inst], TcDictBinds)
+         -> TcM ([Inst], TcDictBinds,
+                 [Inst])               -- needed givens
 -- Precondition: givens are completely rigid
 -- Postcondition: returned Insts are zonked
 
 checkLoop env wanteds
 -- Precondition: givens are completely rigid
 -- Postcondition: returned Insts are zonked
 
 checkLoop env wanteds
-  = do { -- Givens are skolems, so no need to zonk them
-        wanteds' <- mappM zonkInst wanteds
+  = go env wanteds []
+  where go env wanteds needed_givens
+         = do {  -- We do need to zonk the givens; cf Note [Zonking RedEnv]
+                ; env'     <- zonkRedEnv env
+               ; wanteds' <- zonkInsts  wanteds
+       
+               ; (improved, binds, irreds, more_needed_givens) <- reduceContext env' wanteds'
 
 
-       ; (improved, binds, irreds) <- reduceContext env wanteds'
+               ; let all_needed_givens = needed_givens ++ more_needed_givens
+       
+               ; if not improved then
+                    return (irreds, binds, all_needed_givens)
+                 else do
+       
+               -- If improvement did some unification, we go round again.
+               -- We start again with irreds, not wanteds
+               -- Using an instance decl might have introduced a fresh type variable
+               -- which might have been unified, so we'd get an infinite loop
+               -- if we started again with wanteds!  See Note [LOOP]
+               { (irreds1, binds1, all_needed_givens1) <- go env' irreds all_needed_givens
+               ; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
+\end{code}
 
 
-       ; if not improved then
-            return (irreds, binds)
-         else do
+Note [Zonking RedEnv]
+~~~~~~~~~~~~~~~~~~~~~
+It might appear as if the givens in RedEnv are always rigid, but that is not
+necessarily the case for programs involving higher-rank types that have class
+contexts constraining the higher-rank variables.  An example from tc237 in the
+testsuite is
+
+  class Modular s a | s -> a
+
+  wim ::  forall a w. Integral a 
+                        => a -> (forall s. Modular s a => M s w) -> w
+  wim i k = error "urk"
+
+  test5  ::  (Modular s a, Integral a) => M s a
+  test5  =   error "urk"
+
+  test4   =   wim 4 test4'
+
+Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
+quantified further outside.  When type checking test4, we have to check
+whether the signature of test5 is an instance of 
+
+  (forall s. Modular s a => M s w)
+
+Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
+givens. 
+
+Given the FD of Modular in this example, class improvement will instantiate
+t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
+Modular s a predicate in that signature).  If we don't zonk (Modular s t_a) in
+the givens, we will get into a loop as improveOne uses the unification engine
+TcGadt.tcUnifyTys, which doesn't know about mutable type variables.
 
 
-       -- If improvement did some unification, we go round again.
-       -- We start again with irreds, not wanteds
-       -- Using an instance decl might have introduced a fresh type variable
-       -- which might have been unified, so we'd get an infinite loop
-       -- if we started again with wanteds!  See Note [LOOP]
-       { (irreds1, binds1) <- checkLoop env irreds
-       ; return (irreds1, binds `unionBags` binds1) } }
-\end{code}
 
 Note [LOOP]
 ~~~~~~~~~~~
 
 Note [LOOP]
 ~~~~~~~~~~~
@@ -1114,7 +1229,8 @@ tcSimplifySuperClasses
        -> [Inst]       -- Wanted
        -> TcM TcDictBinds
 tcSimplifySuperClasses loc givens sc_wanteds
        -> [Inst]       -- Wanted
        -> TcM TcDictBinds
 tcSimplifySuperClasses loc givens sc_wanteds
-  = do { (irreds, binds1) <- checkLoop env sc_wanteds
+  = do { traceTc (text "tcSimplifySuperClasses")
+       ; (irreds,binds1,_) <- checkLoop env sc_wanteds
        ; let (tidy_env, tidy_irreds) = tidyInsts irreds
        ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
        ; return binds1 }
        ; let (tidy_env, tidy_irreds) = tidyInsts irreds
        ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
        ; return binds1 }
@@ -1241,7 +1357,8 @@ tcSimplifyRestricted      -- Used for restricted binding groups
 
 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- Zonk everything in sight
 
 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- Zonk everything in sight
-  = do { wanteds' <- mappM zonkInst wanteds
+  = do { traceTc (text "tcSimplifyRestricted")
+       ; wanteds' <- zonkInsts wanteds
 
        -- 'ReduceMe': Reduce as far as we can.  Don't stop at
        -- dicts; the idea is to get rid of as many type
 
        -- 'ReduceMe': Reduce as far as we can.  Don't stop at
        -- dicts; the idea is to get rid of as many type
@@ -1253,12 +1370,12 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- HOWEVER, some unification may take place, if we instantiate
        --          a method Inst with an equality constraint
        ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
        -- HOWEVER, some unification may take place, if we instantiate
        --          a method Inst with an equality constraint
        ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
-       ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
+       ; (_imp, _binds, constrained_dicts, _) <- reduceContext env wanteds'
 
        -- Next, figure out the tyvars we will quantify over
        ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
        ; gbl_tvs' <- tcGetGlobalTyVars
 
        -- Next, figure out the tyvars we will quantify over
        ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
        ; gbl_tvs' <- tcGetGlobalTyVars
-       ; constrained_dicts' <- mappM zonkInst constrained_dicts
+       ; constrained_dicts' <- zonkInsts constrained_dicts
 
        ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
                                -- As in tcSimplifyInfer
 
        ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
                                -- As in tcSimplifyInfer
@@ -1302,7 +1419,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
                           (is_nested_group || isDict inst) = Stop
                          | otherwise            = ReduceMe AddSCs
              env = mkNoImproveRedEnv doc try_me
                           (is_nested_group || isDict inst) = Stop
                          | otherwise            = ReduceMe AddSCs
              env = mkNoImproveRedEnv doc try_me
-       ; (_imp, binds, irreds) <- reduceContext env wanteds'
+       ; (_imp, binds, irreds, _) <- reduceContext env wanteds'
 
        -- See "Notes on implicit parameters, Question 4: top level"
        ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured
 
        -- See "Notes on implicit parameters, Question 4: top level"
        ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured
@@ -1392,7 +1509,8 @@ tcSimplifyRuleLhs wanteds
                                 -- to fromInteger; this looks fragile to me
             ; lookup_result <- lookupSimpleInst w'
             ; case lookup_result of
                                 -- to fromInteger; this looks fragile to me
             ; lookup_result <- lookupSimpleInst w'
             ; case lookup_result of
-                GenInst ws' rhs -> go dicts (addBind binds (instToId w) rhs) (ws' ++ ws)
+                GenInst ws' rhs -> 
+                   go dicts (addInstToDictBind binds w rhs) (ws' ++ ws)
                 NoInstance      -> pprPanic "tcSimplifyRuleLhs" (ppr w)
          }
 \end{code}
                 NoInstance      -> pprPanic "tcSimplifyRuleLhs" (ppr w)
          }
 \end{code}
@@ -1445,12 +1563,12 @@ tcSimplifyIPs :: [Inst]         -- The implicit parameters bound here
        -- makes them the same.
 
 tcSimplifyIPs given_ips wanteds
        -- makes them the same.
 
 tcSimplifyIPs given_ips wanteds
-  = do { wanteds'   <- mappM zonkInst wanteds
-       ; given_ips' <- mappM zonkInst given_ips
+  = do { wanteds'   <- zonkInsts wanteds
+       ; given_ips' <- zonkInsts given_ips
                -- Unusually for checking, we *must* zonk the given_ips
 
        ; let env = mkRedEnv doc try_me given_ips'
                -- Unusually for checking, we *must* zonk the given_ips
 
        ; let env = mkRedEnv doc try_me given_ips'
-       ; (improved, binds, irreds) <- reduceContext env wanteds'
+       ; (improved, binds, irreds, _) <- reduceContext env wanteds'
 
        ; if not improved then 
                ASSERT( all is_free irreds )
 
        ; if not improved then 
                ASSERT( all is_free irreds )
@@ -1510,12 +1628,11 @@ bindInstsOfLocalFuns wanteds local_ids
     returnM emptyLHsBinds
 
   | otherwise
     returnM emptyLHsBinds
 
   | otherwise
-  = do { (irreds, binds) <- checkLoop env for_me
+  = do { (irreds, binds) <- gentleInferLoop doc for_me
        ; extendLIEs not_for_me 
        ; extendLIEs irreds
        ; return binds }
   where
        ; extendLIEs not_for_me 
        ; extendLIEs irreds
        ; return binds }
   where
-    env = mkRedEnv doc try_me []
     doc                     = text "bindInsts" <+> ppr local_ids
     overloaded_ids   = filter is_overloaded local_ids
     is_overloaded id = isOverloadedTy (idType id)
     doc                     = text "bindInsts" <+> ppr local_ids
     overloaded_ids   = filter is_overloaded local_ids
     is_overloaded id = isOverloadedTy (idType id)
@@ -1524,8 +1641,6 @@ bindInstsOfLocalFuns wanteds local_ids
     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
     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 | isMethod inst = ReduceMe NoSCs
-               | otherwise     = Stop
 \end{code}
 
 
 \end{code}
 
 
@@ -1545,6 +1660,8 @@ data RedEnv
           , red_givens :: [Inst]               -- All guaranteed rigid
                                                -- Always dicts
                                                -- but see Note [Rigidity]
           , red_givens :: [Inst]               -- All guaranteed rigid
                                                -- Always dicts
                                                -- but see Note [Rigidity]
+          , red_reft :: Refinement             -- The refinement to apply to the 'givens'
+                                               -- You should think of it as 'given equalities'
           , red_stack  :: (Int, [Inst])        -- Recursion stack (for err msg)
                                                -- See Note [RedStack]
   }
           , red_stack  :: (Int, [Inst])        -- Recursion stack (for err msg)
                                                -- See Note [RedStack]
   }
@@ -1566,14 +1683,17 @@ data RedEnv
 mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
 mkRedEnv doc try_me givens
   = RedEnv { red_doc = doc, red_try_me = try_me,
 mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
 mkRedEnv doc try_me givens
   = RedEnv { red_doc = doc, red_try_me = try_me,
-            red_givens = givens, red_stack = (0,[]),
+            red_givens = givens, 
+            red_reft = emptyRefinement,
+            red_stack = (0,[]),
             red_improve = True }       
 
 mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
 -- Do not do improvement; no givens
 mkNoImproveRedEnv doc try_me
   = RedEnv { red_doc = doc, red_try_me = try_me,
             red_improve = True }       
 
 mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
 -- Do not do improvement; no givens
 mkNoImproveRedEnv doc try_me
   = RedEnv { red_doc = doc, red_try_me = try_me,
-            red_givens = [], red_stack = (0,[]),
+            red_givens = [], red_reft = emptyRefinement,
+            red_stack = (0,[]),
             red_improve = True }       
 
 data WhatToDo
             red_improve = True }       
 
 data WhatToDo
@@ -1591,21 +1711,41 @@ data WantSCs = NoSCs | AddSCs   -- Tells whether we should add the superclasses
                                -- of a predicate when adding it to the avails
        -- The reason for this flag is entirely the super-class loop problem
        -- Note [SUPER-CLASS LOOP 1]
                                -- of a predicate when adding it to the avails
        -- The reason for this flag is entirely the super-class loop problem
        -- Note [SUPER-CLASS LOOP 1]
+
+zonkRedEnv :: RedEnv -> TcM RedEnv
+zonkRedEnv env 
+  = do { givens' <- mappM zonkInst (red_givens env)
+       ; return $ env {red_givens = givens'}
+       }
 \end{code}
 
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \subsection[reduce]{@reduce@}
 %*                                                                     *
 %************************************************************************
 
 %************************************************************************
 %*                                                                     *
 \subsection[reduce]{@reduce@}
 %*                                                                     *
 %************************************************************************
 
+Note [Ancestor Equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+During context reduction, we add to the wanted equalities also those
+equalities that (transitively) occur in superclass contexts of wanted
+class constraints.  Consider the following code
+
+  class a ~ Int => C a
+  instance C Int
+
+If (C a) is wanted, we want to add (a ~ Int), which will be discharged by
+substituting Int for a.  Hence, we ultimately want (C Int), which we
+discharge with the explicit instance.
 
 \begin{code}
 reduceContext :: RedEnv
              -> [Inst]                 -- Wanted
              -> TcM (ImprovementDone,
                      TcDictBinds,      -- Dictionary bindings
 
 \begin{code}
 reduceContext :: RedEnv
              -> [Inst]                 -- Wanted
              -> TcM (ImprovementDone,
                      TcDictBinds,      -- Dictionary bindings
-                     [Inst])           -- Irreducible
+                     [Inst],           -- Irreducible
+                     [Inst])           -- Needed givens
 
 reduceContext env wanteds
   = do { traceTc (text "reduceContext" <+> (vcat [
 
 reduceContext env wanteds
   = do { traceTc (text "reduceContext" <+> (vcat [
@@ -1616,32 +1756,112 @@ reduceContext env wanteds
             text "----------------------"
             ]))
 
             text "----------------------"
             ]))
 
-        -- Build the Avail mapping from "givens"
-       ; init_state <- foldlM addGiven emptyAvails (red_givens env)
-
-        -- Do the real work
-       -- Process non-implication constraints first, so that they are
-       -- available to help solving the implication constraints
-       --      ToDo: seems a bit inefficient and ad-hoc
-       ; let (implics, rest) = partition isImplicInst wanteds
-       ; avails <- reduceList env (rest ++ implics) init_state
 
 
-       ; let improved = availsImproved avails
-       ; (binds, irreds) <- extractResults avails wanteds
+       ; let givens                       = red_givens env
+             (given_eqs0, given_dicts0)   = partition isEqInst givens
+             (wanted_eqs0, wanted_dicts0) = partition isEqInst wanteds
+
+          -- We want to add as wanted equalities those that (transitively) 
+          -- occur in superclass contexts of wanted class constraints.
+          -- See Note [Ancestor Equalities]
+       ; ancestor_eqs <- ancestorEqualities wanted_dicts0
+        ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
+       ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
+
+         -- 1. Normalise the *given* *equality* constraints
+       ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0
+
+         -- 2. Normalise the *given* *dictionary* constraints
+         --    wrt. the toplevel and given equations
+       ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs
+                                                            given_dicts0
+
+          -- 5. Build the Avail mapping from "given_dicts"
+         --    Add dicts refined by the current type refinement
+       ; (init_state, extra_givens) <- getLIE $ do 
+               { init_state <- foldlM addGiven emptyAvails given_dicts
+               ; let reft = red_reft env
+               ; if isEmptyRefinement reft then return init_state
+                 else foldlM (addRefinedGiven reft)
+                                   init_state given_dicts }
+
+       -- *** ToDo: what to do with the "extra_givens"?  For the
+       -- moment I'm simply discarding them, which is probably wrong
+
+         -- 7. Normalise the *wanted* *dictionary* constraints
+         --    wrt. the toplevel and given equations
+         -- NB: normalisation includes zonking as part of what it does
+         --     so it's important to do it after any unifications
+         --     that happened as a result of the addGivens
+       ; (wanted_dicts,normalise_binds1) <- normaliseWantedDicts given_eqs wanted_dicts0
+
+          -- 6. Solve the *wanted* *dictionary* constraints
+         --    This may expose some further equational constraints...
+       ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+       ; let (binds, irreds1, needed_givens) = extractResults avails wanted_dicts
+       ; traceTc $ text "reduceContext extractresults" <+> vcat
+                     [ppr avails,ppr wanted_dicts,ppr binds,ppr needed_givens]
+
+       -- *** ToDo: what to do with the "extra_eqs"?  For the
+       -- moment I'm simply discarding them, which is probably wrong
+
+         -- 3. Solve the *wanted* *equation* constraints
+       ; eq_irreds0 <- solveWantedEqs given_eqs wanted_eqs
+
+         -- 4. Normalise the *wanted* equality constraints with respect to
+         --    each other 
+       ; eq_irreds <- normaliseWantedEqs eq_irreds0
+
+         -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
+       ; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
+               
+         -- 9. eliminate the artificial skolem constants introduced in 1.
+       ; eliminate_skolems     
+
+         -- Figure out whether we should go round again
+         -- My current plan is to see if any of the mutable tyvars in
+         -- givens or irreds has been filled in by improvement.  
+         -- If so, there is merit in going around again, because
+         -- we may make further progress
+         -- 
+         -- ToDo: is it only mutable stuff?  We may have exposed new
+         --       equality constraints and should probably go round again
+         --       then as well.  But currently we are dropping them on the
+         --       floor anyway.
+
+       ; let all_irreds = irreds ++ eq_irreds
+       ; improved <- anyM isFilledMetaTyVar $ varSetElems $
+                     tyVarsOfInsts (givens ++ all_irreds)
+
+       -- The old plan (fragile)
+       -- improveed   = availsImproved avails 
+       --               || (not $ isEmptyBag normalise_binds1)
+       --               || (not $ isEmptyBag normalise_binds2)
+       --               || (any isEqInst irreds)
 
        ; traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
             red_doc env,
 
        ; traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
             red_doc env,
-            text "given" <+> ppr (red_givens env),
+            text "given" <+> ppr givens,
+            text "given_eqs" <+> ppr given_eqs,
             text "wanted" <+> ppr wanteds,
             text "wanted" <+> ppr wanteds,
+            text "wanted_dicts" <+> ppr wanted_dicts,
             text "----",
             text "avails" <+> pprAvails avails,
             text "improved =" <+> ppr improved,
             text "----",
             text "avails" <+> pprAvails avails,
             text "improved =" <+> ppr improved,
-            text "irreds = " <+> ppr irreds,
+            text "(all) irreds = " <+> ppr all_irreds,
+            text "binds = " <+> ppr binds,
+            text "needed givens = " <+> ppr needed_givens,
             text "----------------------"
             ]))
 
             text "----------------------"
             ]))
 
-       ; return (improved, binds, irreds) }
+       ; return (improved, 
+                  given_binds `unionBags` normalise_binds1 
+                              `unionBags` normalise_binds2 
+                              `unionBags` binds, 
+                  all_irreds,
+                  needed_givens) 
+        }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
 tcImproveOne avails inst
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
 tcImproveOne avails inst
@@ -1690,7 +1910,8 @@ The main context-reduction function is @reduce@.  Here's its game plan.
 \begin{code}
 reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
 reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
 \begin{code}
 reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
 reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
-  = do         { dopts <- getDOpts
+  = do         { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state))
+       ; dopts <- getDOpts
 #ifdef DEBUG
        ; if n > 8 then
                dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n) 
 #ifdef DEBUG
        ; if n > 8 then
                dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n) 
@@ -1710,34 +1931,37 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
 reduce env wanted avails
     -- It's the same as an existing inst, or a superclass thereof
   | Just avail <- findAvail avails wanted
 reduce env wanted avails
     -- It's the same as an existing inst, or a superclass thereof
   | Just avail <- findAvail avails wanted
-  = returnM avails     
+  = do { traceTc (text "reduce: found " <+> ppr wanted)
+       ; returnM avails        
+       }
 
   | otherwise
 
   | otherwise
-  = case red_try_me env wanted of {
-    ; Stop -> try_simple (addIrred NoSCs)      -- See Note [No superclasses for Stop]
-
-    ; ReduceMe want_scs ->     -- It should be reduced
-       reduceInst env avails wanted      `thenM` \ (avails, lookup_result) ->
-       case lookup_result of
-           NoInstance ->    -- No such instance!
+  = do { traceTc (text "reduce" <+> ppr wanted $$ ppr avails)
+       ; case red_try_me env wanted of {
+           Stop -> try_simple (addIrred NoSCs);
+                       -- See Note [No superclasses for Stop]
+
+           ReduceMe want_scs -> do     -- It should be reduced
+               { (avails, lookup_result) <- reduceInst env avails wanted
+               ; case lookup_result of
+                   NoInstance -> addIrred want_scs avails wanted
                             -- Add it and its superclasses
                             -- Add it and its superclasses
-                            addIrred want_scs avails wanted
-
-           GenInst [] rhs -> addWanted want_scs avails wanted rhs []
+                            
+                   GenInst [] rhs -> addWanted want_scs avails wanted rhs []
 
 
-           GenInst wanteds' rhs -> do  { avails1 <- addIrred NoSCs avails wanted
-                                       ; avails2 <- reduceList env wanteds' avails1
-                                       ; addWanted want_scs avails2 wanted rhs wanteds' }
+                   GenInst wanteds' rhs 
+                         -> do { avails1 <- addIrred NoSCs avails wanted
+                               ; avails2 <- reduceList env wanteds' avails1
+                               ; addWanted want_scs avails2 wanted rhs wanteds' } }
                -- Temporarily do 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
                -- Temporarily do 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
+               --     superclasses too, and that 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
                --     the examples in [SUPERCLASS-LOOP]
                -- So we do an addIrred before, and then overwrite it afterwards with addWanted
-
-    }
+    } }
   where
        -- First, see if the inst can be reduced to a constant in one step
        -- Works well for literals (1::Int) and constant dictionaries (d::Num Int)
   where
        -- First, see if the inst can be reduced to a constant in one step
        -- Works well for literals (1::Int) and constant dictionaries (d::Num Int)
@@ -1837,19 +2061,46 @@ contributing clauses.
 \begin{code}
 ---------------------------------------------
 reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
 \begin{code}
 ---------------------------------------------
 reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
+reduceInst env avails (ImplicInst { tci_name = name,
+                                   tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
                                    tci_given = extra_givens, tci_wanted = wanteds })
                                    tci_given = extra_givens, tci_wanted = wanteds })
-  = reduceImplication env avails reft tvs extra_givens wanteds loc
+  = reduceImplication env avails name reft tvs extra_givens wanteds loc
 
 reduceInst env avails other_inst
   = do { result <- lookupSimpleInst other_inst
        ; return (avails, result) }
 \end{code}
 
 
 reduceInst env avails other_inst
   = do { result <- lookupSimpleInst other_inst
        ; return (avails, result) }
 \end{code}
 
+Note [Equational Constraints in Implication Constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+An implication constraint is of the form 
+       Given => Wanted 
+where Given and Wanted may contain both equational and dictionary
+constraints. The delay and reduction of these two kinds of constraints
+is distinct:
+
+-) In the generated code, wanted Dictionary constraints are wrapped up in an
+   implication constraint that is created at the code site where the wanted
+   dictionaries can be reduced via a let-binding. This let-bound implication
+   constraint is deconstructed at the use-site of the wanted dictionaries.
+
+-) While the reduction of equational constraints is also delayed, the delay
+   is not manifest in the generated code. The required evidence is generated
+   in the code directly at the use-site. There is no let-binding and deconstruction
+   necessary. The main disadvantage is that we cannot exploit sharing as the
+   same evidence may be generated at multiple use-sites. However, this disadvantage
+   is limited because it only concerns coercions which are erased.
+
+The different treatment is motivated by the different in representation. Dictionary
+constraints require manifest runtime dictionaries, while equations require coercions
+which are types.
+
 \begin{code}
 ---------------------------------------------
 reduceImplication :: RedEnv
                 -> Avails
 \begin{code}
 ---------------------------------------------
 reduceImplication :: RedEnv
                 -> Avails
+                -> Name
                 -> Refinement  -- May refine the givens; often empty
                 -> [TcTyVar]   -- Quantified type variables; all skolems
                 -> [Inst]      -- Extra givens; all rigid
                 -> Refinement  -- May refine the givens; often empty
                 -> [TcTyVar]   -- Quantified type variables; all skolems
                 -> [Inst]      -- Extra givens; all rigid
@@ -1880,61 +2131,130 @@ Note that
 \begin{code}
        -- ToDo: should we instantiate tvs?  I think it's not necessary
        --
 \begin{code}
        -- ToDo: should we instantiate tvs?  I think it's not necessary
        --
-       -- ToDo: what about improvement?  There may be some improvement
-       --       exposed as a result of the simplifications done by reduceList
-       --       which are discarded if we back off.  
-       --       This is almost certainly Wrong, but we'll fix it when dealing
-       --       better with equality constraints
-reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
+       -- Note on coercion variables:
+       --
+       --      The extra given coercion variables are bound at two different sites:
+       --      -) in the creation context of the implication constraint        
+       --              the solved equational constraints use these binders
+       --
+       --      -) at the solving site of the implication constraint
+       --              the solved dictionaries use these binders               
+       --              these binders are generated by reduceImplication
+       --
+reduceImplication env orig_avails name reft tvs extra_givens wanteds inst_loc
   = do {       -- Add refined givens, and the extra givens
   = do {       -- Add refined givens, and the extra givens
-         (refined_red_givens, avails) 
-               <- if isEmptyRefinement reft then return (red_givens env, orig_avails)
-                  else foldlM (addRefinedGiven reft) ([], orig_avails) (red_givens env)
-       ; avails <- foldlM addGiven avails extra_givens
+               -- Todo fix this 
+--       (refined_red_givens,refined_avails)
+--             <- if isEmptyRefinement reft then return (red_givens env,orig_avails)
+--                else foldlM (addRefinedGiven reft) ([],orig_avails) (red_givens env)
+--     Commented out SLPJ Sept 07; see comment with extractLocalResults below
+         let refined_red_givens = []
 
                -- Solve the sub-problem
        ; let try_me inst = ReduceMe AddSCs     -- Note [Freeness and implications]
 
                -- Solve the sub-problem
        ; let try_me inst = ReduceMe AddSCs     -- Note [Freeness and implications]
-             env' = env { red_givens = refined_red_givens ++ extra_givens
+             env' = env { red_givens = extra_givens ++ availsInsts orig_avails
+                        , red_reft = reft
+                        , red_doc = sep [ptext SLIT("reduceImplication for") <+> ppr name,
+                                         nest 2 (parens $ ptext SLIT("within") <+> red_doc env)]
                         , red_try_me = try_me }
 
        ; traceTc (text "reduceImplication" <+> vcat
                        [ ppr orig_avails,
                          ppr (red_givens env), ppr extra_givens, 
                         , red_try_me = try_me }
 
        ; traceTc (text "reduceImplication" <+> vcat
                        [ ppr orig_avails,
                          ppr (red_givens env), ppr extra_givens, 
-                         ppr reft, ppr wanteds, ppr avails ])
-       ; avails <- reduceList env' wanteds avails
+                         ppr reft, ppr wanteds])
+       ; (irreds,binds,needed_givens0) <- checkLoop env' wanteds
+       ; let   (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
+                       -- SLPJ Sept 07: I think this is bogus; currently
+                       -- there are no Eqinsts in extra_givens
+               dict_ids = map instToId extra_dict_givens 
+
+               -- needed_givens0 is the free vars of the bindings
+               -- Remove the ones we are going to lambda-bind
+               -- Use the actual dictionary identity *not* equality on Insts
+               -- (Mind you, it should make no difference here.)
+        ; let needed_givens = [ng | ng <- needed_givens0
+                                  , instToVar ng `notElem` dict_ids]
 
 
-               -- Extract the results 
                -- Note [Reducing implication constraints]
                -- Note [Reducing implication constraints]
-       ; (binds, irreds) <- extractResults avails wanteds
-       ; let (outer, inner) = partition (isJust . findAvail orig_avails) irreds
+               -- Tom -- update note, put somewhere!
 
        ; traceTc (text "reduceImplication result" <+> vcat
 
        ; traceTc (text "reduceImplication result" <+> vcat
-                       [ ppr outer, ppr inner, ppr binds])
+                       [ppr irreds, ppr binds, ppr needed_givens])
+
+       ; -- extract superclass binds
+         --  (sc_binds,_) <- extractResults avails []
+--     ; traceTc (text "reduceImplication sc_binds" <+> vcat
+--                     [ppr sc_binds, ppr avails])
+--  
 
                -- We always discard the extra avails we've generated;
                -- but we remember if we have done any (global) improvement
 
                -- We always discard the extra avails we've generated;
                -- but we remember if we have done any (global) improvement
-       ; let ret_avails = updateImprovement orig_avails avails
+--     ; let ret_avails = avails
+       ; let ret_avails = orig_avails
+--     ; let ret_avails = updateImprovement orig_avails avails
 
 
-       ; if isEmptyLHsBinds binds && null outer then   -- No progress
+       -- SLPJ Sept 07: what if improvement happened inside the checkLoop?
+       -- Then we must iterate the outer loop too!
+
+       ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
+
+--     Progress is no longer measered by the number of bindings
+       ; if (isEmptyLHsBinds binds) && (not $ null irreds) then        -- No progress
+               -- If there are any irreds, we back off and return NoInstance
                return (ret_avails, NoInstance)
          else do
                return (ret_avails, NoInstance)
          else do
-       { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens inner
-
-       ; let   dict_ids = map instToId extra_givens
-               co  = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
+       { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
+                       -- This binding is useless if the recursive simplification
+                       -- made no progress; but currently we don't try to optimise that
+                       -- case.  After all, we only try hard to reduce at top level, or
+                       -- when inferring types.
+
+       ; let   dict_wanteds = filter (not . isEqInst) wanteds
+               -- TOMDO: given equational constraints bug!
+               --  we need a different evidence for given
+               --  equations depending on whether we solve
+               --  dictionary constraints or equational constraints
+
+               eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens
+                       -- SLPJ Sept07: this looks Utterly Wrong to me, but I think
+                       --              that current extra_givens has no EqInsts, so
+                       --              it makes no difference
+               co  = wrap_inline       -- Note [Always inline implication constraints]
+                     <.> mkWpTyLams tvs
+                     <.> mkWpTyLams eq_tyvars
+                     <.> mkWpLams dict_ids
+                     <.> WpLet (binds `unionBags` bind)
+               wrap_inline | null dict_ids = idHsWrapper
+                           | otherwise     = WpInline
                rhs = mkHsWrap co payload
                loc = instLocSpan inst_loc
                rhs = mkHsWrap co payload
                loc = instLocSpan inst_loc
-               payload | [wanted] <- wanteds = HsVar (instToId wanted)
-                       | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
+               payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted)
+                       | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed
 
 
-       ; return (ret_avails, GenInst (implic_insts ++ outer) (L loc rhs))
-  } }
+       
+       ; traceTc (vcat [text "reduceImplication" <+> ppr name,
+                        ppr implic_insts,
+                        text "->" <+> sep [ppr needed_givens, ppr rhs]])
+       ; return (ret_avails, GenInst (implic_insts ++ needed_givens) (L loc rhs))
+       } 
+    }
 \end{code}
 
 \end{code}
 
+Note [Always inline implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose an implication constraint floats out of an INLINE function.
+Then although the implication has a single call site, it won't be 
+inlined.  And that is bad because it means that even if there is really
+*no* overloading (type signatures specify the exact types) there will
+still be dictionary passing in the resulting code.  To avert this,
+we mark the implication constraints themselves as INLINE, at least when
+there is no loss of sharing as a result.
+
 Note [Reducing implication constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we are trying to simplify
 Note [Reducing implication constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we are trying to simplify
-       (Ord a, forall b. C a b => (W [a] b, D c b))
+       ( do: Ord a, 
+         ic: (forall b. C a b => (W [a] b, D c b)) )
 where
        instance (C a b, Ord a) => W [a] b
 When solving the implication constraint, we'll start with
 where
        instance (C a b, Ord a) => W [a] b
 When solving the implication constraint, we'll start with
@@ -1942,16 +2262,26 @@ When solving the implication constraint, we'll start with
 in the Avails.  Then we add (C a b -> Given) and solve. Extracting
 the results gives us a binding for the (W [a] b), with an Irred of 
 (Ord a, D c b).  Now, the (Ord a) comes from "outside" the implication,
 in the Avails.  Then we add (C a b -> Given) and solve. Extracting
 the results gives us a binding for the (W [a] b), with an Irred of 
 (Ord a, D c b).  Now, the (Ord a) comes from "outside" the implication,
-but the (D d b) is from "inside".  So we want to generate a Rhs binding
+but the (D d b) is from "inside".  So we want to generate a GenInst
 like this
 
 like this
 
-       ic = /\b \dc:C a b). (df a b dc do, ic' b dc)
-          depending on
-               do :: Ord a
-               ic' :: forall b. C a b => D c b
+   ic = GenInst 
+          [ do  :: Ord a,
+            ic' :: forall b. C a b => D c b]
+          (/\b \(dc:C a b). (df a b dc do, ic' b dc))
+
+The first arg of GenInst gives the free dictionary variables of the
+second argument -- the "needed givens".  And that list in turn is
+vital because it's used to determine what other dicts must be solved.
+This very list ends up in the second field of the Rhs, and drives
+extractResults.
 
 
-The 'depending on' part of the Rhs is important, because it drives
-the extractResults code.
+The need for this field is why we have to return "needed givens"
+from extractResults, reduceContext, checkLoop, and so on.
+
+NB: the "needed givens" in a GenInst or Rhs, may contain two dicts
+with the same type but different Ids, e.g. [d12 :: Eq a, d81 :: Eq a]
+That says we must generate a binding for both d12 and d81.
 
 The "inside" and "outside" distinction is what's going on with 'inner' and
 'outer' in reduceImplication
 
 The "inside" and "outside" distinction is what's going on with 'inner' and
 'outer' in reduceImplication
@@ -2012,10 +2342,10 @@ type ImprovementDone = Bool     -- True <=> some unification has happened
 
 type AvailEnv = FiniteMap Inst AvailHow
 data AvailHow
 
 type AvailEnv = FiniteMap Inst AvailHow
 data AvailHow
-  = IsIrred TcId       -- Used for irreducible dictionaries,
+  = IsIrred            -- Used for irreducible dictionaries,
                        -- which are going to be lambda bound
 
                        -- which are going to be lambda bound
 
-  | Given TcId                 -- Used for dictionaries for which we have a binding
+  | Given Inst                 -- Used for dictionaries for which we have a binding
                        -- e.g. those "given" in a signature
 
   | Rhs                -- Used when there is a RHS
                        -- e.g. those "given" in a signature
 
   | Rhs                -- Used when there is a RHS
@@ -2027,17 +2357,19 @@ instance Outputable Avails where
 
 pprAvails (Avails imp avails)
   = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty)
 
 pprAvails (Avails imp avails)
   = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty)
-        , nest 2 (vcat [sep [ppr inst, nest 2 (equals <+> ppr avail)]
-                       | (inst,avail) <- fmToList avails ])]
+        , nest 2 $ braces $ 
+          vcat [ sep [ppr inst, nest 2 (equals <+> ppr avail)]
+               | (inst,avail) <- fmToList avails ]]
 
 instance Outputable AvailHow where
     ppr = pprAvail
 
 -------------------------
 pprAvail :: AvailHow -> SDoc
 
 instance Outputable AvailHow where
     ppr = pprAvail
 
 -------------------------
 pprAvail :: AvailHow -> SDoc
-pprAvail (IsIrred x)   = text "Irred" <+> ppr x
+pprAvail IsIrred       = text "Irred"
 pprAvail (Given x)     = text "Given" <+> ppr x
 pprAvail (Given x)     = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs)   = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)]
+pprAvail (Rhs rhs bs)   = sep [text "Rhs" <+> ppr bs,
+                              nest 2 (ppr rhs)]
 
 -------------------------
 extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
 
 -------------------------
 extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
@@ -2080,47 +2412,56 @@ We assume that they'll be wrapped in a big Rec, so that the
 dependency analyser can sort them out later
 
 \begin{code}
 dependency analyser can sort them out later
 
 \begin{code}
+type DoneEnv = FiniteMap Inst [Id]
+-- Tracks which things we have evidence for
+
 extractResults :: Avails
               -> [Inst]                -- Wanted
 extractResults :: Avails
               -> [Inst]                -- Wanted
-              -> TcM ( TcDictBinds,    -- Bindings
-                       [Inst])         -- Irreducible ones
+              -> (TcDictBinds,         -- Bindings
+                  [Inst],              -- Irreducible ones
+                  [Inst])              -- Needed givens, i.e. ones used in the bindings
+                       -- Postcondition: needed-givens = free vars( binds ) \ irreds
+                       --                needed-gives is subset of Givens in incoming Avails
+                       -- Note [Reducing implication constraints]
 
 extractResults (Avails _ avails) wanteds
 
 extractResults (Avails _ avails) wanteds
-  = go avails emptyBag [] wanteds
+  = go emptyBag [] [] emptyFM wanteds
   where
   where
-    go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
-       -> TcM (TcDictBinds, [Inst])
-    go avails binds irreds [] 
-      = returnM (binds, irreds)
-
-    go avails binds irreds (w:ws)
+    go :: TcDictBinds  -- Bindings for dicts
+       -> [Inst]       -- Irreds
+       -> [Inst]       -- Needed givens
+       -> DoneEnv      -- Has an entry for each inst in the above three sets
+       -> [Inst]       -- Wanted
+       -> (TcDictBinds, [Inst], [Inst])
+    go binds irreds givens done [] 
+      = (binds, irreds, givens)
+
+    go binds irreds givens done (w:ws)
+      | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
+      = if w_id `elem` done_ids then
+          go binds irreds givens done ws
+       else
+          go (add_bind (nlHsVar done_id)) irreds givens 
+             (addToFM done w (done_id : w_id : rest_done_ids)) ws
+
+      | otherwise      -- Not yet done
       = case findAvailEnv avails w of
          Nothing -> pprTrace "Urk: extractResults" (ppr w) $
       = case findAvailEnv avails w of
          Nothing -> pprTrace "Urk: extractResults" (ppr w) $
-                    go avails binds irreds ws
-
-         Just (Given id) 
-               | id == w_id -> go avails binds irreds ws 
-               | otherwise  -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
-               -- 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!
-
-         Just (IsIrred _) -> go (add_given avails w) binds (w:irreds) ws
-               -- | otherwise  -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
-               -- The add_given handles the case where we want (Ord a, Eq a), and we
-               -- don't want to emit *two* Irreds for Ord a, one via the superclass chain
-               -- This showed up in a dupliated Ord constraint in the error message for 
-               --      test tcfail043
-
-         Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
-                            where      
-                               new_binds = addBind binds w_id rhs
-      where
-       w_id = instToId w       
+                    go binds irreds givens done ws
 
 
-    add_given avails w = extendAvailEnv avails w (Given (instToId w))
-       -- Don't add the same binding twice
+         Just IsIrred -> go binds (w:irreds) givens done' ws
 
 
-addBind binds id rhs = binds `unionBags` unitBag (L (getSrcSpan id) (VarBind id rhs))
+         Just (Rhs rhs ws') -> go (add_bind rhs) irreds givens done' (ws' ++ ws)
+
+         Just (Given g) -> go binds' irreds (g:givens) (addToFM done w [g_id]) ws 
+               where
+                 g_id = instToId g
+                 binds' | w_id == g_id = binds
+                        | otherwise    = add_bind (nlHsVar g_id)
+      where
+       w_id  = instToId w      
+       done' = addToFM done w [w_id]
+       add_bind rhs = addInstToDictBind binds w rhs
 \end{code}
 
 
 \end{code}
 
 
@@ -2142,15 +2483,15 @@ addWanted want_scs avails wanted rhs_expr wanteds
     avail = Rhs rhs_expr wanteds
 
 addGiven :: Avails -> Inst -> TcM Avails
     avail = Rhs rhs_expr wanteds
 
 addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
+addGiven avails given = addAvailAndSCs AddSCs avails given (Given given)
        -- Always add superclasses for 'givens'
        --
        -- No ASSERT( not (given `elemAvails` 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
 
        -- Always add superclasses for 'givens'
        --
        -- No ASSERT( not (given `elemAvails` 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
 
-addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails)
-addRefinedGiven reft (refined_givens, avails) given
+addRefinedGiven :: Refinement -> Avails -> Inst -> TcM Avails
+addRefinedGiven reft avails given
   | isDict given       -- We sometimes have 'given' methods, but they
                        -- are always optional, so we can drop them
   , let pred = dictPred given
   | isDict given       -- We sometimes have 'given' methods, but they
                        -- are always optional, so we can drop them
   , let pred = dictPred given
@@ -2159,13 +2500,12 @@ addRefinedGiven reft (refined_givens, avails) given
   = do         { new_given <- newDictBndr (instLoc given) pred
        ; let rhs = L (instSpan given) $
                    HsWrap (WpCo co) (HsVar (instToId given))
   = do         { new_given <- newDictBndr (instLoc given) pred
        ; let rhs = L (instSpan given) $
                    HsWrap (WpCo co) (HsVar (instToId given))
-       ; avails <- addAvailAndSCs AddSCs avails new_given (Rhs rhs [given])
-       ; return (new_given:refined_givens, avails) }
+       ; addAvailAndSCs AddSCs avails new_given (Rhs rhs [given]) }
            -- ToDo: the superclasses of the original given all exist in Avails 
            -- so we could really just cast them, but it's more awkward to do,
            -- and hopefully the optimiser will spot the duplicated work
   | otherwise
            -- ToDo: the superclasses of the original given all exist in Avails 
            -- so we could really just cast them, but it's more awkward to do,
            -- and hopefully the optimiser will spot the duplicated work
   | otherwise
-  = return (refined_givens, avails)
+  = return avails
 \end{code}
 
 Note [ImplicInst rigidity]
 \end{code}
 
 Note [ImplicInst rigidity]
@@ -2192,7 +2532,7 @@ than with the Avails handling stuff in TcSimplify
 \begin{code}
 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
 addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
 \begin{code}
 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
 addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
-                                addAvailAndSCs want_scs avails irred (IsIrred (instToId irred))
+                                addAvailAndSCs want_scs avails irred IsIrred
 
 addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
 addAvailAndSCs want_scs avails inst avail
 
 addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
 addAvailAndSCs want_scs avails inst avail
@@ -2204,7 +2544,7 @@ addAvailAndSCs want_scs avails inst avail
   where
     is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
                        -- Note: this compares by *type*, not by Unique
   where
     is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
                        -- Note: this compares by *type*, not by Unique
-    deps         = findAllDeps (unitVarSet (instToId inst)) avail
+    deps         = findAllDeps (unitVarSet (instToVar inst)) avail
     dep_tys     = map idType (varSetElems deps)
 
     findAllDeps :: IdSet -> AvailHow -> IdSet
     dep_tys     = map idType (varSetElems deps)
 
     findAllDeps :: IdSet -> AvailHow -> IdSet
@@ -2217,6 +2557,7 @@ addAvailAndSCs want_scs avails inst avail
 
     find_all :: IdSet -> Inst -> IdSet
     find_all so_far kid
 
     find_all :: IdSet -> Inst -> IdSet
     find_all so_far kid
+      | isEqInst kid                       = so_far
       | kid_id `elemVarSet` so_far        = so_far
       | Just avail <- findAvail avails kid = findAllDeps so_far' avail
       | otherwise                         = so_far'
       | kid_id `elemVarSet` so_far        = so_far
       | Just avail <- findAvail avails kid = findAllDeps so_far' avail
       | otherwise                         = so_far'
@@ -2226,7 +2567,7 @@ addAvailAndSCs want_scs avails inst avail
 
 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
        -- Add all the superclasses of the Inst to 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
+       -- The first param says "don't do this because the original thing
        --      depends on this one, so you'd build a loop"
        -- Invariant: the Inst is already in Avails.
 
        --      depends on this one, so you'd build a loop"
        -- Invariant: the Inst is already in Avails.
 
@@ -2237,7 +2578,8 @@ addSCs is_loop avails dict
   where
     (clas, tys) = getDictClassTys dict
     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
   where
     (clas, tys) = getDictClassTys dict
     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
-    sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
+    sc_theta' = filter (not . isEqPred) $
+                  substTheta (zipTopTvSubst tyvars tys) sc_theta
 
     add_sc avails (sc_dict, sc_sel)
       | is_loop (dictPred sc_dict) = return avails     -- See Note [SUPERCLASS-LOOP 2]
 
     add_sc avails (sc_dict, sc_sel)
       | is_loop (dictPred sc_dict) = return avails     -- See Note [SUPERCLASS-LOOP 2]
@@ -2246,14 +2588,41 @@ addSCs is_loop avails dict
                                        ; addSCs is_loop avails' sc_dict }
       where
        sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
                                        ; addSCs is_loop avails' sc_dict }
       where
        sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
-       co_fn      = WpApp (instToId dict) <.> mkWpTyApps tys
+       co_fn      = WpApp (instToVar dict) <.> mkWpTyApps tys
 
     is_given :: Inst -> Bool
     is_given sc_dict = case findAvail avails sc_dict of
                          Just (Given _) -> True        -- Given is cheaper than superclass selection
                          other          -> False       
 
     is_given :: Inst -> Bool
     is_given sc_dict = case findAvail avails sc_dict of
                          Just (Given _) -> True        -- Given is cheaper than superclass selection
                          other          -> False       
+
+-- From the a set of insts obtain all equalities that (transitively) occur in
+-- superclass contexts of class constraints (aka the ancestor equalities). 
+--
+ancestorEqualities :: [Inst] -> TcM [Inst]
+ancestorEqualities
+  =   mapM mkWantedEqInst               -- turn only equality predicates..
+    . filter isEqPred                   -- ..into wanted equality insts
+    . bagToList 
+    . addAEsToBag emptyBag              -- collect the superclass constraints..
+    . map dictPred                      -- ..of all predicates in a bag
+    . filter isClassDict
+  where
+    addAEsToBag :: Bag PredType -> [PredType] -> Bag PredType
+    addAEsToBag bag []           = bag
+    addAEsToBag bag (pred:preds)
+      | pred `elemBag` bag = addAEsToBag bag         preds
+      | isEqPred pred      = addAEsToBag bagWithPred preds
+      | isClassPred pred   = addAEsToBag bagWithPred predsWithSCs
+      | otherwise          = addAEsToBag bag         preds
+      where
+        bagWithPred  = bag `snocBag` pred
+        predsWithSCs = preds ++ substTheta (zipTopTvSubst tyvars tys) sc_theta
+        --
+        (tyvars, sc_theta, _, _) = classBigSig clas
+        (clas, tys)             = getClassPredTys pred 
 \end{code}
 
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \section{tcSimplifyTop: defaulting}
 %************************************************************************
 %*                                                                     *
 \section{tcSimplifyTop: defaulting}
@@ -2290,11 +2659,15 @@ tcSimplifyInteractive wanteds
 -- error message generation for the monomorphism restriction
 tc_simplify_top doc interactive wanteds
   = do { dflags <- getDOpts
 -- error message generation for the monomorphism restriction
 tc_simplify_top doc interactive wanteds
   = do { dflags <- getDOpts
-       ; wanteds <- mapM zonkInst wanteds
+       ; wanteds <- zonkInsts wanteds
        ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
 
        ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
 
+       ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
        ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
        ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
+--     ; (irreds1, binds1) <- gentleInferLoop doc1 wanteds
+       ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
        ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
        ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
+       ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
 
                -- Use the defaulting rules to do extra unification
                -- NB: irreds2 are already zonked
 
                -- Use the defaulting rules to do extra unification
                -- NB: irreds2 are already zonked
@@ -2357,7 +2730,7 @@ disambiguate doc interactive dflags insts
   = return (insts, emptyBag)
 
   | null defaultable_groups
   = return (insts, emptyBag)
 
   | null defaultable_groups
-  = do { traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+  = do { traceTc (text "disambigutate, no defaultable groups" <+> vcat [ppr unaries, ppr insts, ppr bad_tvs, ppr defaultable_groups])
        ; return (insts, emptyBag) }
 
   | otherwise
        ; return (insts, emptyBag) }
 
   | otherwise
@@ -2420,7 +2793,7 @@ disambigGroup :: [Type]                   -- The default types
 disambigGroup default_tys dicts
   = try_default default_tys
   where
 disambigGroup default_tys dicts
   = try_default default_tys
   where
-    (_,_,tyvar) = head dicts   -- Should be non-empty
+    (_,_,tyvar) = ASSERT(not (null dicts)) head dicts  -- Should be non-empty
     classes = [c | (_,c,_) <- dicts]
 
     try_default [] = return ()
     classes = [c | (_,c,_) <- dicts]
 
     try_default [] = return ()
@@ -2435,7 +2808,9 @@ disambigGroup default_tys dicts
 
                -- After this we can't fail
           ; warnDefault dicts default_ty
 
                -- After this we can't fail
           ; warnDefault dicts default_ty
-          ; unifyType default_ty (mkTyVarTy tyvar) }
+          ; unifyType default_ty (mkTyVarTy tyvar) 
+          ; return () -- TOMDO: do something with the coercion
+          }
 
 
 -----------------------
 
 
 -----------------------
@@ -2511,7 +2886,6 @@ tcSimplifyDeriv :: InstOrigin
                -> TcM ThetaType        -- Needed
 -- Given  instance (wanted) => C inst_ty 
 -- Simplify 'wanted' as much as possible
                -> TcM ThetaType        -- Needed
 -- Given  instance (wanted) => C inst_ty 
 -- Simplify 'wanted' as much as possible
--- The inst_ty is needed only for the termination check
 
 tcSimplifyDeriv orig tyvars theta
   = do { (tvs, _, tenv) <- tcInstTyVars tyvars
 
 tcSimplifyDeriv orig tyvars theta
   = do { (tvs, _, tenv) <- tcInstTyVars tyvars
@@ -2521,8 +2895,9 @@ tcSimplifyDeriv orig tyvars theta
        ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
        ; (irreds, _) <- tryHardCheckLoop doc wanteds
 
        ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
        ; (irreds, _) <- tryHardCheckLoop doc wanteds
 
-       ; let (tv_dicts, others) = partition isTyVarDict irreds
+       ; let (tv_dicts, others) = partition ok irreds
        ; addNoInstanceErrs others
        ; addNoInstanceErrs others
+       -- See Note [Exotic derived instance contexts] in TcMType
 
        ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
              simpl_theta = substTheta rev_env (map dictPred tv_dicts)
 
        ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
              simpl_theta = substTheta rev_env (map dictPred tv_dicts)
@@ -2532,49 +2907,10 @@ tcSimplifyDeriv orig tyvars theta
        ; return simpl_theta }
   where
     doc = ptext SLIT("deriving classes for a data type")
        ; return simpl_theta }
   where
     doc = ptext SLIT("deriving classes for a data type")
-\end{code}
-
-Note [Exotic derived instance contexts]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-       data T a b c = MkT (Foo a b c) deriving( Eq )
-       instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
-
-Notice that this instance (just) satisfies the Paterson termination 
-conditions.  Then we *could* derive an instance decl like this:
-
-       instance (C Int a, Eq b, Eq c) => Eq (T a b c) 
 
 
-even though there is no instance for (C Int a), because there just
-*might* be an instance for, say, (C Int Bool) at a site where we
-need the equality instance for T's.  
-
-However, this seems pretty exotic, and it's quite tricky to allow
-this, and yet give sensible error messages in the (much more common)
-case where we really want that instance decl for C.
-
-So for now we simply require that the derived instance context
-should have only type-variable constraints.
-
-Here is another example:
-       data Fix f = In (f (Fix f)) deriving( Eq )
-Here, if we are prepared to allow -fallow-undecidable-instances we
-could derive the instance
-       instance Eq (f (Fix f)) => Eq (Fix f)
-but this is so delicate that I don't think it should happen inside
-'deriving'. If you want this, write it yourself!
-
-NB: if you want to lift this condition, make sure you still meet the
-termination conditions!  If not, the deriving mechanism generates
-larger and larger constraints.  Example:
-  data Succ a = S a
-  data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
-
-Note the lack of a Show instance for Succ.  First we'll generate
-  instance (Show (Succ a), Show a) => Show (Seq a)
-and then
-  instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
-and so on.  Instead we want to complain of no instance for (Show (Succ a)).
+    ok dict | isDict dict = validDerivPred (dictPred dict)
+           | otherwise   = False
+\end{code}
 
 
 @tcSimplifyDefault@ just checks class-type constraints, essentially;
 
 
 @tcSimplifyDefault@ just checks class-type constraints, essentially;
@@ -2592,7 +2928,7 @@ tcSimplifyDefault theta
     if null irreds then
        returnM ()
     else
     if null irreds then
        returnM ()
     else
-       failM
+       traceTc (ptext SLIT("tcSimplifyDefault failing")) >> failM
   where
     doc = ptext SLIT("default declaration")
 \end{code}
   where
     doc = ptext SLIT("default declaration")
 \end{code}
@@ -2616,11 +2952,10 @@ groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
 -- We want to report them together in error messages
 
 groupErrs report_err [] 
 -- We want to report them together in error messages
 
 groupErrs report_err [] 
-  = returnM ()
+  = return ()
 groupErrs report_err (inst:insts) 
 groupErrs report_err (inst:insts) 
-  = do_one (inst:friends)              `thenM_`
-    groupErrs report_err others
-
+  = do { do_one (inst:friends)
+       ; groupErrs report_err 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,
   where
        -- (It may seem a bit crude to compare the error messages,
        --  but it makes sure that we combine just what the user sees,
@@ -2680,14 +3015,17 @@ reportNoInstances tidy_env mb_what insts
   = groupErrs (report_no_instances tidy_env mb_what) insts
 
 report_no_instances tidy_env mb_what insts
   = groupErrs (report_no_instances tidy_env mb_what) insts
 
 report_no_instances tidy_env mb_what insts
-  = do { inst_envs <- tcGetInstEnvs
-       ; let (implics, insts1)  = partition isImplicInst insts
-             (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
-       ; traceTc (text "reportNoInstnces" <+> vcat 
-                       [ppr implics, ppr insts1, ppr insts2])
-       ; mapM_ complain_implic implics
-       ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
-       ; groupErrs complain_no_inst insts2 }
+  = do { inst_envs <- tcGetInstEnvs
+       ; let (implics, insts1)  = partition isImplicInst insts
+            (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
+             (eqInsts, insts3)  = partition isEqInst insts2
+       ; traceTc (text "reportNoInstances" <+> vcat 
+                       [ppr insts, ppr implics, ppr insts1, ppr insts2])
+       ; mapM_ complain_implic implics
+       ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
+       ; groupErrs complain_no_inst insts3 
+       ; mapM_ (addErrTcM . mk_eq_err) eqInsts
+       }
   where
     complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
 
   where
     complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
 
@@ -2703,9 +3041,9 @@ report_no_instances tidy_env mb_what insts
        | not (isClassDict wanted) = Left wanted
        | otherwise
        = case lookupInstEnv inst_envs clas tys of
        | not (isClassDict wanted) = Left wanted
        | otherwise
        = case lookupInstEnv 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
+               -- The case of exactly one match and no unifiers means a
+               -- successful lookup.  That can't happen here, because dicts
+               -- only end up here if they didn't match in Inst.lookupInst
 #ifdef DEBUG
                ([m],[]) -> pprPanic "reportNoInstance" (ppr wanted)
 #endif
 #ifdef DEBUG
                ([m],[]) -> pprPanic "reportNoInstance" (ppr wanted)
 #endif
@@ -2728,10 +3066,13 @@ report_no_instances tidy_env mb_what insts
                parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
                                 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
                              ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"),
                parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
                                 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
                              ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"),
-                             ptext SLIT("when compiling the other instances")])]
+                             ptext SLIT("when compiling the other instance declarations")])]
       where
        ispecs = [ispec | (ispec, _) <- matches]
 
       where
        ispecs = [ispec | (ispec, _) <- matches]
 
+    mk_eq_err :: Inst -> (TidyEnv, SDoc)
+    mk_eq_err inst = misMatchMsg tidy_env (eqInstTys inst)
+
     mk_no_inst_err insts
       | null insts = empty
 
     mk_no_inst_err insts
       | null insts = empty
 
@@ -2817,10 +3158,6 @@ mkMonomorphismMsg tidy_env inst_tvs
                nest 2 (vcat docs),
                monomorphism_fix dflags]
 
                nest 2 (vcat docs),
                monomorphism_fix dflags]
 
-isRuntimeUnk :: TcTyVar -> Bool
-isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
-               | otherwise = False
-
 monomorphism_fix :: DynFlags -> SDoc
 monomorphism_fix dflags
   = ptext SLIT("Probable fix:") <+> vcat
 monomorphism_fix :: DynFlags -> SDoc
 monomorphism_fix dflags
   = ptext SLIT("Probable fix:") <+> vcat