Refactor the treatment of predicate types
[ghc.git] / compiler / typecheck / TcInteract.hs
index c7ec560..3914db6 100644 (file)
@@ -3,39 +3,33 @@
 module TcInteract (
      solveSimpleGivens,   -- Solves [Ct]
      solveSimpleWanteds,  -- Solves Cts
-
-     solveCallStack,      -- for use in TcSimplify
   ) where
 
 #include "HsVersions.h"
 
-import BasicTypes ( infinity, IntWithInf, intGtLimit )
-import HsTypes ( HsIPName(..) )
+import GhcPrelude
+import BasicTypes ( SwapFlag(..), isSwapped,
+                    infinity, IntWithInf, intGtLimit )
 import TcCanonical
 import TcFlatten
+import TcUnify( canSolveByUnification )
 import VarSet
 import Type
-import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
+import InstEnv( DFunInstType )
 import CoAxiom( sfInteractTop, sfInteractInert )
 
 import Var
 import TcType
-import Name
-import PrelNames ( knownNatClassName, knownSymbolClassName,
-                   typeableClassName, coercibleTyConKey,
-                   heqTyConKey, ipClassKey )
-import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
-                    coercibleDataCon )
-import TysPrim    ( eqPrimTyCon, eqReprPrimTyCon )
-import Id( idType )
-import CoAxiom ( Eqn, CoAxiom(..), CoAxBranch(..), fromBranches )
+import PrelNames ( coercibleTyConKey,
+                   heqTyConKey, eqTyConKey, ipClassKey )
+import CoAxiom ( TypeEqn, CoAxiom(..), CoAxBranch(..), fromBranches )
 import Class
 import TyCon
-import DataCon( dataConWrapId )
 import FunDeps
 import FamInst
+import ClsInst( ClsInstResult(..), InstanceWhat(..), safeOverlap )
 import FamInstEnv
-import Unify ( tcUnifyTyWithTFs )
+import Unify ( tcUnifyTyWithTFs, ruleMatchTyKiX )
 
 import TcEvidence
 import Outputable
@@ -43,8 +37,9 @@ import Outputable
 import TcRnTypes
 import TcSMonad
 import Bag
-import MonadUtils ( concatMapM )
+import MonadUtils ( concatMapM, foldlM )
 
+import CoreSyn
 import Data.List( partition, foldl', deleteFirstsBy )
 import SrcLoc
 import VarEnv
@@ -57,6 +52,9 @@ import DynFlags
 import Util
 import qualified GHC.LanguageExtensions as LangExt
 
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.Maybe
+
 {-
 **********************************************************************
 *                                                                    *
@@ -132,16 +130,14 @@ that prepareInertsForImplications will discard the insolubles, so we
 must keep track of them separately.
 -}
 
-solveSimpleGivens :: [Ct] -> TcS Cts
+solveSimpleGivens :: [Ct] -> TcS ()
 solveSimpleGivens givens
   | null givens  -- Shortcut for common case
-  = return emptyCts
+  = return ()
   | otherwise
   = do { traceTcS "solveSimpleGivens {" (ppr givens)
        ; go givens
-       ; given_insols <- takeGivenInsolubles
-       ; traceTcS "End solveSimpleGivens }" (text "Insoluble:" <+> pprCts given_insols)
-       ; return given_insols }
+       ; traceTcS "End solveSimpleGivens }" empty }
   where
     go givens = do { solveSimples (listToBag givens)
                    ; new_givens <- runTcPluginsGiven
@@ -151,6 +147,7 @@ solveSimpleGivens givens
 solveSimpleWanteds :: Cts -> TcS WantedConstraints
 -- NB: 'simples' may contain /derived/ equalities, floated
 --     out from a nested implication. So don't discard deriveds!
+-- The result is not necessarily zonked
 solveSimpleWanteds simples
   = do { traceTcS "solveSimpleWanteds {" (ppr simples)
        ; dflags <- getDynFlags
@@ -165,7 +162,7 @@ solveSimpleWanteds simples
       | n `intGtLimit` limit
       = failTcS (hang (text "solveSimpleWanteds: too many iterations"
                        <+> parens (text "limit =" <+> ppr limit))
-                    2 (vcat [ text "Set limit with -fsolver-iterations=n; n=0 for no limit"
+                    2 (vcat [ text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
                             , text "Simples =" <+> ppr simples
                             , text "WC ="      <+> ppr wc ]))
 
@@ -182,23 +179,24 @@ solveSimpleWanteds simples
 
           ; if unif_count == 0 && not rerun_plugin
             then return (n, wc2)             -- Done
-            else do { traceTcS "solveSimple going round again:" (ppr rerun_plugin)
+            else do { traceTcS "solveSimple going round again:" $
+                      ppr unif_count $$ ppr rerun_plugin
                     ; go (n+1) limit wc2 } }      -- Loop
 
 
 solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
 -- Try solving these constraints
 -- Affects the unification state (of course) but not the inert set
-solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
+-- The result is not necessarily zonked
+solve_simple_wanteds (WC { wc_simple = simples1, wc_impl = implics1 })
   = nestTcS $
     do { solveSimples simples1
-       ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
+       ; (implics2, tv_eqs, fun_eqs, others) <- getUnsolvedInerts
        ; (unif_count, unflattened_eqs) <- reportUnifications $
-                                          unflatten tv_eqs fun_eqs
+                                          unflattenWanteds tv_eqs fun_eqs
             -- See Note [Unflatten after solving the simple wanteds]
        ; return ( unif_count
                 , WC { wc_simple = others `andCts` unflattened_eqs
-                     , wc_insol  = insols1 `andCts` insols2
                      , wc_impl   = implics1 `unionBags` implics2 }) }
 
 {- Note [The solveSimpleWanteds loop]
@@ -248,8 +246,9 @@ runTcPluginsGiven
        ; if null givens then return [] else
     do { p <- runTcPlugins plugins (givens,[],[])
        ; let (solved_givens, _, _) = pluginSolvedCts p
+             insols                = pluginBadCts p
        ; updInertCans (removeInertCts solved_givens)
-       ; mapM_ emitInsoluble (pluginBadCts p)
+       ; updInertIrreds (\irreds -> extendCtsList irreds insols)
        ; return (pluginNewCts p) } } }
 
 -- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
@@ -258,7 +257,7 @@ runTcPluginsGiven
 -- 'solveSimpleWanteds' should feed the updated wanteds back into the
 -- main solver.
 runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
-runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
+runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_impl = implics1 })
   | isEmptyBag simples1
   = return (False, wc)
   | otherwise
@@ -272,15 +271,17 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl =
        ; let (_, _,                solved_wanted)   = pluginSolvedCts p
              (_, unsolved_derived, unsolved_wanted) = pluginInputCts p
              new_wanted                             = pluginNewCts p
+             insols                                 = pluginBadCts p
 
 -- SLPJ: I'm deeply suspicious of this
 --       ; updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)
 
        ; mapM_ setEv solved_wanted
        ; return ( notNull (pluginNewCts p)
-                , WC { wc_simple = listToBag new_wanted `andCts` listToBag unsolved_wanted
-                                                        `andCts` listToBag unsolved_derived
-                     , wc_insol  = listToBag (pluginBadCts p) `andCts` insols1
+                , WC { wc_simple = listToBag new_wanted       `andCts`
+                                   listToBag unsolved_wanted  `andCts`
+                                   listToBag unsolved_derived `andCts`
+                                   listToBag insols
                      , wc_impl   = implics1 } ) } }
   where
     setEv :: (EvTerm,Ct) -> TcS ()
@@ -354,11 +355,8 @@ runTcPlugins plugins all_cts
     without = deleteFirstsBy eqCt
 
     eqCt :: Ct -> Ct -> Bool
-    eqCt c c' = case (ctEvidence c, ctEvidence c') of
-      (CtGiven   pred _ _, CtGiven   pred' _ _) -> pred `eqType` pred'
-      (CtWanted  pred _ _, CtWanted  pred' _ _) -> pred `eqType` pred'
-      (CtDerived pred _  , CtDerived pred' _  ) -> pred `eqType` pred'
-      (_                 , _                  ) -> False
+    eqCt c c' = ctFlavour c == ctFlavour c'
+             && ctPred c `tcEqType` ctPred c'
 
     add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
     add xs scs = foldl' addOne scs xs
@@ -379,25 +377,26 @@ runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
 -- Run this item down the pipeline, leaving behind new work and inerts
 runSolverPipeline pipeline workItem
   = do { wl <- getWorkList
+       ; inerts <- getTcSInerts
+       ; tclevel <- getTcLevel
+       ; traceTcS "----------------------------- " empty
        ; traceTcS "Start solver pipeline {" $
-                  vcat [ text "work item =" <+> ppr workItem
+                  vcat [ text "tclevel =" <+> ppr tclevel
+                       , text "work item =" <+> ppr workItem
+                       , text "inerts =" <+> ppr inerts
                        , text "rest of worklist =" <+> ppr wl ]
 
        ; bumpStepCountTcS    -- One step for each constraint processed
        ; final_res  <- run_pipeline pipeline (ContinueWith workItem)
 
-       ; final_is <- getTcSInerts
        ; case final_res of
            Stop ev s       -> do { traceFireTcS ev s
-                                 ; traceTcS "End solver pipeline (discharged) }"
-                                       (text "inerts =" <+> ppr final_is)
+                                 ; traceTcS "End solver pipeline (discharged) }" empty
                                  ; return () }
-           ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (text "Kept as inert")
+           ContinueWith ct -> do { addInertCan ct
+                                 ; traceFireTcS (ctEvidence ct) (text "Kept as inert")
                                  ; traceTcS "End solver pipeline (kept as inert) }" $
-                                       vcat [ text "final_item =" <+> ppr ct
-                                            , pprTvBndrs $ tyCoVarsOfCtList ct
-                                            , text "inerts     =" <+> ppr final_is]
-                                 ; addInertCan ct }
+                                            (text "final_item =" <+> ppr ct) }
        }
   where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
                      -> TcS (StopOrContinue Ct)
@@ -459,7 +458,7 @@ But this isn't quite true.  Suppose we have,
     c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
 After processing the first two, we get
      c1: [G] beta ~ [alpha], c2 : [W] blah
-Now, c3 does not interact with the the given c1, so when we spontaneously
+Now, c3 does not interact with the given c1, so when we spontaneously
 solve c3, we must re-react it with the inert set.  So we can attempt a
 reaction between inert c2 [W] and work-item c3 [G].
 
@@ -475,8 +474,6 @@ or, equivalently,
 
 -- Interaction result of  WorkItem <~> Ct
 
-type StopNowFlag = Bool    -- True <=> stop after this interaction
-
 interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
 -- Precondition: if the workitem is a CTyEqCan then it will not be able to
 -- react with anything at this stage.
@@ -485,94 +482,106 @@ interactWithInertsStage wi
   = do { inerts <- getTcSInerts
        ; let ics = inert_cans inerts
        ; case wi of
-             CTyEqCan    {} -> interactTyVarEq ics wi
-             CFunEqCan   {} -> interactFunEq   ics wi
-             CIrredEvCan {} -> interactIrred   ics wi
-             CDictCan    {} -> interactDict    ics wi
+             CTyEqCan  {} -> interactTyVarEq ics wi
+             CFunEqCan {} -> interactFunEq   ics wi
+             CIrredCan {} -> interactIrred   ics wi
+             CDictCan  {} -> interactDict    ics wi
              _ -> pprPanic "interactWithInerts" (ppr wi) }
                 -- CHoleCan are put straight into inert_frozen, so never get here
                 -- CNonCanonical have been canonicalised
 
 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
+   = KeepInert   -- Keep the inert item, and solve the work item from it
+                 -- (if the latter is Wanted; just discard it if not)
+   | KeepWork    -- Keep the work item, and solve the intert item from it
 
 instance Outputable InteractResult where
-  ppr IRKeep    = text "keep"
-  ppr IRReplace = text "replace"
-  ppr IRDelete  = text "delete"
+  ppr KeepInert = text "keep inert"
+  ppr KeepWork  = text "keep work-item"
 
 solveOneFromTheOther :: CtEvidence  -- Inert
                      -> CtEvidence  -- WorkItem
-                     -> TcS (InteractResult, StopNowFlag)
--- Preconditions:
--- 1) inert and work item represent evidence for the /same/ predicate
--- 2) ip/class/irred constraints only; not used for equalities
+                     -> TcS InteractResult
+-- Precondition:
+-- * inert and work item represent evidence for the /same/ predicate
+--
+-- We can always solve one from the other: even if both are wanted,
+-- although we don't rewrite wanteds with wanteds, we can combine
+-- two wanteds into one by solving one from the other
+
 solveOneFromTheOther ev_i ev_w
   | isDerived ev_w         -- Work item is Derived; just discard it
-  = return (IRKeep, True)
+  = return KeepInert
 
-  | isDerived ev_i            -- The inert item is Derived, we can just throw it away,
-  = return (IRDelete, False)  -- The ev_w is inert wrt earlier inert-set items,
-                              -- so it's safe to continue on from this point
+  | isDerived ev_i     -- The inert item is Derived, we can just throw it away,
+  = return KeepWork    -- The ev_w is inert wrt earlier inert-set items,
+                       -- so it's safe to continue on from this point
 
   | CtWanted { ctev_loc = loc_w } <- ev_w
   , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
-  = return (IRDelete, False)
+  = -- inert must be Given
+    do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
+       ; return KeepWork }
 
-  | CtWanted { ctev_dest = dest } <- ev_w
+  | CtWanted {} <- ev_w
        -- Inert is Given or Wanted
-  = do { setWantedEvTerm dest (ctEvTerm ev_i)
-       ; return (IRKeep, True) }
+  = return KeepInert
+
+  -- From here on the work-item is Given
 
-  | CtWanted { ctev_loc = loc_i } <- ev_i   -- Work item is Given
+  | CtWanted { ctev_loc = loc_i } <- ev_i
   , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
-  = return (IRKeep, False)  -- Just discard the un-usable Given
-                            -- This never actually happens because
-                            -- Givens get processed first
+  = do { traceTcS "prohibitedClassSolve2" (ppr ev_i $$ ppr ev_w)
+       ; return KeepInert }      -- Just discard the un-usable Given
+                                 -- This never actually happens because
+                                 -- Givens get processed first
 
-  | CtWanted { ctev_dest = dest } <- ev_i
-  = do { setWantedEvTerm dest (ctEvTerm ev_w)
-       ; return (IRReplace, True) }
+  | CtWanted {} <- ev_i
+  = return KeepWork
 
-  -- So they are both Given
+  -- From here on both are Given
   -- See Note [Replacement vs keeping]
+
   | lvl_i == lvl_w
