Comments and layout only
[ghc-hetmet.git] / compiler / typecheck / TcInteract.lhs
index a403bc4..cb9d342 100644 (file)
@@ -211,9 +211,6 @@ getFDImprovements :: InertSet -> FDImprovements
 getFDImprovements = inert_fds 
 
 
 getFDImprovements = inert_fds 
 
 
-isWantedCt :: CanonicalCt -> Bool 
-isWantedCt ct = isWanted (cc_flavor ct)
-
 {- TODO: Later ...
 data Inert = IS { class_inerts :: FiniteMap Class Atomics
                  ip_inerts    :: FiniteMap Class Atomics
 {- TODO: Later ...
 data Inert = IS { class_inerts :: FiniteMap Class Atomics
                  ip_inerts    :: FiniteMap Class Atomics
@@ -287,50 +284,27 @@ Note [Basic plan]
    Superclass decomposition belongs in (4), see note [Superclasses]
 
 \begin{code}
    Superclass decomposition belongs in (4), see note [Superclasses]
 
 \begin{code}
-
 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 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. 
-data WorkList    = WL { wl_eqs   :: CanonicalCts -- Equalities (CTyEqCan, CFunEqCan) 
-                      , wl_other :: CanonicalCts   -- Other 
-                      }
-type SWorkList         = WorkList        -- A worklist of solved 
+type WorkList = CanonicalCts
+type SWorkList = WorkList        -- A worklist of solved 
 
 unionWorkLists :: WorkList -> WorkList -> WorkList 
 
 unionWorkLists :: WorkList -> WorkList -> WorkList 
-unionWorkLists wl1 wl2 
-  = WL { wl_eqs   = andCCan (wl_eqs wl1) (wl_eqs wl2)
-       , wl_other = andCCan (wl_other wl1) (wl_other wl2) }
-
-foldWorkListEqCtsM :: Monad m => (a -> WorkItem -> m a) -> a -> WorkList -> m a 
--- Fold over the equalities of a worklist 
-foldWorkListEqCtsM f r wl = Bag.foldlBagM f r (wl_eqs wl) 
-
-foldWorkListOtherCtsM :: Monad m => (a -> WorkItem -> m a) -> a -> WorkList -> m a 
--- Fold over non-equality constraints of a worklist
-foldWorkListOtherCtsM f r wl = Bag.foldlBagM f r (wl_other wl) 
+unionWorkLists = andCCan
 
 isEmptyWorkList :: WorkList -> Bool 
 
 isEmptyWorkList :: WorkList -> Bool 
-isEmptyWorkList wl = isEmptyCCan (wl_eqs wl) && isEmptyCCan (wl_other wl) 
+isEmptyWorkList = isEmptyCCan 
 
 emptyWorkList :: WorkList
 
 emptyWorkList :: WorkList
-emptyWorkList = WL { wl_eqs = emptyCCan, wl_other = emptyCCan } 
-
-workListFromCCans :: CanonicalCts -> WorkList 
--- Generic, no precondition 
-workListFromCCans cts = WL eqs others 
-  where (eqs, others) = Bag.partitionBag isTyEqCCan cts
+emptyWorkList = emptyCCan
 
 workListFromCCan :: CanonicalCt -> WorkList 
 
 workListFromCCan :: CanonicalCt -> WorkList 
-workListFromCCan ct | isTyEqCCan ct = WL (singleCCan ct) emptyCCan 
-                    | otherwise     = WL emptyCCan (singleCCan ct) 
--- TODO: 
--- At the call sites of workListFromCCan(s), sometimes we know whether the new work
--- involves equalities or not. It's probably a good idea to add specialized calls for 
--- those, to avoid asking whether 'isTyEqCCan' all the time.
-
+workListFromCCan = singleCCan
 
 
+------------------------
 data StopOrContinue 
   = Stop                       -- Work item is consumed
   | ContinueWith WorkItem      -- Not consumed
 data StopOrContinue 
   = Stop                       -- Work item is consumed
   | ContinueWith WorkItem      -- Not consumed
@@ -358,9 +332,6 @@ instance Outputable StageResult where
                  , ptext (sLit "new work =") <+> ppr work <> comma
                  , ptext (sLit "stop =") <+> ppr stop])
 
                  , ptext (sLit "new work =") <+> ppr work <> comma
                  , ptext (sLit "stop =") <+> ppr stop])
 
-instance Outputable WorkList where 
-  ppr (WL eqcts othercts) = vcat [ppr eqcts, ppr othercts] 
-
 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult 
 
 -- Combine a sequence of simplifier 'stages' to create a pipeline 
 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult 
 
 -- Combine a sequence of simplifier 'stages' to create a pipeline 
@@ -429,8 +400,7 @@ React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canoni
 solveInteract :: InertSet -> CanonicalCts -> TcS InertSet
 solveInteract inert ws 
   = do { dyn_flags <- getDynFlags
 solveInteract :: InertSet -> CanonicalCts -> TcS InertSet
 solveInteract inert ws 
   = do { dyn_flags <- getDynFlags
-       ; let worklist = workListFromCCans ws 
-       ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert worklist
+       ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws
        }
 solveOne :: InertSet -> WorkItem -> TcS InertSet 
 solveOne inerts workItem 
        }
 solveOne :: InertSet -> WorkItem -> TcS InertSet 
 solveOne inerts workItem 
