Major patch to add -fwarn-redundant-constraints
[ghc.git] / compiler / typecheck / TcInteract.hs
index edb3303..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,22 +13,18 @@ import TcFlatten
 import VarSet
 import Type
 import Unify
-import InstEnv( lookupInstEnv, instanceDFunId )
+import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
 import CoAxiom(sfInteractTop, sfInteractInert)
 
 import Var
 import TcType
 import PrelNames (knownNatClassName, knownSymbolClassName, ipClassNameKey )
-import TysWiredIn ( coercibleClass )
 import Id( idType )
 import Class
 import TyCon
-import DataCon
-import Name
-import RdrName ( GlobalRdrEnv, lookupGRE_Name, mkRdrQual, is_as,
-                 is_decl, Provenance(Imported), gre_prov )
 import FunDeps
 import FamInst
+import Inst( tyVarsOfCt )
 
 import TcEvidence
 import Outputable
@@ -43,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 )
@@ -79,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.
 
@@ -100,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!
 
@@ -113,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
@@ -125,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
@@ -135,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) }
@@ -189,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
@@ -206,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
@@ -224,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
@@ -454,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")
@@ -476,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
@@ -683,7 +753,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
   = do { let matching_funeqs = findFunEqsByTyCon funeqs tc
        ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk)
              do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev })
-                = mapM_ (emitNewDerivedEq (ctEvLoc iev))
+                = mapM_ (unifyDerived (ctEvLoc iev) Nominal)
                         (interact iargs (lookupFlattenTyVar eqs ifsk))
              do_one ct = pprPanic "interactFunEq" (ppr ct)
        ; mapM_ do_one matching_funeqs
@@ -701,11 +771,12 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
 interactFunEq _ wi = pprPanic "interactFunEq" (ppr wi)
 
 lookupFlattenTyVar :: TyVarEnv EqualCtList -> TcTyVar -> TcType
--- ^ Look up a flatten-tyvar in the inert TyVarEqs
+-- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
+-- this is used only when dealing with a CFunEqCan
 lookupFlattenTyVar inert_eqs ftv
   = case lookupVarEnv inert_eqs ftv of
-      Just (CTyEqCan { cc_rhs = rhs } : _) -> rhs
-      _                                    -> mkTyVarTy ftv
+      Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _) -> rhs
+      _                                                       -> mkTyVarTy ftv
 
 reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F tys ~ fsk1
            -> CtEvidence -> TcTyVar    -- Solve this :: F tys ~ fsk2
@@ -816,35 +887,38 @@ test when solving pairwise CFunEqCan.
 
 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 -- CTyEqCans are always consumed, so always returns Stop
-interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs , cc_ev = ev })
+interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
+                                          , cc_rhs = rhs
+                                          , cc_ev = ev
+                                          , cc_eq_rel = eq_rel })
   | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
-                             <- findTyEqs (inert_eqs inerts) tv
+                             <- findTyEqs inerts tv
                          , ev_i `canRewriteOrSame` ev
                          , 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
   , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
-                             <- findTyEqs (inert_eqs inerts) tv_rhs
+                             <- findTyEqs inerts tv_rhs
                          , ev_i `canRewriteOrSame` ev
                          , 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)" }
 
   | otherwise
   = do { tclvl <- getTcLevel
-       ; if canSolveByUnification tclvl ev tv rhs
+       ; if canSolveByUnification tclvl ev eq_rel tv rhs
          then do { solveByUnification ev tv rhs
-                 ; n_kicked <- kickOutRewritable givenFlavour tv
-                               -- givenFlavour because the tv := xi is given
+                 ; n_kicked <- kickOutRewritable Given NomEq tv
+                               -- Given because the tv := xi is given
+                               -- NomEq because only nom. equalities are solved
+                               -- by unification
                  ; return (Stop ev (ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked)) }
 
          else do { traceTcS "Can't solve tyvar equality"
@@ -854,7 +928,9 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs , cc_ev
                                        <+> text "is" <+> ppr (metaTyVarTcLevel tv))
                              , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
                              , text "TcLevel =" <+> ppr tclvl ])