-  = do { binds <- getTcEvBindsMap
-       ; return (same_level_strategy binds, True) }
+  = do { ev_binds_var <- getTcEvBindsVar
+       ; binds <- getTcEvBindsMap ev_binds_var
+       ; return (same_level_strategy binds) }
 
   | otherwise   -- Both are Given, levels differ
-  = return (different_level_strategy, True)
+  = return different_level_strategy
   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
+     ev_id_i = ctEvEvId ev_i
+     ev_id_w = ctEvEvId ev_w
 
-     different_level_strategy
-       | isIPPred pred, lvl_w > lvl_i = IRReplace
-       | lvl_w < lvl_i                = IRReplace
-       | otherwise                    = IRKeep
+     different_level_strategy  -- Both Given
+       | isIPPred pred, lvl_w > lvl_i = KeepWork
+       | lvl_w < lvl_i                = KeepWork
+       | otherwise                    = KeepInert
 
-     same_level_strategy binds        -- Both Given
+     same_level_strategy binds -- Both Given
        | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
        = case ctLocOrigin loc_w of
-            GivenOrigin (InstSC s_w) | s_w < s_i -> IRReplace
-                                     | otherwise -> IRKeep
-            _                                    -> IRReplace
+            GivenOrigin (InstSC s_w) | s_w < s_i -> KeepWork
+                                     | otherwise -> KeepInert
+            _                                    -> KeepWork
 
        | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
-       = IRKeep
+       = KeepInert
 
-       | has_binding binds ev_w
-       , not (has_binding binds ev_i)
-       = IRReplace
+       | has_binding binds ev_id_w
+       , not (has_binding binds ev_id_i)
+       , not (ev_id_i `elemVarSet` findNeededEvVars binds (unitVarSet ev_id_w))
+       = KeepWork
 
-       | otherwise = IRKeep
+       | otherwise
+       = KeepInert
 
-     has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
+     has_binding binds ev_id = isJust (lookupEvBind binds ev_id)
 
 {-
 Note [Replacement vs keeping]
@@ -597,25 +606,37 @@ we keep?  More subtle than you might think!
 
   * Constraints coming from the same level (i.e. same implication)
 
-       - Always get rid of InstSC ones if possible, since they are less
-         useful for solving.  If both are InstSC, choose the one with
-         the smallest TypeSize
-         See Note [Solving superclass constraints] in TcInstDcls
+       (a) Always get rid of InstSC ones if possible, since they are less
+           useful for solving.  If both are InstSC, choose the one with
+           the smallest TypeSize
+           See Note [Solving superclass constraints] in TcInstDcls
 
-       - Keep the one that has a non-trivial evidence binding.
-            Example:  f :: (Eq a, Ord a) => blah
-            then we may find [G] d3 :: Eq a
-                             [G] d2 :: Eq a
-              with bindings  d3 = sc_sel (d1::Ord a)
+       (b) Keep the one that has a non-trivial evidence binding.
+              Example:  f :: (Eq a, Ord a) => blah
+              then we may find [G] d3 :: Eq a
+                               [G] d2 :: Eq a
+                with bindings  d3 = sc_sel (d1::Ord a)
             We want to discard d2 in favour of the superclass selection from
             the Ord dictionary.
-         Why? See Note [Tracking redundant constraints] in TcSimplify again.
-
-  * Finally, when there is still a choice, use IRKeep rather than
-    IRReplace, to avoid unnecessary munging of the inert set.
+            Why? See Note [Tracking redundant constraints] in TcSimplify again.
+
+       (c) But don't do (b) if the evidence binding depends transitively on the
+           one without a binding.  Example (with RecursiveSuperClasses)
+              class C a => D a
+              class D a => C a
+           Inert:     d1 :: C a, d2 :: D a
+           Binds:     d3 = sc_sel d2, d2 = sc_sel d1
+           Work item: d3 :: C a
+           Then it'd be ridiculous to replace d1 with d3 in the inert set!
+           Hence the findNeedEvVars test.  See Trac #14774.
+
+  * Finally, when there is still a choice, use KeepInert rather than
+    KeepWork, for two reasons:
+      - to avoid unnecessary munging of the inert set.
+      - to cut off superclass loops; see Note [Superclass loops] in TcCanonical
 
 Doing the depth-check for implicit parameters, rather than making the work item
-always overrride, is important.  Consider
+always override, is important.  Consider
 
     data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }
 
@@ -639,6 +660,18 @@ that this chain of events won't happen, but that's very fragile.)
                    interactIrred
 *                                                                               *
 *********************************************************************************
+
+Note [Multiple matching irreds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+You might think that it's impossible to have multiple irreds all match the
+work item; after all, interactIrred looks for matches and solves one from the
+other. However, note that interacting insoluble, non-droppable irreds does not
+do this matching. We thus might end up with several insoluble, non-droppable,
+matching irreds in the inert set. When another irred comes along that we have
+not yet labeled insoluble, we can find multiple matches. These multiple matches
+cause no harm, but it would be wrong to ASSERT that they aren't there (as we
+once had done). This problem can be tickled by typecheck/should_compile/holes.
+
 -}
 
 -- Two pieces of irreducible evidence: if their types are *exactly identical*
@@ -647,76 +680,375 @@ that this chain of events won't happen, but that's very fragile.)
 -- mean that (ty1 ~ ty2)
 interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 
-interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
-  | let pred = ctEvPred ev_w
-        (matching_irreds, others)
-          = partitionBag (\ct -> ctPred ct `tcEqTypeNoKindCheck` pred)
-                         (inert_irreds inerts)
-  , (ct_i : rest) <- bagToList matching_irreds
-  , let ctev_i = ctEvidence ct_i
-  = ASSERT( null rest )
-    do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
-       ; case inert_effect of
-            IRKeep    -> return ()
-            IRDelete  -> updInertIrreds (\_ -> others)
-            IRReplace -> updInertIrreds (\_ -> others `snocCts` workItem)
-                         -- These const upd's assume that solveOneFromTheOther
-                         -- has no side effects on InertCans
-       ; if stop_now then
-            return (Stop ev_w (text "Irred equal" <+> parens (ppr inert_effect)))
-       ; else
-            continueWith workItem }
+interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
+  | insoluble  -- For insolubles, don't allow the constaint to be dropped
+               -- which can happen with solveOneFromTheOther, so that
+               -- we get distinct error messages with -fdefer-type-errors
+               -- See Note [Do not add duplicate derived insolubles]
+  , not (isDroppableCt workItem)
+  = continueWith workItem
+
+  | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
+  , ((ct_i, swap) : _rest) <- bagToList matching_irreds
+        -- See Note [Multiple matching irreds]
+  , let ev_i = ctEvidence ct_i
+  = do { what_next <- solveOneFromTheOther ev_i ev_w
+       ; traceTcS "iteractIrred" (ppr workItem $$ ppr what_next $$ ppr ct_i)
+       ; case what_next of
+            KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
+                            ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
+            KeepWork ->  do { setEvBindIfWanted ev_i (swap_me swap ev_w)
+                            ; updInertIrreds (\_ -> others)
+                            ; continueWith workItem } }
 
   | otherwise
   = continueWith workItem
 
+  where
+    swap_me :: SwapFlag -> CtEvidence -> EvTerm
+    swap_me swap ev
+      = case swap of
+           NotSwapped -> ctEvTerm ev
+           IsSwapped  -> evCoercion (mkTcSymCo (evTermCoercion (ctEvTerm ev)))
+
 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
 