@@ -450,12 +420,13 @@ solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
 
   | otherwise 
   = do { traceTcS "solveInteractWithDepth" $ 
 
   | otherwise 
   = do { traceTcS "solveInteractWithDepth" $ 
-         vcat [ text "Current depth =" <+> ppr n
-              , text "Max depth =" <+> ppr max_depth
-              ]
-       ; is_from_eqs <- foldWorkListEqCtsM (solveOneWithDepth ctxt) inert ws 
-       ; foldWorkListOtherCtsM (solveOneWithDepth ctxt) is_from_eqs ws
-       }
+              vcat [ text "Current depth =" <+> ppr n
+                   , text "Max depth =" <+> ppr max_depth ]
+
+             -- Solve equalities first
+       ; let (eqs, non_eqs) = Bag.partitionBag isTyEqCCan ws
+       ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
+       ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
 
 ------------------
 -- Fully interact the given work item with an inert set, and return a
 
 ------------------
 -- Fully interact the given work item with an inert set, and return a
@@ -491,6 +462,64 @@ thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
 *                                                                               *
 *********************************************************************************
 
 *                                                                               *
 *********************************************************************************
 
+Note [Efficient Orientation] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+There are two cases where we have to be careful about 
+orienting equalities to get better efficiency. 
+
+Case 2: In Rewriting Equalities (function rewriteEqLHS) 
+
+    When rewriting two equalities with the same LHS:
+          (a)  (tv ~ xi1) 
+          (b)  (tv ~ xi2) 
+    We have a choice of producing work (xi1 ~ xi2) (up-to the
+    canonicalization invariants) However, to prevent the inert items
+    from getting kicked out of the inerts first, we prefer to
+    canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
+    ~ xi1) if (a) comes from the inert set.
+    
+    This choice is implemented using the WhichComesFromInert flag. 
+
+Case 2: In Spontaneous Solving 
+     Example 2a:
+     Inerts:   [w1] : D alpha 
+               [w2] : C beta 
+               [w3] : F alpha ~ Int 
+               [w4] : H beta  ~ Int 
+     Untouchables = [beta] 
+     Then a wanted (beta ~ alpha) comes along. 
+        1) While interacting with the inerts it is going to kick w2,w4
+           out of the inerts
+        2) Then, it will spontaneoulsy be solved by (alpha := beta)
+        3) Now (and here is the tricky part), to add him back as
+           solved (alpha ~ beta) is no good because, in the next
+           iteration, it will kick out w1,w3 as well so we will end up
+           with *all* the inert equalities back in the worklist!
+      
+      So it is tempting to just add (beta ~ alpha) instead, that is, 
+      maintain the original orietnation of the constraint. 
+
+      But that does not work very well, because it may cause the 
+      "double unification problem" (See Note [Avoid double unifications]). 
+      For instance: 
+
+      Example 2b: 
+           [w1] : fsk1 ~ alpha 
+           [w2] : fsk2 ~ alpha 
+           ---
+      At the end of the interaction suppose we spontaneously solve alpha := fsk1 
+      but keep [Given] fsk1 ~ alpha. Then, the second time around we see the 
+      constraint (fsk2 ~ alpha), and we unify *again* alpha := fsk2, which is wrong.
+
+      Our conclusion is that, while in some cases (Example 2a), it makes sense to 
+      preserve the original orientation, it is hard to do this in a sound way. 
+      So we *don't* do this for now, @solveWithIdentity@ outputs a constraint that 
+      is oriented with the unified variable on the left. 
+
+Case 3: Functional Dependencies and IP improvement work
+    TODO. Optimisation not yet implemented there. 
+
 \begin{code}
 spontaneousSolveStage :: SimplifierStage 
 spontaneousSolveStage workItem inerts 
 \begin{code}
 spontaneousSolveStage :: SimplifierStage 
 spontaneousSolveStage workItem inerts 
@@ -501,10 +530,27 @@ spontaneousSolveStage workItem inerts
                            , sr_inerts     = inerts
                            , sr_stop       = ContinueWith workItem }
 
                            , sr_inerts     = inerts
                            , sr_stop       = ContinueWith workItem }
 
-           Just workList' -> -- He has been solved; workList' are all givens
-               return $ SR { sr_new_work = workList'
-                           , sr_inerts   = inerts 
-                           , sr_stop     = Stop }
+           Just (workItem', workList')
+               | not (isGivenCt workItem) 
+                -- Original was wanted or derived but we have now made him 
+                 -- given so we have to interact him with the inerts due to
+                 -- 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 
+                             [ ("recursive interact with inert eqs", interactWithInertEqsStage)
+                             , ("recursive interact with inerts", interactWithInertsStage)
+                             ] inerts workItem'
+                     ; return $ SR { sr_new_work = new_work `unionWorkLists` workList'
+                                       , sr_inerts   = new_inert -- will include workItem' 
+                                       , sr_stop     = Stop }
+                     }
+               | otherwise 
+                   -> -- Original was given; he must then be inert all right, and
+                      -- workList' are all givens from flattening
+                      return $ SR { sr_new_work = workList' 
+                                  , sr_inerts   = inerts `updInertSet` workItem' 
+                                  , sr_stop     = Stop }
        }
 
 -- @trySpontaneousSolve wi@ solves equalities where one side is a
        }
 
 -- @trySpontaneousSolve wi@ solves equalities where one side is a
