Introducing a datatype for WorkLists that properly prioritizes equalities.
[ghc.git] / compiler / typecheck / TcInteract.lhs
index f9d3d97..4a049aa 100644 (file)
@@ -20,7 +20,6 @@ import TcType
 import HsBinds
 
 import Inst( tyVarsOfEvVar )
-import InstEnv
 import Class
 import TyCon
 import Name
@@ -226,22 +225,6 @@ Note [Basic plan]
 type AtomicInert = CanonicalCt     -- constraint pulled from InertSet
 type WorkItem    = CanonicalCt     -- constraint pulled from WorkList
 
--- A mixture of Given, Wanted, and Derived constraints. 
--- We split between equalities and the rest to process equalities first. 
-type WorkList = CanonicalCts
-
-unionWorkLists :: WorkList -> WorkList -> WorkList 
-unionWorkLists = andCCan
-
-isEmptyWorkList :: WorkList -> Bool 
-isEmptyWorkList = isEmptyCCan 
-
-emptyWorkList :: WorkList
-emptyWorkList = emptyCCan
-
-workListFromCCan :: CanonicalCt -> WorkList 
-workListFromCCan = singleCCan
-
 ------------------------
 data StopOrContinue 
   = Stop                       -- Work item is consumed
@@ -270,21 +253,24 @@ instance Outputable StageResult where
                  , ptext (sLit "new work =") <+> ppr work <> comma
                  , ptext (sLit "stop =") <+> ppr stop])
 
-type SimplifierStage = WorkItem -> InertSet -> TcS StageResult 
+type SubGoalDepth = Int          -- Starts at zero; used to limit infinite
+                         -- recursion of sub-goals
+type SimplifierStage = SubGoalDepth -> WorkItem -> InertSet -> TcS StageResult 
 
 -- Combine a sequence of simplifier 'stages' to create a pipeline 
-runSolverPipeline :: [(String, SimplifierStage)]
-                  -> InertSet -> WorkItem 
+runSolverPipeline :: SubGoalDepth
+                  -> [(String, SimplifierStage)]
+                 -> InertSet -> WorkItem 
                   -> TcS (InertSet, WorkList)
 -- Precondition: non-empty list of stages 
-runSolverPipeline pipeline inerts workItem
+runSolverPipeline depth pipeline inerts workItem
   = do { traceTcS "Start solver pipeline" $ 
             vcat [ ptext (sLit "work item =") <+> ppr workItem
                  , ptext (sLit "inerts    =") <+> ppr inerts]
 
        ; let itr_in = SR { sr_inerts = inerts
-                        , sr_new_work = emptyWorkList
-                        , sr_stop = ContinueWith workItem }
+                         , sr_new_work = emptyWorkList
+                         , sr_stop = ContinueWith workItem }
        ; itr_out <- run_pipeline pipeline itr_in
        ; let new_inert 
               = case sr_stop itr_out of 
@@ -301,9 +287,9 @@ runSolverPipeline pipeline inerts workItem
                  (SR { sr_new_work = accum_work
                      , sr_inerts   = inerts
                      , sr_stop     = ContinueWith work_item })
-      = do { itr <- stage work_item inerts 
+      = do { itr <- stage depth work_item inerts 
            ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
-           ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
+           ; let itr' = itr { sr_new_work = accum_work `unionWorkList` sr_new_work itr }
            ; run_pipeline stages itr' }
 \end{code}
 
@@ -363,7 +349,10 @@ solveInteract inert ws
                                                    -> (ct,evVarPred ev)) ws)
               , text "inert = " <+> ppr inert ]
 
-       ; (flag, inert_ret) <- foldlBagM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) ws 
+       ; can_ws <- mkCanonicalFEVs ws
+
+       ; (flag, inert_ret)
+           <- foldrWorkListM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) can_ws
 
        ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $
          vcat [ text "No interaction happened = " <+> ppr flag
@@ -371,29 +360,32 @@ solveInteract inert ws
 
        ; return (flag, inert_ret) }
 
-
 tryPreSolveAndInteract :: SimplContext
                        -> DynFlags
+                       -> CanonicalCt
                        -> (Bool, InertSet)
-                       -> FlavoredEvVar
                        -> TcS (Bool, InertSet)
 -- Returns: True if it was able to discharge this constraint AND all previous ones
-tryPreSolveAndInteract sctx dyn_flags (all_previous_discharged, inert)
-                       flavev@(EvVarX ev_var fl)
+tryPreSolveAndInteract sctx dyn_flags ct (all_previous_discharged, inert)
   = do { let inert_cts = get_inert_cts (evVarPred ev_var)
 
-       ; this_one_discharged <- dischargeFromCCans inert_cts flavev
+       ; this_one_discharged <- 
+           if isCFrozenErr ct then 
+               return False
+           else
+               dischargeFromCCans inert_cts ev_var fl
 
        ; if this_one_discharged
          then return (all_previous_discharged, inert)
 
          else do
-       { extra_cts <- mkCanonical fl ev_var
-       ; inert_ret <- solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[])
-                                             inert extra_cts
+       { inert_ret <- solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) ct inert
        ; return (False, inert_ret) } }
 
   where
+    ev_var = cc_id ct
+    fl = cc_flavor ct 
+
     get_inert_cts (ClassP clas _)
       | simplEqsOnly sctx = emptyCCan
       | otherwise         = fst (getRelevantCts clas (inert_dicts inert))
@@ -404,21 +396,30 @@ tryPreSolveAndInteract sctx dyn_flags (all_previous_discharged, inert)
     get_inert_cts (EqPred {})
       = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert)
 
