Numerous small changes to the constraint solver

The main thing is that we now keep unsolved Derived constraints in the
wc_flats of a WantedConstraints, rather than discarding them each time.
This actually fixes a poential (admittedly obscure) bug, when we currently
discard a superclass constraint, and may never re-generate it, and may
thereby miss a functional dependency.

Instead, reportErrors filters out Derived constraints that we don't want
to report.

The other changes are all small refactorings following our walk-through.

6 files changed, 228 insertions, 332 deletions

diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index c0762daeb2..bbf5ae6181 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -143,7 +143,8 @@ reportWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = implics }
   where
     env = cec_tidy ctxt
     tidy_insols = mapBag (tidyCt env) insols
-    tidy_flats  = mapBag (tidyCt env) flats
+    tidy_flats  = mapBag (tidyCt env) (keepWanted flats)
+                  -- See Note [Do not report derived but soluble errors]
 
 reportTidyWanteds :: ReportErrCtxt -> Bag Ct -> Bag Ct -> Bag Implication -> TcM ()
 reportTidyWanteds ctxt insols flats implics
@@ -372,6 +373,56 @@ getUserGivens (CEC {cec_encl = ctxt})
                     , not (null givens) ]
 \end{code}
 
+Note [Do not report derived but soluble errors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The wc_flats include Derived constraints that have not been solved, but are
+not insoluble (in that case they'd be in wc_insols).  We do not want to report
+these as errors:
+
+* Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
+  an unsolved [D] Eq a, and we do not want to report that; it's just noise.
+
+* Functional dependencies.  For givens, consider
+      class C a b | a -> b
+      data T a where
+         MkT :: C a d => [d] -> T a
+      f :: C a b => T a -> F Int
+      f (MkT xs) = length xs
+  Then we get a [D] b~d.  But there *is* a legitimate call to
+  f, namely   f (MkT [True]) :: T Bool, in which b=d.  So we should
+  not reject the program.
+
+  For wanteds, something similar
+      data T a where
+        MkT :: C Int b => a -> b -> T a 
+      g :: C Int c => c -> ()
+      f :: T a -> ()
+      f (MkT x y) = g x
+  Here we get [G] C Int b, [W] C Int a, hence [D] a~b.
+  But again f (MkT True True) is a legitimate call.
+
+(We leave the Deriveds in wc_flat until reportErrors, so that we don't lose
+derived superclasses between iterations of the solver.)
+
+For functional dependencies, here is a real example, 
+stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs
+
+  class C a b | a -> b
+  g :: C a b => a -> b -> () 
+  f :: C a b => a -> b -> () 
+  f xa xb = 
+      let loop = g xa 
+      in loop xb
+
+We will first try to infer a type for loop, and we will succeed:
+    C a b' => b' -> ()
+Subsequently, we will type check (loop xb) and all is good. But, 
+recall that we have to solve a final implication constraint: 
+    C a b => (C a b' => .... cts from body of loop .... )) 
+And now we have a problem as we will generate an equality b ~ b' and fail to 
+solve it. 
+
+
 %************************************************************************
 %*                  *
                 Irreducible predicate errors
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 922b2cd404..d1a82b225d 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -1158,26 +1158,25 @@ zonkEvBinds env binds
 
 zonkEvBind :: ZonkEnv -> EvBind -> TcM EvBind
 zonkEvBind env (EvBind var term)
-  -- This function has some special cases for avoiding re-zonking the
-  -- same types many types. See Note [Optimized Evidence Binding Zonking]
   = case term of 
-      -- Fast path for reflexivity coercions:
+      -- Special-case fast paths for small coercions
+      -- NB: could be optimized further! (e.g. SymCo cv)
+      -- See Note [Optimized Evidence Binding Zonking]
       EvCoercion co 
         | Just ty <- isTcReflCo_maybe co
-        ->
-          do { zty  <- zonkTcTypeToType env ty
-             ; let var' = setVarType var (mkEqPred zty zty)
-             ; return (EvBind var' (EvCoercion (mkTcReflCo zty))) }
+        -> do { zty  <- zonkTcTypeToType env ty
+              ; let var' = setVarType var (mkEqPred zty zty)
+                  -- Here we save the task of zonking var's type, 
+                  -- because we know just what it is!
+              ; return (EvBind var' (EvCoercion (mkTcReflCo zty))) }
 
-      -- Fast path for variable-variable bindings 
-      -- NB: could be optimized further! (e.g. SymCo cv)
         | Just cv <- getTcCoVar_maybe co 
         -> do { let cv'   = zonkIdOcc env cv -- Just lazily look up
                     term' = EvCoercion (TcCoVarCo cv')
                     var'  = setVarType var (varType cv')
               ; return (EvBind var' term') }
 
-      -- Ugly safe and slow path
+      -- The default path
       _ -> do { var'  <- {-# SCC "zonkEvBndr" #-} zonkEvBndr env var
               ; term' <- zonkEvTerm env term 
               ; return (EvBind var' term')
@@ -1238,29 +1237,16 @@ not the ill-kinded Any BOX).
 
 Note [Optimized Evidence Binding Zonking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-When optimising evidence binds we may come accross situations where 
-a coercion is just reflexivity: 
+When optimising evidence binds we may come across situations where 
+a coercion looks like
       cv = ReflCo ty
-In such a case it is a waste of time to zonk both ty and the type 
-of the coercion, especially if the types involved are huge. For this
-reason this case is optimized to only zonk 'ty' and set the type of 
-the variable to be that zonked type.
-
-Another case that hurts a lot are simple coercion bindings of the form:
-      cv1 = cv2
-      cv3 = cv1
-      cv4 = cv2 
-etc. In all such cases it is very easy to just get the zonked type of 
-cv2 and use it to set the type of the LHS coercion variable without zonking
-twice. Though this case is funny, it can happen due the way that evidence 
-from spontaneously solved goals is now used.
-See Note [Optimizing Spontaneously Solved Goals] about this.
-
-NB: That these optimizations are independently useful, regardless of the 
-constraint solver strategy.
-
-DV, TODO: followup on this note mentioning new examples I will add to perf/
+or    cv1 = cv2
+where the type 'ty' is big.  In such cases it is a waste of time to zonk both 
+  * The variable on the LHS
+  * The coercion on the RHS
+Rather, we can zonk the coercion, take its type and use that for 
+the variable.  For big coercions this might be a lose, though, so we
+just have a fast case for a couple of special cases.
 
 
 \begin{code}
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index adff5ea182..2c2dc54c1b 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -47,7 +47,6 @@ import Control.Monad ( foldM )
 
 import VarEnv
 import qualified Data.Traversable as Traversable
-import Data.Maybe ( isJust )
 
 import Control.Monad( when, unless )
 import Pair ()
@@ -763,19 +762,6 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
                                   , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 }) 
                     wi@(CFunEqCan { cc_ev = fl2, cc_fun = tc2
                                   , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
-{-  ToDo: Check with Dimitrios
-  | lhss_match  
-  , isSolved fl1 -- Inert is solved and we can simply ignore it
-                 -- when workitem is given/solved
-  , isGiven fl2
-  = irInertConsumed "FunEq/FunEq"
-  | lhss_match
-  , isSolved fl2 -- Workitem is solved and we can ignore it when
-                 -- the inert is given/solved
-  , isGiven fl1                 
-  = irWorkItemConsumed "FunEq/FunEq" 
--}
-
   | fl1 `canSolve` fl2 && lhss_match
   = do { traceTcS "interact with inerts: FunEq/FunEq" $ 
          vcat [ text "workItem =" <+> ppr wi
@@ -934,12 +920,6 @@ solveOneFromTheOther info ifl workItem
 		  -- so it's safe to continue on from this point
   = irInertConsumed ("Solved[DI] " ++ info)
   
-{-  ToDo: Check with Dimitrios
-  | isSolved ifl, isGiven wfl
-    -- Same if the inert is a GivenSolved -- just get rid of it
-  = irInertConsumed ("Solved[SI] " ++ info)
--}
-
   | otherwise
   = ASSERT( ifl `canSolve` wfl )
       -- Because of Note [The Solver Invariant], plus Derived dealt with
@@ -1443,16 +1423,32 @@ doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
 --   (b) See Note [Given constraint that matches an instance declaration] 
 --       for some design decisions for given dictionaries. 
 
-doTopReact inerts workItem@(CDictCan { cc_ev = fl
-                                     , cc_class = cls, cc_tyargs = xis, cc_depth = depth })
+doTopReact inerts workItem
   = do { traceTcS "doTopReact" (ppr workItem)
-       ; instEnvs <- getInstEnvs 
-       ; let fd_eqns = improveFromInstEnv instEnvs (mkClassPred cls xis, arising_sdoc)
+       ; case workItem of
+      	   CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis
+      	            , cc_depth = d }
+      	      -> doTopReactDict inerts workItem fl cls xis d
+
+      	   CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args
+      	             , cc_rhs = xi, cc_depth = d }
+      	      -> doTopReactFunEq fl tc args xi d
+
+      	   _  -> -- Any other work item does not react with any top-level equations
+      	         return NoTopInt  }
+
+--------------------
+doTopReactDict :: InertSet -> WorkItem -> CtEvidence -> Class -> [Xi]
+               -> SubGoalDepth -> TcS TopInteractResult
+doTopReactDict inerts workItem fl cls xis depth
+  = do { instEnvs <- getInstEnvs 
+       ; let fd_eqns = improveFromInstEnv instEnvs 
+                           (mkClassPred cls xis, arising_sdoc)
              
        ; m <- rewriteWithFunDeps fd_eqns xis fl
        ; case m of
            Just (_xis',fd_work) ->
-               do { emitFDWorkAsDerived fd_work (cc_depth workItem)
+               do { emitFDWorkAsDerived fd_work depth
                   ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
                                       , tir_new_item = ContinueWith workItem } }
            Nothing 
@@ -1493,106 +1489,54 @@ doTopReact inerts workItem@(CDictCan { cc_ev = fl
                SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
                           , tir_new_item = Stop } }
 
-
--- Otherwise, it's a Given, Derived, or Wanted
-doTopReact _inerts workItem@(CFunEqCan { cc_ev = fl, cc_depth = d
-                                       , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
-  = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far 
+--------------------
+doTopReactFunEq :: CtEvidence -> TyCon -> [Xi] -> Xi
+                -> SubGoalDepth -> TcS TopInteractResult
+doTopReactFunEq fl tc args xi d
+  = ASSERT (isSynFamilyTyCon tc) -- No associated data families have 
+                                 -- reached that far 
+
+    -- First look in the cache of solved funeqs
+    do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
+       ; case lookupFamHead fun_eq_cache (mkTyConApp tc args) of {
+            Just ctev -> ASSERT( not (isDerived ctev) )
+                         ASSERT( isEqPred (ctEvPred ctev) )
+                         succeed_with (evTermCoercion (ctEvTerm ctev)) 
+                                      (snd (getEqPredTys (ctEvPred ctev))) ;
+            Nothing -> 
+
+    -- No cached solved, so look up in top-level instances
     do { match_res <- matchFam tc args   -- See Note [MATCHING-SYNONYMS]
-       ; case match_res of
-           Nothing -> return NoTopInt 
-           Just (famInst, rep_tys)
-             -> do { mb_already_solved <- lkpSolvedFunEqCache (mkTyConApp tc args)
-                   ; traceTcS "doTopReact: Family instance matches" $ 
-                     vcat [ text "solved-fun-cache" <+> if isJust mb_already_solved 
-                                                        then text "hit" else text "miss"
-                          , text "workItem =" <+> ppr workItem ]
-                   ; let (coe,rhs_ty) 
-                           | Just ctev <- mb_already_solved
-                           , not (isDerived ctev)
-                           = ASSERT( isEqPred (ctEvPred ctev) )
-                             (evTermCoercion (ctEvTerm ctev), snd (getEqPredTys (ctEvPred ctev)))
-                           | otherwise 
-                           = let coe_ax = famInstAxiom famInst
-                             in (mkTcAxInstCo coe_ax rep_tys, 
-                                              mkAxInstRHS coe_ax rep_tys)
-                                
-                         xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)]
-                         xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x)
-                         xcomp _   = panic "No more goals!"
-                         
-                         xev = XEvTerm xcomp xdecomp
-                   ; ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
-                   ; case ctevs of
-                       [ctev] -> updWorkListTcS $ extendWorkListEq $
-                                 CNonCanonical { cc_ev = ctev
-                                               , cc_depth  = d+1 }
-                       ctevs -> -- No subgoal (because it's cached)
-                                ASSERT( null ctevs) return () 
-
-                   ; unless (isDerived fl) $
-                     do { addSolvedFunEq fl
-                        ; addToSolved fl }
-                   ; return $ SomeTopInt { tir_rule = "Fun/Top"
-                                       , tir_new_item = Stop } } }
-            
--- Any other work item does not react with any top-level equations
-doTopReact _inerts _workItem = return NoTopInt 
-
-
-lkpSolvedFunEqCache :: TcType -> TcS (Maybe CtEvidence)
-lkpSolvedFunEqCache fam_head 
-  = do { (_subst,_inscope) <- getInertEqs 
-       ; fun_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
-       ; traceTcS "lkpFunEqCache" $ vcat [ text "fam_head    =" <+> ppr fam_head
-                                         , text "funeq cache =" <+> ppr fun_cache ]
-       ; return (lookupFamHead fun_cache fam_head) }
-
-{-             ToDo; talk to Dimitrios.  I have no idea what is happening here
-
-       ; rewrite_cached (lookupFamHead fun_cache fam_head) }
--- The two different calls do not seem to make a significant difference in 
--- terms of hit/miss rate for many memory-critical/performance tests but the
--- latter blows up the space on the heap somehow ... It maybe the niFixTvSubst.
--- So, I am simply disabling it for now, until we investigate a bit more.
---       lookupTypeMap_mod subst cc_rhs fam_head (unCtFamHeadMap fun_cache) }
- 
-  where rewrite_cached Nothing = return Nothing
-        rewrite_cached (Just ct@(CFunEqCan { cc_ev = fl, cc_depth = d
-                                           , cc_fun = tc, cc_tyargs = xis
-                                           , cc_rhs = xi}))
-          = do { (xis_subst,cos) <- flattenMany d FMFullFlatten fl xis 
-                                    -- cos :: xis_subst ~ xis 
-               ; (xi_subst,co) <- flatten d FMFullFlatten fl xi
-                                    -- co :: xi_subst ~ xi
-               ; let flat_fam_head = mkTyConApp tc xis_subst 
-
-               ; unless (flat_fam_head `eqType` fam_head) $ 
-                        pprPanic "lkpFunEqCache" (vcat [ text "Cached (solved) constraint =" <+> ppr ct
-                                                       , text "Flattened constr. head     =" <+> ppr flat_fam_head ])
-               ; traceTcS "lkpFunEqCache" $ text "Flattened constr. rhs = " <+> ppr xi_subst 
-                                                  
-
-               ; let new_pty = mkTcEqPred (mkTyConApp tc xis_subst) xi_subst
-                     new_co  = mkTcTyConAppCo eqTyCon [ mkTcReflCo (defaultKind $ typeKind xi_subst)
-                                                      , mkTcTyConAppCo tc cos
-                                                      , co ]
-                               -- new_co :: (F xis_subst ~  xi_subst) ~ (F xis ~ xi)
-                               -- new_co = (~) <k> (F cos) co
-               ; new_fl <- rewriteCtFlavor fl new_pty new_co 
-               ; case new_fl of
-                    Nothing 
-                      -> return Nothing -- Strange: cached?
-                    Just fl' 
-                      -> return $ 
-                         Just (CFunEqCan { cc_ev = fl'
-                                         , cc_depth = d
-                                         , cc_fun = tc
-                                         , cc_tyargs = xis_subst
-                                         , cc_rhs = xi_subst }) }
-        rewrite_cached (Just other_ct) 
-          = pprPanic "lkpFunEqCache:not family equation!" $ ppr other_ct
--}
+       ; case match_res of {
+           Nothing -> return NoTopInt ;
+           Just (famInst, rep_tys) -> 
+
+    -- Found a top-level instance
+    do {    -- Add it to the solved goals
+         unless (isDerived fl) $
+         do { addSolvedFunEq fl            
+            ; addToSolved fl }
+
+       ; let coe_ax = famInstAxiom famInst 
+       ; succeed_with (mkTcAxInstCo coe_ax rep_tys)
+                      (mkAxInstRHS coe_ax rep_tys) } } } } }
+  where
+    succeed_with :: TcCoercion -> TcType -> TcS TopInteractResult
+    succeed_with coe rhs_ty 
+      = do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
+           ; case ctevs of
+               [ctev] -> updWorkListTcS $ extendWorkListEq $
+                         CNonCanonical { cc_ev = ctev
+                                       , cc_depth  = d+1 }
+               ctevs -> -- No subgoal (because it's cached)
+                        ASSERT( null ctevs) return () 
+           ; return $ SomeTopInt { tir_rule = "Fun/Top"
+                                 , tir_new_item = Stop } }
+      where
+        xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)]
+        xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x)
+        xcomp _   = panic "No more goals!"
+        xev = XEvTerm xcomp xdecomp
 \end{code}
 
 
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index ac35c37df2..0eb1efe509 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -857,8 +857,8 @@ type SubGoalDepth = Int -- An ever increasing number used to restrict
 data Ct
   -- Atomic canonical constraints 
   = CDictCan {  -- e.g.  Num xi
-      cc_ev :: CtEvidence, 
-      cc_class  :: Class, 
+      cc_ev :: CtEvidence,   -- See Note [Ct/evidence invariant]
+      cc_class  :: Class,   
       cc_tyargs :: [Xi],
 
       cc_depth  :: SubGoalDepth -- Simplification depth of this constraint
@@ -866,7 +866,7 @@ data Ct
     }
 
   | CIrredEvCan {  -- These stand for yet-unknown predicates
-      cc_ev :: CtEvidence,
+      cc_ev :: CtEvidence,   -- See Note [Ct/evidence invariant]
       cc_ty     :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin)
                        -- Since, if it were a type constructor application, that'd make the
                        -- whole constraint a CDictCan, or CTyEqCan. And it can't be
@@ -880,7 +880,7 @@ data Ct
        --   * typeKind xi `compatKind` typeKind tv
        --       See Note [Spontaneous solving and kind compatibility]
        --   * We prefer unification variables on the left *JUST* for efficiency
-      cc_ev :: CtEvidence, 
+      cc_ev :: CtEvidence,    -- See Note [Ct/evidence invariant]
       cc_tyvar  :: TcTyVar, 
       cc_rhs    :: Xi,
 
@@ -890,7 +890,7 @@ data Ct
   | CFunEqCan {  -- F xis ~ xi  
                  -- Invariant: * isSynFamilyTyCon cc_fun 
                  --            * typeKind (F xis) `compatKind` typeKind xi
-      cc_ev :: CtEvidence, 
+      cc_ev :: CtEvidence,      -- See Note [Ct/evidence invariant]
       cc_fun    :: TyCon,	-- A type function
       cc_tyargs :: [Xi],	-- Either under-saturated or exactly saturated
       cc_rhs    :: Xi,      	--    *never* over-saturated (because if so
@@ -904,9 +904,16 @@ data Ct
       cc_ev :: CtEvidence, 
       cc_depth  :: SubGoalDepth
     }
-
 \end{code}
 
+Note [Ct/evidence invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If  ct :: Ct, then extra fields of 'ct' cache precisely the ctev_pred field
+of (cc_ev ct).   Eg for CDictCan, 
+   ctev_pred (cc_ev ct) = (cc_class ct) (cc_tyargs ct)
+This holds by construction; look at the unique place where CDictCan is
+built (in TcCanonical)
+
 \begin{code}
 mkNonCanonical :: CtEvidence -> Ct
 mkNonCanonical flav = CNonCanonical { cc_ev = flav, cc_depth = 0}
@@ -915,6 +922,7 @@ ctEvidence :: Ct -> CtEvidence
 ctEvidence = cc_ev
 
 ctPred :: Ct -> PredType 
+-- See Note [Ct/evidence invariant]
 ctPred ct = ctEvPred (cc_ev ct)
 
 keepWanted :: Cts -> Cts
@@ -922,18 +930,6 @@ keepWanted = filterBag isWantedCt
     -- DV: there used to be a note here that read: 
     -- ``Important: use fold*r*Bag to preserve the order of the evidence variables'' 
     -- DV: Is this still relevant? 
-
--- ToDo Check with Dimitrios
-{-
-ctPred (CNonCanonical { cc_ev = fl }) = ctEvPred fl
-ctPred (CDictCan { cc_class = cls, cc_tyargs = xis }) 
-  = mkClassPred cls xis
-ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) 
-  = mkTcEqPred (mkTyVarTy tv) xi
-ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 }) 
-  = mkTcEqPred (mkTyConApp fn xis1) xi2
-ctPred (CIrredEvCan { cc_ty = xi }) = xi
--}
 \end{code}
 
 