@@ -513,8 +559,8 @@ spontaneousSolveStage workItem inerts
 --   * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
 --                 See Note [Touchables and givens] 
 -- NB: just passing the inerts through for the skolem equivalence classes
 --   * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
 --                 See Note [Touchables and givens] 
 -- NB: just passing the inerts through for the skolem equivalence classes
-trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList)
-trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts 
+trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe (WorkItem, SWorkList)) 
+trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts 
   | isGiven gw
   = return Nothing
   | Just tv2 <- tcGetTyVar_maybe xi
   | isGiven gw
   = return Nothing
   | Just tv2 <- tcGetTyVar_maybe xi
@@ -528,7 +574,9 @@ trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_r
   | otherwise
   = do { tch1 <- isTouchableMetaTyVar tv1
        ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
   | otherwise
   = do { tch1 <- isTouchableMetaTyVar tv1
        ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
-                 else return Nothing }
+                 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem) 
+                         ; return Nothing }
+       }
 
   -- No need for 
   --      trySpontaneousSolve (CFunEqCan ...) = ...
 
   -- No need for 
   --      trySpontaneousSolve (CFunEqCan ...) = ...
@@ -536,26 +584,29 @@ trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_r
 trySpontaneousSolve _ _ = return Nothing 
 
 ----------------
 trySpontaneousSolve _ _ = return Nothing 
 
 ----------------
-trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
-                       -> TcS (Maybe SWorkList)
+trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi 
+                       -> TcS (Maybe (WorkItem,SWorkList))
 -- tv is a MetaTyVar, not untouchable
 trySpontaneousEqOneWay inerts cv gw tv xi      
   | not (isSigTyVar tv) || isTyVarTy xi 
 -- tv is a MetaTyVar, not untouchable
 trySpontaneousEqOneWay inerts cv gw tv xi      
   | not (isSigTyVar tv) || isTyVarTy xi 
-  = if typeKind xi `isSubKind` tyVarKind tv then
-        solveWithIdentity inerts cv gw tv xi
-    else if tyVarKind tv `isSubKind` typeKind xi then 
+  = do { kxi <- zonkTcTypeTcS xi >>= return . typeKind  -- Must look through the TcTyBinds
+                                                        -- hence kxi and not typeKind xi
+                                                        -- See Note [Kind Errors]
+       ; if kxi `isSubKind` tyVarKind tv then
+             solveWithIdentity inerts cv gw tv xi
+         else if tyVarKind tv `isSubKind` kxi then 
              return Nothing -- kinds are compatible but we can't solveWithIdentity this way
                             -- This case covers the  a_touchable :: * ~ b_untouchable :: ?? 
                             -- which has to be deferred or floated out for someone else to solve 
                             -- it in a scope where 'b' is no longer untouchable. 
          else kindErrorTcS gw (mkTyVarTy tv) xi -- See Note [Kind errors]
              return Nothing -- kinds are compatible but we can't solveWithIdentity this way
                             -- This case covers the  a_touchable :: * ~ b_untouchable :: ?? 
                             -- which has to be deferred or floated out for someone else to solve 
                             -- it in a scope where 'b' is no longer untouchable. 
          else kindErrorTcS gw (mkTyVarTy tv) xi -- See Note [Kind errors]
-
+       }
   | otherwise -- Still can't solve, sig tyvar and non-variable rhs
   = return Nothing 
 
 ----------------
 trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
   | otherwise -- Still can't solve, sig tyvar and non-variable rhs
   = return Nothing 
 
 ----------------
 trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
-                       -> TcS (Maybe SWorkList)
+                       -> TcS (Maybe (WorkItem,SWorkList))
 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
 trySpontaneousEqTwoWay inerts cv gw tv1 tv2
   | k1 `isSubKind` k2
 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
 trySpontaneousEqTwoWay inerts cv gw tv1 tv2
   | k1 `isSubKind` k2
@@ -582,6 +633,17 @@ constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately
 
 The same applies in canonicalization code in case of kind errors in the givens. 
 
 
 The same applies in canonicalization code in case of kind errors in the givens. 
 
+However, when we canonicalize givens we only check for compatibility (@compatKind@). 
+If there were a kind error in the givens, this means some form of inconsistency or dead code. 
+
+When we spontaneously solve wanteds we may have to look through the bindings, hence we 
+call zonkTcTypeTcS above. The reason is that maybe xi is @alpha@ where alpha :: ? and 
+a previous spontaneous solving has set (alpha := f) with (f :: *). The reason that xi is 
+still alpha and not f is becasue the solved constraint may be oriented as (f ~ alpha) instead
+of (alpha ~ f). Then we should be using @xi@s "real" kind, which is * and not ?, when we try
+to detect whether spontaneous solving is possible. 
+
+
 Note [Spontaneous solving and kind compatibility] 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Note [Spontaneous solving and kind compatibility] 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -611,8 +673,11 @@ Caveat:
      Whereas we would be able to apply the type instance, we would not be able to 
      use the given (T Bool ~ (->)) in the body of 'flop' 
 
      Whereas we would be able to apply the type instance, we would not be able to 
      use the given (T Bool ~ (->)) in the body of 'flop' 
 