-dischargeFromCCans :: CanonicalCts -> FlavoredEvVar -> TcS Bool
-dischargeFromCCans cans (EvVarX ev fl)
-  = Bag.foldlBagM discharge_ct False cans
-  where discharge_ct :: Bool -> CanonicalCt -> TcS Bool
-        discharge_ct True _ct = return True
-        discharge_ct False ct
-          | evVarPred (cc_id ct) `tcEqPred` evVarPred ev
-          , cc_flavor ct `canSolve` fl
-          = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct) 
-               ; return True }
-          where set_ev_bind x y
-                    | EqPred {} <- evVarPred y
-                    = setEvBind x (EvCoercion (mkCoVarCoercion y))
-                    | otherwise = setEvBind x (EvId y)
-        discharge_ct False _ct = return False
+dischargeFromCCans :: CanonicalCts -> EvVar -> CtFlavor -> TcS Bool
+-- See if this (pre-canonicalised) work-item is identical to a 
+-- one already in the inert set. Reasons:
+--    a) Avoid creating superclass constraints for millions of incoming (Num a) constraints
+--    b) Termination for improve_eqs in TcSimplify.simpl_loop
+dischargeFromCCans cans ev fl
+  = Bag.foldrBag discharge_ct (return False) cans
+  where 
+    the_pred = evVarPred ev
+
+    discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool
+    discharge_ct ct _rest
+      | evVarPred (cc_id ct) `tcEqPred` the_pred
+      , cc_flavor ct `canSolve` fl
+      = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct) 
+                -- Deriveds need no evidence
+                -- For Givens, we already have evidence, and we don't need it twice 
+           ; return True }
+      where 
+         set_ev_bind x y
+            | EqPred {} <- evVarPred y = setEvBind x (EvCoercion (mkCoVarCoercion y))
+            | otherwise                = setEvBind x (EvId y)
+
+    discharge_ct _ct rest = rest
 \end{code}
 
 Note [Avoiding the superclass explosion] 
@@ -437,16 +438,16 @@ canonicals. If so, we add nothing to the returned canonical
 constraints.
 
 \begin{code}
-solveOne :: InertSet -> WorkItem -> TcS InertSet 
-solveOne inerts workItem 
+solveOne :: WorkItem -> InertSet -> TcS InertSet 
+solveOne workItem inerts 
   = do { dyn_flags <- getDynFlags
-       ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
+       ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) workItem inerts
        }
 
 -----------------
 solveInteractWithDepth :: (Int, Int, [WorkItem])
-                       -> InertSet -> WorkList -> TcS InertSet
-solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws 
+                       -> WorkList -> InertSet -> TcS InertSet
+solveInteractWithDepth ctxt@(max_depth,n,stack) ws inert
   | isEmptyWorkList ws
   = return inert
 
@@ -456,33 +457,29 @@ solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
   | otherwise 
   = do { traceTcS "solveInteractWithDepth" $ 
               vcat [ text "Current depth =" <+> ppr n
-                   , text "Max depth =" <+> ppr max_depth ]
+                   , text "Max depth =" <+> ppr max_depth
+                   , text "ws =" <+> ppr ws ]
+
 
-             -- Solve equalities first
-       ; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws
-       ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
-       ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
+       ; foldrWorkListM (solveOneWithDepth ctxt) inert ws }
+              -- use foldr to preserve the order
 
 ------------------
 -- Fully interact the given work item with an inert set, and return a
 -- new inert set which has assimilated the new information.
 solveOneWithDepth :: (Int, Int, [WorkItem])
-                  -> InertSet -> WorkItem -> TcS InertSet
-solveOneWithDepth (max_depth, n, stack) inert work
-  = do { traceTcS0 (indent ++ "Solving {") (ppr work)
-       ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
+                  -> WorkItem -> InertSet -> TcS InertSet
+solveOneWithDepth (max_depth, depth, stack) work inert
+  = do { traceFireTcS depth (text "Solving {" <+> ppr work)
+       ; (new_inert, new_work) <- runSolverPipeline depth thePipeline inert work
          
-       ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
-
         -- Recursively solve the new work generated 
          -- from workItem, with a greater depth
-       ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
-                                new_inert new_work 
+       ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack) new_work new_inert 
+
+       ; traceFireTcS depth (text "Done }" <+> ppr work) 
 
-       ; traceTcS0 (indent ++ "Done }") (ppr work) 
        ; return res_inert }
-  where
-    indent = replicate (2*n) ' '
 
 thePipeline :: [(String,SimplifierStage)]
 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
@@ -524,7 +521,7 @@ Case 3: IP improvement work
 
 \begin{code}
 spontaneousSolveStage :: SimplifierStage 