+findMatchingIrreds :: Cts -> CtEvidence -> (Bag (Ct, SwapFlag), Bag Ct)
+findMatchingIrreds irreds ev
+  | EqPred eq_rel1 lty1 rty1 <- classifyPredType pred
+    -- See Note [Solving irreducible equalities]
+  = partitionBagWith (match_eq eq_rel1 lty1 rty1) irreds
+  | otherwise
+  = partitionBagWith match_non_eq irreds
+  where
+    pred = ctEvPred ev
+    match_non_eq ct
+      | ctPred ct `tcEqTypeNoKindCheck` pred = Left (ct, NotSwapped)
+      | otherwise                            = Right ct
+
+    match_eq eq_rel1 lty1 rty1 ct
+      | EqPred eq_rel2 lty2 rty2 <- classifyPredType (ctPred ct)
+      , eq_rel1 == eq_rel2
+      , Just swap <- match_eq_help lty1 rty1 lty2 rty2
+      = Left (ct, swap)
+      | otherwise
+      = Right ct
+
+    match_eq_help lty1 rty1 lty2 rty2
+      | lty1 `tcEqTypeNoKindCheck` lty2, rty1 `tcEqTypeNoKindCheck` rty2
+      = Just NotSwapped
+      | lty1 `tcEqTypeNoKindCheck` rty2, rty1 `tcEqTypeNoKindCheck` lty2
+      = Just IsSwapped
+      | otherwise
+      = Nothing
+
+{- Note [Solving irreducible equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (Trac #14333)
+  [G] a b ~R# c d
+  [W] c d ~R# a b
+Clearly we should be able to solve this! Even though the constraints are
+not decomposable. We solve this when looking up the work-item in the
+irreducible constraints to look for an identical one.  When doing this
+lookup, findMatchingIrreds spots the equality case, and matches either
+way around. It has to return a swap-flag so we can generate evidence
+that is the right way round too.
+
+Note [Do not add duplicate derived insolubles]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In general we *must* add an insoluble (Int ~ Bool) even if there is
+one such there already, because they may come from distinct call
+sites.  Not only do we want an error message for each, but with
+-fdefer-type-errors we must generate evidence for each.  But for
+*derived* insolubles, we only want to report each one once.  Why?
+
+(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
+    equality many times, as the original constraint is successively rewritten.
+
+(b) Ditto the successive iterations of the main solver itself, as it traverses
+    the constraint tree. See example below.
+
+Also for *given* insolubles we may get repeated errors, as we
+repeatedly traverse the constraint tree.  These are relatively rare
+anyway, so removing duplicates seems ok.  (Alternatively we could take
+the SrcLoc into account.)
+
+Note that the test does not need to be particularly efficient because
+it is only used if the program has a type error anyway.
+
+Example of (b): assume a top-level class and instance declaration:
+
+  class D a b | a -> b
+  instance D [a] [a]
+
+Assume we have started with an implication:
+
+  forall c. Eq c => { wc_simple = D [c] c [W] }
+
+which we have simplified to:
+
+  forall c. Eq c => { wc_simple = D [c] c [W]
+                                  (c ~ [c]) [D] }
+
+For some reason, e.g. because we floated an equality somewhere else,
+we might try to re-solve this implication. If we do not do a
+dropDerivedWC, then we will end up trying to solve the following
+constraints the second time:
+
+  (D [c] c) [W]
+  (c ~ [c]) [D]
+
+which will result in two Deriveds to end up in the insoluble set:
+
+  wc_simple   = D [c] c [W]
+               (c ~ [c]) [D], (c ~ [c]) [D]
+-}
+
 {-
 *********************************************************************************
 *                                                                               *
                    interactDict
 *                                                                               *
 *********************************************************************************
+
+Note [Shortcut solving]
+~~~~~~~~~~~~~~~~~~~~~~~
+When we interact a [W] constraint with a [G] constraint that solves it, there is
+a possibility that we could produce better code if instead we solved from a
+top-level instance declaration (See #12791, #5835). For example:
+
+    class M a b where m :: a -> b
+
+    type C a b = (Num a, M a b)
+
+    f :: C Int b => b -> Int -> Int
+    f _ x = x + 1
+
+The body of `f` requires a [W] `Num Int` instance. We could solve this
+constraint from the givens because we have `C Int b` and that provides us a
+solution for `Num Int`. This would let us produce core like the following
+(with -O2):
+
+    f :: forall b. C Int b => b -> Int -> Int
+    f = \ (@ b) ($d(%,%) :: C Int b) _ (eta1 :: Int) ->
+        + @ Int
+          (GHC.Classes.$p1(%,%) @ (Num Int) @ (M Int b) $d(%,%))
+          eta1
+          A.f1
+
+This is bad! We could do /much/ better if we solved [W] `Num Int` directly
+from the instance that we have in scope:
+
+    f :: forall b. C Int b => b -> Int -> Int
+    f = \ (@ b) _ _ (x :: Int) ->
+        case x of { GHC.Types.I# x1 -> GHC.Types.I# (GHC.Prim.+# x1 1#) }
+
+** NB: It is important to emphasize that all this is purely an optimization:
+** exactly the same programs should typecheck with or without this
+** procedure.
+
+Solving fully
+~~~~~~~~~~~~~
+There is a reason why the solver does not simply try to solve such
+constraints with top-level instances. If the solver finds a relevant
+instance declaration in scope, that instance may require a context
+that can't be solved for. A good example of this is:
+
+    f :: Ord [a] => ...
+    f x = ..Need Eq [a]...
+
+If we have instance `Eq a => Eq [a]` in scope and we tried to use it, we would
+be left with the obligation to solve the constraint Eq a, which we cannot. So we
+must be conservative in our attempt to use an instance declaration to solve the
+[W] constraint we're interested in.
+
+Our rule is that we try to solve all of the instance's subgoals
+recursively all at once. Precisely: We only attempt to solve
+constraints of the form `C1, ... Cm => C t1 ... t n`, where all the Ci
+are themselves class constraints of the form `C1', ... Cm' => C' t1'
+... tn'` and we only succeed if the entire tree of constraints is
+solvable from instances.
+
+An example that succeeds:
+
+    class Eq a => C a b | b -> a where
+      m :: b -> a
+
+    f :: C [Int] b => b -> Bool
+    f x = m x == []
+
+We solve for `Eq [Int]`, which requires `Eq Int`, which we also have. This
+produces the following core:
+
+    f :: forall b. C [Int] b => b -> Bool
+    f = \ (@ b) ($dC :: C [Int] b) (x :: b) ->
+        GHC.Classes.$fEq[]_$s$c==
+          (m @ [Int] @ b $dC x) (GHC.Types.[] @ Int)
+
+An example that fails:
+
+    class Eq a => C a b | b -> a where
+      m :: b -> a
+
+    f :: C [a] b => b -> Bool
+    f x = m x == []
+
+Which, because solving `Eq [a]` demands `Eq a` which we cannot solve, produces:
+
+    f :: forall a b. C [a] b => b -> Bool
+    f = \ (@ a) (@ b) ($dC :: C [a] b) (eta :: b) ->
+        ==
+          @ [a]
+          (A.$p1C @ [a] @ b $dC)
+          (m @ [a] @ b $dC eta)
+          (GHC.Types.[] @ a)
+
+Note [Shortcut solving: type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have (Trac #13943)
+  class Take (n :: Nat) where ...
+  instance {-# OVERLAPPING #-}                    Take 0 where ..
+  instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where ..
+
+And we have [W] Take 3.  That only matches one instance so we get
+[W] Take (3-1).  Really we should now flatten to reduce the (3-1) to 2, and
+so on -- but that is reproducing yet more of the solver.  Sigh.  For now,
+we just give up (remember all this is just an optimisation).
+
+But we must not just naively try to lookup (Take (3-1)) in the
+InstEnv, or it'll (wrongly) appear not to match (Take 0) and get a
+unique match on the (Take n) instance.  That leads immediately to an
+infinite loop.  Hence the check that 'preds' have no type families
+(isTyFamFree).
+
+Note [Shortcut solving: overlap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+  instance {-# OVERLAPPABLE #-} C a where ...
+and we are typechecking
+  f :: C a => a -> a
+  f = e  -- Gives rise to [W] C a
+
+We don't want to solve the wanted constraint with the overlappable
+instance; rather we want to use the supplied (C a)! That was the whole
+point of it being overlappable!  Trac #14434 wwas an example.
+
+Note [Shortcut solving: incoherence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This optimization relies on coherence of dictionaries to be correct. When we
+cannot assume coherence because of IncoherentInstances then this optimization
+can change the behavior of the user's code.
+
+The following four modules produce a program whose output would change depending
+on whether we apply this optimization when IncoherentInstances is in effect:
+
+#########
+    {-# LANGUAGE MultiParamTypeClasses #-}
+    module A where
+
+    class A a where
+      int :: a -> Int
+
+    class A a => C a b where
+      m :: b -> a -> a
+
+#########
+    {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
+    module B where
+
+    import A
+
+    instance A a where
+      int _ = 1
+
+    instance C a [b] where
+      m _ = id
+
+#########
+    {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
+    {-# LANGUAGE IncoherentInstances #-}
+    module C where
+
+    import A
+
+    instance A Int where
+      int _ = 2
+
+    instance C Int [Int] where
+      m _ = id
+
+    intC :: C Int a => a -> Int -> Int
+    intC _ x = int x
+
+#########
+    module Main where
+
+    import A
+    import B
+    import C
+
+    main :: IO ()
+    main = print (intC [] (0::Int))
+
+The output of `main` if we avoid the optimization under the effect of
+IncoherentInstances is `1`. If we were to do the optimization, the output of
+`main` would be `2`.
+
+Note [Shortcut try_solve_from_instance]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The workhorse of the short-cut solver is
+    try_solve_from_instance :: (EvBindMap, DictMap CtEvidence)
+                            -> CtEvidence       -- Solve this
+                            -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
+Note that:
+
+* The CtEvidence is teh goal to be solved
+
+* The MaybeT anages early failure if we find a subgoal that
+  cannot be solved from instances.
+
+* The (EvBindMap, DictMap CtEvidence) is an accumulating purely-functional
+  state that allows try_solve_from_instance to augmennt the evidence
+  bindings and inert_solved_dicts as it goes.
+
+  If it succeeds, we commit all these bindings and solved dicts to the
+  main TcS InertSet.  If not, we abandon it all entirely.
+
+Passing along the solved_dicts important for two reasons:
+
+* We need to be able to handle recursive super classes. The
+  solved_dicts state  ensures that we remember what we have already
+  tried to solve to avoid looping.
+
+* As Trac #15164 showed, it can be important to exploit sharing between
+  goals. E.g. To solve G we may need G1 and G2. To solve G1 we may need H;
+  and to solve G2 we may need H. If we don't spot this sharing we may
+  solve H twice; and if this pattern repeats we may get exponentially bad
+  behaviour.
 -}
 
 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
-  | isWanted ev_w
-  , Just ip_name      <- isCallStackPred (ctPred workItem)
-  , OccurrenceOf func <- ctLocOrigin (ctEvLoc ev_w)
-  -- If we're given a CallStack constraint that arose from a function
-  -- call, we need to push the current call-site onto the stack instead
-  -- of solving it directly from a given.
-  -- See Note [Overview of implicit CallStacks]
-  = do { let loc = ctEvLoc ev_w
-
-         -- First we emit a new constraint that will capture the
-         -- given CallStack.
-       ; let new_loc      = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
-                            -- We change the origin to IPOccOrigin so
-                            -- this rule does not fire again.
-                            -- See Note [Overview of implicit CallStacks]
-
-       ; mb_new <- newWantedEvVar new_loc (ctEvPred ev_w)
-       ; emitWorkNC (freshGoals [mb_new])
-
-         -- Then we solve the wanted by pushing the call-site onto the
-         -- newly emitted CallStack.
-       ; let ev_cs = EvCsPushCall func (ctLocSpan loc) (getEvTerm mb_new)
-       ; solveCallStack ev_w ev_cs
-       ; stopWith ev_w "Wanted CallStack IP" }
-
-  | Just ctev_i <- lookupInertDict inerts cls tys
-  = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
-       ; case inert_effect of
-           IRKeep    -> return ()
-           IRDelete  -> updInertDicts $ \ ds -> delDict ds cls tys
-           IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
-       ; if stop_now then
-            return (Stop ev_w (text "Dict equal" <+> parens (ppr inert_effect)))
+  | Just ev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
+  = -- There is a matching dictionary in the inert set
+    do { -- First to try to solve it /completely/ from top level instances
+         -- See Note [Shortcut solving]
+         dflags <- getDynFlags
+       ; short_cut_worked <- shortCutSolver dflags ev_w ev_i
+       ; if short_cut_worked
+         then stopWith ev_w "interactDict/solved from instance"
          else
-            continueWith workItem }
+
+    do { -- Ths short-cut solver didn't fire, so we
+         -- solve ev_w from the matching inert ev_i we found
+         what_next <- solveOneFromTheOther ev_i ev_w
+       ; traceTcS "lookupInertDict" (ppr what_next)
+       ; case what_next of
+           KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
+                           ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) }
+           KeepWork  -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w)
+                           ; updInertDicts $ \ ds -> delDict ds cls tys
+                           ; continueWith workItem } } }
 
   | cls `hasKey` ipClassKey
   , isGiven ev_w
@@ -728,28 +1060,139 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
 
 interactDict _ wi = pprPanic "interactDict" (ppr wi)
 
+-- See Note [Shortcut solving]
+shortCutSolver :: DynFlags
+               -> CtEvidence -- Work item
+               -> CtEvidence -- Inert we want to try to replace
+               -> TcS Bool   -- True <=> success
+shortCutSolver dflags ev_w ev_i
+  | isWanted ev_w
+ && isGiven ev_i
+ -- We are about to solve a [W] constraint from a [G] constraint. We take
+ -- a moment to see if we can get a better solution using an instance.
+ -- Note that we only do this for the sake of performance. Exactly the same
+ -- programs should typecheck regardless of whether we take this step or
+ -- not. See Note [Shortcut solving]
+
+ && not (xopt LangExt.IncoherentInstances dflags)
+ -- If IncoherentInstances is on then we cannot rely on coherence of proofs
+ -- in order to justify this optimization: The proof provided by the
+ -- [G] constraint's superclass may be different from the top-level proof.
+ -- See Note [Shortcut solving: incoherence]
+
+ && gopt Opt_SolveConstantDicts dflags
+ -- Enabled by the -fsolve-constant-dicts flag
+  = do { ev_binds_var <- getTcEvBindsVar
+       ; ev_binds <- ASSERT2( not (isCoEvBindsVar ev_binds_var ), ppr ev_w )
+                     getTcEvBindsMap ev_binds_var
+       ; solved_dicts <- getSolvedDicts
+
+       ; mb_stuff <- runMaybeT $ try_solve_from_instance
+                                   (ev_binds, solved_dicts) ev_w
+
+       ; case mb_stuff of
+           Nothing -> return False
+           Just (ev_binds', solved_dicts')
+              -> do { setTcEvBindsMap ev_binds_var ev_binds'
+                    ; setSolvedDicts solved_dicts'
+                    ; return True } }
+
+  | otherwise
+  = return False
+  where
+    -- This `CtLoc` is used only to check the well-staged condition of any
+    -- candidate DFun. Our subgoals all have the same stage as our root
+    -- [W] constraint so it is safe to use this while solving them.
+    loc_w = ctEvLoc ev_w
+
+    try_solve_from_instance   -- See Note [Shortcut try_solve_from_instance]
+      :: (EvBindMap, DictMap CtEvidence) -> CtEvidence
+      -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
+    try_solve_from_instance (ev_binds, solved_dicts) ev
+      | let pred = ctEvPred ev
+            loc  = ctEvLoc  ev
+      , ClassPred cls tys <- classifyPredType pred
+      = do { inst_res <- lift $ matchGlobalInst dflags True cls tys
+           ; case inst_res of
+               OneInst { cir_new_theta = preds
+                       , cir_mk_ev     = mk_ev
+                       , cir_what      = what }
+                 | safeOverlap what
+                 , all isTyFamFree preds  -- Note [Shortcut solving: type families]
+                 -> do { let solved_dicts' = addDict solved_dicts cls tys ev
+                             -- solved_dicts': it is important that we add our goal
+                             -- to the cache before we solve! Otherwise we may end
+                             -- up in a loop while solving recursive dictionaries.
+
+                       ; lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
+                       ; loc' <- lift $ checkInstanceOK loc what pred
+
+                       ; evc_vs <- mapM (new_wanted_cached loc' solved_dicts') preds
+                                  -- Emit work for subgoals but use our local cache
+                                  -- so we can solve recursive dictionaries.
+
+                       ; let ev_tm     = mk_ev (map getEvExpr evc_vs)
+                             ev_binds' = extendEvBinds ev_binds $
+                                         mkWantedEvBind (ctEvEvId ev) ev_tm
+
+                       ; foldlM try_solve_from_instance
+                                (ev_binds', solved_dicts')
+                                (freshGoals evc_vs) }
+
+               _ -> mzero }
+      | otherwise = mzero
+
+
+    -- Use a local cache of solved dicts while emitting EvVars for new work
+    -- We bail out of the entire computation if we need to emit an EvVar for
+    -- a subgoal that isn't a ClassPred.
+    new_wanted_cached :: CtLoc -> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
+    new_wanted_cached loc cache pty
+      | ClassPred cls tys <- classifyPredType pty
+      = lift $ case findDict cache loc_w cls tys of
+          Just ctev -> return $ Cached (ctEvExpr ctev)
+          Nothing   -> Fresh <$> newWantedNC loc pty
+      | otherwise = mzero
+
 addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
 -- Add derived constraints from type-class functional dependencies.
 addFunDepWork inerts work_ev cls
+  | isImprovable work_ev
   = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
                -- No need to check flavour; fundeps work between
                -- any pair of constraints, regardless of flavour
                -- Importantly we don't throw workitem back in the
                -- worklist because this can cause loops (see #5236)
+  | otherwise
+  = return ()
   where
     work_pred = ctEvPred work_ev
     work_loc  = ctEvLoc work_ev
+
     add_fds inert_ct
-      = emitFunDepDeriveds $
+      | isImprovable inert_ev
+      = do { traceTcS "addFunDepWork" (vcat
+                [ ppr work_ev
+                , pprCtLoc work_loc, ppr (isGivenLoc work_loc)
+                , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc)
+                , pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ]) ;
+
+        emitFunDepDeriveds $
         improveFromAnother derived_loc inert_pred work_pred
                -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
                -- NB: We do create FDs for given to report insoluble equations that arise
                -- from pairs of Givens, and also because of floating when we approximate
                -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
+        }
+      | otherwise
+      = return ()
       where
-        inert_pred = ctPred inert_ct
-        inert_loc  = ctLoc inert_ct
-        derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred  work_loc
+        inert_ev   = ctEvidence inert_ct
+        inert_pred = ctEvPred inert_ev
+        inert_loc  = ctEvLoc inert_ev
+        derived_loc = work_loc { ctl_depth  = ctl_depth work_loc `maxSubGoalDepth`
+                                              ctl_depth inert_loc
+                               , ctl_origin = FunDepOrigin1 work_pred  work_loc
                                                             inert_pred inert_loc }
 
 {-
@@ -780,10 +1223,8 @@ interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
 
 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
 
-
-{-
-Note [Shadowing of Implicit Parameters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Shadowing of Implicit Parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider the following example:
 
 f :: (?x :: Char) => Char
@@ -806,9 +1247,19 @@ signature, and we implement this as follows: when we add a new
 *given* implicit parameter to the inert set, it replaces any existing
 givens for the same implicit parameter.
 
-This works for the normal cases but it has an odd side effect
-in some pathological programs like this:
+Similarly, consider
+   f :: (?x::a) => Bool -> a
 
+   g v = let ?x::Int = 3
+         in (f v, let ?x::Bool = True in f v)
+
+This should probably be well typed, with
+   g :: Bool -> (Int, Bool)
+
+So the inner binding for ?x::Bool *overrides* the outer one.
+
+All this works for the normal cases but it has an odd side effect in
+some pathological programs like this:
 -- This is accepted, the second parameter shadows
 f1 :: (?x :: Int, ?x :: Char) => Char
 f1 = ?x
@@ -818,12 +1269,12 @@ f2 :: (?x :: Int, ?x :: Char) => Int
 f2 = ?x
 
 Both of these are actually wrong:  when we try to use either one,
-we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
+we'll get two incompatible wanted constraints (?x :: Int, ?x :: Char),
 which would lead to an error.
 
 I can think of two ways to fix this:
 
-  1. Simply disallow multiple constratits for the same implicit
+  1. Simply disallow multiple constraints for the same implicit
     parameter---this is never useful, and it can be detected completely
     syntactically.
 
@@ -841,129 +1292,137 @@ I can think of two ways to fix this:
 
 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 -- Try interacting the work item with the inert set
-interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
-                                         , cc_tyargs = args, cc_fsk = fsk })
-  | Just (CFunEqCan { cc_ev = ev_i
-                    , cc_fsk = fsk_i }) <- matching_inerts
-  = if ev_i `funEqCanDischarge` ev
-    then  -- Rewrite work-item using inert
-      do { traceTcS "reactFunEq (discharge work item):" $
-           vcat [ text "workItem =" <+> ppr workItem
-                , text "inertItem=" <+> ppr ev_i ]
-         ; reactFunEq ev_i fsk_i ev fsk
-         ; stopWith ev "Inert rewrites work item" }
-    else  -- Rewrite inert using work-item
-      ASSERT2( ev `funEqCanDischarge` ev_i, ppr ev $$ ppr ev_i )
-      do { traceTcS "reactFunEq (rewrite inert item):" $
-           vcat [ text "workItem =" <+> ppr workItem
-                , text "inertItem=" <+> ppr ev_i ]
-         ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
-               -- Do the updInertFunEqs before the reactFunEq, so that
-               -- we don't kick out the inertItem as well as consuming it!
-         ; reactFunEq ev fsk ev_i fsk_i
-         ; stopWith ev "Work item rewrites inert" }
+interactFunEq inerts work_item@(CFunEqCan { cc_ev = ev, cc_fun = tc
+                                          , cc_tyargs = args, cc_fsk = fsk })
+  | Just inert_ct@(CFunEqCan { cc_ev = ev_i
+                             , cc_fsk = fsk_i })
+         <- findFunEq (inert_funeqs inerts) tc args
+  , pr@(swap_flag, upgrade_flag) <- ev_i `funEqCanDischarge` ev
+  = do { traceTcS "reactFunEq (rewrite inert item):" $
+         vcat [ text "work_item =" <+> ppr work_item
+              , text "inertItem=" <+> ppr ev_i
+              , text "(swap_flag, upgrade)" <+> ppr pr ]
+       ; if isSwapped swap_flag
+         then do {   -- Rewrite inert using work-item
+                   let work_item' | upgrade_flag = upgradeWanted work_item
+                                  | otherwise    = work_item
+                 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args work_item'
+                      -- Do the updInertFunEqs before the reactFunEq, so that
+                      -- we don't kick out the inertItem as well as consuming it!
+                 ; reactFunEq ev fsk ev_i fsk_i
+                 ; stopWith ev "Work item rewrites inert" }
+         else do {   -- Rewrite work-item using inert
+                 ; when upgrade_flag $
+                   updInertFunEqs $ \ feqs -> insertFunEq feqs tc args
+                                                 (upgradeWanted inert_ct)
+                 ; reactFunEq ev_i fsk_i ev fsk
+                 ; stopWith ev "Inert rewrites work item" } }
 
   | otherwise   -- Try improvement
-  = do { improveLocalFunEqs loc inerts tc args fsk
-       ; continueWith workItem }
-  where
-    loc             = ctEvLoc ev
-    funeqs          = inert_funeqs inerts
-    matching_inerts = findFunEq funeqs tc args
+  = do { improveLocalFunEqs ev inerts tc args fsk
+       ; continueWith work_item }
+
+interactFunEq _ work_item = pprPanic "interactFunEq" (ppr work_item)
 
-interactFunEq _ workItem = pprPanic "interactFunEq" (ppr workItem)
+upgradeWanted :: Ct -> Ct
+-- We are combining a [W] F tys ~ fmv1 and [D] F tys ~ fmv2
+-- so upgrade the [W] to [WD] before putting it in the inert set
+upgradeWanted ct = ct { cc_ev = upgrade_ev (cc_ev ct) }
+  where
+    upgrade_ev ev = ASSERT2( isWanted ev, ppr ct )
+                    ev { ctev_nosh = WDeriv }
 
-improveLocalFunEqs :: CtLoc -> InertCans -> TyCon -> [TcType] -> TcTyVar
+improveLocalFunEqs :: CtEvidence -> InertCans -> TyCon -> [TcType] -> TcTyVar
                    -> TcS ()
 -- Generate derived improvement equalities, by comparing
 -- the current work item with inert CFunEqs
 -- E.g.   x + y ~ z,   x + y' ~ z   =>   [D] y ~ y'
-improveLocalFunEqs loc inerts fam_tc args fsk
+--
+-- See Note [FunDep and implicit parameter reactions]
+improveLocalFunEqs work_ev inerts fam_tc args fsk
+  | isGiven work_ev -- See Note [No FunEq improvement for Givens]
+    || not (isImprovable work_ev)
+  = return ()
+
   | not (null improvement_eqns)
   = do { traceTcS "interactFunEq improvements: " $
          vcat [ text "Eqns:" <+> ppr improvement_eqns
               , text "Candidates:" <+> ppr funeqs_for_tc
-              , text "Model:" <+> ppr model ]
-       ; mapM_ (unifyDerived loc Nominal) improvement_eqns }
+              , text "Inert eqs:" <+> ppr ieqs ]
+       ; emitFunDepDeriveds improvement_eqns }
+
   | otherwise
   = return ()
+
   where
-    model         = inert_model inerts
+    ieqs          = inert_eqs inerts
     funeqs        = inert_funeqs inerts
     funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
-    rhs           = lookupFlattenTyVar model fsk
+    rhs           = lookupFlattenTyVar ieqs fsk
+    work_loc      = ctEvLoc work_ev
+    work_pred     = ctEvPred work_ev
+    fam_inj_info  = tyConInjectivityInfo fam_tc
 
     --------------------
+    improvement_eqns :: [FunDepEqn CtLoc]
     improvement_eqns
       | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
       =    -- Try built-in families, notably for arithmethic
          concatMap (do_one_built_in ops) funeqs_for_tc
 
-      | Injective injective_args <- familyTyConInjectivityInfo fam_tc
+      | Injective injective_args <- fam_inj_info
       =    -- Try improvement from type families with injectivity annotations
-         concatMap (do_one_injective injective_args) funeqs_for_tc
+        concatMap (do_one_injective injective_args) funeqs_for_tc
 
       | otherwise
       = []
 
     --------------------
-    do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
-      = sfInteractInert ops args rhs iargs (lookupFlattenTyVar model ifsk)
+    do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = inert_ev })
+      = mk_fd_eqns inert_ev (sfInteractInert ops args rhs iargs
+                                             (lookupFlattenTyVar ieqs ifsk))
+
     do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
 
     --------------------
     -- See Note [Type inference for type families with injectivity]
-    do_one_injective injective_args
-                    (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
-      | rhs `tcEqType` lookupFlattenTyVar model ifsk
-      = [Pair arg iarg | (arg, iarg, True)
-                           <- zip3 args iargs injective_args ]
+    do_one_injective inj_args (CFunEqCan { cc_tyargs = inert_args
+                                         , cc_fsk = ifsk, cc_ev = inert_ev })
+      | isImprovable inert_ev
+      , rhs `tcEqType` lookupFlattenTyVar ieqs ifsk
+      = mk_fd_eqns inert_ev $
+            [ Pair arg iarg
+            | (arg, iarg, True) <- zip3 args inert_args inj_args ]
       | otherwise
       = []
+
     do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
 
--------------
-lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType
--- See Note [lookupFlattenTyVar]
-lookupFlattenTyVar model ftv
-  = case lookupVarEnv model ftv of
-      Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs
-      _                                                   -> mkTyVarTy ftv
+    --------------------
+    mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn CtLoc]
+    mk_fd_eqns inert_ev eqns
+      | null eqns  = []
+      | otherwise  = [ FDEqn { fd_qtvs = [], fd_eqs = eqns
+                             , fd_pred1 = work_pred
+                             , fd_pred2 = ctEvPred inert_ev
+                             , fd_loc   = loc } ]
+      where
+        inert_loc = ctEvLoc inert_ev
+        loc = inert_loc { ctl_depth = ctl_depth inert_loc `maxSubGoalDepth`
+                                      ctl_depth work_loc }
 
+-------------
 reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F args1 ~ fsk1
            -> CtEvidence -> TcTyVar    -- Solve this :: F args2 ~ fsk2
            -> TcS ()
 reactFunEq from_this fsk1 solve_this fsk2
-  | CtGiven { ctev_evar = evar, ctev_loc = loc } <- solve_this
-  = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar) `mkTcTransCo`
-                         ctEvCoercion from_this
-                         -- :: fsk2 ~ fsk1
-             fsk_eq_pred = mkTcEqPredLikeEv solve_this
-                             (mkTyVarTy fsk2) (mkTyVarTy fsk1)
-
-       ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
-       ; emitWorkNC [new_ev] }
-
-  | otherwise
-  = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fsk1 $$
-                                ppr solve_this $$ ppr fsk2)
-       ; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
+  = do { traceTcS "reactFunEq"
+            (vcat [ppr from_this, ppr fsk1, ppr solve_this, ppr fsk2])
+       ; dischargeFunEq solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
        ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
                                      ppr solve_this $$ ppr fsk2) }
 
-{- Note [lookupFlattenTyVar]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Supppose we have an injective function F and
-  inert_funeqs:   F t1 ~ fsk1
-                  F t2 ~ fsk2
-  model           fsk1 ~ fsk2
-
-We never rewrite the RHS (cc_fsk) of a CFunEqCan.  But we /do/ want to
-get the [D] t1 ~ t2 from the injectiveness of F.  So we look up the
-cc_fsk of CFunEqCans in the model when trying to find derived
-equalities arising from injectivity.
-
-Note [Type inference for type families with injectivity]
+{- Note [Type inference for type families with injectivity]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have a type family with an injectivity annotation:
     type family F a b = r | r -> b
@@ -1012,9 +1471,9 @@ Initial inert set:
 Work item:
   [W] g2 : F a ~ beta2
 The work item will react with the inert yielding the _same_ inert set plus:
-    i)   Will set g2 := g1 `cast` g3
-    ii)  Will add to our solved cache that [S] g2 : F a ~ beta2
-    iii) Will emit [W] g3 : beta1 ~ beta2
+    (i)   Will set g2 := g1 `cast` g3
+    (ii)  Will add to our solved cache that [S] g2 : F a ~ beta2
+    (iii) Will emit [W] g3 : beta1 ~ beta2
 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
 will set
@@ -1090,90 +1549,82 @@ 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
-                                          , cc_eq_rel = eq_rel })
-  | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
+inertsCanDischarge :: InertCans -> TcTyVar -> TcType -> CtFlavourRole
+                   -> Maybe ( CtEvidence  -- The evidence for the inert
+                            , SwapFlag    -- Whether we need mkSymCo
+                            , Bool)       -- True <=> keep a [D] version
+                                          --          of the [WD] constraint
+inertsCanDischarge inerts tv rhs fr
+  | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i
+                                    , cc_eq_rel = eq_rel }
                              <- findTyEqs inerts tv