-Note [Loopy spontaneous solving] 
+Note [Loopy Spontaneous Solving] 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Example 1: [The problem of loopy spontaneous solving]
+----------
 Consider the original wanted: 
    wanted :  Maybe (E alpha) ~ alpha 
 where E is a type family, such that E (T x) = x. After canonicalization, 
 Consider the original wanted: 
    wanted :  Maybe (E alpha) ~ alpha 
 where E is a type family, such that E (T x) = x. After canonicalization, 
@@ -629,6 +694,8 @@ actually solving. But this occurs check *must look through* flatten skolems.
 However, it may be the case that the flatten skolem in hand is equal to some other 
 flatten skolem whith *does not* mention our unification variable. Here's a typical example:
 
 However, it may be the case that the flatten skolem in hand is equal to some other 
 flatten skolem whith *does not* mention our unification variable. Here's a typical example:
 
+Example 2: [The need of keeping track of flatten skolem equivalence classes]
+----------
 Original wanteds: 
    g: F alpha ~ F beta 
    w: alpha ~ F alpha 
 Original wanteds: 
    g: F alpha ~ F beta 
    w: alpha ~ F alpha 
@@ -647,6 +714,8 @@ We will look inside f2, which immediately mentions (F alpha), so it's not good t
 by looking at the equivalence class of the flatten skolems, we can see that it is fine to 
 unify (alpha ~ f1) which solves our goals! 
 
 by looking at the equivalence class of the flatten skolems, we can see that it is fine to 
 unify (alpha ~ f1) which solves our goals! 
 
+Example 3: [The need of looking through TyBinds for already spontaneously solved variables]
+----------
 A similar problem happens because of other spontaneous solving. Suppose we have the 
 following wanteds, arriving in this exact order:
   (first)  w: beta ~ alpha 
 A similar problem happens because of other spontaneous solving. Suppose we have the 
 following wanteds, arriving in this exact order:
   (first)  w: beta ~ alpha 
@@ -660,6 +729,50 @@ that is wrong since fsk mentions beta, which has already secretly been unified t
 To avoid this problem, the same occurs check must unveil rewritings that can happen because 
 of spontaneously having solved other constraints. 
 
 To avoid this problem, the same occurs check must unveil rewritings that can happen because 
 of spontaneously having solved other constraints. 
 
+Example 4: [Orientation of (tv ~ xi) equalities] 
+----------
+We orient equalities (tv ~ xi) so that flatten skolems appear on the left, if possible. Here
+is an example of why this is needed: 
+
+  [Wanted] w1: alpha ~ fsk 
+  [Given]  g1: F alpha ~ fsk 
+  [Given]  g2: b ~ fsk 
+  Flatten skolem equivalence class = [] 
+
+Assume that g2 is *not* oriented properly, as shown above. Then we would like to spontaneously
+solve w1 but we can't set alpha := fsk, since fsk hides the type F alpha. However, by using 
+the equation g2 it would be possible to solve w1 by setting  alpha := b. In other words, it is
+not enough to look at a flatten skolem equivalence class to try to find alternatives to unify
+with. We may have to go to other variables. 
+
+By orienting the equalities so that flatten skolems are in the LHS we are eliminating them
+as much as possible from the RHS of other wanted equalities, and hence it suffices to look 
+in their flatten skolem equivalence classes. 
+
+NB: This situation appears in the IndTypesPerf test case, inside indexed-types/.
+
+Caveat: You may wonder if we should be doing this for unification variables as well. 
+However, Note [Efficient Orientation], Case 2, demonstrates that this is not possible 
+at least for touchable unification variables which we have to keep oriented with the 
+touchable on the LHS to be able to eliminate it. So then, what about untouchables? 
+
+Example 4a: 
+-----------
+  Untouchable = beta, Touchable = alpha 
+
+  [Wanted] w1: alpha ~ fsk 
+  [Given]  g1: F alpha ~ fsk 
+  [Given]  g2: beta ~ fsk 
+  Flatten skolem equivalence class = [] 
+
+Should we be able to unify  alpha := beta to solve the constraint? Arguably yes, but 
+that implies that an *untouchable* unification variable (beta) is in the same equivalence
+class as a flatten skolem that mentions @alpha@. I.e. g2 means that: 
+  beta ~ F alpha
+But I do not think that there is any way to produce evidence for such a constraint from
+the outside other than beta := F alpha, which violates the OutsideIn-ness.  
+
+
 
 Note [Avoid double unifications] 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Note [Avoid double unifications] 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -683,44 +796,67 @@ unification variables as RHS of type family equations: F xis ~ alpha.
 ----------------
 solveWithIdentity :: InertSet 
                   -> CoVar -> CtFlavor -> TcTyVar -> Xi 
 ----------------
 solveWithIdentity :: InertSet 
                   -> CoVar -> CtFlavor -> TcTyVar -> Xi 
