Major patch to add -fwarn-redundant-constraints
[ghc.git] / compiler / typecheck / TcInteract.hs
index 475e490..d38036c 100644 (file)
@@ -1,8 +1,8 @@
 {-# LANGUAGE CPP #-}
 
 module TcInteract (
-     solveFlatGivens,    -- Solves [EvVar],GivenLoc
-     solveFlatWanteds    -- Solves Cts
+     solveSimpleGivens,    -- Solves [EvVar],GivenLoc
+     solveSimpleWanteds    -- Solves Cts
   ) where
 
 #include "HsVersions.h"
@@ -13,7 +13,7 @@ import TcFlatten
 import VarSet
 import Type
 import Unify
-import InstEnv( lookupInstEnv, instanceDFunId )
+import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
 import CoAxiom(sfInteractTop, sfInteractInert)
 
 import Var
@@ -39,6 +39,7 @@ import Data.List( partition, foldl', deleteFirstsBy )
 import VarEnv
 
 import Control.Monad
+import Maybes( isJust )
 import Pair (Pair(..))
 import Unique( hasKey )
 import FastString ( sLit )
@@ -75,12 +76,12 @@ Note [Basic Simplifier Plan]
 If in Step 1 no such element exists, we have exceeded our context-stack
 depth and will simply fail.
 
-Note [Unflatten after solving the flat wanteds]
+Note [Unflatten after solving the simple wanteds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We unflatten after solving the wc_flats of an implication, and before attempting
+We unflatten after solving the wc_simples of an implication, and before attempting
 to float. This means that
 
- * The fsk/fmv flatten-skolems only survive during solveFlats.  We don't
+ * The fsk/fmv flatten-skolems only survive during solveSimples.  We don't
    need to worry about then across successive passes over the constraint tree.
    (E.g. we don't need the old ic_fsk field of an implication.
 
@@ -96,7 +97,7 @@ to float. This means that
        (c ~ False) => b ~ gamma
 
    Obviously this is soluble with gamma := F c a b, and unflattening
-   will do exactly that after solving the flat constraints and before
+   will do exactly that after solving the simple constraints and before
    attempting the implications.  Before, when we were not unflattening,
    we had to push Wanted funeqs in as new givens.  Yuk!
 
@@ -109,9 +110,8 @@ to float. This means that
 
 Note [Running plugins on unflattened wanteds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-There is an annoying mismatch between solveFlatGivens and
-solveFlatWanteds, because the latter needs to fiddle with the inert
+There is an annoying mismatch between solveSimpleGivens and
+solveSimpleWanteds, because the latter needs to fiddle with the inert
 set, unflatten and and zonk the wanteds.  It passes the zonked wanteds
 to runTcPluginsWanteds, which produces a replacement set of wanteds,
 some additional insolubles and a flag indicating whether to go round
@@ -121,8 +121,8 @@ that prepareInertsForImplications will discard the insolubles, so we
 must keep track of them separately.
 -}
 
-solveFlatGivens :: CtLoc -> [EvVar] -> TcS ()
-solveFlatGivens loc givens
+solveSimpleGivens :: CtLoc -> [EvVar] -> TcS ()
+solveSimpleGivens loc givens
   | null givens  -- Shortcut for common case
   = return ()
   | otherwise
@@ -131,42 +131,43 @@ solveFlatGivens loc givens
     mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evtm = EvId ev_id
                                                 , ctev_pred = evVarPred ev_id
                                                 , ctev_loc  = loc })
-    go givens = do { solveFlats (listToBag givens)
+    go givens = do { solveSimples (listToBag givens)
                    ; new_givens <- runTcPluginsGiven
                    ; when (notNull new_givens) (go new_givens)
                    }
 
-solveFlatWanteds :: Cts -> TcS WantedConstraints
-solveFlatWanteds = go emptyBag
+solveSimpleWanteds :: Cts -> TcS WantedConstraints
+solveSimpleWanteds = go emptyBag
   where
     go insols0 wanteds
-      = do { solveFlats wanteds
+      = do { solveSimples wanteds
            ; (implics, tv_eqs, fun_eqs, insols, others) <- getUnsolvedInerts
            ; unflattened_eqs <- unflatten tv_eqs fun_eqs
-              -- See Note [Unflatten after solving the flat wanteds]
+              -- See Note [Unflatten after solving the simple wanteds]
 
-           ; zonked <- zonkFlats (others `andCts` unflattened_eqs)
-             -- Postcondition is that the wl_flats are zonked
+           ; zonked <- zonkSimples (others `andCts` unflattened_eqs)
+             -- Postcondition is that the wl_simples are zonked
 
            ; (wanteds', insols', rerun) <- runTcPluginsWanted zonked
               -- See Note [Running plugins on unflattened wanteds]
            ; let all_insols = insols0 `unionBags` insols `unionBags` insols'
+
            ; if rerun then do { updInertTcS prepareInertsForImplications
                               ; go all_insols wanteds' }
-                      else return (WC { wc_flat  = wanteds'
-                                      , wc_insol = all_insols
-                                      , wc_impl  = implics }) }
+                      else return (WC { wc_simple = wanteds'
+                                      , wc_insol  = all_insols
+                                      , wc_impl   = implics }) }
 
 
 -- The main solver loop implements Note [Basic Simplifier Plan]
 ---------------------------------------------------------------
-solveFlats :: Cts -> TcS ()
+solveSimples :: Cts -> TcS ()
 -- Returns the final InertSet in TcS
 -- Has no effect on work-list or residual-iplications
 -- The constraints are initially examined in left-to-right order
 
-solveFlats cts
-  = {-# SCC "solveFlats" #-}
+solveSimples cts
+  = {-# SCC "solveSimples" #-}
     do { dyn_flags <- getDynFlags
        ; updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
        ; solve_loop (maxSubGoalDepth dyn_flags) }
@@ -185,7 +186,7 @@ solveFlats cts
 
 -- | Extract the (inert) givens and invoke the plugins on them.
 -- Remove solved givens from the inert set and emit insolubles, but
--- return new work produced so that 'solveFlatGivens' can feed it back
+-- return new work produced so that 'solveSimpleGivens' can feed it back
 -- into the main solver.
 runTcPluginsGiven :: TcS [Ct]
 runTcPluginsGiven = do
@@ -202,7 +203,7 @@ runTcPluginsGiven = do
 -- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
 -- them and produce an updated bag of wanteds (possibly with some new
 -- work) and a bag of insolubles.  The boolean indicates whether
--- 'solveFlatWanteds' should feed the updated wanteds back into the
+-- 'solveSimpleWanteds' should feed the updated wanteds back into the
 -- main solver.
 runTcPluginsWanted :: Cts -> TcS (Cts, Cts, Bool)
 runTcPluginsWanted zonked_wanteds
@@ -220,7 +221,7 @@ runTcPluginsWanted zonked_wanteds
   where
     setEv :: (EvTerm,Ct) -> TcS ()
     setEv (ev,ct) = case ctEvidence ct of
-      CtWanted {ctev_evar = evar} -> setEvBind evar ev
+      CtWanted {ctev_evar = evar} -> setWantedEvBind evar ev
       _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
 
 -- | A triple of (given, derived, wanted) constraints to pass to plugins
@@ -450,7 +451,11 @@ interactWithInertsStage wi
                 -- CHoleCan are put straight into inert_frozen, so never get here
                 -- CNonCanonical have been canonicalised
 
-data InteractResult = IRKeep | IRReplace | IRDelete
+data InteractResult
+   = IRKeep      -- Keep the existing inert constraint in the inert set
+   | IRReplace   -- Replace the existing inert constraint with the work item
+   | IRDelete    -- Delete the existing inert constraint from the inert set
+
 instance Outputable InteractResult where
   ppr IRKeep    = ptext (sLit "keep")
   ppr IRReplace = ptext (sLit "replace")
@@ -472,19 +477,88 @@ solveOneFromTheOther ev_i ev_w
   = return (IRDelete, False)
 
   | CtWanted { ctev_evar = ev_id } <- ev_w
-  = do { setEvBind ev_id (ctEvTerm ev_i)
+  = do { setWantedEvBind ev_id (ctEvTerm ev_i)
        ; return (IRKeep, True) }
 
   | CtWanted { ctev_evar = ev_id } <- ev_i
-  = do { setEvBind ev_id (ctEvTerm ev_w)
+  = do { setWantedEvBind ev_id (ctEvTerm ev_w)
        ; return (IRReplace, True) }
 
-  | otherwise      -- If both are Given, we already have evidence; no need to duplicate
-                   -- But the work item *overrides* the inert item (hence IRReplace)
-                   -- See Note [Shadowing of Implicit Parameters]
-  = return (IRReplace, True)
+  -- So they are both Given
+  -- See Note [Replacement vs keeping]
+  | lvl_i == lvl_w
+  = do { binds <- getTcEvBindsMap
+       ; if has_binding binds ev_w && not (has_binding binds ev_i)
+         then return (IRReplace, True)
+         else return (IRKeep,    True) }
+
+   | otherwise   -- Both are Given
+   = return (if use_replacement then IRReplace else IRKeep, True)
+   where
+     pred  = ctEvPred ev_i
+     loc_i = ctEvLoc ev_i
+     loc_w = ctEvLoc ev_w
+     lvl_i = ctLocLevel loc_i
+     lvl_w = ctLocLevel loc_w
+
+     has_binding binds ev
+       | EvId v <- ctEvTerm ev = isJust (lookupEvBind binds v)
+       | otherwise             = True
+
+     use_replacement
+       | isIPPred pred = lvl_w > lvl_i
+       | otherwise     = lvl_w < lvl_i
 
 {-
+Note [Replacement vs keeping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we have two Given constraints both of type (C tys), say, which should
+we keep?
+
+  * For implicit parameters we want to keep the innermost (deepest)
+    one, so that it overrides the outer one.
+    See Note [Shadowing of Implicit Parameters]
+
+  * For everything else, we want to keep the outermost one.  Reason: that
+    makes it more likely that the inner one will turn out to be unused,
+    and can be reported as redundant.  See Note [Tracking redundant constraints]
+    in TcSimplify.
+
+    It transpires that using the outermost one is reponsible for an
+    8% performance improvement in nofib cryptarithm2, compared to
+    just rolling the dice.  I didn't investigate why.
+
+  * If there is no "outermost" one, we keep the one that has a non-trivial
+    evidence binding.  Note [Tracking redundant constraints] again.
+    Example:  f :: (Eq a, Ord a) => blah
+    then we may find [G] sc_sel (d1::Ord a) :: Eq a
+                     [G] d2 :: Eq a
+    We want to discard d2 in favour of the superclass selection from
+    the Ord dictionary.
+
+  * Finally, when there is still a choice, use IRKeep rather than
+    IRReplace, to avoid unnecesary munging of the inert set.
+
+Doing the depth-check for implicit parameters, rather than making the work item
+always overrride, is important.  Consider
+
+    data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }
+
+    f :: (?x::a) => T a -> Int
+    f T1 = ?x
+    f T2 = 3
+
+We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
+two new givens in the work-list:  [G] (?x::Int)
+                                  [G] (a ~ Int)
+Now consider these steps
+  - process a~Int, kicking out (?x::a)
+  - process (?x::Int), the inner given, adding to inert set
+  - process (?x::a), the outer given, overriding the inner given
+Wrong!  The depth-check ensures that the inner implicit parameter wins.
+(Actually I think that the order in which the work-list is processed means
+that this chain of events won't happen, but that's very fragile.)
+
 *********************************************************************************
 *                                                                               *
                    interactIrred
@@ -823,8 +897,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
                          , rhs_i `tcEqType` rhs ]
   =  -- Inert:     a ~ b
      -- Work item: a ~ b
-    do { when (isWanted ev) $
-         setEvBind (ctev_evar ev) (ctEvTerm ev_i)
+    do { setEvBindIfWanted ev (ctEvTerm ev_i)
        ; stopWith ev "Solved from inert" }
 
   | Just tv_rhs <- getTyVar_maybe rhs
@@ -834,8 +907,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
                          , rhs_i `tcEqType` mkTyVarTy tv ]
   =  -- Inert:     a ~ b
      -- Work item: b ~ a
-    do { when (isWanted ev) $
-         setEvBind (ctev_evar ev)
+    do { setEvBindIfWanted ev
                    (EvCoercion (mkTcSymCo (ctEvCoercion ev_i)))
        ; stopWith ev "Solved from inert (r)" }
 
@@ -901,8 +973,6 @@ solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
 -- Precondition: kind(xi) is a sub-kind of kind(tv)
 -- Precondition: CtEvidence is Wanted or Derived
 -- Precondition: CtEvidence is nominal
--- See [New Wanted Superclass Work] to see why solveByUnification
---     must work for Derived as well as Wanted
 -- Returns: workItem where
 --        workItem = the new Given constraint
 --
@@ -927,8 +997,7 @@ solveByUnification wd tv xi
                -- cf TcUnify.uUnboundKVar
 
        ; setWantedTyBind tv xi'
-       ; when (isWanted wd) $
-         setEvBind (ctEvId wd) (EvCoercion (mkTcNomReflCo xi')) }
+       ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi')) }
 
 
 ppr_kicked :: Int -> SDoc
@@ -1100,342 +1169,6 @@ double unifications is the main reason we disallow touchable
 unification variables as RHS of type family equations: F xis ~ alpha.
 
 
-
-Note [Superclasses and recursive dictionaries]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-    Overlaps with Note [SUPERCLASS-LOOP 1]
-                  Note [SUPERCLASS-LOOP 2]
-                  Note [Recursive instances and superclases]
-    ToDo: check overlap and delete redundant stuff
-
-Right before adding a given into the inert set, we must
-produce some more work, that will bring the superclasses
-of the given into scope. The superclass constraints go into
-our worklist.
-
-When we simplify a wanted constraint, if we first see a matching
-instance, we may produce new wanted work. To (1) avoid doing this work
-twice in the future and (2) to handle recursive dictionaries we may ``cache''
-this item as given into our inert set WITHOUT adding its superclass constraints,
-otherwise we'd be in danger of creating a loop [In fact this was the exact reason
-for doing the isGoodRecEv check in an older version of the type checker].
-
-But now we have added partially solved constraints to the worklist which may
-interact with other wanteds. Consider the example:
-
-Example 1:
-
-    class Eq b => Foo a b        --- 0-th selector
-    instance Eq a => Foo [a] a   --- fooDFun
-
-and wanted (Foo [t] t). We are first going to see that the instance matches
-and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
-       d1 :_g Foo [t] t                 d1 := EvDFunApp fooDFun d3
-Our work list is going to contain a new *wanted* goal
-       d3 :_w Eq t
-
-Ok, so how do we get recursive dictionaries, at all:
-
-Example 2:
-
-    data D r = ZeroD | SuccD (r (D r));
-
-    instance (Eq (r (D r))) => Eq (D r) where
-        ZeroD     == ZeroD     = True
-        (SuccD a) == (SuccD b) = a == b
-        _         == _         = False;
-
-    equalDC :: D [] -> D [] -> Bool;
-    equalDC = (==);
-
-We need to prove (Eq (D [])). Here's how we go:
-
-        d1 :_w Eq (D [])
-
-by instance decl, holds if
-        d2 :_w Eq [D []]
-        where   d1 = dfEqD d2
-
-*BUT* we have an inert set which gives us (no superclasses):
-        d1 :_g Eq (D [])
-By the instance declaration of Eq we can show the 'd2' goal if
-        d3 :_w Eq (D [])
-        where   d2 = dfEqList d3
-                d1 = dfEqD d2
-Now, however this wanted can interact with our inert d1 to set:
-        d3 := d1
-and solve the goal. Why was this interaction OK? Because, if we chase the
-evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
-are really setting
-        d3 := dfEqD2 (dfEqList d3)
-which is FINE because the use of d3 is protected by the instance function
-applications.
-
-So, our strategy is to try to put solved wanted dictionaries into the
-inert set along with their superclasses (when this is meaningful,
-i.e. when new wanted goals are generated) but solve a wanted dictionary
-from a given only in the case where the evidence variable of the
-wanted is mentioned in the evidence of the given (recursively through
-the evidence binds) in a protected way: more instance function applications
-than superclass selectors.
-
-Here are some more examples from GHC's previous type checker
-
-
-Example 3:
-This code arises in the context of "Scrap Your Boilerplate with Class"
-
-    class Sat a
-    class Data ctx a
-    instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
-    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2
-
-    class Data Maybe a => Foo a
-
-    instance Foo t => Sat (Maybe t)                             -- dfunSat
-
-    instance Data Maybe a => Foo a                              -- dfunFoo1
-    instance Foo a        => Foo [a]                            -- dfunFoo2
-    instance                 Foo [Char]                         -- dfunFoo3
-
-Consider generating the superclasses of the instance declaration
-         instance Foo a => Foo [a]
-
-So our problem is this
-    [G] d0 : Foo t
-    [W] d1 : Data Maybe [t]   -- Desired superclass
-
-We may add the given in the inert set, along with its superclasses
-[assuming we don't fail because there is a matching instance, see
- topReactionsStage, given case ]
-  Inert:
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  WorkList
-    [W] d1 : Data Maybe [t]
-
-Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
-  Inert:
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-  WorkList
-    [W] d2 : Sat (Maybe [t])
-    [W] d3 : Data Maybe t
-
-Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
-  Inert:
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-        d2 : Sat (Maybe [t])
-  WorkList:
-    [W] d3 : Data Maybe t
-    [W] d4 : Foo [t]
-
-Now, we can just solve d3 from d01; d3 := d01
-  Inert
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-        d2 : Sat (Maybe [t])
-  WorkList
-    [W] d4 : Foo [t]
-
-Now, solve d4 using dfunFoo2;  d4 := dfunFoo2 d5
-  Inert
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-        d2 : Sat (Maybe [t])
-        d4 : Foo [t]
-  WorkList:
-    [W] d5 : Foo t
-
-Now, d5 can be solved! d5 := d0
-
-Result
-   d1 := dfunData2 d2 d3
-   d2 := dfunSat d4
-   d3 := d01
-   d4 := dfunFoo2 d5
-   d5 := d0
-
-      d0 :_g Foo t
-      d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
-      d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
-      d4 :_g Foo [t]                  d4 := dfunFoo2 d5
-      d5 :_g Foo t                    d5 := dfunFoo1 d7
-  WorkList:
-      d7 :_w Data Maybe t
-      d6 :_g Data Maybe [t]
-      d8 :_g Data Maybe t            d8 := EvDictSuperClass d5 0
-      d01 :_g Data Maybe t
-
-Now, two problems:
-   [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
-       we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
-       that must not be used (look at case interactInert where both inert and workitem
-       are givens). So we have several options:
-       - Drop the workitem always (this will drop d8)
-              This feels very unsafe -- what if the work item was the "good" one
-              that should be used later to solve another wanted?
-       - Don't drop anyone: the inert set may contain multiple givens!
-              [This is currently implemented]
-
-The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
-  [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
-      d7. Now the [isRecDictEv] function in the ineration solver
-      [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
-      precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
-
-      So, no interaction happens there. Then we meet d01 and there is no recursion
-      problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
-
-Note [SUPERCLASS-LOOP 1]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We have to be very, very careful when generating superclasses, lest we
-accidentally build a loop. Here's an example:
-
-  class S a
-
-  class S a => C a where { opc :: a -> a }
-  class S b => D b where { opd :: b -> b }
-
-  instance C Int where
-     opc = opd
-
-  instance D Int where
-     opd = opc
-
-From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
-Simplifying, we may well get:
-        $dfCInt = :C ds1 (opd dd)
-        dd  = $dfDInt
-        ds1 = $p1 dd
-Notice that we spot that we can extract ds1 from dd.
-
-Alas!  Alack! We can do the same for (instance D Int):
-
-        $dfDInt = :D ds2 (opc dc)
-        dc  = $dfCInt
-        ds2 = $p1 dc
-
-And now we've defined the superclass in terms of itself.
-Two more nasty cases are in
-        tcrun021
-        tcrun033
-
-Solution:
-  - Satisfy the superclass context *all by itself*
-    (tcSimplifySuperClasses)
-  - And do so completely; i.e. no left-over constraints
-    to mix with the constraints arising from method declarations
-
-
-Note [SUPERCLASS-LOOP 2]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We need to be careful when adding "the constaint we are trying to prove".
-Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
-
-        class Ord a => C a where
-        instance Ord [a] => C [a] where ...
-
-Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
-superclasses of C [a] to avails.  But we must not overwrite the binding
-for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
-build a loop!
-
-Here's another variant, immortalised in tcrun020
-        class Monad m => C1 m
-        class C1 m => C2 m x
-        instance C2 Maybe Bool
-For the instance decl we need to build (C1 Maybe), and it's no good if
-we run around and add (C2 Maybe Bool) and its superclasses to the avails
-before we search for C1 Maybe.
-
-Here's another example
-        class Eq b => Foo a b
-        instance Eq a => Foo [a] a
-If we are reducing
-        (Foo [t] t)
-
-we'll first deduce that it holds (via the instance decl).  We must not
-then overwrite the Eq t constraint with a superclass selection!
-
-At first I had a gross hack, whereby I simply did not add superclass constraints
-in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
-because it lost legitimate superclass sharing, and it still didn't do the job:
-I found a very obscure program (now tcrun021) in which improvement meant the
-simplifier got two bites a the cherry... so something seemed to be an Stop
-first time, but reducible next time.
-
-Now we implement the Right Solution, which is to check for loops directly
-when adding superclasses.  It's a bit like the occurs check in unification.
-
-Note [Recursive instances and superclases]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this code, which arises in the context of "Scrap Your
-Boilerplate with Class".
-
-    class Sat a
-    class Data ctx a
-    instance  Sat (ctx Char)             => Data ctx Char
-    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
-
-    class Data Maybe a => Foo a
-
-    instance Foo t => Sat (Maybe t)
-
-    instance Data Maybe a => Foo a
-    instance Foo a        => Foo [a]
-    instance                 Foo [Char]
-
-In the instance for Foo [a], when generating evidence for the superclasses
-(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
-Using the instance for Data, we therefore need
-        (Sat (Maybe [a], Data Maybe a)
-But we are given (Foo a), and hence its superclass (Data Maybe a).
-So that leaves (Sat (Maybe [a])).  Using the instance for Sat means
-we need (Foo [a]).  And that is the very dictionary we are bulding
-an instance for!  So we must put that in the "givens".  So in this
-case we have
-        Given:  Foo a, Foo [a]
-        Wanted: Data Maybe [a]
-
-BUT we must *not not not* put the *superclasses* of (Foo [a]) in
-the givens, which is what 'addGiven' would normally do. Why? Because
-(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
-by selecting a superclass from Foo [a], which simply makes a loop.
-
-On the other hand we *must* put the superclasses of (Foo a) in
-the givens, as you can see from the derivation described above.
-
-Conclusion: in the very special case of tcSimplifySuperClasses
-we have one 'given' (namely the "this" dictionary) whose superclasses
-must not be added to 'givens' by addGiven.
-
-There is a complication though.  Suppose there are equalities
-      instance (Eq a, a~b) => Num (a,b)
-Then we normalise the 'givens' wrt the equalities, so the original
-given "this" dictionary is cast to one of a different type.  So it's a
-bit trickier than before to identify the "special" dictionary whose
-superclasses must not be added. See test
-   indexed-types/should_run/EqInInstance
-
-We need a persistent property of the dictionary to record this
-special-ness.  Current I'm using the InstLocOrigin (a bit of a hack,
-but cool), which is maintained by dictionary normalisation.
-Specifically, the InstLocOrigin is
-             NoScOrigin
-then the no-superclass thing kicks in.  WATCH OUT if you fiddle
-with InstLocOrigin!
-
-
 ************************************************************************
 *                                                                      *
 *          Functional dependencies, instantiation of equations
@@ -1498,9 +1231,6 @@ doTopReact :: InertSet -> WorkItem -> TcS (StopOrContinue Ct)
 --   (a) The place to add superclasses in not here in doTopReact stage.
 --       Instead superclasses are added in the worklist as part of the
 --       canonicalization process. See Note [Adding superclasses].
---
---   (b) See Note [Given constraint that matches an instance declaration]
---       for some design decisions for given dictionaries.
 
 doTopReact inerts work_item
   = do { traceTcS "doTopReact" (ppr work_item)
@@ -1519,7 +1249,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
   = try_fundeps_and_return
 
   | Just ev <- lookupSolvedDict inerts loc cls xis   -- Cached
-  = do { setEvBind dict_id (ctEvTerm ev);
+  = do { setWantedEvBind dict_id (ctEvTerm ev);
        ; stopWith fl "Dict/Top (cached)" }
 
   | otherwise  -- Not cached
@@ -1539,12 +1269,12 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
         | null evs
         = do { traceTcS "doTopReact/found nullary instance for" $
                ppr dict_id
-             ; setEvBind dict_id ev_term
+             ; setWantedEvBind dict_id ev_term
              ; stopWith fl "Dict/Top (solved, no new work)" }
         | otherwise
         = do { traceTcS "doTopReact/found non-nullary instance for" $
                ppr dict_id
-             ; setEvBind dict_id ev_term
+             ; setWantedEvBind dict_id ev_term
              ; let mk_new_wanted ev
                        = mkNonCanonical (ev {ctev_loc = bumpCtLocDepth CountConstraints loc })
              ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
@@ -1670,7 +1400,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
                -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
 
        ; new_ev <- newWantedEvVarNC loc (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
-       ; setEvBind (ctEvId old_ev)
+       ; setWantedEvBind (ctEvId old_ev)
                    (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
                                       `mkTcTransCo` ctEvCoercion new_ev))
 
@@ -1693,7 +1423,7 @@ dischargeFmv :: EvVar -> TcTyVar -> TcCoercion -> TcType -> TcS ()
 dischargeFmv evar fmv co xi
   = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr evar $$ ppr fmv $$ ppr xi )
     do { setWantedTyBind fmv xi
-       ; setEvBind evar (EvCoercion co)
+       ; setWantedEvBind evar (EvCoercion co)
        ; n_kicked <- kickOutRewritable Given NomEq fmv
        ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
 
@@ -1834,113 +1564,6 @@ This should probably be well typed, with
 
 So the inner binding for ?x::Bool *overrides* the outer one.
 Hence a work-item Given overrides an inert-item Given.
-
-Note [Given constraint that matches an instance declaration]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What should we do when we discover that one (or more) top-level
-instances match a given (or solved) class constraint? We have
-two possibilities:
-
-  1. Reject the program. The reason is that there may not be a unique
-     best strategy for the solver. Example, from the OutsideIn(X) paper:
-       instance P x => Q [x]
-       instance (x ~ y) => R [x] y
-
-       wob :: forall a b. (Q [b], R b a) => a -> Int
-
-       g :: forall a. Q [a] => [a] -> Int
-       g x = wob x
-
-       will generate the impliation constraint:
-            Q [a] => (Q [beta], R beta [a])
-       If we react (Q [beta]) with its top-level axiom, we end up with a
-       (P beta), which we have no way of discharging. On the other hand,
-       if we react R beta [a] with the top-level we get  (beta ~ a), which
-       is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
-       now solvable by the given Q [a].
-
-     However, this option is restrictive, for instance [Example 3] from
-     Note [Recursive instances and superclases] will fail to work.
-
-  2. Ignore the problem, hoping that the situations where there exist indeed
-     such multiple strategies are rare: Indeed the cause of the previous
-     problem is that (R [x] y) yields the new work (x ~ y) which can be
-     *spontaneously* solved, not using the givens.
-
-We are choosing option 2 below but we might consider having a flag as well.
-
-
-Note [New Wanted Superclass Work]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Even in the case of wanted constraints, we may add some superclasses
-as new given work. The reason is:
-
-        To allow FD-like improvement for type families. Assume that
-        we have a class
-             class C a b | a -> b
-        and we have to solve the implication constraint:
-             C a b => C a beta
-        Then, FD improvement can help us to produce a new wanted (beta ~ b)
-
-        We want to have the same effect with the type family encoding of
-        functional dependencies. Namely, consider:
-             class (F a ~ b) => C a b
-        Now suppose that we have:
-               given: C a b
-               wanted: C a beta
-        By interacting the given we will get given (F a ~ b) which is not
-        enough by itself to make us discharge (C a beta). However, we
-        may create a new derived equality from the super-class of the
-        wanted constraint (C a beta), namely derived (F a ~ beta).
-        Now we may interact this with given (F a ~ b) to get:
-                  derived :  beta ~ b
-        But 'beta' is a touchable unification variable, and hence OK to
-        unify it with 'b', replacing the derived evidence with the identity.
-
-        This requires trySpontaneousSolve to solve *derived*
-        equalities that have a touchable in their RHS, *in addition*
-        to solving wanted equalities.
-
-We also need to somehow use the superclasses to quantify over a minimal,
-constraint see note [Minimize by Superclasses] in TcSimplify.
-
-
-Finally, here is another example where this is useful.
-
-Example 1:
-----------
-   class (F a ~ b) => C a b
-And we are given the wanteds:
-      w1 : C a b
-      w2 : C a c
-      w3 : b ~ c
-We surely do *not* want to quantify over (b ~ c), since if someone provides
-dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
-of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
-
-     Step 1: We will get new *given* superclass work,
-             provisionally to our solving of w1 and w2
-
-               g1: F a ~ b, g2 : F a ~ c,
-               w1 : C a b, w2 : C a c, w3 : b ~ c
-
-             The evidence for g1 and g2 is a superclass evidence term:
-
-               g1 := sc w1, g2 := sc w2
-
-     Step 2: The givens will solve the wanted w3, so that
-               w3 := sym (sc w1) ; sc w2
-
-     Step 3: Now, one may naively assume that then w2 can be solve from w1
-             after rewriting with the (now solved equality) (b ~ c).
-
-             But this rewriting is ruled out by the isGoodRectDict!
-
-Conclusion, we will (correctly) end up with the unsolved goals
-    (C a b, C a c)
-
-NB: The desugarer needs be more clever to deal with equalities
-    that participate in recursive dictionary bindings.
 -}
 
 data LookupInstResult
@@ -2030,20 +1653,16 @@ matchClassInst inerts clas tys loc
    where
      pred = mkClassPred clas tys
 
-     match_one :: DFunId -> [Maybe TcType] -> TcS LookupInstResult
+     match_one :: DFunId -> [DFunInstType] -> TcS LookupInstResult
                   -- See Note [DFunInstType: instantiating types] in InstEnv
      match_one dfun_id mb_inst_tys
        = do { checkWellStagedDFun pred dfun_id loc
-            ; (tys, dfun_phi) <- instDFunType dfun_id mb_inst_tys
-            ; let (theta, _) = tcSplitPhiTy dfun_phi
-            ; if null theta then
-                  return (GenInst [] (EvDFunApp dfun_id tys []))
-              else do
-            { evc_vars <- instDFunConstraints loc theta
+            ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
+            ; evc_vars <- mapM (newWantedEvVar loc) theta
             ; let new_ev_vars = freshGoals evc_vars
                       -- new_ev_vars are only the real new variables that can be emitted
                   dfun_app = EvDFunApp dfun_id tys (map (ctEvTerm . fst) evc_vars)
-            ; return $ GenInst new_ev_vars dfun_app } }
+            ; return $ GenInst new_ev_vars dfun_app }
 
      givens_for_this_clas :: Cts
      givens_for_this_clas
@@ -2072,22 +1691,27 @@ matchClassInst inerts clas tys loc
 {-
 Note [Instance and Given overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Assume that we have an inert set that looks as follows:
-       [Given] D [Int]
-And an instance declaration:
-       instance C a => D [a]
-A new wanted comes along of the form:
-       [Wanted] D [alpha]
-
-One possibility is to apply the instance declaration which will leave us
-with an unsolvable goal (C alpha). However, later on a new constraint may
-arise (for instance due to a functional dependency between two later dictionaries),
-that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
-will be transformed to [Wanted] D [Int], which could have been discharged by the given.
-
-The solution is that in matchClassInst and eventually in topReact, we get back with
-a matching instance, only when there is no Given in the inerts which is unifiable to
-this particular dictionary.
+Example, from the OutsideIn(X) paper:
+       instance P x => Q [x]
+       instance (x ~ y) => R y [x]
+
+       wob :: forall a b. (Q [b], R b a) => a -> Int
+
+       g :: forall a. Q [a] => [a] -> Int
+       g x = wob x
+
+This will generate the impliation constraint:
+            Q [a] => (Q [beta], R beta [a])
+If we react (Q [beta]) with its top-level axiom, we end up with a
+(P beta), which we have no way of discharging. On the other hand,
+if we react R beta [a] with the top-level we get  (beta ~ a), which
+is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
+now solvable by the given Q [a].
+
+The solution is that:
+  In matchClassInst (and thus in topReact), we return a matching
+  instance only when there is no Given in the inerts which is
+  unifiable to this particular dictionary.
 
 The end effect is that, much as we do for overlapping instances, we delay choosing a
 class instance if there is a possibility of another instance OR a given to match our