@@ -1197,6 +1193,12 @@ At the end, we will hopefully have substituted uf1 := F alpha, and we
 will be able to report a more informative error:
     'Can't construct the infinite type beta ~ F alpha beta'
 
+Insoluble constraints *do* include Derived constraints. For example,
+a functional dependency might give rise to [D] Int ~ Bool, and we must
+report that.  If insolubles did not contain Deriveds, reportErrors would
+never see it.
+
+
 %************************************************************************
 %*									*
             Pretty printing
@@ -1233,14 +1235,12 @@ ctev_evar; instead we look at the cte_pred field.  The evtm/evar field
 may be un-zonked.
 
 \begin{code}
-data CtEvidence   -- Rename to CtEvidence
+data CtEvidence 
   = Given { ctev_gloc :: GivenLoc
           , ctev_pred :: TcPredType
           , ctev_evtm :: EvTerm }          -- See Note [Evidence field of CtEvidence]
     -- Truly given, not depending on subgoals
     -- NB: Spontaneous unifications belong here
-    -- DV TODOs: (i)  Consider caching actual evidence _term_
-    --           (ii) Revisit Note [Optimizing Spontaneously Solved Coercions]
     
   | Wanted { ctev_wloc :: WantedLoc
            , ctev_pred :: TcPredType
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 9fb24064bc..aa92866ec6 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -140,7 +140,7 @@ import Digraph
 import Maybes ( orElse, catMaybes )
 
 
-import Control.Monad( when, zipWithM )
+import Control.Monad( unless, when, zipWithM )
 import StaticFlags( opt_PprStyle_Debug )
 import Data.IORef
 import TrieMap
@@ -171,7 +171,6 @@ mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
 
 Note [WorkList]
 ~~~~~~~~~~~~~~~
-
 A WorkList contains canonical and non-canonical items (of all flavors). 
 Notice that each Ct now has a simplification depth. We may 
 consider using this depth for prioritization as well in the future. 
@@ -496,8 +495,10 @@ The reason for all this is simply to avoid re-solving goals we have solved alrea
 
 * A solved Given is just given
 
-* A solved Derived is possible; purpose is to avoid creating tons of identical
-  Derived goals.
+* A solved Derived in inert_solved is possible; purpose is to avoid
+  creating tons of identical Derived goals.
+
+  But there are no solved Deriveds in inert_solved_funeqs
 
 
 \begin{code}
@@ -516,7 +517,9 @@ data InertSet
               -- Key is by family head. We use this field during flattening only
               -- Not necessarily inert wrt top-level equations (or inert_cans)
 
-       , inert_solved_funeqs :: FamHeadMap CtEvidence  -- Of form co :: F xis ~ xi
+       , inert_solved_funeqs :: FamHeadMap CtEvidence  -- Of form co :: F xis ~ xi 
+                                                       -- No Deriveds 
+
        , inert_solved        :: PredMap    CtEvidence  -- All others
        	      -- These two fields constitute a cache of solved (only!) constraints
               -- See Note [Solved constraints]
@@ -1123,11 +1126,16 @@ emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
 emitFrozenError fl depth 
   = do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
        ; inert_ref <- getTcSInertsRef 
-       ; inerts <- wrapTcS (TcM.readTcRef inert_ref)
-       ; let ct = CNonCanonical { cc_ev = fl
-                                , cc_depth = depth } 
-             inerts_new = inerts { inert_frozen = extendCts (inert_frozen inerts) ct } 
-       ; wrapTcS (TcM.writeTcRef inert_ref inerts_new) }
+       ; wrapTcS $ do
+       { inerts <- TcM.readTcRef inert_ref
+       ; let old_insols = inert_frozen inerts
+             ct = CNonCanonical { cc_ev = fl, cc_depth = depth } 
+             inerts_new = inerts { inert_frozen = extendCts old_insols ct } 
+             this_pred = ctEvPred fl
+             already_there = not (isWanted fl) && anyBag (eqType this_pred . ctPred) old_insols
+	     -- See Note [Do not add duplicate derived insolubles]
+       ; unless already_there $
+         TcM.writeTcRef inert_ref inerts_new } }
 
 instance HasDynFlags TcS where
     getDynFlags = wrapTcS getDynFlags