-                  -> TcS (Maybe SWorkList)
+                  -> TcS (Maybe (WorkItem, SWorkList)) 
 -- Solve with the identity coercion 
 -- Precondition: kind(xi) is a sub-kind of kind(tv)
 -- Precondition: CtFlavor is Wanted or Derived
 -- See [New Wanted Superclass Work] to see why solveWithIdentity 
 --     must work for Derived as well as Wanted
 -- Solve with the identity coercion 
 -- Precondition: kind(xi) is a sub-kind of kind(tv)
 -- Precondition: CtFlavor is Wanted or Derived
 -- See [New Wanted Superclass Work] to see why solveWithIdentity 
 --     must work for Derived as well as Wanted
+-- Returns: (workItem, workList) where 
+--        workItem = the new Given constraint
+--        workList = some additional work that may have been produced as a result of flattening
+--                   in case we did some chasing through flatten skolem equivalence classes.
 solveWithIdentity inerts cv gw tv xi 
   = do { tybnds <- getTcSTyBindsMap
        ; case occurCheck tybnds inerts tv xi of 
            Nothing              -> return Nothing 
            Just (xi_unflat,coi) -> solve_with xi_unflat coi }
   where
 solveWithIdentity inerts cv gw tv xi 
   = do { tybnds <- getTcSTyBindsMap
        ; case occurCheck tybnds inerts tv xi of 
            Nothing              -> return Nothing 
            Just (xi_unflat,coi) -> solve_with xi_unflat coi }
   where
-    solve_with xi_unflat coi  -- coi : xi_unflat ~ xi  
+    solve_with xi_unflat coi  -- coi : xi_unflat ~ xi
       = do { traceTcS "Sneaky unification:" $ 
                        vcat [text "Coercion variable:  " <+> ppr gw, 
                              text "Coercion:           " <+> pprEq (mkTyVarTy tv) xi,
                              text "Left  Kind is     : " <+> ppr (typeKind (mkTyVarTy tv)),
                              text "Right Kind is     : " <+> ppr (typeKind xi)
                   ]
       = do { traceTcS "Sneaky unification:" $ 
                        vcat [text "Coercion variable:  " <+> ppr gw, 
                              text "Coercion:           " <+> pprEq (mkTyVarTy tv) xi,
                              text "Left  Kind is     : " <+> ppr (typeKind (mkTyVarTy tv)),
                              text "Right Kind is     : " <+> ppr (typeKind xi)
                   ]
+
            ; setWantedTyBind tv xi_unflat        -- Set tv := xi_unflat
            ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
            ; let flav = mkGivenFlavor gw UnkSkol 
            ; setWantedTyBind tv xi_unflat        -- Set tv := xi_unflat
            ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
            ; let flav = mkGivenFlavor gw UnkSkol 
-           ; (cts, co) <- case coi of 
-               ACo co  -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
-                             ; return (can_eqs, co) }
-               IdCo co -> return $ 
-                          (singleCCan (CTyEqCan { cc_id = cv_given 
-                                                , cc_flavor = mkGivenFlavor gw UnkSkol
-                                                , cc_tyvar = tv, cc_rhs = xi }
-                                                -- xi, *not* xi_unflat because 
-                                                -- xi_unflat may require flattening!
-                                      ), co)
+           ; (ct,cts, co) <- case coi of 
+               ACo co  -> do { (cc,ccs) <- canEqLeafTyVarLeft flav cv_given tv xi_unflat
+                             ; return (cc, ccs, co) } 
+               IdCo co -> return $ (CTyEqCan { cc_id = cv_given 
+                                             , cc_flavor = mkGivenFlavor gw UnkSkol
+                                             , cc_tyvar = tv, cc_rhs = xi }
+                                      -- xi, *not* xi_unflat because 
+                                      -- xi_unflat may require flattening!
+                                   , emptyWorkList, co)
            ; case gw of 
                Wanted  {} -> setWantedCoBind  cv co
                Derived {} -> setDerivedCoBind cv co 
                _          -> pprPanic "Can't spontaneously solve *given*" empty 
            ; case gw of 
                Wanted  {} -> setWantedCoBind  cv co
                Derived {} -> setDerivedCoBind cv co 
                _          -> pprPanic "Can't spontaneously solve *given*" empty 
-                     -- See Note [Avoid double unifications] 
-           ; return $ Just (workListFromCCans cts)  }
+                     -- See Note [Avoid double unifications]
+           ; return $ Just (ct,cts)
+           }
+
+--            ; let flav = mkGivenFlavor gw UnkSkol 
+--            ; (cts, co) <- case coi of 
+--                             -- TODO: Optimise this, along the way it used to be 
+--                ACo co  -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv)  xi_unflat xi_unflat
+--                              ; setWantedTyBind tv xi_unflat
+--                              ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
+--                              ; return (can_eqs, co) }
+--                IdCo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi 
+--                              ; setWantedTyBind tv xi
+--                              ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi
+--                              ; return (can_eqs, co) }
+--            ; case gw of 
+--                Wanted  {} -> setWantedCoBind  cv co
+--                Derived {} -> setDerivedCoBind cv co 
+--                _          -> pprPanic "Can't spontaneously solve *given*" empty 
+--                   -- See Note [Avoid double unifications] 
+--            ; return $ Just cts }
 
 occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet
            -> TcTyVar -> TcType -> Maybe (TcType,CoercionI) 
 
 occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet
            -> TcTyVar -> TcType -> Maybe (TcType,CoercionI) 
