Comments only
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index 8a5ad1a..534c5d0 100644 (file)
@@ -971,17 +971,17 @@ makeImplicationBind :: InstLoc -> [TcTyVar]
                    -> [Inst] -> [Inst]
                    -> TcM ([Inst], TcDictBinds)
 -- Make a binding that binds 'irreds', by generating an implication
--- constraint for them, *and* throwing the constraint into the LIE
+-- constraint for them.
+--
 -- The binding looks like
 --     (ir1, .., irn) = f qtvs givens
 -- where f is (evidence for) the new implication constraint
---     f :: forall qtvs. {reft} givens => (ir1, .., irn)
--- qtvs includes coercion variables
+--     f :: forall qtvs. givens => (ir1, .., irn)
+-- qtvs includes coercion variables.
 --
 -- This binding must line up the 'rhs' in reduceImplication
 makeImplicationBind loc all_tvs
-                   givens      -- Guaranteed all Dicts
-                               -- or EqInsts
+                   givens      -- Guaranteed all Dicts or EqInsts
                    irreds
  | null irreds                 -- If there are no irreds, we are done
  = return ([], emptyBag)
@@ -989,28 +989,38 @@ makeImplicationBind loc all_tvs
  = 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
+                -- extract equality binders
+              eq_cotvs = map eqInstType eq_givens
+
+                -- make the implication constraint instance
+             name = mkInternalName uniq (mkVarOcc "ic") span
              implic_inst = ImplicInst { tci_name = name,
                                         tci_tyvars = all_tvs, 
                                         tci_given = (eq_givens ++ dict_givens),
-                                        tci_wanted = irreds, tci_loc = loc }
-       ; let   -- only create binder for dict_irreds
-             (_, dict_irreds) = partition isEqInst irreds
+                                                       -- same order as binders
+                                        tci_wanted = irreds, 
+                                         tci_loc = loc }
+
+               -- create binders for the irreducible dictionaries
+             dict_irreds    = filter (not . isEqInst) irreds
              dict_irred_ids = map instToId dict_irreds
              lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)
-             rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
-             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 = lpat, 
-                                                 pat_rhs = unguardedGRHSs rhs, 
-                                                 pat_rhs_ty = hsLPatType lpat,
-                                                 bind_fvs = placeHolderNames }
+
+                -- create the binding
+             rhs  = L span (mkHsWrap co (HsVar (instToId implic_inst)))
+             co   =     mkWpApps (map instToId dict_givens)
+                    <.> mkWpTyApps eq_cotvs
+                    <.> mkWpTyApps (mkTyVarTys all_tvs)
+             bind | [dict_irred_id] <- dict_irred_ids  
+                   = VarBind dict_irred_id rhs
+                  | otherwise        
+                   = PatBind { pat_lhs = lpat
+                            , pat_rhs = unguardedGRHSs rhs 
+                            , pat_rhs_ty = hsLPatType lpat
+                            , bind_fvs = placeHolderNames 
+                             }
+
        ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
        ; return ([implic_inst], unitBag (L span bind)) 
         }
@@ -1021,11 +1031,11 @@ tryHardCheckLoop :: SDoc
             -> TcM ([Inst], TcDictBinds)
 
 tryHardCheckLoop doc wanteds