-                 ; n_kicked <- kickOutRewritable ev tv
+                 ; n_kicked <- kickOutRewritable (ctEvFlavour ev)
+                                                 (ctEvEqRel ev)
+                                                 tv
                  ; updInertCans (\ ics -> addInertCan ics workItem)
                  ; return (Stop ev (ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked)) } }
 
@@ -863,8 +939,12 @@ interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
 -- @trySpontaneousSolve wi@ solves equalities where one side is a
 -- touchable unification variable.
 -- Returns True <=> spontaneous solve happened
-canSolveByUnification :: TcLevel -> CtEvidence -> TcTyVar -> Xi -> Bool
-canSolveByUnification tclvl gw tv xi
+canSolveByUnification :: TcLevel -> CtEvidence -> EqRel
+                      -> TcTyVar -> Xi -> Bool
+canSolveByUnification tclvl gw eq_rel tv xi
+  | ReprEq <- eq_rel   -- we never solve representational equalities this way.
+  = False
+
   | isGiven gw   -- See Note [Touchables and givens]
   = False
 
@@ -892,8 +972,7 @@ solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
 -- Solve with the identity coercion
 -- Precondition: kind(xi) is a sub-kind of kind(tv)
 -- Precondition: CtEvidence is Wanted or Derived
--- See [New Wanted Superclass Work] to see why solveByUnification
---     must work for Derived as well as Wanted
+-- Precondition: CtEvidence is nominal
 -- Returns: workItem where
 --        workItem = the new Given constraint
 --
@@ -918,34 +997,27 @@ solveByUnification wd tv xi
                -- cf TcUnify.uUnboundKVar
 
        ; setWantedTyBind tv xi'