-                         , ev_i `eqCanDischarge` ev
+                         , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
                          , rhs_i `tcEqType` rhs ]
   =  -- Inert:     a ~ ty
      -- Work item: a ~ ty
-    do { setEvBindIfWanted ev $
-          EvCoercion (tcDowngradeRole (eqRelRole eq_rel)
-                                      (ctEvRole ev_i)
-                                      (ctEvCoercion ev_i))
-
-       ; stopWith ev "Solved from inert" }
+    Just (ev_i, NotSwapped, keep_deriv ev_i)
 
   | Just tv_rhs <- getTyVar_maybe rhs
-  , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
+  , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i
+                                    , cc_eq_rel = eq_rel }
                              <- findTyEqs inerts tv_rhs
-                         , ev_i `eqCanDischarge` ev
+                         , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
                          , rhs_i `tcEqType` mkTyVarTy tv ]
   =  -- Inert:     a ~ b
      -- Work item: b ~ a
-    do { setEvBindIfWanted ev $
-           EvCoercion (mkTcSymCo $
-                       tcDowngradeRole (eqRelRole eq_rel)
-                                       (ctEvRole ev_i)
-                                       (ctEvCoercion ev_i))
+     Just (ev_i, IsSwapped, keep_deriv ev_i)
+
+  | otherwise
+  = Nothing
+
+  where
+    keep_deriv ev_i
+      | Wanted WOnly  <- ctEvFlavour ev_i  -- inert is [W]
+      , (Wanted WDeriv, _) <- fr           -- work item is [WD]
+      = True   -- Keep a derived verison of the work item
+      | otherwise
+      = False  -- Work item is fully discharged
+
+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
+                                          , cc_eq_rel = eq_rel })
+  | Just (ev_i, swapped, keep_deriv)
+       <- inertsCanDischarge inerts tv rhs (ctEvFlavour ev, eq_rel)
+  = do { setEvBindIfWanted ev $
+         evCoercion (maybeSym swapped $
+                     tcDowngradeRole (eqRelRole eq_rel)
+                                     (ctEvRole ev_i)
+                                     (ctEvCoercion ev_i))
+
+       ; let deriv_ev = CtDerived { ctev_pred = ctEvPred ev
+                                  , ctev_loc  = ctEvLoc  ev }
+       ; when keep_deriv $
+         emitWork [workItem { cc_ev = deriv_ev }]
+         -- As a Derived it might not be fully rewritten,
+         -- so we emit it as new work
 
-       ; stopWith ev "Solved from inert (r)" }
+       ; stopWith ev "Solved from inert" }
+
+  | ReprEq <- eq_rel   -- See Note [Do not unify representational equalities]
+  = do { traceTcS "Not unifying representational equality" (ppr workItem)
+       ; continueWith workItem }
+
+  | isGiven ev         -- See Note [Touchables and givens]
+  = continueWith workItem
 
   | otherwise
   = do { tclvl <- getTcLevel
-       ; if canSolveByUnification tclvl ev eq_rel tv rhs
+       ; if canSolveByUnification tclvl tv rhs
          then do { solveByUnification ev tv rhs
                  ; n_kicked <- kickOutAfterUnification tv
-                 ; return (Stop ev (text "Solved by unification" <+> ppr_kicked n_kicked)) }
-
-         else do { traceTcS "Can't solve tyvar equality"
-                       (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
-                             , ppWhen (isMetaTyVar tv) $
-                               nest 4 (text "TcLevel of" <+> ppr tv
-                                       <+> text "is" <+> ppr (metaTyVarTcLevel tv))
-                             , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
-                             , text "TcLevel =" <+> ppr tclvl ])
-                 ; addInertEq workItem
-                 ; return (Stop ev (text "Kept as inert")) } }
+                 ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }
 
-interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
+         else continueWith workItem }
 
--- @trySpontaneousSolve wi@ solves equalities where one side is a
--- touchable unification variable.
--- Returns True <=> spontaneous solve happened
-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
-
-  | isTouchableMetaTyVar tclvl tv
-  = case metaTyVarInfo tv of
-      SigTv -> is_tyvar xi
-      _     -> True
-
-  | otherwise    -- Untouchable
-  = False
-  where
-    is_tyvar xi
-      = case tcGetTyVar_maybe xi of
-          Nothing -> False
-          Just tv -> case tcTyVarDetails tv of
-                       MetaTv { mtv_info = info }
-                                   -> case info of
-                                        SigTv -> True
-                                        _     -> False
-                       SkolemTv {} -> True
-                       FlatSkol {} -> False
-                       RuntimeUnk  -> True
+interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
 
 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
 -- Solve with the identity coercion
@@ -1199,11 +1650,7 @@ solveByUnification wd tv xi
                              text "Right Kind is:" <+> ppr (typeKind xi) ]
 
        ; unifyTyVar tv xi