-  = do { (irreds,binds) <- checkLoop (mkRedEnv doc try_me []) wanteds
+  = do { (irreds,binds) <- checkLoop (mkInferRedEnv doc try_me) wanteds
        ; return (irreds,binds)
        }
   where
-    try_me _ = ReduceMe AddSCs
+    try_me _ = ReduceMe
        -- Here's the try-hard bit
 
 -----------------------------------------------------------
@@ -1041,7 +1051,7 @@ gentleCheckLoop inst_loc givens wanteds
   where
     env = mkRedEnv (pprInstLoc inst_loc) try_me givens
 
-    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+    try_me inst | isMethodOrLit inst = ReduceMe
                | otherwise          = Stop
        -- When checking against a given signature 
        -- we MUST be very gentle: Note [Check gently]
@@ -1052,8 +1062,8 @@ 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
+    env = mkInferRedEnv doc try_me
+    try_me inst | isMethodOrLit inst = ReduceMe
                | otherwise          = Stop
 \end{code}
 
@@ -1201,30 +1211,87 @@ Alas!  Alack! We can do the same for (instance D Int):
        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
 
+Solution: 
+  - Satisfy the superclass context *all by itself* 
+    (tcSimplifySuperClasses)
+  - And do so completely; i.e. no left-over constraints
+    to mix with the constraints arising from method declarations
+
+
+Note [Recursive instances and superclases]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this code, which arises in the context of "Scrap Your 
+Boilerplate with Class".  
+
+    class Sat a
+    class Data ctx a
+    instance  Sat (ctx Char)             => Data ctx Char
+    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
+
+    class Data Maybe a => Foo a
+
+    instance Foo t => Sat (Maybe t)
+
+    instance Data Maybe a => Foo a
+    instance Foo a        => Foo [a]
+    instance                 Foo [Char]
+
+In the instance for Foo [a], when generating evidence for the superclasses
+(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
+Using the instance for Data, we therefore need
+        (Sat (Maybe [a], Data Maybe a)
+But we are given (Foo a), and hence its superclass (Data Maybe a).
+So that leaves (Sat (Maybe [a])).  Using the instance for Sat means
+we need (Foo [a]).  And that is the very dictionary we are bulding
+an instance for!  So we must put that in the "givens".  So in this
+case we have
+       Given:  Foo a, Foo [a]
+       Watend: Data Maybe [a]
+
+BUT we must *not not not* put the *superclasses* of (Foo [a]) in
+the givens, which is what 'addGiven' would normally do. Why? Because
+(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted 
+by selecting a superclass from Foo [a], which simply makes a loop.
+
+On the other hand we *must* put the superclasses of (Foo a) in
+the givens, as you can see from the derivation described above.
+
+Conclusion: in the very special case of tcSimplifySuperClasses
+we have one 'given' (namely the "this" dictionary) whose superclasses
+must not be added to 'givens' by addGiven.  That is the *whole* reason
+for the red_given_scs field in RedEnv, and the function argument to
+addGiven.
+
 \begin{code}
-tcSimplifySuperClasses 
+tcSimplifySuperClasses
        :: InstLoc 
+       -> Inst         -- The dict whose superclasses 
+                       -- are being figured out
        -> [Inst]       -- Given 
        -> [Inst]       -- Wanted
        -> TcM TcDictBinds
-tcSimplifySuperClasses loc givens sc_wanteds
+tcSimplifySuperClasses loc this givens 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 }
   where
-    env = mkRedEnv (pprInstLoc loc) try_me givens
-    try_me _ = ReduceMe NoSCs
-       -- Like tryHardCheckLoop, but with NoSCs
+    env =  RedEnv { red_doc = pprInstLoc loc, 
+                   red_try_me = try_me,
+                   red_givens = this:givens, 
+                   red_given_scs = add_scs,
+                   red_stack = (0,[]),
+                   red_improve = False }  -- No unification vars
+    add_scs g | g==this   = NoSCs
+             | otherwise = AddSCs
+
+    try_me _ = ReduceMe  -- Try hard, so we completely solve the superclass 
+                        -- constraints right here. See Note [SUPERCLASS-LOOP 1]
 \end{code}
 
 
@@ -1356,7 +1423,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- BUT do no improvement!  See Plan D above
        -- HOWEVER, some unification may take place, if we instantiate
        --          a method Inst with an equality constraint
-       ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe AddSCs)
+       ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe)
        ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
 
        -- Next, figure out the tyvars we will quantify over
@@ -1404,7 +1471,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        ; let is_nested_group = isNotTopLevel top_lvl
              try_me inst | isFreeWrtTyVars qtvs inst,
                           (is_nested_group || isDict inst) = Stop
-                         | otherwise            = ReduceMe AddSCs
+                         | otherwise                       = ReduceMe 
              env = mkNoImproveRedEnv doc try_me
        ; (_imp, binds, irreds) <- reduceContext env wanteds'
 
@@ -1524,9 +1591,9 @@ tcSimplifyRuleLhs wanteds
          }
 
        -- Sigh: we need to reduce inside implications