-spontaneousSolveStage workItem inerts 
+spontaneousSolveStage depth workItem inerts 
   = do { mSolve <- trySpontaneousSolve workItem
 
        ; case mSolve of 
@@ -540,7 +537,9 @@ spontaneousSolveStage workItem inerts
                  -- its status change. This in turn may produce more work.
                 -- We do this *right now* (rather than just putting workItem'
                 -- back into the work-list) because we've solved 
-               -> do { (new_inert, new_work) <- runSolverPipeline 
+               -> do { bumpStepCountTcS
+                    ; traceFireTcS depth (ptext (sLit "Spontaneous (w/d)") <+> ppr workItem)
+                     ; (new_inert, new_work) <- runSolverPipeline depth
                              [ ("recursive interact with inert eqs", interactWithInertEqsStage)
                              , ("recursive interact with inerts", interactWithInertsStage)
                              ] inerts workItem'
@@ -551,9 +550,11 @@ spontaneousSolveStage workItem inerts
                | otherwise 
                    -> -- Original was given; he must then be inert all right, and
                       -- workList' are all givens from flattening
-                      return $ SR { sr_new_work = emptyWorkList
-                                  , sr_inerts   = inerts `updInertSet` workItem' 
-                                  , sr_stop     = Stop }
+                      do { bumpStepCountTcS
+                        ; traceFireTcS depth (ptext (sLit "Spontaneous (g)") <+> ppr workItem)
+                         ; return $ SR { sr_new_work = emptyWorkList
+                                       , sr_inerts   = inerts `updInertSet` workItem' 
+                                       , sr_stop     = Stop } }
            SPError -> -- Return with no new work
                return $ SR { sr_new_work = emptyWorkList
                            , sr_inerts   = inerts
@@ -584,7 +585,8 @@ trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar =
   | otherwise
   = do { tch1 <- isTouchableMetaTyVar tv1
        ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
-                 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem) 
+                 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" 
+                                    (ppr workItem) 
                          ; return SPCantSolve }
        }
 
@@ -725,7 +727,7 @@ solveWithIdentity cv wd tv xi
        ; setWantedTyBind tv xi
        ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi xi
 
-       ; when (isWanted wd) (setWantedCoBind cv xi)
+       ; when (isWanted wd) (setCoBind cv xi)
            -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
 
        ; return $ SPSolved (CTyEqCan { cc_id = cv_given
@@ -734,14 +736,37 @@ solveWithIdentity cv wd tv xi
 \end{code}
 
 
-
-
 *********************************************************************************
 *                                                                               * 
                        The interact-with-inert Stage
 *                                                                               *
 *********************************************************************************
 
+Note [The Solver Invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We always add Givens first.  So you might think that the solver has
+the invariant
+
+   If the work-item is Given, 
+   then the inert item must Given
+
+But this isn't quite true.  Suppose we have, 
+    c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
+After processing the first two, we get
+     c1: [G] beta ~ [alpha], c2 : [W] blah
+Now, c3 does not interact with the the given c1, so when we spontaneously
+solve c3, we must re-react it with the inert set.  So we can attempt a 
+reaction between inert c2 [W] and work-item c3 [G].
+
+It *is* true that [Solver Invariant]
+   If the work-item is Given, 
+   AND there is a reaction
+   then the inert item must Given
+or, equivalently,
+   If the work-item is Given, 
+   and the inert item is Wanted/Derived
+   then there is no reaction
+
 \begin{code}
 -- Interaction result of  WorkItem <~> AtomicInert
 data InteractResult
@@ -758,24 +783,32 @@ data InteractResult
 
         , ir_new_work     :: WorkList
             -- new work items to add to the WorkList
+
+        , ir_fire :: Maybe String    -- Tells whether a rule fired, and if so what
         }
 
 -- What to do with the inert reactant.
-data InertAction = KeepInert 
-                 | DropInert 
-                 | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert
+data InertAction = KeepInert | DropInert 
 
-mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
-mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork 
+mkIRContinue :: String -> WorkItem -> InertAction -> WorkList -> TcS InteractResult
+mkIRContinue rule wi keep newWork 
+  = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep
+                , ir_new_work = newWork, ir_fire = Just rule }
 
-mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
-mkIRStop keep newWork = return $ IR Stop keep newWork 
+mkIRStopK :: String -> WorkList -> TcS InteractResult
+mkIRStopK rule newWork
+  = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert
+                , ir_new_work = newWork, ir_fire = Just rule }
 
-dischargeWorkItem :: Monad m => m InteractResult
-dischargeWorkItem = mkIRStop KeepInert emptyWorkList
+mkIRStopD :: String -> WorkList -> TcS InteractResult
+mkIRStopD rule newWork
+  = return $ IR { ir_stop = Stop, ir_inert_action = DropInert
+                , ir_new_work = newWork, ir_fire = Just rule }
 
 noInteraction :: Monad m => WorkItem -> m InteractResult
-noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
+noInteraction wi
+  = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert
+                , ir_new_work = emptyWorkList, ir_fire = Nothing }
 
 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert 
      -- See Note [Efficient Orientation] 
@@ -788,8 +821,9 @@ data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
 -- interact the WorkItem with the entire equalities of the InertSet
 
 interactWithInertEqsStage :: SimplifierStage 
-interactWithInertEqsStage workItem inert
-  = Bag.foldlBagM interactNext initITR (inert_eqs inert)
+interactWithInertEqsStage depth workItem inert
+  = Bag.foldrBagM (interactNext depth) initITR (inert_eqs inert)
+                        -- use foldr to preserve the order          
   where
     initITR = SR { sr_inerts   = inert { inert_eqs = emptyCCan }
                  , sr_new_work = emptyWorkList
@@ -802,12 +836,13 @@ interactWithInertEqsStage workItem inert
 -- "Other" constraints it contains!
 
 interactWithInertsStage :: SimplifierStage
-interactWithInertsStage workItem inert
+interactWithInertsStage depth workItem inert
   = let (relevant, inert_residual) = getISRelevant workItem inert 
         initITR = SR { sr_inerts   = inert_residual
                      , sr_new_work = emptyWorkList
                      , sr_stop     = ContinueWith workItem } 
-    in Bag.foldlBagM interactNext initITR relevant 
+    in Bag.foldrBagM (interactNext depth) initITR relevant 
+                        -- use foldr to preserve the order
   where 
     getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet) 
     getISRelevant (CFrozenErr {}) is = (emptyCCan, is)
@@ -834,37 +869,51 @@ interactWithInertsStage workItem inert
                     , inert_ips    = emptyCCanMap
                     , inert_funeqs = emptyCCanMap })
 