-       ; when (isWanted wd) $
-         setEvBind (ctEvId wd) (EvCoercion (mkTcNomReflCo xi')) }
-
+       ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi')) }
 
-givenFlavour :: CtEvidence
--- Used just to pass to kickOutRewritable
--- and to guide 'flatten' for givens
-givenFlavour = CtGiven { ctev_pred = panic "givenFlavour:ev"
-                       , ctev_evtm = panic "givenFlavour:tm"
-                       , ctev_loc  = panic "givenFlavour:loc" }
 
 ppr_kicked :: Int -> SDoc
 ppr_kicked 0 = empty
 ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
 
-kickOutRewritable :: CtEvidence   -- Flavour of the equality that is
+kickOutRewritable :: CtFlavour    -- Flavour of the equality that is
                                   -- being added to the inert set
+                  -> EqRel        -- of the new equality
                   -> TcTyVar      -- The new equality is tv ~ ty
                   -> TcS Int
-kickOutRewritable new_ev new_tv
-  | not (new_ev `eqCanRewrite` new_ev)
-  = return 0  -- If new_ev can't rewrite itself, it can't rewrite
+kickOutRewritable new_flavour new_eq_rel new_tv
+  | not ((new_flavour, new_eq_rel) `eqCanRewriteFR` (new_flavour, new_eq_rel))
+  = return 0  -- If new_flavour can't rewrite itself, it can't rewrite
               -- anything else, so no need to kick out anything
               -- This is a common case: wanteds can't rewrite wanteds
 
   | otherwise
   = do { ics <- getInertCans
-       ; let (kicked_out, ics') = kick_out new_ev new_tv ics
+       ; let (kicked_out, ics') = kick_out new_flavour new_eq_rel new_tv ics
        ; setInertCans ics'
        ; updWorkListTcS (appendWorkList kicked_out)
 
@@ -957,46 +1029,50 @@ kickOutRewritable new_ev new_tv
                     , ppr kicked_out ])
        ; return (workListSize kicked_out) }
 
-kick_out :: CtEvidence -> TcTyVar -> InertCans -> (WorkList, InertCans)
-kick_out new_ev new_tv (IC { inert_eqs = tv_eqs
-                           , inert_dicts  = dictmap
-                           , inert_funeqs = funeqmap
-                           , inert_irreds = irreds
-                           , inert_insols = insols })
+kick_out :: CtFlavour -> EqRel -> TcTyVar -> InertCans -> (WorkList, InertCans)
+kick_out new_flavour new_eq_rel new_tv (IC { inert_eqs      = tv_eqs
+                                           , inert_dicts    = dictmap
+                                           , inert_funeqs   = funeqmap
+                                           , inert_irreds   = irreds
+                                           , inert_insols   = insols })
   = (kicked_out, inert_cans_in)
   where
                 -- NB: Notice that don't rewrite
                 -- inert_solved_dicts, and inert_solved_funeqs
                 -- optimistically. But when we lookup we have to
                 -- take the substitution into account
-    inert_cans_in = IC { inert_eqs = tv_eqs_in
-                       , inert_dicts = dicts_in
-                       , inert_funeqs = feqs_in
-                       , inert_irreds = irs_in
-                       , inert_insols = insols_in }
+    inert_cans_in = IC { inert_eqs      = tv_eqs_in
+                       , inert_dicts    = dicts_in
+                       , inert_funeqs   = feqs_in
+                       , inert_irreds   = irs_in
+                       , inert_insols   = insols_in }
 
     kicked_out = WL { wl_eqs    = tv_eqs_out
-                    , wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
+                    , wl_funeqs = feqs_out
                     , wl_rest   = bagToList (dicts_out `andCts` irs_out
                                              `andCts` insols_out)
                     , wl_implics = emptyBag }
 
-    (tv_eqs_out,  tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
-    (feqs_out,   feqs_in)    = partitionFunEqs  kick_out_ct funeqmap
-    (dicts_out,  dicts_in)   = partitionDicts   kick_out_ct dictmap
-    (irs_out,    irs_in)     = partitionBag     kick_out_irred irreds
-    (insols_out, insols_in)  = partitionBag     kick_out_ct    insols
+    (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
+    (feqs_out,   feqs_in)   = partitionFunEqs  kick_out_ct funeqmap
+    (dicts_out,  dicts_in)  = partitionDicts   kick_out_ct dictmap
+    (irs_out,    irs_in)    = partitionBag     kick_out_irred irreds
+    (insols_out, insols_in) = partitionBag     kick_out_ct    insols
       -- Kick out even insolubles; see Note [Kick out insolubles]
 
+    can_rewrite :: CtEvidence -> Bool
+    can_rewrite = ((new_flavour, new_eq_rel) `eqCanRewriteFR`) . ctEvFlavourRole
+
     kick_out_ct :: Ct -> Bool
     kick_out_ct ct = kick_out_ctev (ctEvidence ct)
 
-    kick_out_ctev ev =  eqCanRewrite new_ev ev
+    kick_out_ctev :: CtEvidence -> Bool
+    kick_out_ctev ev =  can_rewrite ev
                      && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
          -- See Note [Kicking out inert constraints]
 
     kick_out_irred :: Ct -> Bool
-    kick_out_irred ct =  eqCanRewrite new_ev (ctEvidence ct)
+    kick_out_irred ct =  can_rewrite (cc_ev ct)
                       && new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct)
           -- See Note [Kicking out Irreds]
 
@@ -1007,17 +1083,31 @@ kick_out new_ev new_tv (IC { inert_eqs = tv_eqs
                                []      -> acc_in
                                (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in)
       where
-        (eqs_out, eqs_in) = partition kick_out_eq eqs
-
-    kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev })
-       =  eqCanRewrite new_ev ev
-       && (tv == new_tv
-           || (ev `eqCanRewrite` ev && new_tv `elemVarSet` tyVarsOfType rhs_ty)
-           || case getTyVar_maybe rhs_ty of { Just tv_r -> tv_r == new_tv; Nothing -> False })
-    kick_out_eq ct = pprPanic "kick_out_eq" (ppr ct)
-    -- SLPJ new piece: Don't kick out a constraint unless it can rewrite itself,
-    --                 If not, it can't rewrite anything else, so no point in
-    --                 kicking it out
+        (eqs_in, eqs_out) = partition keep_eq eqs
+
+    -- implements criteria K1-K3 in Note [The inert equalities] in TcFlatten
+    keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
+                      , cc_eq_rel = eq_rel })
+      | tv == new_tv
+      = not (can_rewrite ev)  -- (K1)
+
+      | otherwise
+      = check_k2 && check_k3
+      where
+        check_k2 = not (ev `eqCanRewrite` ev)
+                || not (can_rewrite ev)
+                || not (new_tv `elemVarSet` tyVarsOfType rhs_ty)
+
+        check_k3
+          | can_rewrite ev
+          = case eq_rel of
+              NomEq  -> not (rhs_ty `eqType` mkTyVarTy new_tv)
+              ReprEq -> isTyVarExposed new_tv rhs_ty
+
+          | otherwise
+          = True
+
+    keep_eq ct = pprPanic "keep_eq" (ppr ct)
 
 {-
 Note [Kicking out inert constraints]
@@ -1059,50 +1149,6 @@ Now it can be decomposed.  Otherwise we end up with a "Can't match
 [Int] ~ [[Int]]" which is true, but a bit confusing because the
 outer type constructors match.
 
-Note [Delicate equality kick-out]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When adding an fully-rewritten work-item CTyEqCan (a ~ xi), we kick
-out an inert CTyEqCan (b ~ phi) when
-
-  a) the work item can rewrite the inert item
-
-AND one of the following hold
-
-(0) If the new tyvar is the same as the old one
-      Work item: [G] a ~ blah
-      Inert:     [W] a ~ foo
-    A particular case is when flatten-skolems get their value we must propagate
-
-(1) If the new tyvar appears in the kind vars of the LHS or RHS of
-    the inert.  Example:
-    Work item: [G] k ~ *
-    Inert:     [W] (a:k) ~ ty
-               [W] (b:*) ~ c :: k
-    We must kick out those blocked inerts so that we rewrite them
-    and can subsequently unify.
-
-(2) If the new tyvar appears in the RHS of the inert
-    AND not (the inert can rewrite the work item)   <---------------------------------
-
-          Work item:  [G] a ~ b
-          Inert:      [W] b ~ [a]
-    Now at this point the work item cannot be further rewritten by the
-    inert (due to the weaker inert flavor). But we can't add the work item
-    as-is because the inert set would then have a cyclic substitution,
-    when rewriting a wanted type mentioning 'a'. So we must kick the inert out.
-
-    We have to do this only if the inert *cannot* rewrite the work item;
-    it it can, then the work item will have been fully rewritten by the
-    inert set during canonicalisation.  So for example:
-         Work item: [W] a ~ Int
-         Inert:     [W] b ~ [a]
-    No need to kick out the inert, beause the inert substitution is not
-    necessarily idemopotent.  See Note [Non-idempotent inert substitution]
-    in TcFlatten.
-
-          Work item:  [G] a ~ Int
-          Inert:      [G] b ~ [a]
-See also Note [Detailed InertCans Invariants]
 
 Note [Avoid double unifications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1123,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
@@ -1495,7 +1205,8 @@ instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
        ; mapM_ (do_one subst) eqs }
   where
     do_one subst (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
-       = emitNewDerivedEq loc (Pair (Type.substTy subst ty1) (Type.substTy subst ty2))
+       = unifyDerived loc Nominal $
+         Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
 
 {-
 *********************************************************************************
@@ -1520,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)
@@ -1541,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
@@ -1561,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))
@@ -1628,6 +1336,9 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
     | otherwise -- We must not assign ufsk := ...ufsk...!
     -> do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
           ; new_ev <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