-    red_env = mkRedEnv doc try_me []
+    red_env = mkInferRedEnv doc try_me
     doc = ptext (sLit "Implication constraint in RULE lhs")
-    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+    try_me inst | isMethodOrLit inst = ReduceMe
                | otherwise          = Stop     -- Be gentle
 \end{code}
 
@@ -1585,12 +1652,20 @@ tcSimplifyIPs given_ips wanteds
        ; let env = mkRedEnv doc try_me given_ips'
        ; (improved, binds, irreds) <- reduceContext env wanteds'
 
-       ; if not improved then 
+       ; if null irreds || not improved then 
                ASSERT( all is_free irreds )
                do { extendLIEs irreds
                   ; return binds }
-         else
-               tcSimplifyIPs given_ips wanteds }
+         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]
+        { binds1 <- tcSimplifyIPs given_ips' irreds
+        ; return $ binds `unionBags` binds1
+        } }
   where
     doc           = text "tcSimplifyIPs" <+> ppr given_ips
     ip_set = mkNameSet (ipNamesOfInsts given_ips)
@@ -1598,7 +1673,7 @@ tcSimplifyIPs given_ips wanteds
 
        -- Simplify any methods that mention the implicit parameter
     try_me inst | is_free inst = Stop
-               | otherwise    = ReduceMe NoSCs
+               | otherwise    = ReduceMe
 \end{code}
 
 
@@ -1673,8 +1748,11 @@ data RedEnv
           , red_try_me :: Inst -> WhatToDo
           , red_improve :: Bool                -- True <=> do improvement
           , red_givens :: [Inst]               -- All guaranteed rigid
-                                               -- Always dicts
+                                               -- Always dicts & equalities
                                                -- but see Note [Rigidity]
+          , red_given_scs :: Inst -> WantSCs   -- See Note [Recursive instances and superclases]
           , red_stack  :: (Int, [Inst])        -- Recursion stack (for err msg)
                                                -- See Note [RedStack]
   }
@@ -1697,6 +1775,16 @@ mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
 mkRedEnv doc try_me givens
   = RedEnv { red_doc = doc, red_try_me = try_me,
             red_givens = givens, 
+            red_given_scs = const AddSCs,
+            red_stack = (0,[]),
+            red_improve = True }       
+
+mkInferRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
+-- No givens at all
+mkInferRedEnv doc try_me
+  = RedEnv { red_doc = doc, red_try_me = try_me,
+            red_givens = [], 
+            red_given_scs = const AddSCs,
             red_stack = (0,[]),
             red_improve = True }       
 
@@ -1705,15 +1793,16 @@ mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
 mkNoImproveRedEnv doc try_me
   = RedEnv { red_doc = doc, red_try_me = try_me,
             red_givens = [], 
+            red_given_scs = const AddSCs,
             red_stack = (0,[]),
             red_improve = True }       
 
 data WhatToDo
- = ReduceMe WantSCs    -- Try to reduce this
-                       -- If there's no instance, 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)!
+ = ReduceMe    -- Try to reduce this
+               -- If there's no instance, 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)!
 
  | Stop                -- Return as irreducible unless it can
                        -- be reduced to a constant in one step
@@ -1788,7 +1877,8 @@ reduceContext env wanteds0
 
           -- Build the Avail mapping from "given_dicts"
        ; (init_state, _) <- getLIE $ do 