-interactNext :: StageResult -> AtomicInert -> TcS StageResult 
-interactNext it inert  
-  | ContinueWith workItem <- sr_stop it
-  = do { let inerts      = sr_inerts it 
-
-       ; ir <- interactWithInert inert workItem
-
-       -- New inerts depend on whether we KeepInert or not and must
-       -- be updated with FD improvement information from the interaction result (ir)
-       ; let inerts_new = case ir_inert_action ir of
-                            KeepInert                   -> inerts `updInertSet` inert
-                            DropInert                   -> inerts
-                            KeepTransformedInert inert' -> inerts `updInertSet` inert'
+interactNext :: SubGoalDepth -> AtomicInert -> StageResult -> TcS StageResult 
+interactNext depth inert it
+  | ContinueWith work_item <- sr_stop it
+  = do { let inerts = sr_inerts it 
+
+       ; IR { ir_new_work = new_work, ir_inert_action = inert_action
+            , ir_fire = fire_info, ir_stop = stop } 
+            <- interactWithInert inert work_item
+
+       ; let mk_msg rule 
+              = text rule <+> keep_doc
+                <+> vcat [ ptext (sLit "Inert =") <+> ppr inert
+                         , ptext (sLit "Work =")  <+> ppr work_item
+                         , ppUnless (isEmptyWorkList new_work) $
+                            ptext (sLit "New =") <+> ppr new_work ]
+             keep_doc = case inert_action of
+                         KeepInert -> ptext (sLit "[keep]")
+                         DropInert -> ptext (sLit "[drop]")
+       ; case fire_info of
+           Just rule -> do { bumpStepCountTcS
+                           ; traceFireTcS depth (mk_msg rule) }
+           Nothing  -> return ()
+
+       -- New inerts depend on whether we KeepInert or not 
+       ; let inerts_new = case inert_action of
+                            KeepInert -> inerts `updInertSet` inert
+                            DropInert -> inerts
 
        ; return $ SR { sr_inerts   = inerts_new
-                     , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
-                     , sr_stop     = ir_stop ir } }
+                     , sr_new_work = sr_new_work it `unionWorkList` new_work
+                     , sr_stop     = stop } }
   | otherwise 
   = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
 
 -- Do a single interaction of two constraints.
 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
-interactWithInert inert workitem 
-  =  do { ctxt <- getTcSContext
-        ; let is_allowed  = allowedInteraction (simplEqsOnly ctxt) inert workitem 
+interactWithInert inert workItem 
+  = do { ctxt <- getTcSContext
+       ; let is_allowed  = allowedInteraction (simplEqsOnly ctxt) inert workItem 
 
-        ; if is_allowed then 
-              doInteractWithInert inert workitem 
+       ; if is_allowed then 
+              doInteractWithInert inert workItem 
           else 
-              noInteraction workitem 
-        }
+              noInteraction workItem 
+       }
 
 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool 
 -- Allowed interactions 
@@ -877,27 +926,73 @@ doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
 -- Identical class constraints.
 
 doInteractWithInert
-           (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) 
-  workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
+  inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) 
+   workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
   | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
-  = solveOneFromTheOther (d1,fl1) workItem 
+  = solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem 
 
   | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
   =     -- See Note [When improvement happens]
     do { let pty1 = ClassP cls1 tys1
              pty2 = ClassP cls2 tys2
-             work_item_pred_loc = (pty2, pprFlavorArising fl2)
              inert_pred_loc     = (pty1, pprFlavorArising fl1)
-            loc                = combineCtLoc fl1 fl2
-             eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
-                             -- See Note [Efficient Orientation]
-
-       ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs
-       ; fd_work <- mapM mkCanonicalFEV derived_evs
-                 -- See Note [Generating extra equalities]
-
-       ; mkIRContinue workItem KeepInert (unionManyBags fd_work)
-       }
+             work_item_pred_loc = (pty2, pprFlavorArising fl2)
+             fd_eqns = improveFromAnother 
+                                  inert_pred_loc     -- the template
+                                  work_item_pred_loc -- the one we aim to rewrite
+                                  -- See Note [Efficient Orientation]
+
+       ; m <- rewriteWithFunDeps fd_eqns tys2 fl2
+       ; case m of 
+           Nothing -> noInteraction workItem
+           Just (rewritten_tys2, cos2, fd_work)
+             | tcEqTypes tys1 rewritten_tys2
+             -> -- Solve him on the spot in this case
+               case fl2 of
+                 Given   {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem)
+                  Derived {} -> mkIRStopK "Cls/Cls fundep (solved)" fd_work
+                 Wanted  {} 
+                   | isDerived fl1 
+                   -> do { setDictBind d2 (EvCast d1 dict_co)
+                        ; let inert_w = inertItem { cc_flavor = fl2 }
+                          -- A bit naughty: we take the inert Derived, 
+                          -- turn it into a Wanted, use it to solve the work-item
+                          -- and put it back into the work-list
+                          -- Maybe rather than starting again, we could *replace* the
+                          -- inert item, but its safe and simple to restart
+                         ; mkIRStopD "Cls/Cls fundep (solved)" $ 
+                           workListFromNonEq inert_w `unionWorkList` fd_work }
+                   | otherwise 
+                    -> do { setDictBind d2 (EvCast d1 dict_co)
+                          ; mkIRStopK "Cls/Cls fundep (solved)" fd_work }
+
+             | otherwise
+             -> -- We could not quite solve him, but we still rewrite him
+               -- Example: class C a b c | a -> b
+               --          Given: C Int Bool x, Wanted: C Int beta y
+               --          Then rewrite the wanted to C Int Bool y
+               --          but note that is still not identical to the given
+               -- The important thing is that the rewritten constraint is
+               -- inert wrt the given.
+               -- However it is not necessarily inert wrt previous inert-set items.
+                --      class C a b c d |  a -> b, b c -> d
+               --      Inert: c1: C b Q R S, c2: C P Q a b
+               --      Work: C P alpha R beta
+               --      Does not react with c1; reacts with c2, with alpha:=Q
+               --      NOW it reacts with c1!
+               -- So we must stop, and put the rewritten constraint back in the work list
+                do { d2' <- newDictVar cls1 rewritten_tys2
+                   ; case fl2 of
+                       Given {}   -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem)
+                       Wanted {}  -> setDictBind d2 (EvCast d2' dict_co)
+                       Derived {} -> return ()
+                   ; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 }
+                   ; mkIRStopK "Cls/Cls fundep (partial)" $ 
+                     workListFromNonEq workItem' `unionWorkList` fd_work } 
+
+             where
+               dict_co = mkTyConCoercion (classTyCon cls1) cos2
+  }
 
 -- Class constraint and given equality: use the equality to rewrite
 -- the class constraint. 