@@ -852,6 +988,7 @@ noInteraction :: Monad m => WorkItem -> m InteractResult
 noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
 
 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert 
 noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
 
 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert 
+     -- See Note [Efficient Orientation, Case 2] 
 
 
 ---------------------------------------------------
 
 
 ---------------------------------------------------
@@ -959,11 +1096,10 @@ doInteractWithInert fdimprs
              eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc         
 
        ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs 
              eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc         
 
        ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs 
-       ; fd_cts <- canWanteds wevvars 
-       ; let fd_work = workListFromCCans fd_cts 
+       ; fd_work <- canWanteds wevvars 
                 -- See Note [Generating extra equalities]
        ; traceTcS "Checking if improvements existed." (ppr fdimprs) 
                 -- See Note [Generating extra equalities]
        ; traceTcS "Checking if improvements existed." (ppr fdimprs) 
-       ; if isEmptyCCan fd_cts || haveBeenImproved fdimprs pty1 pty2 then
+       ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then
              -- Must keep going
              mkIRContinue workItem KeepInert fd_work 
          else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2))
              -- Must keep going
              mkIRContinue workItem KeepInert fd_work 
          else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2))
@@ -1038,7 +1174,7 @@ doInteractWithInert _fdimprs
     do { co_var <- newWantedCoVar ty1 ty2 
        ; let flav = Wanted (combineCtLoc ifl wfl) 
        ; cans <- mkCanonical flav co_var 
     do { co_var <- newWantedCoVar ty1 ty2 
        ; let flav = Wanted (combineCtLoc ifl wfl) 
        ; cans <- mkCanonical flav co_var 
-       ; mkIRContinue workItem KeepInert (workListFromCCans cans) }
+       ; mkIRContinue workItem KeepInert cans }
 
 
 -- Inert: equality, work item: function equality
 
 
 -- Inert: equality, work item: function equality
@@ -1077,10 +1213,10 @@ doInteractWithInert _fdimprs
                                , cc_tyargs = args2, cc_rhs = xi2 })
   | fl1 `canSolve` fl2 && lhss_match
   = do { cans <- rewriteEqLHS LeftComesFromInert  (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) 
                                , cc_tyargs = args2, cc_rhs = xi2 })
   | fl1 `canSolve` fl2 && lhss_match
   = do { cans <- rewriteEqLHS LeftComesFromInert  (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) 
-       ; mkIRStop KeepInert (workListFromCCans cans) } 
+       ; mkIRStop KeepInert cans } 
   | fl2 `canSolve` fl1 && lhss_match
   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) 
   | fl2 `canSolve` fl1 && lhss_match
   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) 
-       ; mkIRContinue workItem DropInert (workListFromCCans cans) }
+       ; mkIRContinue workItem DropInert cans }
   where
     lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) 
 
   where
     lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) 
 
@@ -1090,19 +1226,19 @@ doInteractWithInert _fdimprs
 -- Check for matching LHS 
   | fl1 `canSolve` fl2 && tv1 == tv2 
   = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) 
 -- Check for matching LHS 
   | fl1 `canSolve` fl2 && tv1 == tv2 
   = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) 
-       ; mkIRStop KeepInert (workListFromCCans cans) } 
+       ; mkIRStop KeepInert cans } 
 
   | fl2 `canSolve` fl1 && tv1 == tv2 
   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) 
 
   | fl2 `canSolve` fl1 && tv1 == tv2 
   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) 
-       ; mkIRContinue workItem DropInert (workListFromCCans cans) } 
+       ; mkIRContinue 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) 
 
 -- Check for rewriting RHS 
   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2 
   = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2) 
-       ; mkIRStop KeepInert (workListFromCCans rewritten_eq) }
+       ; mkIRStop KeepInert rewritten_eq }
   | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
   = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) 
   | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
   = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) 
-       ; mkIRContinue workItem DropInert (workListFromCCans rewritten_eq) } 
+       ; mkIRContinue workItem DropInert rewritten_eq } 
 
 -- Finally, if workitem is a Flatten Equivalence Class constraint and the 
 -- inert is a wanted constraint, even when the workitem cannot rewrite the 
 
 -- Finally, if workitem is a Flatten Equivalence Class constraint and the 
 -- inert is a wanted constraint, even when the workitem cannot rewrite the 
@@ -1169,7 +1305,7 @@ rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
                            , cc_rhs = xi2 }) }
 
 
                            , cc_rhs = xi2 }) }
 
 
-rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS CanonicalCts
+rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
 -- Use the first equality to rewrite the second, flavors already checked. 
 -- E.g.          c1 : tv1 ~ xi1   c2 : tv2 ~ xi2
 -- rewrites c2 to give
 -- Use the first equality to rewrite the second, flavors already checked. 
 -- E.g.          c1 : tv1 ~ xi1   c2 : tv2 ~ xi2
 -- rewrites c2 to give
@@ -1194,26 +1330,20 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
                     mkCoVarCoercion cv2 `mkTransCoercion` co2'
 
        ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2 
                     mkCoVarCoercion cv2 `mkTransCoercion` co2'
 
        ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2 