-               { init_state <- foldlM addGiven emptyAvails givens'
+               { init_state <- foldlM (addGiven (red_given_scs env)) 
+                                      emptyAvails givens'
                ; return init_state
                 }
 
@@ -1796,6 +1886,8 @@ reduceContext env wanteds0
          -- This may expose some further equational constraints...
        ; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds'
        ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+                  -- The getLIE is reqd because reduceList does improvement
+                  -- (via extendAvails) which may in turn do unification
        ; (dict_binds, 
            bound_dicts, 
            dict_irreds)       <- extractResults avails wanted_dicts
@@ -1806,8 +1898,12 @@ reduceContext env wanteds0
          -- as "given"   all the dicts that were originally given, 
          --              *or* for which we now have bindings, 
          --              *or* which are now irreds
-       ; let implic_env = env { red_givens = givens ++ bound_dicts ++
-                                              dict_irreds }
+          -- NB: Equality irreds need to be converted, as the recursive 
+          --     invocation of the solver will still treat them as wanteds
+          --     otherwise.
+       ; let implic_env = env { red_givens 
+                                   = givens ++ bound_dicts ++
+                                     map wantedToLocalEqInst dict_irreds }
        ; (implic_binds_s, implic_irreds_s) 
             <- mapAndUnzipM (reduceImplication implic_env) wanted_implics
        ; let implic_binds  = unionManyBags implic_binds_s
@@ -1819,12 +1915,16 @@ reduceContext env wanteds0
           --     improvement (i.e., instantiated type variables).
           -- (2) If we uncovered extra equalities.  We will try to solve them
           --     in the next iteration.
+          -- (3) If we reduced dictionaries (i.e., got dictionary bindings),
+          --     they may have exposed further opportunities to normalise
+          --     family applications.  See Note [Dictionary Improvement]
 
        ; let all_irreds       = dict_irreds ++ implic_irreds ++ extra_eqs
              avails_improved  = availsImproved avails
               improvedFlexible = avails_improved || eq_improved
               extraEqs         = (not . null) extra_eqs
-              improved         = improvedFlexible || extraEqs
+              reduced_dicts    = not (isEmptyBag dict_binds)
+              improved         = improvedFlexible || extraEqs || reduced_dicts
               --
               improvedHint  = (if avails_improved then " [AVAILS]" else "") ++
                               (if eq_improved then " [EQ]" else "") ++
@@ -1906,6 +2006,44 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
        ; return (tidy_env, msg) }
 \end{code}
 
+Note [Dictionary Improvement]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In reduceContext, we first reduce equalities and then class constraints.
+However, the letter may expose further opportunities for the former.  Hence,
+we need to go around again if dictionary reduction produced any dictionary
+bindings.  The following example demonstrated the point:
+
+  data EX _x _y (p :: * -> *)
+  data ANY
+
+  class Base p
+
+  class Base (Def p) => Prop p where
+   type Def p
+
+  instance Base ()
+  instance Prop () where
+   type Def () = ()
+
+  instance (Base (Def (p ANY))) => Base (EX _x _y p)
+  instance (Prop (p ANY)) => Prop (EX _x _y p) where
+   type Def (EX _x _y p) = EX _x _y p
+
+  data FOO x
+  instance Prop (FOO x) where
+   type Def (FOO x) = ()
+
+  data BAR
+  instance Prop BAR where
+   type Def BAR = EX () () FOO
+
+During checking the last instance declaration, we need to check the superclass
+cosntraint Base (Def BAR), which family normalisation reduced to 
+Base (EX () () FOO).  Chasing the instance for Base (EX _x _y p), gives us
+Base (Def (FOO ANY)), which again requires family normalisation of Def to
+Base () before we can finish.
+
+
 The main context-reduction function is @reduce@.  Here's its game plan.
 
 \begin{code}
@@ -1928,6 +2066,12 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
     -- Base case: we're done!
 reduce :: RedEnv -> Inst -> Avails -> TcM Avails
 reduce env wanted avails