+          ; emitWorkNC [new_ev]
+              -- By emitting this as non-canonical, we deal with all
+              -- flattening, occurs-check, and ufsk := ufsk issues
           ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
               --    ax_co :: fam_tc args ~ rhs_ty
               --       ev :: alpha ~ rhs_ty
@@ -1638,9 +1349,6 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
             vcat [ text "old_ev:" <+> ppr old_ev
                  , nest 2 (text ":=") <+> ppr final_co
                  , text "new_ev:" <+> ppr new_ev ]
-          ; emitWorkNC [new_ev]
-              -- By emitting this as non-canonical, we deal with all
-              -- flattening, occurs-check, and ufsk := ufsk issues
           ; stopWith old_ev "Fun/Top (wanted)" } } }
   where
     loc = ctEvLoc old_ev
@@ -1650,7 +1358,7 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
       | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
       = do { inert_eqs <- getInertEqs
            ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk)
-           ; mapM_ (emitNewDerivedEq loc) eqns }
+           ; mapM_ (unifyDerived loc Nominal) eqns }
       | otherwise
       = return ()
 
@@ -1660,7 +1368,10 @@ shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
                   -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
 shortCutReduction old_ev fsk ax_co fam_tc tc_args
   | isGiven old_ev
-  = do { (xis, cos) <- flattenMany (FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }) tc_args
+  = ASSERT( ctEvEqRel old_ev == NomEq )
+    runFlatten $
+    do { let fmode = mkFlattenEnv FM_FlattenAll old_ev
+       ; (xis, cos) <- flatten_many fmode (repeat Nominal) tc_args
                -- ax_co :: F args ~ G tc_args
                -- cos   :: xis ~ tc_args
                -- old_ev :: F args ~ fsk
@@ -1673,12 +1384,15 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
                                         `mkTcTransCo` ctEvCoercion old_ev) )
 
        ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