@@ -1184,52 +1192,8 @@ setWantedTyBind tv ty
 
 
 \end{code}
-Note [Optimizing Spontaneously Solved Coercions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
-
-Spontaneously solved coercions such as alpha := tau used to be bound as everything else
-in the evidence binds. Subsequently they were used for rewriting other wanted or solved
-goals. For instance: 
-
-WorkItem = [S] g1 : a ~ tau
-Inerts   = [S] g2 : b ~ [a]
-           [S] g3 : c ~ [(a,a)]
-
-Would result, eventually, after the workitem rewrites the inerts, in the
-following evidence bindings:
-
-        g1 = ReflCo tau
-        g2 = ReflCo [a]
-        g3 = ReflCo [(a,a)]
-        g2' = g2 ; [g1] 
-        g3' = g3 ; [(g1,g1)]
-
-This ia annoying because it puts way too much stress to the zonker and
-desugarer, since we /know/ at the generation time (spontaneously
-solving) that the evidence for a particular evidence variable is the
-identity.
-
-For this reason, our solution is to cache inside the GivenSolved
-flavor of a constraint the term which is actually solving this
-constraint. Whenever we perform a setEvBind, a new flavor is returned
-so that if it was a GivenSolved to start with, it remains a
-GivenSolved with a new evidence term inside. Then, when we use solved
-goals to rewrite other constraints we simply use whatever is in the
-GivenSolved flavor and not the constraint cc_id.
-
-In our particular case we'd get the following evidence bindings, eventually: 
-
-       g1 = ReflCo tau
-       g2 = ReflCo [a]
-       g3 = ReflCo [(a,a)]
-       g2'= ReflCo [a]
-       g3'= ReflCo [(a,a)]
-
-Since we use smart constructors to get rid of g;ReflCo t ~~> g etc.
 
 \begin{code}
-
-
 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
 warnTcS loc warn_if doc 
   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
@@ -1285,6 +1249,52 @@ isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
 
 \end{code}
 
+Note [Do not add duplicate derived insolubles]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In general we do want to add an insoluble (Int ~ Bool) even if there is one
+such there already, because they may come from distinct call sites.  But for
+*derived* insolubles, we only want to report each one once.  Why?
+
+(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
+    equality many times, as the original constraint is sucessively rewritten.
+
+(b) Ditto the successive iterations of the main solver itself, as it traverses
+    the constraint tree. See example below.
+
+Also for *given* insolubles we may get repeated errors, as we
+repeatedly traverse the constraint tree.  These are relatively rare
+anyway, so removing duplicates seems ok.  (Alternatively we could take
+the SrcLoc into account.)
+
+Note that the test does not need to be particularly efficient because
+it is only used if the program has a type error anyway.
+
+Example of (b): assume a top-level class and instance declaration:
+
+  class D a b | a -> b 
+  instance D [a] [a] 
+
+Assume we have started with an implication:
+
+  forall c. Eq c => { wc_flat = D [c] c [W] }
+
+which we have simplified to:
+
+  forall c. Eq c => { wc_flat = D [c] c [W]
+                    , wc_insols = (c ~ [c]) [D] }
+
+For some reason, e.g. because we floated an equality somewhere else,
+we might try to re-solve this implication. If we do not do a
+keepWanted, then we will end up trying to solve the following
+constraints the second time:
+
+  (D [c] c) [W]
+  (c ~ [c]) [D]
+
+which will result in two Deriveds to end up in the insoluble set:
+
+  wc_flat   = D [c] c [W]
+  wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
 
 Note [Touchable meta type variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1681,25 +1691,6 @@ getCtCoercion :: EvBindMap -> Ct -> TcCoercion
 getCtCoercion _bs ct 
   = ASSERT( not (isDerivedCt ct) )
     evTermCoercion (ctEvTerm (ctEvidence ct))
-{-       ToDo: check with Dimitrios that we can dump this stuff
-         WARNING: if we *do* need this stuff, we need to think again about cyclic bindings.
-  = case lookupEvBind bs cc_id of
-        -- Given and bound to a coercion term
-      Just (EvBind _ (EvCoercion co)) -> co
-                -- NB: The constraint could have been rewritten due to spontaneous 
-                -- unifications but because we are optimizing away mkRefls the evidence
-                -- variable may still have type (alpha ~ [beta]). The constraint may 
-                -- however have a more accurate type (alpha ~ [Int]) (where beta ~ Int has
-                -- been previously solved by spontaneous unification). So if we are going 
-                -- to use the evidence variable for rewriting other constraints, we'd better 
-                -- make sure it's of the right type!
-                -- Always the ctPred type is more accurate, so we just pick that type
-
-      _ -> mkTcCoVarCo (setVarType cc_id (ctPred ct))
-      
-  where 
-    cc_id = ctId ct
--}
 \end{code}
 
 
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 914d463f1f..04f05282ec 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -771,10 +771,10 @@ solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols
 
          -- Try the flat bit, including insolubles. Solving insolubles a 
          -- second time round is a bit of a waste but the code is simple 
-         -- and the program is wrong anyway. 
-         -- Why keepWanted insols? See Note [KeepWanted in SolveWanteds] 
-       ; let all_flats = flats `unionBags` keepWanted insols
-             -- DV: Used to be 'keepWanted insols' but just insols is
+         -- and the program is wrong anyway, and we don't run the danger 
+         -- of adding Derived insolubles twice; see 
+         -- TcSMonad Note [Do not add duplicate derived insolubles] 
+       ; let all_flats = flats `unionBags` insols
                          
        ; impls_from_flats <- solveInteractCts $ bagToList all_flats
 
@@ -917,10 +917,7 @@ solveImplication tcs_untouchables
        ; let (res_flat_free, res_flat_bound)
                  = floatEqualities skols givens unsolved_flats
 
-       ; let res_wanted = WC { wc_flat  = keepWanted $ res_flat_bound
-                               -- I think this keepWanted must eventually go away, but it is
-                               -- a real code-breaking change. 
-                               -- See Note [KeepWanted in SolveImplication]
+       ; let res_wanted = WC { wc_flat  = res_flat_bound
                              , wc_impl  = unsolved_implics
                              , wc_insol = insols }
 
@@ -940,81 +937,8 @@ solveImplication tcs_untouchables
 
 \end{code}
 
-Note [KeepWanted in SolveWanteds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Why do we have:
-   let all_flats = flats `unionBags` keepWanted insols
-instead of the simpler:
-   let all_flats = flats `unionBags` insols
-in solve_wanteds?
-
-Assume a top-level class and instance declaration:
-
-  class D a b | a -> b 
-  instance D [a] [a] 
-
-Assume we have started with an implication:
-
-  forall c. Eq c => { wc_flat = D [c] c [W] }
-
-which we have simplified to:
-
-  forall c. Eq c => { wc_flat = D [c] c [W]
-                    , wc_insols = (c ~ [c]) [D] }
-
-For some reason, e.g. because we floated an equality somewhere else,
-we might try to re-solve this implication. If we do not do a
-keepWanted, then we will end up trying to solve the following
-constraints the second time:
-
-  (D [c] c) [W]
-  (c ~ [c]) [D]
-
-which will result in two Deriveds to end up in the insoluble set:
-
-  wc_flat   = D [c] c [W]
-  wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
-
-which can result in reporting the same error twice.  
-
-So, do we /lose/ some potentially useful information by doing this? 
-
-No, because the insoluble Derived/Given are going to be equalities, 
-which are going to be derivable anyway from the rest of the flat 
-constraints. 
-
-
-Note [KeepWanted in SolveImplication]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Here is a real example, 
-stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs
-
-  class C a b | a -> b
-  g :: C a b => a -> b -> () 
-  f :: C a b => a -> b -> () 
-  f xa xb = 
-      let loop = g xa 
-      in loop xb
-
-We will first try to infer a type for loop, and we will succeed:
-    C a b' => b' -> ()
-Subsequently, we will type check (loop xb) and all is good. But, 
-recall that we have to solve a final implication constraint: 
-    C a b => (C a b' => .... cts from body of loop .... )) 
-And now we have a problem as we will generate an equality b ~ b' and fail to 
-solve it. 
-
-I actually think this is a legitimate behaviour (to fail). After all, if we had 
-given the inferred signature to foo we would have failed as well, but we have to 
-find a workaround because library code breaks.
-
-For now I keep the 'keepWanted' though it seems problematic e.g. we might discard 
-a useful Derived!
 
 \begin{code}
-
-
 floatEqualities :: [TcTyVar] -> [EvVar] -> Cts -> (Cts, Cts)
 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
 -- and come from the input wanted ev vars or deriveds