-       ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi)) }
-
-ppr_kicked :: Int -> SDoc
-ppr_kicked 0 = empty
-ppr_kicked n = parens (int n <+> text "kicked out")
+       ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) }
 
 {- Note [Avoid double unifications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1223,6 +1670,22 @@ See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
 double unifications is the main reason we disallow touchable
 unification variables as RHS of type family equations: F xis ~ alpha.
 
+Note [Do not unify representational equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider   [W] alpha ~R# b
+where alpha is touchable. Should we unify alpha := b?
+
+Certainly not!  Unifying forces alpha and be to be the same; but they
+only need to be representationally equal types.
+
+For example, we might have another constraint [W] alpha ~# N b
+where
+  newtype N b = MkN b
+and we want to get alpha := N b.
+
+See also Trac #15144, which was caused by unifying a representational
+equality (in the unflattener).
+
 
 ************************************************************************
 *                                                                      *
@@ -1245,17 +1708,88 @@ constraint right away.  This avoids two dangers
 
 To achieve this required some refactoring of FunDeps.hs (nicer
 now!).
+
+Note [FunDep and implicit parameter reactions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Currently, our story of interacting two dictionaries (or a dictionary
+and top-level instances) for functional dependencies, and implicit
+parameters, is that we simply produce new Derived equalities.  So for example
+
+        class D a b | a -> b where ...
+    Inert:
+        d1 :g D Int Bool
+    WorkItem:
+        d2 :w D Int alpha
+
+    We generate the extra work item
+        cv :d alpha ~ Bool
+    where 'cv' is currently unused.  However, this new item can perhaps be
+    spontaneously solved to become given and react with d2,
+    discharging it in favour of a new constraint d2' thus:
+        d2' :w D Int Bool
+        d2 := d2' |> D Int cv
+    Now d2' can be discharged from d1
+
+We could be more aggressive and try to *immediately* solve the dictionary
+using those extra equalities, but that requires those equalities to carry
+evidence and derived do not carry evidence.
+
+If that were the case with the same inert set and work item we might dischard
+d2 directly:
+
+        cv :w alpha ~ Bool
+        d2 := d1 |> D Int cv
+
+But in general it's a bit painful to figure out the necessary coercion,
+so we just take the first approach. Here is a better example. Consider:
+    class C a b c | a -> b
+And:
+     [Given]  d1 : C T Int Char
+     [Wanted] d2 : C T beta Int
+In this case, it's *not even possible* to solve the wanted immediately.
+So we should simply output the functional dependency and add this guy
+[but NOT its superclasses] back in the worklist. Even worse:
+     [Given] d1 : C T Int beta
+     [Wanted] d2: C T beta Int
+Then it is solvable, but its very hard to detect this on the spot.
+
+It's exactly the same with implicit parameters, except that the
+"aggressive" approach would be much easier to implement.
+
+Note [Weird fundeps]
+~~~~~~~~~~~~~~~~~~~~
+Consider   class Het a b | a -> b where
+              het :: m (f c) -> a -> m b
+
+           class GHet (a :: * -> *) (b :: * -> *) | a -> b
+           instance            GHet (K a) (K [a])
+           instance Het a b => GHet (K a) (K b)
+
+The two instances don't actually conflict on their fundeps,
+although it's pretty strange.  So they are both accepted. Now
+try   [W] GHet (K Int) (K Bool)
+This triggers fundeps from both instance decls;
+      [D] K Bool ~ K [a]
+      [D] K Bool ~ K beta
+And there's a risk of complaining about Bool ~ [a].  But in fact
+the Wanted matches the second instance, so we never get as far
+as the fundeps.
+
+Trac #7875 is a case in point.
 -}
 
 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
+-- See Note [FunDep and implicit parameter reactions]
 emitFunDepDeriveds fd_eqns
   = mapM_ do_one_FDEqn fd_eqns
   where
     do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
      | null tvs  -- Common shortcut
-     = mapM_ (unifyDerived loc Nominal) eqs
+     = do { traceTcS "emitFunDepDeriveds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc))
+          ; mapM_ (unifyDerived loc Nominal) eqs }
      | otherwise
-     = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
+     = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs)
+          ; subst <- instFlexi tvs  -- Takes account of kind substitution
           ; mapM_ (do_one_eq loc subst) eqs }
 
     do_one_eq loc subst (Pair ty1 ty2)
@@ -1271,314 +1805,242 @@ emitFunDepDeriveds fd_eqns
 -}
 
 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
-topReactionsStage wi
- = do { tir <- doTopReact wi
-      ; case tir of
-          ContinueWith wi -> continueWith wi
-          Stop ev s       -> return (Stop ev (text "Top react:" <+> s)) }
-
-doTopReact :: WorkItem -> TcS (StopOrContinue Ct)
--- The work item does not react with the inert set, so try interaction with top-level
--- instances. Note:
---
---   (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].
-
-doTopReact work_item
+-- The work item does not react with the inert set,
+-- so try interaction with top-level instances. Note:
+topReactionsStage work_item
   = do { traceTcS "doTopReact" (ppr work_item)
        ; case work_item of
            CDictCan {}  -> do { inerts <- getTcSInerts
                               ; doTopReactDict inerts work_item }
            CFunEqCan {} -> doTopReactFunEq work_item
+           CIrredCan {} -> doTopReactOther work_item
+           CTyEqCan {}  -> doTopReactOther work_item
            _  -> -- Any other work item does not react with any top-level equations
                  continueWith work_item  }
 
---------------------
-doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
--- Try to use type-class instance declarations to simplify the constraint
-doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
-                                          , cc_tyargs = xis })
-  | isGiven fl   -- Never use instances for Given constraints
-  = do { try_fundep_improvement
-       ; continueWith work_item }
-
-  | Just ev <- lookupSolvedDict inerts cls xis   -- Cached
-  = do { setEvBindIfWanted fl (ctEvTerm ev)
-       ; stopWith fl "Dict/Top (cached)" }
-
-  | isDerived fl  -- Use type-class instances for Deriveds, in the hope
-                  -- of generating some improvements
-                  -- C.f. Example 3 of Note [The improvement story]
-                  -- It's easy because no evidence is involved
-   = do { dflags <- getDynFlags
-        ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
-        ; case lkup_inst_res of
-               GenInst { lir_new_theta = preds
-                       , lir_safe_over = s } ->
-                 do { emitNewDeriveds dict_loc preds
-                    ; unless s $ insertSafeOverlapFailureTcS work_item
-                    ; stopWith fl "Dict/Top (solved)" }
-
-               NoInstance ->
-                 do { -- If there is no instance, try improvement
-                      try_fundep_improvement
-                    ; continueWith work_item } }
-
-  | otherwise  -- Wanted, but not cached
-   = do { dflags <- getDynFlags
-        ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
-        ; case lkup_inst_res of
-               GenInst { lir_new_theta = theta
-                       , lir_mk_ev     = mk_ev
-                       , lir_safe_over = s } ->
-                 do { addSolvedDict fl cls xis
-                    ; unless s $ insertSafeOverlapFailureTcS work_item
-                    ; solve_from_instance theta mk_ev }
-               NoInstance ->
-                 do { try_fundep_improvement
-                    ; continueWith work_item } }
-   where
-     dict_pred   = mkClassPred cls xis
-     dict_loc    = ctEvLoc fl
-     dict_origin = ctLocOrigin dict_loc
-     deeper_loc  = zap_origin (bumpCtLocDepth dict_loc)
-
-     zap_origin loc  -- After applying an instance we can set ScOrigin to
-                     -- infinity, so that prohibitedSuperClassSolve never fires
-       | ScOrigin {} <- dict_origin
-       = setCtLocOrigin loc (ScOrigin infinity)
-       | otherwise
-       = loc
-
-     solve_from_instance :: [TcPredType]
-                         -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct)
-      -- Precondition: evidence term matches the predicate workItem
-     solve_from_instance theta mk_ev
-        | null theta
-        = do { traceTcS "doTopReact/found nullary instance for" $ ppr fl
-             ; setWantedEvBind (ctEvId fl) (mk_ev [])
-             ; stopWith fl "Dict/Top (solved, no new work)" }
-        | otherwise
-        = do { checkReductionDepth deeper_loc dict_pred
-             ; traceTcS "doTopReact/found non-nullary instance for" $ ppr fl
-             ; evc_vars <- mapM (newWanted deeper_loc) theta
-             ; setWantedEvBind (ctEvId fl) (mk_ev (map getEvTerm evc_vars))
-             ; emitWorkNC (freshGoals evc_vars)
-             ; stopWith fl "Dict/Top (solved, more work)" }
-
-     -- We didn't solve it; so try functional dependencies with
-     -- the instance environment, and return
-     -- See also Note [Weird fundeps]
-     try_fundep_improvement
-        = do { traceTcS "try_fundeps" (ppr work_item)
-             ; instEnvs <- getInstEnvs
-             ; emitFunDepDeriveds $
-               improveFromInstEnv instEnvs mk_ct_loc dict_pred }
 
-     mk_ct_loc :: PredType   -- From instance decl
-               -> SrcSpan    -- also from instance deol
-               -> CtLoc
-     mk_ct_loc inst_pred inst_loc
-       = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
-                                               inst_pred inst_loc }
+--------------------
+doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
+-- Try local quantified constraints for
+--     CTyEqCan  e.g.  (a ~# ty)
+-- and CIrredCan e.g.  (c a)
+--
+-- Why equalities? See TcCanonical
+-- Note [Equality superclasses in quantified constraints]
+doTopReactOther work_item
+  | isGiven ev
+  = continueWith work_item
+
+  | EqPred eq_rel t1 t2 <- classifyPredType pred
+  = -- See Note [Looking up primitive equalities in quantified constraints]
+    case boxEqPred eq_rel t1 t2 of
+      Nothing -> continueWith work_item
+      Just (cls, tys)
+        -> do { res <- matchLocalInst (mkClassPred cls tys) loc
+              ; case res of
+                  OneInst { cir_mk_ev = mk_ev }
+                    -> chooseInstance work_item
+                           (res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
+                    where
+                  _ -> continueWith work_item }
 
-doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
+  | otherwise
+  = do { res <- matchLocalInst pred loc
+       ; case res of
+           OneInst {} -> chooseInstance work_item res
+           _          -> continueWith work_item }
+  where
+    ev = ctEvidence work_item
+    loc  = ctEvLoc ev
+    pred = ctEvPred ev
+
+    mk_eq_ev cls tys mk_ev evs
+      = case (mk_ev evs) of
+          EvExpr e -> EvExpr (Var sc_id `mkTyApps` tys `App` e)
+          ev       -> pprPanic "mk_eq_ev" (ppr ev)
+      where
+        [sc_id] = classSCSelIds cls
+
+{- Note [Looking up primitive equalities in quantified constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For equalities (a ~# b) look up (a ~ b), and then do a superclass
+selection. This avoids having to support quantified constraints whose
+kind is not Constraint, such as (forall a. F a ~# b)
+
+See
+ * Note [Evidence for quantified constraints] in Type
+ * Note [Equality superclasses in quantified constraints]
+   in TcCanonical
+-}
 
 --------------------
 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
                                      , cc_tyargs = args, cc_fsk = fsk })
+
+  | fsk `elemVarSet` tyCoVarsOfTypes args
+  = no_reduction    -- See Note [FunEq occurs-check principle]
+
+  | otherwise  -- Note [Reduction for Derived CFunEqCans]
   = do { match_res <- matchFam fam_tc args
                            -- Look up in top-level instances, or built-in axiom
                            -- See Note [MATCHING-SYNONYMS]
        ; case match_res of
-           Nothing -> do { improveTopFunEqs (ctEvLoc old_ev) fam_tc args fsk
-                         ; continueWith work_item }
-           Just (ax_co, rhs_ty)
-             -> reduce_top_fun_eq old_ev fsk ax_co rhs_ty }
+           Nothing         -> no_reduction
+           Just match_info -> reduce_top_fun_eq old_ev fsk match_info }
+  where
+    no_reduction
+      = do { improveTopFunEqs old_ev fam_tc args fsk
+           ; continueWith work_item }
 
 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
 
-reduce_top_fun_eq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType
+reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
                   -> TcS (StopOrContinue Ct)
--- Found an applicable top-level axiom: use it to reduce
-reduce_top_fun_eq old_ev fsk ax_co rhs_ty
-  | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
+-- We have found an applicable top-level axiom: use it to reduce
+-- Precondition: fsk is not free in rhs_ty
+reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
+  | not (isDerived old_ev)  -- Precondition of shortCutReduction
+  , Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
   , isTypeFamilyTyCon tc
   , tc_args `lengthIs` tyConArity tc    -- Short-cut
-  = shortCutReduction old_ev fsk ax_co tc tc_args
-       -- Try shortcut; see Note [Short cut for top-level reaction]
-
-  | isGiven old_ev  -- Not shortcut
-  = do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
-              -- final_co :: fsk ~ rhs_ty
-       ; new_ev <- newGivenEvVar deeper_loc (mkPrimEqPred (mkTyVarTy fsk) rhs_ty,
-                                             EvCoercion final_co)
-       ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
-       ; stopWith old_ev "Fun/Top (given)" }
-
-  -- So old_ev is Wanted or Derived
-  | not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
-  = do { dischargeFmv old_ev fsk ax_co rhs_ty
+  = -- RHS is another type-family application
+    -- Try shortcut; see Note [Top-level reductions for type functions]
+    do { shortCutReduction old_ev fsk ax_co tc tc_args
+       ; stopWith old_ev "Fun/Top (shortcut)" }
+
+  | otherwise
+  = ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
+           , ppr old_ev $$ ppr rhs_ty )
+           -- Guaranteed by Note [FunEq occurs-check principle]
+    do { dischargeFunEq old_ev fsk ax_co rhs_ty
        ; traceTcS "doTopReactFunEq" $
          vcat [ text "old_ev:" <+> ppr old_ev
               , nest 2 (text ":=") <+> ppr ax_co ]
-       ; stopWith old_ev "Fun/Top (wanted)" }
-
-  | otherwise -- We must not assign ufsk := ...ufsk...!
-  = do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
-       ; new_ev <- case old_ev of
-           CtWanted {}  -> do { (ev, _) <- newWantedEq loc Nominal alpha_ty rhs_ty
-                              ; updWorkListTcS $
-                                  extendWorkListEq (mkNonCanonical ev)
-                              ; return ev }
-           CtDerived {} -> do { ev <- newDerivedNC loc pred
-                              ; updWorkListTcS (extendWorkListDerived loc ev)
-                              ; return ev }
-             where pred = mkPrimEqPred alpha_ty rhs_ty
-           _ -> pprPanic "reduce_top_fun_eq" (ppr old_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
-            --     ufsk := alpha
-            -- final_co :: fam_tc args ~ alpha
-       ; dischargeFmv old_ev fsk final_co alpha_ty
-       ; traceTcS "doTopReactFunEq (occurs)" $
-         vcat [ text "old_ev:" <+> ppr old_ev
-              , nest 2 (text ":=") <+> ppr final_co
-              , text "new_ev:" <+> ppr new_ev ]
-       ; stopWith old_ev "Fun/Top (wanted)" }
-  where
-    loc = ctEvLoc old_ev
-    deeper_loc = bumpCtLocDepth loc
+       ; stopWith old_ev "Fun/Top" }
+
+improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcTyVar -> TcS ()
+-- See Note [FunDep and implicit parameter reactions]
+improveTopFunEqs ev fam_tc args fsk
+  | isGiven ev            -- See Note [No FunEq improvement for Givens]
+    || not (isImprovable ev)
+  = return ()
 