-       ; return (singleCCan $ CTyEqCan { cc_id = cv2' 
-                                       , cc_flavor = gw 
-                                       , cc_tyvar = tv2 
-                                       , cc_rhs   = xi2'' })
+       ; canEq gw cv2' (mkTyVarTy tv2) xi2''
        }
   where 
     xi2' = substTyWith [tv1] [xi1] xi2 
     co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2  -- xi2 ~ xi2[xi1/tv1]
 
 
        }
   where 
     xi2' = substTyWith [tv1] [xi1] xi2 
     co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2  -- xi2 ~ xi2[xi1/tv1]
 
 
-rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
+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 
 -- 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 
--- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This 
--- depends on whether the left or the right equality comes from the inert set. 
--- We must:  
---     prefer to create (xi2 ~ xi1) if the first comes from the inert 
---     prefer to create (xi1 ~ xi2) if the second comes from the inert 
+-- 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) ->
 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2) 
   = do { cv2' <- case (isWanted gw, which) of 
                    (True,LeftComesFromInert) ->
@@ -1664,20 +1794,60 @@ allowedTopReaction _        _             = True
 doTopReact :: WorkItem -> TcS TopInteractResult 
 -- The work item does not react with the inert set, 
 -- so try interaction with top-level instances
 doTopReact :: WorkItem -> TcS TopInteractResult 
 -- The work item does not react with the inert set, 
 -- so try interaction with top-level instances
+
+-- Given dictionary; just add superclasses
+-- See Note [Given constraint that matches an instance declaration]
+doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Given loc
+                              , cc_class = cls, cc_tyargs = xis })
+  = do { sc_work <- newGivenSCWork dv loc cls xis 
+       ; return $ SomeTopInt sc_work (ContinueWith workItem) }
+
+-- Derived dictionary
+-- Do not add any further derived superclasses; their 
+-- full transitive closure has already been added. 
+-- But do look for functional dependencies
+doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Derived loc _
+                              , cc_class = cls, cc_tyargs = xis })
+  = do { fd_work <- findClassFunDeps dv cls xis loc
+       ; if isEmptyWorkList fd_work then 
+              return NoTopInt
+         else return $ SomeTopInt { tir_new_work = fd_work
+                                  , tir_new_inert = ContinueWith workItem } }
+
 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = 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 
 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = 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) 
-                            ; funDepReact }
+           NoInstance -> 
+             do { traceTcS "doTopReact/ no class instance for" (ppr dv) 
+                ; fd_work <- findClassFunDeps dv cls xis loc
+                ; if isEmptyWorkList fd_work then 
+                      do { sc_work <- newDerivedSCWork dv loc cls xis
+                                 -- See Note [Adding Derived Superclasses] 
+                                -- NB: workItem is inert, but it isn't solved
+                                -- keep it as inert, although it's not solved 
+                                -- because we have now reacted all its 
+                                -- top-level fundep-induced equalities!
+                         ; return $ SomeTopInt 
+                              { tir_new_work = fd_work `unionWorkLists` sc_work
+                              , tir_new_inert = ContinueWith workItem } }
+
+                  else -- More fundep work produced, don't do any superclass stuff, 
+                       -- just thow him back in the worklist, which will prioritize 
+                       -- the solution of fd equalities
+                       return $ SomeTopInt 
+                              { tir_new_work = fd_work `unionWorkLists` 
+                                               workListFromCCan workItem
+                              , 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 
            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 
-                  ; workList <- canWanteds wtvs
+                  ; inst_work <- canWanteds wtvs
                   ; if null wtvs
                     -- Solved in one step and no new wanted work produced. 
                     -- i.e we directly matched a top-level instance
                   ; if null wtvs
                     -- Solved in one step and no new wanted work produced. 
                     -- i.e we directly matched a top-level instance
@@ -1690,55 +1860,10 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
                     else do { let solved = makeSolvedByInst workItem
                             ; sc_work <- newDerivedSCWork dv loc cls xis
                                          -- See Note [Adding Derived Superclasses]
                     else do { let solved = makeSolvedByInst workItem
                             ; sc_work <- newDerivedSCWork dv loc cls xis
                                          -- See Note [Adding Derived Superclasses]
-                            ; let inst_work = workListFromCCans workList
                             ; return $ SomeTopInt 
                                   { tir_new_work  = inst_work `unionWorkLists` sc_work 
                                   , tir_new_inert = ContinueWith solved } }
                             ; return $ SomeTopInt 
                                   { tir_new_work  = inst_work `unionWorkLists` sc_work 
                                   , tir_new_inert = ContinueWith solved } }
-                  }
-       }
-  where 
-    -- Try for a fundep reaction beween the wanted item 
-    -- and a top-level instance declaration
-    funDepReact 
-      = do { instEnvs <- getInstEnvs
-           ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
-                                                    (ClassP cls xis, ppr dv)
-           ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs 
-                     -- NB: fundeps generate some wanted equalities, but 
-                     --     we don't use their evidence for anything
-           ; fd_cts <- canWanteds wevvars 
-           ; let fd_work = workListFromCCans fd_cts
-
-           ; if isEmptyCCan fd_cts then 
-                 do { sc_work <- newDerivedSCWork dv loc cls xis
-                                 -- See Note [Adding Derived Superclasses] 
-                    ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work
-                                          , tir_new_inert = ContinueWith workItem }
-                    }
-             else -- More fundep work produced, don't do any superlcass stuff, just 
-                  -- thow him back in the worklist prioritizing the solution of fd equalities
-                 return $ 
-                 SomeTopInt { tir_new_work = fd_work `unionWorkLists` workListFromCCan workItem
-                            , tir_new_inert = Stop }
-
-           -- NB: workItem is inert, but it isn't solved
-          -- keep it as inert, although it's not solved because we
-           -- have now reacted all its top-level fundep-induced equalities!
-                    
-           -- See Note [FunDep Reactions]
-           }
-
--- Derived, do not add any further derived superclasses; their full transitive 
--- closure has already been added. 
-doTopReact (CDictCan { cc_flavor = fl })
-  | isDerived fl
-  = return NoTopInt
-
-doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Given loc
-                              , cc_class = cls, cc_tyargs = xis })
-  = do { sc_work <- newGivenSCWork dv loc cls xis 
-       ; return $ SomeTopInt sc_work (ContinueWith workItem) }
-    -- See Note [Given constraint that matches an instance declaration]
+       }          }
 
 -- Type functions
 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
 
 -- Type functions
 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