+
+    -- We don't reduce equalities here (and they must not end up as irreds
+    -- in the Avails!)
+  | isEqInst wanted
+  = return avails
+
     -- It's the same as an existing inst, or a superclass thereof
   | Just _ <- findAvail avails wanted
   = do { traceTc (text "reduce: found " <+> ppr wanted)
@@ -1940,18 +2084,18 @@ reduce env wanted avails
            Stop -> try_simple (addIrred NoSCs);
                        -- See Note [No superclasses for Stop]
 
-           ReduceMe want_scs -> do     -- It should be reduced
+           ReduceMe -> do      -- It should be reduced
                { (avails, lookup_result) <- reduceInst env avails wanted
                ; case lookup_result of
-                   NoInstance -> addIrred want_scs avails wanted
+                   NoInstance -> addIrred AddSCs avails wanted
                             -- Add it and its superclasses
                             
-                   GenInst [] rhs -> addWanted want_scs avails wanted rhs []
+                   GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
 
                    GenInst wanteds' rhs
                          -> do { avails1 <- addIrred NoSCs avails wanted
                                ; avails2 <- reduceList env wanteds' avails1
-                               ; addWanted want_scs avails2 wanted rhs wanteds' } }
+                               ; addWanted AddSCs 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
@@ -1973,10 +2117,46 @@ reduce env wanted avails
 \end{code}
 
 
+Note [RECURSIVE DICTIONARIES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider 
+    data D r = ZeroD | SuccD (r (D r));
+    
+    instance (Eq (r (D r))) => Eq (D r) where
+        ZeroD     == ZeroD     = True
+        (SuccD a) == (SuccD b) = a == b
+        _         == _         = False;
+    
+    equalDC :: D [] -> D [] -> Bool;
+    equalDC = (==);
+
+We need to prove (Eq (D [])).  Here's how we go:
+
+       d1 : Eq (D [])
+
+by instance decl, holds if
+       d2 : Eq [D []]
+       where   d1 = dfEqD d2
+
+by instance decl of Eq, holds if
+       d3 : D []
+       where   d2 = dfEqList d3
+               d1 = dfEqD d2
+
+But now we can "tie the knot" to give
+
+       d3 = d1
+       d2 = dfEqList d3
+       d1 = dfEqD d2
+
+and it'll even run!  The trick is to put the thing we are trying to prove
+(in this case Eq (D []) into the database before trying to prove its
+contributing clauses.
+       
 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
+We need to be careful when adding "the constaint we are trying to prove".
+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 ...
@@ -2014,42 +2194,6 @@ Now we implement the Right Solution, which is to check for loops directly
 when adding superclasses.  It's a bit like the occurs check in unification.
 
 
-Note [RECURSIVE DICTIONARIES]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider 
-    data D r = ZeroD | SuccD (r (D r));
-    
-    instance (Eq (r (D r))) => Eq (D r) where
-        ZeroD     == ZeroD     = True
-        (SuccD a) == (SuccD b) = a == b
-        _         == _         = False;
-    
-    equalDC :: D [] -> D [] -> Bool;
-    equalDC = (==);
-
-We need to prove (Eq (D [])).  Here's how we go:
-
-       d1 : Eq (D [])
-
-by instance decl, holds if
-       d2 : Eq [D []]
-       where   d1 = dfEqD d2
-
-by instance decl of Eq, holds if
-       d3 : D []
-       where   d2 = dfEqList d3
-               d1 = dfEqD d2
-
-But now we can "tie the knot" to give
-
-       d3 = d1
-       d2 = dfEqList d3
-       d1 = dfEqD d2
-
-and it'll even run!  The trick is to put the thing we are trying to prove
-(in this case Eq (D []) into the database before trying to prove its
-contributing clauses.
-       
 
 %************************************************************************
 %*                                                                     *
@@ -2118,20 +2262,32 @@ Note that
        --
        -- Note on coercion variables:
        --
-       --      The extra given coercion variables are bound at two different sites:
+       --      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               
+       --              the solved dictionaries use these binders;
        --              these binders are generated by reduceImplication
        --
+        -- Note [Binders for equalities]
+        -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+        -- To reuse the binders of local/given equalities in the binders of 
+        -- implication constraints, it is crucial that these given equalities
+        -- always have the form
+        --   cotv :: t1 ~ t2
+        -- where cotv is a simple coercion type variable (and not a more
+        -- complex coercion term).  We require that the extra_givens always
+        -- have this form and exploit the special form when generating binders.
 reduceImplication env
        orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
                                  tci_tyvars = tvs,
-                                 tci_given = extra_givens, tci_wanted = wanteds })
+                                 tci_given = extra_givens, tci_wanted = wanteds
+                                 })
   = do {       -- Solve the sub-problem
-       ; let try_me _ = ReduceMe AddSCs  -- Note [Freeness and implications]
+       ; let try_me _ = ReduceMe  -- Note [Freeness and implications]
              env' = env { red_givens = extra_givens ++ red_givens env
                         , red_doc = sep [ptext (sLit "reduceImplication for") 
                                             <+> ppr name,
@@ -2143,13 +2299,6 @@ reduceImplication env
                        [ ppr (red_givens env), ppr extra_givens, 
                          ppr wanteds])
        ; (irreds, binds) <- 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 
-
-               -- Note [Reducing implication constraints]
-               -- Tom -- update note, put somewhere!
 
        ; traceTc (text "reduceImplication result" <+> vcat
                        [ppr irreds, ppr binds])
@@ -2163,17 +2312,17 @@ reduceImplication env
        -- SLPJ Sept 07: what if improvement happened inside the checkLoop?
        -- Then we must iterate the outer loop too!
 
+        ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
+                                   -- we solve wanted eqs by side effect!
+
+            -- Progress is no longer measered by the number of bindings
+            -- If there are any irreds, but no bindings and no solved
+            -- equalities, we back off and do nothing
         ; let backOff = isEmptyLHsBinds binds &&   -- no new bindings
                         (not $ null irreds)   &&   -- but still some irreds
-                        all (not . isEqInst) wanteds  
-                          -- we may have instantiated a cotv 
-                          -- => must make a new implication constraint!
-
-       ; traceTc $ text "reduceImplication condition" <+> ppr backOff
+                        didntSolveWantedEqs        -- no instantiated cotv
 
-          -- Progress is no longer measered by the number of bindings
        ; if backOff then       -- No progress
-               -- If there are any irreds, we back off and do nothing
                return (emptyBag, [orig_implic])
          else do
        { (simpler_implic_insts, bind) 
@@ -2183,26 +2332,29 @@ reduceImplication env
                -- 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
-                     <.> mkWpLams eq_tyvars
-                     <.> mkWpLams dict_ids
-                     <.> WpLet (binds `unionBags` bind)
-               wrap_inline | null dict_ids = idHsWrapper
-                           | otherwise     = WpInline
-               rhs = mkLHsWrap co payload
-               loc = instLocSpan inst_loc
-               payload = mkBigLHsTup (map (L loc . HsVar . instToId) dict_wanteds)
+       ; let   -- extract Id binders for dicts and CoTyVar binders for eqs;
+                -- see Note [Binders for equalities]
+             (extra_eq_givens, extra_dict_givens) = partition isEqInst 
+                                                               extra_givens
+              eq_cotvs = map instToVar extra_eq_givens
+             dict_ids = map instToId  extra_dict_givens 
+
+                        -- Note [Always inline implication constraints]
+              wrap_inline | null dict_ids = idHsWrapper
+                          | otherwise    = WpInline
+              co         = wrap_inline
+                           <.> mkWpTyLams tvs
+                           <.> mkWpTyLams eq_cotvs
+                           <.> mkWpLams dict_ids
+                           <.> WpLet (binds `unionBags` bind)
+              rhs        = mkLHsWrap co payload
+              loc        = instLocSpan inst_loc
+                            -- wanted equalities are solved by updating their
+                             -- cotv; we don't generate bindings for them
+              dict_bndrs =   map (L loc . HsVar . instToId) 
+                           . filter (not . isEqInst) 
+                           $ wanteds
+              payload    = mkBigLHsTup dict_bndrs
 
        
        ; traceTc (vcat [text "reduceImplication" <+> ppr name,
@@ -2388,6 +2540,9 @@ extractResults (Avails _ avails) wanteds
       = return (binds, bound_dicts, irreds)
 
     go binds bound_dicts irreds done (w:ws)
+      | isEqInst w
+      = go binds bound_dicts (w:irreds) done' ws
+
       | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
       = if w_id `elem` done_ids then
           go binds bound_dicts irreds done ws
@@ -2433,9 +2588,10 @@ addWanted want_scs avails wanted rhs_expr wanteds
   where
     avail = Rhs rhs_expr wanteds
 
-addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given given)
-       -- Always add superclasses for 'givens'
+addGiven :: (Inst -> WantSCs) -> Avails -> Inst -> TcM Avails
+addGiven want_scs avails given = addAvailAndSCs (want_scs given) avails given (Given given)
+       -- Conditionally add superclasses for 'givens'
+       -- See Note [Recursive instances and superclases]
        --
        -- 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',