-improveTopFunEqs :: CtLoc -> TyCon -> [TcType] -> TcTyVar -> TcS ()
-improveTopFunEqs loc fam_tc args fsk
-  = do { model <- getInertModel
+  | otherwise
+  = do { ieqs <- getInertEqs
        ; fam_envs <- getFamInstEnvs
        ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
-                                    (lookupFlattenTyVar model fsk)
+                                    (lookupFlattenTyVar ieqs fsk)
+       ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr fsk
+                                          , ppr eqns ])
        ; mapM_ (unifyDerived loc Nominal) eqns }
+  where
+    loc = ctEvLoc ev  -- ToDo: this location is wrong; it should be FunDepOrigin2
+                      -- See Trac #14778
 
 improve_top_fun_eqs :: FamInstEnvs
                     -> TyCon -> [TcType] -> TcType
-                    -> TcS [Eqn]
+                    -> TcS [TypeEqn]
 improve_top_fun_eqs fam_envs fam_tc args rhs_ty
   | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
   = return (sfInteractTop ops args rhs_ty)
 
   -- see Note [Type inference for type families with injectivity]
   | isOpenTypeFamilyTyCon fam_tc
-  , Injective injective_args <- familyTyConInjectivityInfo fam_tc
+  , Injective injective_args <- tyConInjectivityInfo fam_tc
+  , let fam_insts = lookupFamInstEnvByTyCon fam_envs fam_tc
   = -- it is possible to have several compatible equations in an open type
     -- family but we only want to derive equalities from one such equation.
-    concatMapM (injImproveEqns injective_args) (take 1 $
-      buildImprovementData (lookupFamInstEnvByTyCon fam_envs fam_tc)
-                           fi_tys fi_rhs (const Nothing))
+    do { let improvs = buildImprovementData fam_insts
+                           fi_tvs fi_tys fi_rhs (const Nothing)
+
+       ; traceTcS "improve_top_fun_eqs2" (ppr improvs)
+       ; concatMapM (injImproveEqns injective_args) $
+         take 1 improvs }
 
   | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
-  , Injective injective_args <- familyTyConInjectivityInfo fam_tc
+  , Injective injective_args <- tyConInjectivityInfo fam_tc
   = concatMapM (injImproveEqns injective_args) $
-      buildImprovementData (fromBranches (co_ax_branches ax))
-                           cab_lhs cab_rhs Just
+    buildImprovementData (fromBranches (co_ax_branches ax))
+                         cab_tvs cab_lhs cab_rhs Just
 
   | otherwise
   = return []
-     where
+
+  where
       buildImprovementData
           :: [a]                     -- axioms for a TF (FamInst or CoAxBranch)
+          -> (a -> [TyVar])          -- get bound tyvars of an axiom
           -> (a -> [Type])           -- get LHS of an axiom
           -> (a -> Type)             -- get RHS of an axiom
           -> (a -> Maybe CoAxBranch) -- Just => apartness check required
-          -> [( [Type], TCvSubst, TyVarSet, Maybe CoAxBranch )]
+          -> [( [Type], TCvSubst, [TyVar], Maybe CoAxBranch )]
              -- Result:
              -- ( [arguments of a matching axiom]
              -- , RHS-unifying substitution
              -- , axiom variables without substitution
              -- , Maybe matching axiom [Nothing - open TF, Just - closed TF ] )
-      buildImprovementData axioms axiomLHS axiomRHS wrap =
+      buildImprovementData axioms axiomTVs axiomLHS axiomRHS wrap =
           [ (ax_args, subst, unsubstTvs, wrap axiom)
           | axiom <- axioms
           , let ax_args = axiomLHS axiom
-          , let ax_rhs  = axiomRHS axiom
+                ax_rhs  = axiomRHS axiom
+                ax_tvs  = axiomTVs axiom
           , Just subst <- [tcUnifyTyWithTFs False ax_rhs rhs_ty]
-          , let tvs           = tyCoVarsOfTypes ax_args
-                notInSubst tv = not (tv `elemVarEnv` getTvSubstEnv subst)
-                unsubstTvs    = filterVarSet (notInSubst <&&> isTyVar) tvs ]
+          , let notInSubst tv = not (tv `elemVarEnv` getTvSubstEnv subst)
+                unsubstTvs    = filter (notInSubst <&&> isTyVar) ax_tvs ]
+                   -- The order of unsubstTvs is important; it must be
+                   -- in telescope order e.g. (k:*) (a:k)
 
       injImproveEqns :: [Bool]
-                     -> ([Type], TCvSubst, TyCoVarSet, Maybe CoAxBranch)
-                     -> TcS [Eqn]
-      injImproveEqns inj_args (ax_args, theta, unsubstTvs, cabr) = do
-        (theta', _) <- instFlexiTcS (varSetElems unsubstTvs)
-        let subst = theta `unionTCvSubst` theta'
-        return [ Pair arg (substTyUnchecked subst ax_arg)
-               | case cabr of
-                  Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
-                  _          -> True
-               , (arg, ax_arg, True) <- zip3 args ax_args inj_args ]
+                     -> ([Type], TCvSubst, [TyCoVar], Maybe CoAxBranch)
+                     -> TcS [TypeEqn]
+      injImproveEqns inj_args (ax_args, subst, unsubstTvs, cabr)
+        = do { subst <- instFlexiX subst unsubstTvs
+                  -- If the current substitution bind [k -> *], and
+                  -- one of the un-substituted tyvars is (a::k), we'd better
+                  -- be sure to apply the current substitution to a's kind.
+                  -- Hence instFlexiX.   Trac #13135 was an example.
+
+             ; return [ Pair (substTyUnchecked subst ax_arg) arg
+                        -- NB: the ax_arg part is on the left
+                        -- see Note [Improvement orientation]
+                      | case cabr of
+                          Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
+                          _          -> True
+                      , (ax_arg, arg, True) <- zip3 ax_args args inj_args ] }
 
 
 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
-                  -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
+                  -> TyCon -> [TcType] -> TcS ()
 -- See Note [Top-level reductions for type functions]
+-- Previously, we flattened the tc_args here, but there's no need to do so.
+-- And, if we did, this function would have all the complication of
+-- TcCanonical.canCFunEqCan. See Note [canCFunEqCan]
 shortCutReduction old_ev fsk ax_co fam_tc tc_args
   = ASSERT( ctEvEqRel old_ev == NomEq)
-    do { (xis, cos) <- flattenManyNom old_ev tc_args
                -- ax_co :: F args ~ G tc_args
-               -- cos   :: xis ~ tc_args
                -- old_ev :: F args ~ fsk
-               -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
-
-       ; new_ev <- case ctEvFlavour old_ev of
+    do { new_ev <- case ctEvFlavour old_ev of
            Given -> newGivenEvVar deeper_loc
-                         ( mkPrimEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
-                         , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
-                                        `mkTcTransCo` mkTcSymCo ax_co
-                                        `mkTcTransCo` ctEvCoercion old_ev) )
+                         ( mkPrimEqPred (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
+                         , evCoercion (mkTcSymCo ax_co
+                                       `mkTcTransCo` ctEvCoercion old_ev) )
 
-           Derived -> newDerivedNC deeper_loc $
-                      mkPrimEqPred (mkTyConApp fam_tc xis)
-                                   (mkTyVarTy fsk)
-
-           Wanted ->
+           Wanted {} ->
              do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal
-                                        (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
-                ; setWantedEq (ctev_dest old_ev) $
-                     ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal
-                                                      fam_tc cos)
-                           `mkTcTransCo` new_co
+                                        (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
+                ; setWantedEq (ctev_dest old_ev) $ ax_co `mkTcTransCo` new_co
                 ; return new_ev }
 
+           Derived -> pprPanic "shortCutReduction" (ppr old_ev)
+
        ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
-                                , cc_tyargs = xis, cc_fsk = fsk }
-       ; updWorkListTcS (extendWorkListFunEq new_ct)
-       ; stopWith old_ev "Fun/Top (shortcut)" }
+                                , cc_tyargs = tc_args, cc_fsk = fsk }
+       ; updWorkListTcS (extendWorkListFunEq new_ct) }
   where
     deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
 
-dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
--- (dischargeFmv x fmv co ty)
---     [W] ev :: F tys ~ fmv
---         co :: F tys ~ xi
--- Precondition: fmv is not filled, and fuv `notElem` xi
---
--- Then set fmv := xi,
---      set ev := co
---      kick out any inert things that are now rewritable
---
--- Does not evaluate 'co' if 'ev' is Derived
-dischargeFmv ev fmv co xi
-  = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
-    do { setEvBindIfWanted ev (EvCoercion co)
-       ; unflattenFmv fmv xi
-       ; n_kicked <- kickOutAfterUnification fmv
-       ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
-
 {- Note [Top-level reductions for type functions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 c.f. Note [The flattening story] in TcFlatten
@@ -1591,15 +2053,14 @@ Here is what we do, in four cases:
     instantiate axiom: ax_co : F tys ~ rhs
 
    Then:
-      Discharge   fmv := alpha
+      Discharge   fmv := rhs
       Discharge   x := ax_co ; sym x2
-      New wanted  [W] x2 : alpha ~ rhs  (Non-canonical)
    This is *the* way that fmv's get unified; even though they are
    "untouchable".
 
-   NB: it can be the case that fmv appears in the (instantiated) rhs.
-   In that case the new Non-canonical wanted will be loopy, but that's
-   ok.  But it's good reason NOT to claim that it is canonical!
+   NB: Given Note [FunEq occurs-check principle], fmv does not appear
+   in tys, and hence does not appear in the instantiated RHS.  So
+   the unification can't make an infinite type.
 
 * Wanteds: short cut firing rule
   Applies when the RHS of the axiom is another type-function application
@@ -1631,6 +2092,36 @@ Here is what we do, in four cases:
      - Add new Canonical given
           [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk   (CFunEqCan)
 
+Note [FunEq occurs-check principle]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+I have spent a lot of time finding a good way to deal with
+CFunEqCan constraints like
+    F (fuv, a) ~ fuv
+where flatten-skolem occurs on the LHS.  Now in principle we
+might may progress by doing a reduction, but in practice its
+hard to find examples where it is useful, and easy to find examples
+where we fall into an infinite reduction loop.  A rule that works
+very well is this:
+
+  *** FunEq occurs-check principle ***
+
+      Do not reduce a CFunEqCan
+          F tys ~ fsk
+      if fsk appears free in tys
+      Instead we treat it as stuck.
+
+Examples:
+
+* Trac #5837 has [G] a ~ TF (a,Int), with an instance
+    type instance TF (a,b) = (TF a, TF b)
+  This readily loops when solving givens.  But with the FunEq occurs
+  check principle, it rapidly gets stuck which is fine.
+
+* Trac #12444 is a good example, explained in comment:2.  We have
+    type instance F (Succ x) = Succ (F x)
+    [W] alpha ~ Succ (F alpha)
+  If we allow the reduction to happen, we get an infinite loop
+
 Note [Cached solved FunEqs]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When trying to solve, say (FunExpensive big-type ~ ty), it's important
@@ -1645,135 +2136,251 @@ When trying to match a dictionary (D tau) to a top-level instance, or a
 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
 we do *not* need to expand type synonyms because the matcher will do that for us.
 
+Note [Improvement orientation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A very delicate point is the orientation of derived equalities
+arising from injectivity improvement (Trac #12522).  Suppse we have
+  type family F x = t | t -> x
+  type instance F (a, Int) = (Int, G a)
+where G is injective; and wanted constraints
+
+  [W] TF (alpha, beta) ~ fuv
+  [W] fuv ~ (Int, <some type>)
+
+The injectivity will give rise to derived constraints
+
+  [D] gamma1 ~ alpha
+  [D] Int ~ beta
+
+The fresh unification variable gamma1 comes from the fact that we
+can only do "partial improvement" here; see Section 5.2 of
+"Injective type families for Haskell" (HS'15).
+
+Now, it's very important to orient the equations this way round,
+so that the fresh unification variable will be eliminated in
+favour of alpha.  If we instead had
+   [D] alpha ~ gamma1
+then we would unify alpha := gamma1; and kick out the wanted
+constraint.  But when we grough it back in, it'd look like
+   [W] TF (gamma1, beta) ~ fuv
+and exactly the same thing would happen again!  Infinite loop.
+
+This all seems fragile, and it might seem more robust to avoid
+introducing gamma1 in the first place, in the case where the
+actual argument (alpha, beta) partly matches the improvement
+template.  But that's a bit tricky, esp when we remember that the
+kinds much match too; so it's easier to let the normal machinery
+handle it.  Instead we are careful to orient the new derived
+equality with the template on the left.  Delicate, but it works.
+
+Note [No FunEq improvement for Givens]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We don't do improvements (injectivity etc) for Givens. Why?
+
+* It generates Derived constraints on skolems, which don't do us
+  much good, except perhaps identify inaccessible branches.
+  (They'd be perfectly valid though.)
+
+* For type-nat stuff the derived constraints include type families;
+  e.g.  (a < b), (b < c) ==> a < c If we generate a Derived for this,
+  we'll generate a Derived/Wanted CFunEqCan; and, since the same
+  InertCans (after solving Givens) are used for each iteration, that
+  massively confused the unflattening step (TcFlatten.unflatten).
+
+  In fact it led to some infinite loops:
+     indexed-types/should_compile/T10806
+     indexed-types/should_compile/T10507
+     polykinds/T10742
+
+Note [Reduction for Derived CFunEqCans]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+You may wonder if it's important to use top-level instances to
+simplify [D] CFunEqCan's.  But it is.  Here's an example (T10226).
+
+   type instance F    Int = Int
+   type instance FInv Int = Int
+
+Suppose we have to solve
+    [WD] FInv (F alpha) ~ alpha
+    [WD] F alpha ~ Int
+
+  --> flatten
+    [WD] F alpha ~ fuv0
+    [WD] FInv fuv0 ~ fuv1  -- (A)
+    [WD] fuv1 ~ alpha
+    [WD] fuv0 ~ Int        -- (B)
+
+  --> Rewwrite (A) with (B), splitting it
+    [WD] F alpha ~ fuv0
+    [W] FInv fuv0 ~ fuv1
+    [D] FInv Int ~ fuv1    -- (C)
+    [WD] fuv1 ~ alpha
+    [WD] fuv0 ~ Int
+
+  --> Reduce (C) with top-level instance
+      **** This is the key step ***
+    [WD] F alpha ~ fuv0
+    [W] FInv fuv0 ~ fuv1
+    [D] fuv1 ~ Int        -- (D)
+    [WD] fuv1 ~ alpha     -- (E)
+    [WD] fuv0 ~ Int
+
+  --> Rewrite (D) with (E)
+    [WD] F alpha ~ fuv0
+    [W] FInv fuv0 ~ fuv1
+    [D] alpha ~ Int       -- (F)
+    [WD] fuv1 ~ alpha
+    [WD] fuv0 ~ Int
+
+  --> unify (F)  alpha := Int, and that solves it
+
+Another example is indexed-types/should_compile/T10634
+-}
 
-Note [RHS-FAMILY-SYNONYMS]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-The RHS of a family instance is represented as yet another constructor which is
-like a type synonym for the real RHS the programmer declared. Eg:
-    type instance F (a,a) = [a]
-Becomes:
-    :R32 a = [a]      -- internal type synonym introduced
-    F (a,a) ~ :R32 a  -- instance
-
-When we react a family instance with a type family equation in the work list
-we keep the synonym-using RHS without expansion.
-
-Note [FunDep and implicit parameter reactions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Currently, our story of interacting two dictionaries (or a dictionary
-and top-level instances) for functional dependencies, and implicit
-paramters, is that we simply produce new Derived equalities.  So for example
-
-        class D a b | a -> b where ...
-    Inert:
-        d1 :g D Int Bool
-    WorkItem:
-        d2 :w D Int alpha
-
-    We generate the extra work item
-        cv :d alpha ~ Bool
-    where 'cv' is currently unused.  However, this new item can perhaps be
-    spontaneously solved to become given and react with d2,
-    discharging it in favour of a new constraint d2' thus:
-        d2' :w D Int Bool
-        d2 := d2' |> D Int cv
-    Now d2' can be discharged from d1
-
-We could be more aggressive and try to *immediately* solve the dictionary
-using those extra equalities, but that requires those equalities to carry
-evidence and derived do not carry evidence.
-
-If that were the case with the same inert set and work item we might dischard
-d2 directly:
-
-        cv :w alpha ~ Bool
-        d2 := d1 |> D Int cv
+{- *******************************************************************
+*                                                                    *
+         Top-level reaction for class constraints (CDictCan)
+*                                                                    *
+**********************************************************************-}
 
-But in general it's a bit painful to figure out the necessary coercion,
-so we just take the first approach. Here is a better example. Consider:
-    class C a b c | a -> b
-And:
-     [Given]  d1 : C T Int Char
-     [Wanted] d2 : C T beta Int
-In this case, it's *not even possible* to solve the wanted immediately.
-So we should simply output the functional dependency and add this guy
-[but NOT its superclasses] back in the worklist. Even worse:
-     [Given] d1 : C T Int beta
-     [Wanted] d2: C T beta Int
-Then it is solvable, but its very hard to detect this on the spot.
+doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
+-- Try to use type-class instance declarations to simplify the constraint
+doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
+                                          , cc_tyargs = xis })
+  | isGiven ev   -- Never use instances for Given constraints
+  = do { try_fundep_improvement
+       ; continueWith work_item }
 
-It's exactly the same with implicit parameters, except that the
-"aggressive" approach would be much easier to implement.
+  | Just solved_ev <- lookupSolvedDict inerts dict_loc cls xis   -- Cached
+  = do { setEvBindIfWanted ev (ctEvTerm solved_ev)
+       ; stopWith ev "Dict/Top (cached)" }
 
+  | otherwise  -- Wanted or Derived, but not cached
+   = do { dflags <- getDynFlags
+        ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc
+        ; case lkup_res of
+               OneInst { cir_what = what }
+                  -> do { unless (safeOverlap what) $
+                          insertSafeOverlapFailureTcS work_item
+                        ; when (isWanted ev) $ addSolvedDict ev cls xis
+                        ; chooseInstance work_item lkup_res }
+               _  ->  -- NoInstance or NotSure
+                     do { when (isImprovable ev) $
+                          try_fundep_improvement
+                        ; continueWith work_item } }
+   where
+     dict_pred   = mkClassPred cls xis
+     dict_loc    = ctEvLoc ev
+     dict_origin = ctLocOrigin dict_loc
 
-Note [Weird fundeps]
-~~~~~~~~~~~~~~~~~~~~
-Consider   class Het a b | a -> b where
-              het :: m (f c) -> a -> m b
+     -- We didn't solve it; so try functional dependencies with
+     -- the instance environment, and return
+     -- See also Note [Weird fundeps]
+     try_fundep_improvement
+        = do { traceTcS "try_fundeps" (ppr work_item)
+             ; instEnvs <- getInstEnvs
+             ; emitFunDepDeriveds $
+               improveFromInstEnv instEnvs mk_ct_loc dict_pred }
 
-           class GHet (a :: * -> *) (b :: * -> *) | a -> b
-           instance            GHet (K a) (K [a])
-           instance Het a b => GHet (K a) (K b)
+     mk_ct_loc :: PredType   -- From instance decl
+               -> SrcSpan    -- also from instance deol
+               -> CtLoc
+     mk_ct_loc inst_pred inst_loc
+       = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
+                                               inst_pred inst_loc }
 
-The two instances don't actually conflict on their fundeps,
-although it's pretty strange.  So they are both accepted. Now
-try   [W] GHet (K Int) (K Bool)
-This triggers fundeps from both instance decls;
-      [D] K Bool ~ K [a]
-      [D] K Bool ~ K beta
-And there's a risk of complaining about Bool ~ [a].  But in fact
-the Wanted matches the second instance, so we never get as far
-as the fundeps.
+doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
 
-Trac #7875 is a case in point.
 
-Note [Overriding implicit parameters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-   f :: (?x::a) -> Bool -> a
+chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct)
+chooseInstance work_item
+               (OneInst { cir_new_theta = theta
+                        , cir_what      = what
+                        , cir_mk_ev     = mk_ev })
+  = do { traceTcS "doTopReact/found instance for" $ ppr ev
+       ; deeper_loc <- checkInstanceOK loc what pred
+       ; if isDerived ev then finish_derived deeper_loc theta
+                         else finish_wanted  deeper_loc theta mk_ev }
+  where
+     ev         = ctEvidence work_item
+     pred       = ctEvPred ev
+     loc        = ctEvLoc ev
 
-   g v = let ?x::Int = 3
-         in (f v, let ?x::Bool = True in f v)
+     finish_wanted :: CtLoc -> [TcPredType]
+                   -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
+      -- Precondition: evidence term matches the predicate workItem
+     finish_wanted loc theta mk_ev
+        = do { evb <- getTcEvBindsVar
+             ; if isCoEvBindsVar evb
+               then -- See Note [Instances in no-evidence implications]
+                    continueWith work_item
+               else
+          do { evc_vars <- mapM (newWanted loc) theta
+             ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars))
+             ; emitWorkNC (freshGoals evc_vars)
+             ; stopWith ev "Dict/Top (solved wanted)" } }
+
+     finish_derived loc theta
+       = -- Use type-class instances for Deriveds, in the hope
+         -- of generating some improvements
+         -- C.f. Example 3 of Note [The improvement story]
+         -- It's easy because no evidence is involved
+         do { emitNewDeriveds loc theta
+            ; traceTcS "finish_derived" (ppr (ctl_depth loc))
+            ; stopWith ev "Dict/Top (solved derived)" }
+
+chooseInstance work_item lookup_res
+  = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res)
+
+checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
+-- Check that it's OK to use this insstance:
+--    (a) the use is well staged in the Template Haskell sense
+--    (b) we have not recursed too deep
+-- Returns the CtLoc to used for sub-goals
+checkInstanceOK loc what pred
+  = do { checkWellStagedDFun loc what pred
+       ; checkReductionDepth deeper_loc pred
+       ; return deeper_loc }
+  where
+     deeper_loc = zap_origin (bumpCtLocDepth loc)
+     origin     = ctLocOrigin loc
 
-This should probably be well typed, with
-   g :: Bool -> (Int, Bool)
+     zap_origin loc  -- After applying an instance we can set ScOrigin to
+                     -- infinity, so that prohibitedSuperClassSolve never fires
+       | ScOrigin {} <- origin
+       = setCtLocOrigin loc (ScOrigin infinity)
+       | otherwise
+       = loc
 
-So the inner binding for ?x::Bool *overrides* the outer one.
-Hence a work-item Given overrides an inert-item Given.
+{- Note [Instances in no-evidence implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In Trac #15290 we had
+  [G] forall p q. Coercible p q => Coercible (m p) (m q))
+  [W] forall <no-ev> a. m (Int, IntStateT m a)
+                          ~R#
+                        m (Int, StateT Int m a)
+
+The Given is an ordinary quantified constraint; the Wanted is an implication
+equality that arises from
+  [W] (forall a. t1) ~R# (forall a. t2)
+
+But because the (t1 ~R# t2) is solved "inside a type" (under that forall a)
+we can't generate any term evidence.  So we can't actually use that
+lovely quantified constraint.  Alas!
+
+This test arranges to ignore the instance-based solution under these
+(rare) circumstances.   It's sad, but I  really don't see what else we can do.
 -}
 
-{- *******************************************************************
-*                                                                    *
-                       Class lookup
-*                                                                    *
-**********************************************************************-}
-
--- | Indicates if Instance met the Safe Haskell overlapping instances safety
--- check.
---
--- See Note [Safe Haskell Overlapping Instances] in TcSimplify
--- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
-type SafeOverlapping = Bool
-
-data LookupInstResult
-  = NoInstance
-  | GenInst { lir_new_theta :: [TcPredType]
-            , lir_mk_ev     :: [EvTerm] -> EvTerm
-            , lir_safe_over :: SafeOverlapping }
-
-instance Outputable LookupInstResult where
-  ppr NoInstance = text "NoInstance"
-  ppr (GenInst { lir_new_theta = ev
-               , lir_safe_over = s })
-    = text "GenInst" <+> vcat [ppr ev, ss]
-    where ss = text $ if s then "[safe]" else "[unsafe]"
 
-
-matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
+matchClassInst :: DynFlags -> InertSet
+               -> Class -> [Type]
+               -> CtLoc -> TcS ClsInstResult
 matchClassInst dflags inerts clas tys loc
 -- First check whether there is an in-scope Given that could
--- match this constraint.  In that case, do not use top-level
--- instances.  See Note [Instance and Given overlap]
+-- match this constraint.  In that case, do not use any instance
+-- whether top level, or local quantified constraints.
+-- ee Note [Instance and Given overlap]
   | not (xopt LangExt.IncoherentInstances dflags)
   , not (naturallyCoherentClass clas)
   , let matchable_givens = matchableGivens loc pred inerts
@@ -1781,27 +2388,39 @@ matchClassInst dflags inerts clas tys loc
   = do { traceTcS "Delaying instance application" $
            vcat [ text "Work item=" <+> pprClassPred clas tys
                 , text "Potential matching givens:" <+> ppr matchable_givens ]
-       ; return NoInstance }
-  where
-     pred = mkClassPred clas tys
-
-matchClassInst dflags _ clas tys loc
- = do { traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr (mkClassPred clas tys) ]
-      ; res <- match_class_inst dflags clas tys loc
-      ; traceTcS "matchClassInst result" $ ppr res
-      ; return res }
-
-match_class_inst :: DynFlags -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
-match_class_inst dflags clas tys loc
-  | cls_name == knownNatClassName     = matchKnownNat        clas tys
-  | cls_name == knownSymbolClassName  = matchKnownSymbol     clas tys
-  | isCTupleClass clas                = matchCTuple          clas tys
-  | cls_name == typeableClassName     = matchTypeable        clas tys
-  | clas `hasKey` heqTyConKey         = matchLiftedEquality       tys
-  | clas `hasKey` coercibleTyConKey   = matchLiftedCoercible      tys
-  | otherwise                         = matchInstEnv dflags clas tys loc
+       ; return NotSure }
+
+  | otherwise
+  = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr pred <+> char '{'
+       ; local_res <- matchLocalInst pred loc
+       ; case local_res of
+           OneInst {} ->  -- See Note [Local instances and incoherence]
+                do { traceTcS "} matchClassInst local match" $ ppr local_res
+                   ; return local_res }
+
+           NotSure -> -- In the NotSure case for local instances
+                      -- we don't want to try global instances
+                do { traceTcS "} matchClassInst local not sure" empty
+                   ; return local_res }
+
+           NoInstance  -- No local instances, so try global ones
+              -> do { global_res <- matchGlobalInst dflags False clas tys
+                    ; traceTcS "} matchClassInst global result" $ ppr global_res
+                    ; return global_res } }
   where