@@ -908,14 +1003,14 @@ doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_r
   = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
             -- Continue with rewritten Dictionary because we can only be in the 
             -- interactWithEqsStage, so the dictionary is inert. 
-       ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
+       ; mkIRContinue "Eq/Cls" rewritten_dict KeepInert emptyWorkList }
     
 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis }) 
            workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
   | wfl `canRewrite` ifl
   , tv `elemVarSet` tyVarsOfTypes xis
   = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
-       ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
+       ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromNonEq rewritten_dict) }
 
 -- Class constraint and given equality: use the equality to rewrite
 -- the class constraint.
@@ -924,14 +1019,14 @@ doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_r
   | ifl `canRewrite` wfl
   , tv `elemVarSet` tyVarsOfType ty 
   = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty) 
-       ; mkIRContinue rewritten_ip KeepInert emptyWorkList } 
+       ; mkIRContinue "Eq/IP" rewritten_ip KeepInert emptyWorkList } 
 
 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty }) 
            workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
   | wfl `canRewrite` ifl
   , tv `elemVarSet` tyVarsOfType ty
   = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty) 
-       ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
+       ; mkIRContinue "IP/Eq" workItem DropInert (workListFromNonEq rewritten_ip) }
 
 -- Two implicit parameter constraints.  If the names are the same,
 -- but their types are not, we generate a wanted type equality 
@@ -944,19 +1039,19 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i
   =    -- See Note [Overriding implicit parameters]
         -- Dump the inert item, override totally with the new one
        -- Do not require type equality
-    mkIRContinue workItem DropInert emptyWorkList
+       -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
+       --              we must *override* the outer one with the inner one
+    mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
 
   | nm1 == nm2 && ty1 `tcEqType` ty2 
-  = solveOneFromTheOther (id1,ifl) workItem 
+  = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem 
 
   | nm1 == nm2
   =    -- See Note [When improvement happens]
-    do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation]
+    do { co_var <- newCoVar ty2 ty1 -- See Note [Efficient Orientation]
        ; let flav = Wanted (combineCtLoc ifl wfl) 
        ; cans <- mkCanonical flav co_var 
-       ; mkIRContinue workItem KeepInert cans }
-
-
+       ; mkIRContinue "IP/IP fundep" workItem KeepInert cans }
 
 -- Never rewrite a given with a wanted equality, and a type function
 -- equality can never rewrite an equality. We rewrite LHS *and* RHS 
@@ -970,7 +1065,7 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_
   | ifl `canRewrite` wfl 
   , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
   = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2) 
-       ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) } 
+       ; mkIRStopK "Eq/FunEq" (workListFromEq rewritten_funeq) } 
          -- Must Stop here, because we may no longer be inert after the rewritting.
 
 -- Inert: function equality, work item: equality
@@ -980,7 +1075,7 @@ doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
   | wfl `canRewrite` ifl
   , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
   = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1) 
-       ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) } 
+       ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromEq rewritten_funeq) } 
          -- One may think that we could (KeepTransformedInert rewritten_funeq) 
          -- but that is wrong, because it may end up not being inert with respect 
          -- to future inerts. Example: 
@@ -996,10 +1091,10 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
                                , cc_tyargs = args2, cc_rhs = xi2 })
   | fl1 `canSolve` fl2 && lhss_match
   = do { cans <- rewriteEqLHS LeftComesFromInert  (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) 
-       ; mkIRStop KeepInert cans } 
+       ; mkIRStopK "FunEq/FunEq" cans } 
   | fl2 `canSolve` fl1 && lhss_match
   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) 
-       ; mkIRContinue workItem DropInert cans }
+       ; mkIRContinue "FunEq/FunEq" workItem DropInert cans }
   where
     lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) 
 
@@ -1008,30 +1103,32 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc
 -- Check for matching LHS 
   | fl1 `canSolve` fl2 && tv1 == tv2 
   = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) 
-       ; mkIRStop KeepInert cans } 
+       ; mkIRStopK "Eq/Eq lhs" cans } 
 
   | fl2 `canSolve` fl1 && tv1 == tv2 
   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) 
-       ; mkIRContinue workItem DropInert cans }
+       ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans }
+
 -- Check for rewriting RHS 
   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2 
   = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2) 
-       ; mkIRStop KeepInert rewritten_eq }
+       ; mkIRStopK "Eq/Eq rhs" rewritten_eq }
+
   | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
   = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) 