@@ -1766,8 +1891,7 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
                                    mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe 
 
                    ; can_cts <- mkCanonical fl cv'
                                    mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe 
 
                    ; can_cts <- mkCanonical fl cv'
-                   ; let workList = workListFromCCans can_cts
-                   ; return $ SomeTopInt workList Stop }
+                   ; return $ SomeTopInt can_cts Stop }
            _ 
              -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
        }
            _ 
              -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
        }
@@ -1775,6 +1899,19 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
 
 -- Any other work item does not react with any top-level equations
 doTopReact _workItem = return NoTopInt 
 
 -- Any other work item does not react with any top-level equations
 doTopReact _workItem = return NoTopInt 
+
+----------------------
+findClassFunDeps :: EvVar -> Class -> [Xi] -> WantedLoc -> TcS WorkList
+-- Look for a fundep reaction beween the wanted item 
+-- and a top-level instance declaration
+findClassFunDeps dv cls xis loc
+ = do { instEnvs <- getInstEnvs
+      ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
+                                               (ClassP cls xis, ppr dv)
+      ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs 
+                     -- NB: fundeps generate some wanted equalities, but 
+                     --     we don't use their evidence for anything
+      ; canWanteds wevvars }
 \end{code}
 
 Note [Adding Derived Superclasses]
 \end{code}
 
 Note [Adding Derived Superclasses]
@@ -2043,26 +2180,26 @@ newGivenSCWork ev loc cls xis
   | NoScSkol <- ctLocOrigin loc  -- Very important!
   = return emptyWorkList
   | otherwise
   | NoScSkol <- ctLocOrigin loc  -- Very important!
   = return emptyWorkList
   | otherwise
-  = newImmSCWorkFromFlavored ev (Given loc) cls xis >>= return . workListFromCCans 
+  = newImmSCWorkFromFlavored ev (Given loc) cls xis >>= return 
 
 newDerivedSCWork :: EvVar -> WantedLoc -> Class -> [Xi] -> TcS WorkList 
 newDerivedSCWork ev loc cls xis 
   =  do { ims <- newImmSCWorkFromFlavored ev flavor cls xis 
 
 newDerivedSCWork :: EvVar -> WantedLoc -> Class -> [Xi] -> TcS WorkList 
 newDerivedSCWork ev loc cls xis 
   =  do { ims <- newImmSCWorkFromFlavored ev flavor cls xis 
-        ; final_cts <- rec_sc_work ims 
-        ; return $ workListFromCCans final_cts } 
-  where rec_sc_work :: CanonicalCts -> TcS CanonicalCts 
-        rec_sc_work cts 
-          = do { bg <- mapBagM (\c -> do { ims <- imm_sc_work c 
-                                         ; recs_ims <- rec_sc_work ims 
-                                         ; return $ consBag c recs_ims }) cts 
-               ; return $ concatBag bg } 
-        imm_sc_work (CDictCan { cc_id = dv, cc_flavor = fl, cc_class = cls, cc_tyargs = xis })
-           = newImmSCWorkFromFlavored dv fl cls xis 
-        imm_sc_work _ct = return emptyCCan 
-
-        flavor = Derived loc DerSC 
-
-newImmSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS CanonicalCts 
+        ; rec_sc_work ims  }
+  where 
+    rec_sc_work :: CanonicalCts -> TcS CanonicalCts 
+    rec_sc_work cts 
+      = do { bg <- mapBagM (\c -> do { ims <- imm_sc_work c 
+                                     ; recs_ims <- rec_sc_work ims 
+                                     ; return $ consBag c recs_ims }) cts 
+           ; return $ concatBag bg } 
+    imm_sc_work (CDictCan { cc_id = dv, cc_flavor = fl, cc_class = cls, cc_tyargs = xis })
+       = newImmSCWorkFromFlavored dv fl cls xis 
+    imm_sc_work _ct = return emptyCCan 
+
+    flavor = Derived loc DerSC 
+
+newImmSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
 -- Returns immediate superclasses 
 newImmSCWorkFromFlavored ev flavor cls xis 
   = do { let (tyvars, sc_theta, _, _) = classBigSig cls 
 -- Returns immediate superclasses 
 newImmSCWorkFromFlavored ev flavor cls xis 
   = do { let (tyvars, sc_theta, _, _) = classBigSig cls