-    cls_name = className clas
+    pred = mkClassPred clas tys
+
+-- | If a class is "naturally coherent", then we needn't worry at all, in any
+-- way, about overlapping/incoherent instances. Just solve the thing!
+-- See Note [Naturally coherent classes]
+-- See also Note [The equality class story] in TysPrim.
+naturallyCoherentClass :: Class -> Bool
+naturallyCoherentClass cls
+  = isCTupleClass cls
+    || cls `hasKey` heqTyConKey
+    || cls `hasKey` eqTyConKey
+    || cls `hasKey` coercibleTyConKey
+
 
 {- Note [Instance and Given overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1814,21 +2433,22 @@ Example, from the OutsideIn(X) paper:
        g :: forall a. Q [a] => [a] -> Int
        g x = wob x
 
-This will generate the impliation constraint:
-            Q [a] => (Q [beta], R beta [a])
+From 'g' we get the impliation constraint:
+            forall a. 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:
+The partial 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.
 
   We treat any meta-tyvar as "unifiable" for this purpose,
-  *including* untouchable ones
+  *including* untouchable ones.  But not skolems like 'a' in
+  the implication constraint above.
 
 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
@@ -1843,6 +2463,13 @@ Other notes:
      - natural numbers
      - Typeable
 
+* Flatten-skolems: we do not treat a flatten-skolem as unifiable
+  for this purpose.
+  E.g.   f :: Eq (F a) => [a] -> [a]
+         f xs = ....(xs==xs).....
+  Here we get [W] Eq [a], and we don't want to refrain from solving
+  it because of the given (Eq (F a)) constraint!
+
 * The given-overlap problem is arguably not easy to appear in practice
   due to our aggressive prioritization of equality solving over other
   constraints, but it is possible. I've added a test case in
@@ -1864,259 +2491,131 @@ Other notes:
 
   But for the Given Overlap check our goal is just related to completeness of
   constraint solving.
--}
-
-
-{- *******************************************************************
-*                                                                    *
-                Class lookup in the instance environment
-*                                                                    *
-**********************************************************************-}
 
-matchInstEnv :: DynFlags -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
-matchInstEnv dflags clas tys loc
-   = do { instEnvs <- getInstEnvs
-        ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
-              (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
-              safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
-        ; case (matches, unify, safeHaskFail) of
-
-            -- Nothing matches
-            ([], _, _)
-                -> do { traceTcS "matchClass not matching" $
-                        vcat [ text "dict" <+> ppr pred ]
-                      ; return NoInstance }
-
-            -- A single match (& no safe haskell failure)
-            ([(ispec, inst_tys)], [], False)
-                -> do   { let dfun_id = instanceDFunId ispec
-                        ; traceTcS "matchClass success" $
-                          vcat [text "dict" <+> ppr pred,
-                                text "witness" <+> ppr dfun_id
-                                               <+> ppr (idType dfun_id) ]
-                                  -- Record that this dfun is needed
-                        ; match_one (null unsafeOverlaps) dfun_id inst_tys }
-
-            -- More than one matches (or Safe Haskell fail!). Defer any
-            -- reactions of a multitude until we learn more about the reagent
-            (matches, _, _)
-                -> do   { traceTcS "matchClass multiple matches, deferring choice" $
-                          vcat [text "dict" <+> ppr pred,
-                                text "matches" <+> ppr matches]
-                        ; return NoInstance } }
-   where
-     pred = mkClassPred clas tys
-
-     match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcS LookupInstResult
-                  -- See Note [DFunInstType: instantiating types] in InstEnv
-     match_one so dfun_id mb_inst_tys
-       = do { checkWellStagedDFun pred dfun_id loc
-            ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
-            ; return $ GenInst { lir_new_theta = theta
-                               , lir_mk_ev     = EvDFunApp dfun_id tys
-                               , lir_safe_over = so } }
-
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for CTuples
-*                                                                     *
-***********************************************************************-}
-
-matchCTuple :: Class -> [Type] -> TcS LookupInstResult
-matchCTuple clas tys   -- (isCTupleClass clas) holds
-  = return (GenInst { lir_new_theta = tys
-                    , lir_mk_ev     = tuple_ev
-                    , lir_safe_over = True })
-            -- The dfun *is* the data constructor!
-  where
-     data_con = tyConSingleDataCon (classTyCon clas)
-     tuple_ev = EvDFunApp (dataConWrapId data_con) tys
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for Literals
-*                                                                     *
-***********************************************************************-}
-
-matchKnownNat :: Class -> [Type] -> TcS LookupInstResult
-matchKnownNat clas [ty]     -- clas = KnownNat
-  | Just n <- isNumLitTy ty = makeLitDict clas ty (EvNum n)
-matchKnownNat _ _           = return NoInstance
-
-matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult
-matchKnownSymbol clas [ty]  -- clas = KnownSymbol
-  | Just n <- isStrLitTy ty = makeLitDict clas ty (EvStr n)
-matchKnownSymbol _ _       = return NoInstance
-
-
-makeLitDict :: Class -> Type -> EvLit -> TcS LookupInstResult
--- makeLitDict adds a coercion that will convert the literal into a dictionary
--- of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]
--- in TcEvidence.  The coercion happens in 2 steps:
---
---     Integer -> SNat n     -- representation of literal to singleton
---     SNat n  -> KnownNat n -- singleton to dictionary
---
---     The process is mirrored for Symbols:
---     String    -> SSymbol n
---     SSymbol n -> KnownSymbol n -}
-makeLitDict clas ty evLit
-    | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
-          -- co_dict :: KnownNat n ~ SNat n
-    , [ meth ]   <- classMethods clas
-    , Just tcRep <- tyConAppTyCon_maybe -- SNat
-                      $ funResultTy         -- SNat n
-                      $ dropForAlls         -- KnownNat n => SNat n
-                      $ idType meth         -- forall n. KnownNat n => SNat n
-    , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
-          -- SNat n ~ Integer
-    , let ev_tm = mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep))
-    = return $ GenInst { lir_new_theta = []
-                       , lir_mk_ev     = \_ -> ev_tm
-                       , lir_safe_over = True }
-
-    | otherwise
-    = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
-                     $$ vcat (map (ppr . idType) (classMethods clas)))
-
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for Typeable
-*                                                                     *
-***********************************************************************-}
-
--- | Assumes that we've checked that this is the 'Typeable' class,
--- and it was applied to the correct argument.
-matchTypeable :: Class -> [Type] -> TcS LookupInstResult
-matchTypeable clas [k,t]  -- clas = Typeable
-  -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
-  | isForAllTy k                      = return NoInstance   -- Polytype
-  | isJust (tcSplitPredFunTy_maybe t) = return NoInstance   -- Qualified type
-
-  -- Now cases that do work
-  | k `eqType` typeNatKind                 = doTyLit knownNatClassName    t
-  | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName t
-  | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
-  , onlyNamedBndrsApplied tc ks            = doTyConApp clas t ks
-  | Just (f,kt)   <- splitAppTy_maybe t    = doTyApp    clas t f kt
-
-matchTypeable _ _ = return NoInstance
-
-doTyConApp :: Class -> Type -> [Kind] -> TcS LookupInstResult
--- Representation for type constructor applied to some kinds
-doTyConApp clas ty args
-  = return $ GenInst (map (mk_typeable_pred clas) args)
-                     (\tms -> EvTypeable ty $ EvTypeableTyCon tms)
-                     True
-
--- Representation for concrete kinds.  We just use the kind itself,
--- but first we must make sure that we've instantiated all kind-
--- polymorphism, but no more.
-onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool
-onlyNamedBndrsApplied tc ks
- = all isNamedBinder used_bndrs &&
-   not (any isNamedBinder leftover_bndrs)
- where
-   bndrs                        = tyConBinders tc
-   (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
-
-doTyApp :: Class -> Type -> Type -> KindOrType -> TcS LookupInstResult
--- Representation for an application of a type to a type-or-kind.
---  This may happen when the type expression starts with a type variable.
---  Example (ignoring kind parameter):
---    Typeable (f Int Char)                      -->
---    (Typeable (f Int), Typeable Char)          -->
---    (Typeable f, Typeable Int, Typeable Char)  --> (after some simp. steps)
---    Typeable f
-doTyApp clas ty f tk
-  | isForAllTy (typeKind f)
-  = return NoInstance -- We can't solve until we know the ctr.
-  | otherwise
-  = return $ GenInst [mk_typeable_pred clas f, mk_typeable_pred clas tk]
-                     (\[t1,t2] -> EvTypeable ty $ EvTypeableTyApp t1 t2)
-                     True
-
--- Emit a `Typeable` constraint for the given type.
-mk_typeable_pred :: Class -> Type -> PredType
-mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
-
-  -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
-  -- we generate a sub-goal for the appropriate class. See #10348 for what
-  -- happens when we fail to do this.
-doTyLit :: Name -> Type -> TcS LookupInstResult
-doTyLit kc t = do { kc_clas <- tcLookupClass kc
-                  ; let kc_pred    = mkClassPred kc_clas [ t ]
-                        mk_ev [ev] = EvTypeable t $ EvTypeableTyLit ev
-                        mk_ev _    = panic "doTyLit"
-                  ; return (GenInst [kc_pred] mk_ev True) }
-
-{- Note [Typeable (T a b c)]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For type applications we always decompose using binary application,
-vai doTyApp, until we get to a *kind* instantiation.  Exmaple
-   Proxy :: forall k. k -> *
-
-To solve Typeable (Proxy (* -> *) Maybe) we
-  - First decompose with doTyApp,
-    to get (Typeable (Proxy (* -> *))) and Typeable Maybe
-  - Then sovle (Typeable (Proxy (* -> *))) with doTyConApp
-
-If we attempt to short-cut by solving it all at once, via
-doTyCOnAPp
-
-
-Note [No Typeable for polytypes or qualified types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We do not support impredicative typeable, such as
-   Typeable (forall a. a->a)
-   Typeable (Eq a => a -> a)
-   Typeable (() => Int)
-   Typeable (((),()) => Int)
-
-See Trac #9858.  For forall's the case is clear: we simply don't have
-a TypeRep for them.  For qualified but not polymorphic types, like
-(Eq a => a -> a), things are murkier.  But:
-
- * We don't need a TypeRep for these things.  TypeReps are for
-   monotypes only.
-
- * Perhaps we could treat `=>` as another type constructor for `Typeable`
-   purposes, and thus support things like `Eq Int => Int`, however,
-   at the current state of affairs this would be an odd exception as
-   no other class works with impredicative types.
-   For now we leave it off, until we have a better story for impredicativity.
+* The solution is only a partial one.  Consider the above example with
+       g :: forall a. Q [a] => [a] -> Int
+       g x = let v = wob x
+             in v
+  and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
+  general type for 'v'.  When generalising v's type we'll simplify its
+  Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
+  will use the instance declaration after all. Trac #11948 was a case
+  in point.
+
+All of this is disgustingly delicate, so to discourage people from writing
+simplifiable class givens, we warn about signatures that contain them;
+see TcValidity Note [Simplifiable given constraints].
+
+Note [Naturally coherent classes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A few built-in classes are "naturally coherent".  This term means that
+the "instance" for the class is bidirectional with its superclass(es).
+For example, consider (~~), which behaves as if it was defined like
+this:
+  class a ~# b => a ~~ b
+  instance a ~# b => a ~~ b
+(See Note [The equality types story] in TysPrim.)
+
+Faced with [W] t1 ~~ t2, it's always OK to reduce it to [W] t1 ~# t2,
+without worrying about Note [Instance and Given overlap].  Why?  Because
+if we had [G] s1 ~~ s2, then we'd get the superclass [G] s1 ~# s2, and
+so the reduction of the [W] constraint does not risk losing any solutions.
+
+On the other hand, it can be fatal to /fail/ to reduce such
+equalities, on the grounds of Note [Instance and Given overlap],
+because many good things flow from [W] t1 ~# t2.
+
+The same reasoning applies to
+
+* (~~)        heqTyCOn
+* (~)         eqTyCon
+* Coercible   coercibleTyCon
+
+And less obviously to:
+
+* Tuple classes.  For reasons described in TcSMonad
+  Note [Tuples hiding implicit parameters], we may have a constraint
+     [W] (?x::Int, C a)
+  with an exactly-matching Given constraint.  We must decompose this
+  tuple and solve the components separately, otherwise we won't solve
+  it at all!  It is perfectly safe to decompose it, because again the
+  superclasses invert the instance;  e.g.
+      class (c1, c2) => (% c1, c2 %)
+      instance (c1, c2) => (% c1, c2 %)
+  Example in Trac #14218
+
+Exammples: T5853, T10432, T5315, T9222, T2627b, T3028b
+
+PS: the term "naturally coherent" doesn't really seem helpful.
+Perhaps "invertible" or something?  I left it for now though.
+
+Note [Local instances and incoherence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   f :: forall b c. (Eq b, forall a. Eq a => Eq (c a))
+                 => c b -> Bool
+   f x = x==x
+
+We get [W] Eq (c b), and we must use the local instance to solve it.
+
+BUT that wanted also unifies with the top-level Eq [a] instance,
+and Eq (Maybe a) etc.  We want the local instance to "win", otherwise
+we can't solve the wanted at all.  So we mark it as Incohherent.
+According to Note [Rules for instance lookup] in InstEnv, that'll
+make it win even if there are other instances that unify.
+
+Moreover this is not a hack!  The evidence for this local instance
+will be constructed by GHC at a call site... from the very instances
+that unify with it here.  It is not like an incoherent user-written
+instance which might have utterly different behaviour.
+
+Consdider  f :: Eq a => blah.  If we have [W] Eq a, we certainly
+get it from the Eq a context, without worrying that there are
+lots of top-level instances that unify with [W] Eq a!  We'll use
+those instances to build evidence to pass to f. That's just the
+nullary case of what's happening here.
 -}
 
-solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
-solveCallStack ev ev_cs = do
-  -- We're given ev_cs :: CallStack, but the evidence term should be a
-  -- dictionary, so we have to coerce ev_cs to a dictionary for
-  -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
-  let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev))
-  setWantedEvBind (ctEvId ev) ev_tm
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for lifted equality
-*                                                                     *
-***********************************************************************-}
-
--- See also Note [The equality types story] in TysPrim
-matchLiftedEquality :: [Type] -> TcS LookupInstResult
-matchLiftedEquality args
-  = return (GenInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
-                    , lir_mk_ev     = EvDFunApp (dataConWrapId heqDataCon) args
-                    , lir_safe_over = True })
-
--- See also Note [The equality types story] in TysPrim
-matchLiftedCoercible :: [Type] -> TcS LookupInstResult
-matchLiftedCoercible args@[k, t1, t2]
-  = return (GenInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
-                    , lir_mk_ev     = EvDFunApp (dataConWrapId coercibleDataCon)
-                                                args
-                    , lir_safe_over = True })
+matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
+-- Look up the predicate in Given quantified constraints,
+-- which are effectively just local instance declarations.
+matchLocalInst pred loc
+  = do { ics <- getInertCans
+       ; case match_local_inst (inert_insts ics) of
+           ([], False) -> return NoInstance
+           ([(dfun_ev, inst_tys)], unifs)
+             | not unifs
+             -> do { let dfun_id = ctEvEvId dfun_ev
+                   ; (tys, theta) <- instDFunType dfun_id inst_tys
+                   ; return $ OneInst { cir_new_theta = theta
+                                      , cir_mk_ev     = evDFunApp dfun_id tys
+                                      , cir_what      = LocalInstance } }
+           _ -> return NotSure }
   where
-    args' = [k, k, t1, t2]
-matchLiftedCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
+    pred_tv_set = tyCoVarsOfType pred
+
+    match_local_inst :: [QCInst]
+                     -> ( [(CtEvidence, [DFunInstType])]
+                        , Bool )      -- True <=> Some unify but do not match
+    match_local_inst []
+      = ([], False)
+    match_local_inst (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred
+                               , qci_ev = ev })
+                     : qcis)
+      | let in_scope = mkInScopeSet (qtv_set `unionVarSet` pred_tv_set)
+      , Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope)
+                                        emptyTvSubstEnv qpred pred
+      , let match = (ev, map (lookupVarEnv tv_subst) qtvs)
+      = (match:matches, unif)
+
+      | otherwise
+      = ASSERT2( disjointVarSet qtv_set (tyCoVarsOfType pred)
+               , ppr qci $$ ppr pred )
+            -- ASSERT: unification relies on the
+            -- quantified variables being fresh
+        (matches, unif || this_unif)
+      where
+        qtv_set = mkVarSet qtvs
+        this_unif = mightMatchLater qpred (ctEvLoc ev) pred loc
+        (matches, unif) = match_local_inst qcis
+