-       ; updWorkListTcS (extendWorkListFunEq new_ct)
+       ; emitFlatWork new_ct
        ; stopWith old_ev "Fun/Top (given, shortcut)" }
 
   | otherwise
   = ASSERT( not (isDerived old_ev) )   -- Caller ensures this
-    do { (xis, cos) <- flattenMany (FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }) tc_args
+    ASSERT( ctEvEqRel old_ev == NomEq )
+    runFlatten $
+    do { let fmode = mkFlattenEnv FM_FlattenAll old_ev
+       ; (xis, cos) <- flatten_many fmode (repeat Nominal) tc_args
                -- ax_co :: F args ~ G tc_args
                -- cos   :: xis ~ tc_args
                -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
@@ -1686,12 +1400,12 @@ 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))
 
        ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
-       ; updWorkListTcS (extendWorkListFunEq new_ct)
+       ; emitFlatWork new_ct
        ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
   where
     loc = ctEvLoc old_ev
@@ -1709,8 +1423,8 @@ 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)
-       ; n_kicked <- kickOutRewritable givenFlavour fmv
+       ; setWantedEvBind evar (EvCoercion co)
+       ; n_kicked <- kickOutRewritable Given NomEq fmv
        ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
 
 {-
@@ -1850,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
@@ -2005,14 +1612,6 @@ matchClassInst _ clas [ ty ] _
     = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
                      $$ vcat (map (ppr . idType) (classMethods clas)))
 