-       ; mkIRContinue workItem DropInert rewritten_eq } 
+       ; mkIRContinue "Eq/Eq rhs" workItem DropInert rewritten_eq } 
 
 doInteractWithInert (CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
                     (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
-       ; mkIRStop KeepInert rewritten_frozen }
+       ; mkIRStopK "Frozen/Eq" rewritten_frozen }
 
 doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
            workItem@(CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
-       ; mkIRContinue workItem DropInert rewritten_frozen }
+       ; mkIRContinue "Frozen/Eq" workItem DropInert rewritten_frozen }
 
 -- Fall-through case for all other situations
 doInteractWithInert _ workItem = noInteraction workItem
@@ -1078,16 +1175,16 @@ rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)                   -- cv2 :: F ar
 
              xi2'    = substTyWith [tv] [xi1] xi2
              xi2_co  = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2' 
-       ; cv2' <- case gw of 
-                   Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2'
-                                   ; setWantedCoBind cv2 $ 
-                                     fun_co `mkTransCoercion` 
-                                            mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co
-                                   ; return cv2' } 
-                   Given {}  -> newGivenCoVar (mkTyConApp tc args') xi2' $
-                                  mkSymCoercion fun_co `mkTransCoercion` 
-                                                mkCoVarCoercion cv2 `mkTransCoercion` xi2_co
-                   Derived {} -> newDerivedId (EqPred (mkTyConApp tc args') xi2')
+
+       ; cv2' <- newCoVar (mkTyConApp tc args') xi2'
+       ; case gw of 
+           Wanted {} -> setCoBind cv2  (fun_co               `mkTransCoercion` 
+                                        mkCoVarCoercion cv2' `mkTransCoercion` 
+                                        mkSymCoercion xi2_co)
+           Given {}  -> setCoBind cv2' (mkSymCoercion fun_co `mkTransCoercion` 
+                                        mkCoVarCoercion cv2  `mkTransCoercion` 
+                                        xi2_co)
+           Derived {} -> return () 
 
        ; return (CFunEqCan { cc_id = cv2'
                            , cc_flavor = gw
@@ -1106,79 +1203,63 @@ rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkLis
 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2) 
   | Just tv2' <- tcGetTyVar_maybe xi2'
   , tv2 == tv2'         -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
-  = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2')) 
-       ; return emptyCCan } 
+  = do { when (isWanted gw) (setCoBind cv2 (mkSymCoercion co2')) 
+       ; return emptyWorkList } 
   | otherwise
-  = do { cv2' <-
-           case gw of
-             Wanted {}
-                 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
-                       ; setWantedCoBind cv2 $
-                         mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
-                       ; return cv2' }
-             Given {} 
-                 -> newGivenCoVar (mkTyVarTy tv2) xi2' $ 
-                    mkCoVarCoercion cv2 `mkTransCoercion` co2'
-             Derived {} 
-                 -> newDerivedId (EqPred (mkTyVarTy tv2) xi2')
-
-       ; canEq gw cv2' (mkTyVarTy tv2) xi2' 
-       }
+  = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2'
+       ; case gw of
+             Wanted {} -> setCoBind cv2 $ mkCoVarCoercion cv2' `mkTransCoercion` 
+                                          mkSymCoercion co2'
+             Given {}  -> setCoBind cv2' $ mkCoVarCoercion cv2 `mkTransCoercion` 
+                                           co2'
+             Derived {} -> return ()
+       ; canEqToWorkList gw cv2' (mkTyVarTy tv2) xi2' }
   where 
     xi2' = substTyWith [tv1] [xi1] xi2 
     co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2  -- xi2 ~ xi2[xi1/tv1]
 
-
 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
 -- Used to ineract two equalities of the following form: 
 -- First Equality:   co1: (XXX ~ xi1)  
 -- Second Equality:  cv2: (XXX ~ xi2) 
--- Where the cv1 `canSolve` cv2 equality 
+-- Where the cv1 `canRewrite` cv2 equality 
 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1), 
 --    See Note [Efficient Orientation] for that 
-rewriteEqLHS which (co1,xi1) (cv2,gw,xi2) 
-  = do { cv2' <- case (isWanted gw, which) of 
-                   (True,LeftComesFromInert) ->
-                       do { cv2' <- newWantedCoVar xi2 xi1 
-                          ; setWantedCoBind cv2 $ 
-                            co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
-                          ; return cv2' } 
-                   (True,RightComesFromInert) -> 
-                       do { cv2' <- newWantedCoVar xi1 xi2 
-                          ; setWantedCoBind cv2 $ 
-                            co1 `mkTransCoercion` mkCoVarCoercion cv2'
-                          ; return cv2' } 
-                   (False,LeftComesFromInert) ->
-                       if isGiven gw then 
-                           newGivenCoVar xi2 xi1 $ 
-                           mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1 
-                       else newDerivedId (EqPred xi2 xi1) 
-                   (False,RightComesFromInert) -> 
-                       if isGiven gw then 
-                           newGivenCoVar xi1 xi2 $
-                           mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
-                       else newDerivedId (EqPred xi1 xi2)
+rewriteEqLHS LeftComesFromInert (co1,xi1) (cv2,gw,xi2) 
+  = do { cv2' <- newCoVar xi2 xi1 
+       ; case gw of 
+           Wanted {} -> setCoBind cv2 $ 
+                        co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
+           Given {}  -> setCoBind cv2' $ 
+                        mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1 
+           Derived {} -> return ()
+       ; mkCanonical gw cv2' }
+
+rewriteEqLHS RightComesFromInert (co1,xi1) (cv2,gw,xi2) 
+  = do { cv2' <- newCoVar xi1 xi2
+       ; case gw of
+           Wanted {} -> setCoBind cv2 $
+                        co1 `mkTransCoercion` mkCoVarCoercion cv2'
+           Given {}  -> setCoBind cv2' $
+                        mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
+           Derived {} -> return ()
        ; mkCanonical gw cv2' }
-                                           
+
 rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList
 rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
-  = do { cv2' <-
-           case fl2 of
-             Wanted {} -> do { cv2' <- newWantedCoVar ty2a' ty2b'
-                                           -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
-                                    ; setWantedCoBind cv2 $
-                                        co2a'                `mkTransCoercion`
-                                        mkCoVarCoercion cv2' `mkTransCoercion`
-                                        mkSymCoercion co2b'
-                                    ; return cv2' }
-
-             Given {} -> newGivenCoVar ty2a' ty2b' $
-                        mkSymCoercion co2a'  `mkTransCoercion`
-                        mkCoVarCoercion cv2  `mkTransCoercion`
-                        co2b'
-
-             Derived {} -> newDerivedId (EqPred ty2a' ty2b')
-      ; return (singleCCan $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) }
+  = do { cv2' <- newCoVar ty2a' ty2b'  -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
+       ; case fl2 of
+             Wanted {} -> setCoBind cv2 $ co2a'                `mkTransCoercion`
+                                                 mkCoVarCoercion cv2' `mkTransCoercion`
+                                                 mkSymCoercion co2b'
+
+             Given {} -> setCoBind cv2' $ mkSymCoercion co2a'  `mkTransCoercion`
+                                         mkCoVarCoercion cv2  `mkTransCoercion`
+                                         co2b'
+
+             Derived {} -> return ()
+
+      ; return (workListFromNonEq $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) }
   where
     (ty2a, ty2b) = coVarKind cv2          -- cv2 : ty2a ~ ty2b
     ty2a' = substTyWith [tv1] [xi1] ty2a
@@ -1187,28 +1268,29 @@ rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
     co2a' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2a  -- ty2a ~ ty2a[xi1/tv1]
     co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b  -- ty2b ~ ty2b[xi1/tv1]
 
-solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
--- First argument inert, second argument workitem. They both represent 
--- wanted/given/derived evidence for the *same* predicate so we try here to 
--- discharge one directly from the other. 
+solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult
+-- First argument inert, second argument work-item. They both represent 
+-- wanted/given/derived evidence for the *same* predicate so 
+-- we can discharge one directly from the other. 
 --
 -- Precondition: value evidence only (implicit parameters, classes) 
 --               not coercion
-solveOneFromTheOther (iid,ifl) workItem
-  | ifl `canSolve` wfl
-  = do { when (isWanted wfl) $ setEvBind wid (EvId iid)
-           -- Overwrite the binding, if one exists
-          -- For Givens, which are lambda-bound, nothing to overwrite,
-       ; dischargeWorkItem }
-  | wfl `canSolve` ifl
-  = do { when (isWanted ifl) $ setEvBind iid (EvId wid)
-       ; mkIRContinue workItem DropInert emptyWorkList }
-
-  | otherwise -- One of the two is Derived, we can just throw it away, 
-              -- preferrably the work item. 
-  = if isDerived wfl then dischargeWorkItem 
-    else mkIRContinue workItem DropInert emptyWorkList
+solveOneFromTheOther info (ev_term,ifl) workItem
+  | isDerived wfl
+  = mkIRStopK ("Solved[DW] " ++ info) emptyWorkList
+
+  | isDerived ifl -- The inert item is Derived, we can just throw it away, 
+                 -- The workItem is inert wrt earlier inert-set items, 
+                 -- so it's safe to continue on from this point
+  = mkIRContinue ("Solved[DI] " ++ info) workItem DropInert emptyWorkList
   
+  | otherwise
+  = ASSERT( ifl `canSolve` wfl )
+      -- Because of Note [The Solver Invariant], plus Derived dealt with
+    do { when (isWanted wfl) $ setEvBind wid ev_term
+           -- Overwrite the binding, if one exists
+          -- If both are Given, we already have evidence; no need to duplicate
+       ; mkIRStopK ("Solved " ++ info) emptyWorkList }
   where 
      wfl = cc_flavor workItem
      wid = cc_id workItem
@@ -1577,7 +1659,7 @@ data TopInteractResult
                                        -- arising from top-level instances.
 
 topReactionsStage :: SimplifierStage 
-topReactionsStage workItem inerts 
+topReactionsStage depth workItem inerts 
   = do { tir <- tryTopReact workItem 
        ; case tir of 
            NoTopInt -> 
@@ -1585,10 +1667,14 @@ topReactionsStage workItem inerts
                            , sr_new_work = emptyWorkList 
                            , sr_stop     = ContinueWith workItem } 
            SomeTopInt tir_new_work tir_new_inert -> 
-               return $ SR { sr_inerts   = inerts 
-                           , sr_new_work = tir_new_work
-                           , sr_stop     = tir_new_inert
-                           }
+               do { bumpStepCountTcS
+                  ; traceFireTcS depth (ptext (sLit "Top react")
+                       <+> vcat [ ptext (sLit "Work =") <+> ppr workItem
+                                , ptext (sLit "New =") <+> ppr tir_new_work ])
+                  ; return $ SR { sr_inerts   = inerts 
+                               , sr_new_work = tir_new_work
+                               , sr_stop     = tir_new_inert
+                               } }
        }
 
 tryTopReact :: WorkItem -> TcS TopInteractResult 
@@ -1618,47 +1704,69 @@ doTopReact (CDictCan { cc_flavor = Given {} })
   = return NoTopInt -- NB: Superclasses already added since it's canonical
 
 -- Derived dictionary: just look for functional dependencies
-doTopReact workItem@(CDictCan { cc_flavor = Derived loc
+doTopReact workItem@(CDictCan { cc_flavor = fl@(Derived loc)
                               , cc_class = cls, cc_tyargs = xis })
-  = do { fd_work <- findClassFunDeps cls xis loc
-       ; if isEmptyWorkList fd_work then 
-              return NoTopInt
-         else return $ SomeTopInt { tir_new_work = fd_work
-                                  , tir_new_inert = ContinueWith workItem } }
+  = do { instEnvs <- getInstEnvs
+       ; let fd_eqns = improveFromInstEnv instEnvs
+                                                (ClassP cls xis, pprArisingAt loc)
+       ; m <- rewriteWithFunDeps fd_eqns xis fl
+       ; case m of
+           Nothing -> return NoTopInt
+           Just (xis',_,fd_work) ->
+               let workItem' = workItem { cc_tyargs = xis' }
+                   -- Deriveds are not supposed to have identity (cc_id is unused!)
+               in return $ SomeTopInt { tir_new_work  = fd_work 
+                                      , tir_new_inert = ContinueWith workItem' } }
+
 -- Wanted dictionary
-doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
-                              , cc_class = cls, cc_tyargs = xis }) 
+doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc)
+                              , cc_class = cls, cc_tyargs = xis })
   = do { -- See Note [MATCHING-SYNONYMS]
        ; lkp_inst_res <- matchClassInst cls xis loc
-       ; case lkp_inst_res of 
-           NoInstance -> 
-             do { traceTcS "doTopReact/ no class instance for" (ppr dv) 
-                ; fd_work <- findClassFunDeps cls xis loc
-                ; return $ SomeTopInt
-                              { tir_new_work  = fd_work
-                              , tir_new_inert = ContinueWith workItem } }
-
-           GenInst wtvs ev_term ->  -- Solved 
+       ; case lkp_inst_res of
+           NoInstance ->
+             do { traceTcS "doTopReact/ no class instance for" (ppr dv)
+
+                ; instEnvs <- getInstEnvs
+                ; let fd_eqns = improveFromInstEnv instEnvs
+                                                         (ClassP cls xis, pprArisingAt loc)
+                ; m <- rewriteWithFunDeps fd_eqns xis fl
+                ; case m of
+                    Nothing -> return NoTopInt
+                    Just (xis',cos,fd_work) ->
+                        do { let dict_co = mkTyConCoercion (classTyCon cls) cos
+                           ; dv'<- newDictVar cls xis'
+                           ; setDictBind dv (EvCast dv' dict_co)
+                           ; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl, 
+                                                        cc_class = cls, cc_tyargs = xis' }
+                           ; return $ 
+                             SomeTopInt { tir_new_work  = workListFromNonEq workItem' `unionWorkList` fd_work
+                                        , tir_new_inert = Stop } } }
+
+           GenInst wtvs ev_term -- Solved 
                   -- No need to do fundeps stuff here; the instance 
                   -- matches already so we won't get any more info
                   -- from functional dependencies
-               do { traceTcS "doTopReact/ found class instance for" (ppr dv) 
-                  ; setDictBind dv ev_term 
-                  ; inst_work <- canWanteds wtvs
-                  ; if null wtvs
+             | null wtvs
+             -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv) 
+                   ; setDictBind dv ev_term 
                     -- Solved in one step and no new wanted work produced. 
                     -- i.e we directly matched a top-level instance
                     -- No point in caching this in 'inert'; hence Stop
-                    then return $ SomeTopInt { tir_new_work  = emptyWorkList 
-                                             , tir_new_inert = Stop }
-
-                    -- Solved and new wanted work produced, you may cache the 
-                   -- (tentatively solved) dictionary as Given! (used to be: Derived)
-                    else do { let solved = makeSolvedByInst workItem
-                            ; return $ SomeTopInt 
-                                  { tir_new_work  = inst_work
-                                  , tir_new_inert = ContinueWith solved } }
-       }          }
+                   ; return $ SomeTopInt { tir_new_work  = emptyWorkList 
+                                         , tir_new_inert = Stop } }
+
+             | otherwise
+             -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv) 
+                   ; setDictBind dv ev_term 
+                        -- Solved and new wanted work produced, you may cache the 
+                        -- (tentatively solved) dictionary as Given! (used to be: Derived)
+                   ; let solved   = workItem { cc_flavor = given_fl }
+                         given_fl = Given (setCtLocOrigin loc UnkSkol) 
+                   ; inst_work <- canWanteds wtvs
+                   ; return $ SomeTopInt { tir_new_work  = inst_work
+                                         , tir_new_inert = ContinueWith solved } }
+       }          
 
 -- Type functions
 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
@@ -1677,8 +1785,8 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
                             -- See Note [Type synonym families] in TyCon
                          coe = mkTyConApp coe_tc rep_tys 
                    ; cv' <- case fl of
-                              Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
-                                              ; setWantedCoBind cv $ 
+                              Wanted {} -> do { cv' <- newCoVar rhs_ty xi
+                                              ; setCoBind cv $ 
                                                     coe `mkTransCoercion`
                                                       mkCoVarCoercion cv'
                                               ; return cv' }
@@ -1694,20 +1802,6 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
 
 -- Any other work item does not react with any top-level equations
 doTopReact _workItem = return NoTopInt 
-
-----------------------
-findClassFunDeps :: Class -> [Xi] -> WantedLoc -> TcS WorkList
--- Look for a fundep reaction beween the wanted item 
--- and a top-level instance declaration
-findClassFunDeps cls xis loc
- = do { instEnvs <- getInstEnvs
-      ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
-                                               (ClassP cls xis, pprArisingAt loc)
-      ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs
-                     -- NB: fundeps generate some wanted equalities, but 
-                     --     we don't use their evidence for anything
-      ; cts <- mapM mkCanonicalFEV derived_evs
-      ; return $ unionManyBags cts }
 \end{code}