-matchClassInst _ clas [ _k, ty1, ty2 ] loc
-  | clas == coercibleClass
-  = do { traceTcS "matchClassInst for" $
-         quotes (pprClassPred clas [ty1,ty2]) <+> text "at depth" <+> ppr (ctLocDepth loc)
-       ; ev <- getCoercibleInst loc ty1 ty2
-       ; traceTcS "matchClassInst returned" $ ppr ev
-       ; return ev }
-
 matchClassInst inerts clas tys loc
    = do { dflags <- getDynFlags
         ; tclvl <- getTcLevel
@@ -2054,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
@@ -2093,207 +1688,30 @@ matchClassInst inerts clas tys loc
                            -- by the overlap check with the instance environment.
      matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
 
--- See Note [Coercible Instances]
--- Changes to this logic should likely be reflected in coercible_msg in TcErrors.
-getCoercibleInst :: CtLoc -> TcType -> TcType -> TcS LookupInstResult
-getCoercibleInst loc ty1 ty2
-  = do { -- Get some global stuff in scope, for nice pattern-guard based code in `go`
-         rdr_env <- getGlobalRdrEnvTcS
-       ; famenv <- getFamInstEnvs
-       ; go famenv rdr_env }
-  where
-  go :: FamInstEnvs -> GlobalRdrEnv -> TcS LookupInstResult
-  go famenv rdr_env
-    -- Also see [Order of Coercible Instances]
-
-    -- Coercible a a                             (see case 1 in [Coercible Instances])
-    | ty1 `tcEqType` ty2
-    = return $ GenInst []
-             $ EvCoercion (TcRefl Representational ty1)
-
-    -- Coercible (forall a. ty) (forall a. ty')  (see case 2 in [Coercible Instances])
-    | tcIsForAllTy ty1
-    , tcIsForAllTy ty2
-    , let (tvs1,body1) = tcSplitForAllTys ty1
-          (tvs2,body2) = tcSplitForAllTys ty2
-    , equalLength tvs1 tvs2
-    = do { ev_term <- deferTcSForAllEq Representational loc (tvs1,body1) (tvs2,body2)
-         ; return $ GenInst [] ev_term }
-
-    -- Coercible NT a                            (see case 3 in [Coercible Instances])
-    | Just (rep_tc, conc_ty, nt_co) <- tcInstNewTyConTF_maybe famenv ty1
-    , dataConsInScope rdr_env rep_tc -- Do not look at all tyConsOfTyCon
-    = do { markDataConsAsUsed rdr_env rep_tc
-         ; (new_goals, residual_co) <- requestCoercible loc conc_ty ty2
-         ; let final_co = nt_co `mkTcTransCo` residual_co
-                          -- nt_co       :: ty1     ~R conc_ty
-                          -- residual_co :: conc_ty ~R ty2
-         ; return $ GenInst new_goals (EvCoercion final_co) }
-
-    -- Coercible a NT                            (see case 3 in [Coercible Instances])
-    | Just (rep_tc, conc_ty, nt_co) <- tcInstNewTyConTF_maybe famenv ty2
-    , dataConsInScope rdr_env rep_tc -- Do not look at all tyConsOfTyCon
-    = do { markDataConsAsUsed rdr_env rep_tc
-         ; (new_goals, residual_co) <- requestCoercible loc ty1 conc_ty
-         ; let final_co = residual_co `mkTcTransCo` mkTcSymCo nt_co
-         ; return $ GenInst new_goals (EvCoercion final_co) }
-
-    -- Coercible (D ty1 ty2) (D ty1' ty2')       (see case 4 in [Coercible Instances])
-    | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1
-    , Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2
-    , tc1 == tc2
-    , nominalArgsAgree tc1 tyArgs1 tyArgs2
-    = do { -- We want evidence for all type arguments of role R
-           arg_stuff <- forM (zip3 (tyConRoles tc1) tyArgs1 tyArgs2) $ \ (r,ta1,ta2) ->
-                        case r of
-                           Representational -> requestCoercible loc ta1 ta2
-                           Phantom          -> return ([], TcPhantomCo ta1 ta2)
-                           Nominal          -> return ([], mkTcNomReflCo ta1)
-                                               -- ta1 == ta2, due to nominalArgsAgree
-         ; let (new_goals_s, arg_cos) = unzip arg_stuff
-               final_co = mkTcTyConAppCo Representational tc1 arg_cos
-         ; return $ GenInst (concat new_goals_s) (EvCoercion final_co) }
-
-    -- Cannot solve this one
-    | otherwise
-    = return NoInstance
-
-nominalArgsAgree :: TyCon -> [Type] -> [Type] -> Bool
-nominalArgsAgree tc tys1 tys2 = all ok $ zip3 (tyConRoles tc) tys1 tys2
-  where ok (r,t1,t2) = r /= Nominal || t1 `tcEqType` t2
-
-dataConsInScope :: GlobalRdrEnv -> TyCon -> Bool
-dataConsInScope rdr_env tc = not hidden_data_cons
-  where
-    data_con_names = map dataConName (tyConDataCons tc)
-    hidden_data_cons = not (isWiredInName (tyConName tc)) &&
-                       (isAbstractTyCon tc || any not_in_scope data_con_names)
-    not_in_scope dc  = null (lookupGRE_Name rdr_env dc)
-
-markDataConsAsUsed :: GlobalRdrEnv -> TyCon -> TcS ()
-markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
-  [ mkRdrQual (is_as (is_decl imp_spec)) occ
-  | dc <- tyConDataCons tc
-  , let dc_name = dataConName dc
-        occ  = nameOccName dc_name
-        gres = lookupGRE_Name rdr_env dc_name
-  , not (null gres)
-  , Imported (imp_spec:_) <- [gre_prov (head gres)] ]
-
-requestCoercible :: CtLoc -> TcType -> TcType
-                 -> TcS ( [CtEvidence]      -- Fresh goals to solve
-                        , TcCoercion )      -- Coercion witnessing (Coercible t1 t2)
-requestCoercible loc ty1 ty2
-  = ASSERT2( typeKind ty1 `tcEqKind` typeKind ty2, ppr ty1 <+> ppr ty2)
-    do { (new_ev, freshness) <- newWantedEvVar loc' (mkCoerciblePred ty1 ty2)
-       ; return ( case freshness of { Fresh -> [new_ev]; Cached -> [] }
-                , ctEvCoercion new_ev) }
-           -- Evidence for a Coercible constraint is always a coercion t1 ~R t2
-  where
-     loc' = bumpCtLocDepth CountConstraints loc
-
 {-
-Note [Coercible Instances]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-The class Coercible is special: There are no regular instances, and the user
-cannot even define them (it is listed as an `abstractClass` in TcValidity).
-Instead, the type checker will create instances and their evidence out of thin
-air, in getCoercibleInst. The following "instances" are present:
-
- 1. instance Coercible a a
-    for any type a at any kind k.
-
- 2. instance (forall a. Coercible t1 t2) => Coercible (forall a. t1) (forall a. t2)
-    (which would be illegal to write like that in the source code, but we have
-    it nevertheless).
-
- 3. instance Coercible r b => Coercible (NT t1 t2 ...) b
-    instance Coercible a r => Coercible a (NT t1 t2 ...)
-    for a newtype constructor NT (or data family instance that resolves to a
-    newtype) where
-     * r is the concrete type of NT, instantiated with the arguments t1 t2 ...
-     * the constructor of NT is in scope.
-
-    The newtype TyCon can appear undersaturated, but only if it has
-    enough arguments to apply the newtype coercion (which is eta-reduced). Examples:
-      newtype NT a = NT (Either a Int)
-      Coercible (NT Int) (Either Int Int) -- ok
-      newtype NT2 a b = NT2 (b -> a)
-      newtype NT3 a b = NT3 (b -> a)
-      Coercible (NT2 Int) (NT3 Int) -- cannot be derived
-
- 4. instance (Coercible t1_r t1'_r, Coercible t2_r t2_r',...) =>
-       Coercible (C t1_r  t2_r  ... t1_p  t2_p  ... t1_n t2_n ...)
-                 (C t1_r' t2_r' ... t1_p' t2_p' ... t1_n t2_n ...)
-    for a type constructor C where
-     * the nominal type arguments are not changed,
-     * the phantom type arguments may change arbitrarily
-     * the representational type arguments are again Coercible
-
-    The type constructor can be used undersaturated; then the Coercible
-    instance is at a higher kind. This does not cause problems.
-
-
-The type checker generates evidence in the form of EvCoercion, but the
-TcCoercion therein has role Representational,  which are turned into Core
-coercions by dsEvTerm in DsBinds.
-
-The evidence for the second case is created by deferTcSForAllEq, for the other
-cases by getCoercibleInst.
-
-When the constraint cannot be solved, it is treated as any other unsolved
-constraint, i.e. it can turn up in an inferred type signature, or reported to
-the user as a regular "Cannot derive instance ..." error. In the latter case,
-coercible_msg in TcErrors gives additional explanations of why GHC could not
-find a Coercible instance, so it duplicates some of the logic from
-getCoercibleInst (in negated form).
-
-Note [Order of Coercible Instances]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-At first glance, the order of the various coercible instances doesn't matter, as
-incoherence is no issue here: We do not care how the evidence is constructed,
-as long as it is.
-
-But because of role annotations, the order *can* matter:
-
-  newtype T a = MkT [a]
-  type role T nominal
-
-  type family F a
-  type instance F Int = Bool
-
-Here T's declared role is more restrictive than its inferred role
-(representational) would be.  If MkT is not in scope, so that the
-newtype-unwrapping instance is not available, then this coercible
-instance would fail:
-  Coercible (T Bool) (T (F Int)
-But MkT was in scope, *and* if we used it before decomposing on T,
-we'd unwrap the newtype (on both sides) to get
-  Coercible Bool (F Int)
-which succeeds.
-
-So our current decision is to apply case 3 (newtype-unwrapping) first,
-followed by decomposition (case 4).  This is strictly more powerful
-if the newtype constructor is in scope.  See Trac #9117 for a discussion.
-
 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