Fix solving of implicit parameter constraints
[ghc.git] / compiler / typecheck / TcInteract.hs
index 5a550b4..1298932 100644 (file)
@@ -1,45 +1,57 @@
 {-# LANGUAGE CPP #-}
 
 module TcInteract (
-     solveSimpleGivens,    -- Solves [EvVar],GivenLoc
-     solveSimpleWanteds,   -- Solves Cts
-     usefulToFloat
+     solveSimpleGivens,   -- Solves [Ct]
+     solveSimpleWanteds,  -- Solves Cts
   ) where
 
 #include "HsVersions.h"
 
-import BasicTypes ( infinity )
-import HsTypes ( hsIPNameFS )
-import FastString
+import GhcPrelude
+
+import BasicTypes ( SwapFlag(..), isSwapped,
+                    infinity, IntWithInf, intGtLimit )
 import TcCanonical
 import TcFlatten
+import TcUnify( canSolveByUnification )
 import VarSet
 import Type
-import Kind ( isKind, isConstraintKind, isSubKind )
-import Unify
+import Kind( isConstraintKind )
 import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
-import CoAxiom(sfInteractTop, sfInteractInert)
+import CoAxiom( sfInteractTop, sfInteractInert )
+
+import TcMType (newMetaTyVars)
 
 import Var
 import TcType
-import PrelNames ( knownNatClassName, knownSymbolClassName, ipClassNameKey,
-                   callStackTyConKey, typeableClassName )
-import Id( idType )
+import Name
+import RdrName ( lookupGRE_FieldLabel )
+import PrelNames ( knownNatClassName, knownSymbolClassName,
+                   typeableClassName, typeableClassKey,
+                   coercibleTyConKey,
+                   hasFieldClassName,
+                   heqTyConKey, eqTyConKey, ipClassKey )
+import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
+                    coercibleDataCon, constraintKindTyCon )
+import TysPrim    ( eqPrimTyCon, eqReprPrimTyCon )
+import Id( idType, isNaughtyRecordSelector )
+import CoAxiom ( TypeEqn, CoAxiom(..), CoAxBranch(..), fromBranches )
 import Class
 import TyCon
 import DataCon( dataConWrapId )
+import FieldLabel
 import FunDeps
 import FamInst
-import Inst( tyVarsOfCt )
+import FamInstEnv
+import Unify ( tcUnifyTyWithTFs )
 
 import TcEvidence
 import Outputable
 
-import qualified TcRnMonad as TcM
 import TcRnTypes
-import TcErrors
 import TcSMonad
 import Bag
+import MonadUtils ( concatMapM )
 
 import Data.List( partition, foldl', deleteFirstsBy )
 import SrcLoc
@@ -51,6 +63,10 @@ import Pair (Pair(..))
 import Unique( hasKey )
 import DynFlags
 import Util
+import qualified GHC.LanguageExtensions as LangExt
+
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.Maybe
 
 {-
 **********************************************************************
@@ -88,7 +104,7 @@ We unflatten after solving the wc_simples of an implication, and before attempti
 to float. This means that
 
  * The fsk/fmv flatten-skolems only survive during solveSimples.  We don't
-   need to worry about then across successive passes over the constraint tree.
+   need to worry about them across successive passes over the constraint tree.
    (E.g. we don't need the old ic_fsk field of an implication.
 
  * When floating an equality outwards, we don't need to worry about floating its
@@ -118,7 +134,7 @@ Note [Running plugins on unflattened wanteds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 There is an annoying mismatch between solveSimpleGivens and
 solveSimpleWanteds, because the latter needs to fiddle with the inert
-set, unflatten and and zonk the wanteds.  It passes the zonked wanteds
+set, unflatten and zonk the wanteds.  It passes the zonked wanteds
 to runTcPluginsWanteds, which produces a replacement set of wanteds,
 some additional insolubles and a flag indicating whether to go round
 the loop again.  If so, prepareInertsForImplications is used to remove
@@ -127,315 +143,96 @@ that prepareInertsForImplications will discard the insolubles, so we
 must keep track of them separately.
 -}
 
-solveSimpleGivens :: CtLoc -> [EvVar] -> TcS Cts
--- Solves the givens, adding them to the inert set
--- Returns any insoluble givens, taking those ones out of the inert set
-solveSimpleGivens loc givens
+solveSimpleGivens :: [Ct] -> TcS ()
+solveSimpleGivens givens
   | null givens  -- Shortcut for common case
-  = return emptyCts
+  = return ()
   | otherwise
-  = do { go (map mk_given_ct givens)
-       ; takeInertInsolubles }
+  = do { traceTcS "solveSimpleGivens {" (ppr givens)
+       ; go givens
+       ; traceTcS "End solveSimpleGivens }" empty }
   where
-    mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
-                                                , ctev_pred = evVarPred ev_id
-                                                , ctev_loc  = loc })
     go givens = do { solveSimples (listToBag givens)
                    ; new_givens <- runTcPluginsGiven
-                   ; when (notNull new_givens) (go new_givens)
-                   }
+                   ; when (notNull new_givens) $
+                     go new_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 "solveSimples {" (ppr simples)
-       ; (n,wc) <- go 1 (emptyWC { wc_simple = simples })
-       ; traceTcS "solveSimples end }" $
-             vcat [ ptext (sLit "iterations =") <+> ppr n
-                  , ptext (sLit "residual =") <+> ppr wc ]
+  = do { traceTcS "solveSimpleWanteds {" (ppr simples)
+       ; dflags <- getDynFlags
+       ; (n,wc) <- go 1 (solverIterations dflags) (emptyWC { wc_simple = simples })
+       ; traceTcS "solveSimpleWanteds end }" $
+             vcat [ text "iterations =" <+> ppr n
+                  , text "residual =" <+> ppr wc ]
        ; return wc }
   where
-    go :: Int -> WantedConstraints -> TcS (Int, WantedConstraints)
-    go n wc
-     | n > 10
-     = do { wrapWarnTcS $ TcM.addWarnTc $
-            hang (ptext (sLit "solveSimpleWanteds: possible loop?"))
-               2 (pprCts simples)
-          ; return (n,wc) }
+    go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
+    go n limit wc
+      | n `intGtLimit` limit
+      = failTcS (hang (text "solveSimpleWanteds: too many iterations"
+                       <+> parens (text "limit =" <+> ppr limit))
+                    2 (vcat [ text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
+                            , text "Simples =" <+> ppr simples
+                            , text "WC ="      <+> ppr wc ]))
 
      | isEmptyBag (wc_simple wc)
      = return (n,wc)
 
      | otherwise
      = do { -- Solve
-            (unifs1, wc1) <- solve_simple_wanteds wc
-
-            -- Try improvement
-            -- See Note [The improvement story]
-          ; (unifs2, wc2) <- try_improvement wc1
+            (unif_count, wc1) <- solve_simple_wanteds wc
 
             -- Run plugins
-          ; (rerun_plugin, wc3) <- runTcPluginsWanted wc2
+          ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
              -- See Note [Running plugins on unflattened wanteds]
 
-          ; if unifs1 || unifs2 || rerun_plugin
-            then go (n+1) wc3        -- Loop
-            else return (n,wc3) }
+          ; if unif_count == 0 && not rerun_plugin
+            then return (n, wc2)             -- Done
+            else do { traceTcS "solveSimple going round again:" $
+                      ppr unif_count $$ ppr rerun_plugin
+                    ; go (n+1) limit wc2 } }      -- Loop
 
-solve_simple_wanteds :: WantedConstraints -> TcS (Bool, WantedConstraints)
+
+solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
 -- Try solving these constraints
--- Return True iff some unification happened *during unflattening*
---                 because this is a form of improvement
---                 See Note [The improvement story]
 -- Affects the unification state (of course) but not the inert set
+-- The result is not necessarily zonked
 solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
   = nestTcS $
     do { solveSimples simples1
        ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
-       ; (unifs_happened, unflattened_eqs) <- reportUnifications $
-                                              unflatten tv_eqs fun_eqs
+       ; (unif_count, unflattened_eqs) <- reportUnifications $
+                                          unflattenWanteds tv_eqs fun_eqs
             -- See Note [Unflatten after solving the simple wanteds]
-       ; return ( unifs_happened
+       ; return ( unif_count
                 , WC { wc_simple = others `andCts` unflattened_eqs
                      , wc_insol  = insols1 `andCts` insols2
                      , wc_impl   = implics1 `unionBags` implics2 }) }
 
-try_improvement :: WantedConstraints -> TcS (Bool, WantedConstraints)
--- See Note [The improvement story]
--- Try doing improvement on these simple constraints
--- Return True iff some unification happened
--- Affects the unification state (of course) but not the inert set
-try_improvement wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
-  | isEmptyBag simples
-  = return (False, wc)
-  | otherwise
-  = nestTcS $ reportUnifications $
-    do { traceTcS "try_improvement {" (ppr wc)
-       ; solveSimples init_derived
-       ; (_, tv_eqs, fun_eqs, derived_insols, _) <- getUnsolvedInerts
-       ; derived_eqs <- unflatten tv_eqs fun_eqs
-       ; let new_derived = filterBag (usefulToFloat is_new) derived_eqs
-             wc1         = WC { wc_simple = simples1 `andCts` new_derived
-                              , wc_insol  = dropDerivedSimples insols `andCts` derived_insols
-                                            -- See Note [Insolubles and improvement]
-                              , wc_impl   = implics }
-       ; traceTcS "try_improvement end }" (ppr wc1)
-       ; return wc1 }
-  where
-    is_new pred = not (any (pred `eqType`) init_eq_preds)
-       -- Sigh: an equality in init_derived may well show up in derived_eqs,
-       --       if no progress has been made, and we don't want to duplicate it.
-       -- But happily these lists are both usually very short.
-
-    -- Drop all derived constraints; we are about to re-generate them!
-    simples1      = dropDerivedSimples simples
-    init_derived  = mapBag mk_derived simples1
-    init_eq_preds = [ pred | ct <- bagToList init_derived
-                           , let pred = ctPred ct
-                           , isEqPred pred ]
-
-    mk_derived :: Ct -> Ct  -- Always non-canonical (so that we generate superclasses)
-    mk_derived ct = mkNonCanonical (CtDerived { ctev_pred = pred, ctev_loc = loc })
-       where
-         pred = ctEvPred ev
-         loc  = ctEvLoc  ev
-         ev   = ctEvidence ct
-
-
-usefulToFloat :: (TcPredType -> Bool) -> Ct -> Bool
-usefulToFloat is_useful_pred ct   -- The constraint is un-flattened and de-canonicalised
-  = is_meta_var_eq pred && is_useful_pred pred
-  where
-    pred = ctPred ct
-
-      -- Float out alpha ~ ty, or ty ~ alpha
-      -- which might be unified outside
-      -- See Note [Do not float kind-incompatible equalities]
-    is_meta_var_eq pred
-      | EqPred NomEq ty1 ty2 <- classifyPredType pred
-      , let k1 = typeKind ty1
-            k2 = typeKind ty2
-      = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
-          (Just tv1, _) | isMetaTyVar tv1
-                        , k2 `isSubKind` k1
-                        -> True
-          (_, Just tv2) | isMetaTyVar tv2
-                        , k1 `isSubKind` k2
-                        -> True
-          _ -> False
-      | otherwise
-      = False
-
-{- Note [The improvement story]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The goal of "improvement" is to use functional dependencies,
-type-function injectivity, etc, to derive some extra equalities that
-could let us unify one or more meta-variables, and hence make progress.
-
+{- Note [The solveSimpleWanteds loop]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Solving a bunch of simple constraints is done in a loop,
 (the 'go' loop of 'solveSimpleWanteds'):
-  1. Try to solve them; some improvement happens here
-  2. Try improvement on any unsolved residual constraints
-  3. If step 2 led to any unifications, go back to step 1
-
-We actually perform step 2 improvement as follows:
-  * Make the residual Wanteds into Deriveds
-  * Solve them, aggressively rewriting Derived with Derived
-
-Some notes about this
-  * As well as allowing unification, the aggressive rewriting may also
-    expose an equality on an /untouchable/ unification variable.  We
-    want to keep this derived equality so that it can float out and
-    unify there.  Hence 'usefulToFloat'.
-
-  * Non-obviously, improvement can also take place during the unflattening
-    that takes place in step (1).  See Example 1 below.
-
-  * During Step 1 we do improvement only for Givens, not for Wanteds;
-    See Note [When improvement happens during solving]
-
------------ Example 1 (Trac #10340)
-     get :: MonadState s m => m s
-     instance MonadState s (State s) where ...
-
-     foo :: State Any Any
-     foo = get
-
-  For 'foo' we instantiate 'get' at types mm ss
-       [W] MonadState ss mm, [W] mm ss ~ State Any Any
-  Flatten, and decompose
-       [W] MnadState ss mm, [W] Any ~ fmv, [W] mm ~ State fmv, [W] fmv ~ ss
-  NB: orientation of fmv ~ ss; see TcFlatten
-      Note [Orient equalities with flatten-meta-vars on the left]
-  Unify mm := State fmv:
-       [W] MonadState ss (State fmv), [W] Any ~ fmv, [W] fmv ~ ss
-  Alas the instance does not match!!  So now we are stuck.
-
-  Unflatten: with fmv := Any, and ss := Any
-       [W] MonadState Any (State Any)
-
-  Note that the unification of 'ss' represents progress!! We must loop!
-
------------ Example 2 (indexed-types/should_fail/T4093a)
-  Ambiguity check for f: (Foo e ~ Maybe e) => Foo e
-
-  We get [G] Foo e ~ Maybe e
-         [W] Foo e ~ Foo ee      -- ee is a unification variable
-         [W] Foo ee ~ Maybe ee
-
-  Flatten: [G] Foo e ~ fsk
-           [G] fsk ~ Maybe e   -- (A)
-
-           [W] Foo ee ~ fmv
-           [W] fmv ~ fsk       -- (B) From Foo e ~ Foo ee
-           [W] fmv ~ Maybe ee
-
-  --> rewrite (B) with (A)
-           [W] Foo ee ~ fmv
-           [W] fmv ~ Maybe e
-           [W] fmv ~ Maybe ee
-
-  But now we are stuck, since we don't rewrite Wanteds with Wanteds
-  Unflatten:
-           [W] Foo ee ~ Maybe e
-           [W] Foo ee ~ Maybe ee
-
-  Improvement; start by flattening again
-           [D] Foo ee ~ fmv
-           [D] fmv ~ Maybe e   -- (A)
-           [D] fmv ~ Maybe ee  -- (B)
-
-  Now we /can/ rewrite (A) with (B), by aggressive rewriting of Deriveds
-  and that soon yields ee := e, and all is well
-
------------ Example 3 (typecheck/should_compile/Improvement.hs)
-    type instance F Int = Bool
-    instance (b~Int) => C Bool b
-
-    [W] w1 : C (F alpha) alpha, [W] w2 : F alpha ~ Bool
-
-  If we rewrote wanteds with wanteds, we could rewrite w1 to
-  C Bool alpha, use the instance to get alpha ~ Int, and solve
-  the whole thing.
-
-  In improvement (step 2), we make both constraints Derived,
-  rewrite one with the other, and do type-class reduction on
-  the Derived constraint
-
------------ Example 4 (Trac #10009, a nasty example):
-
-    f :: (UnF (F b) ~ b) => F b -> ()
-
-    g :: forall a. (UnF (F a) ~ a) => a -> ()
-    g _ = f (undefined :: F a)
-
-  For g we get [G] UnF (F a) ~ a
-               [W] UnF (F beta) ~ beta
-               [W] F a ~ F beta
-  Flatten:
-      [G] g1: F a ~ fsk1         fsk1 := F a
-      [G] g2: UnF fsk1 ~ fsk2    fsk2 := UnF fsk1
-      [G] g3: fsk2 ~ a
-
-      [W] w1: F beta ~ fmv1
-      [W] w2: UnF fmv1 ~ fmv2
-      [W] w3: fmv2 ~ beta
-      [W] w5: fsk1 ~ fmv1   -- From F a ~ F beta
-                            -- using flat-cache
-
-  Solving (step 1) makes no progress.  So unflatten again
-      [W] w3: UnF (F beta) ~ beta
-      [W] w5: fsk1 ~ F beta
-
-  Try improvement:
-      [D] F beta ~ fmv1
-      [D] UnF fmv1 ~ fmv2    -- (A)
-      [D] fmv2 ~ beta
-      [D] fmv1 ~ fsk1        -- (B) From F a ~ F beta
-                             -- NB: put fmv on left
-
-    --> rewrite (A) with (B), and match with g2
-      [D] F beta ~ fmv1
-      [D] fmv2 ~ fsk2        -- (C)
-      [D] fmv2 ~ beta        -- (D)
-      [D] fmv1 ~ fsk1
-
-    --> rewrite (D) with (C) and re-orient
-      [D] F beta ~ fmv1
-      [D] fmv2 ~ fsk2
-      [D] beta ~ fsk2       -- (E)
-      [D] fmv1 ~ fsk1
-
-    -- Now we can unify beta!  Hallelujah!
-
-
-Note [Insolubles and improvement]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We drop all the derived wanted insolubles before improvement, because
-they will all be regenerated by the improvement step.
-
-We want to keep all the derived insolubles, because they are looked
-at by simplifyInfer, to decide whether to generalise.  Example:
-    [W] a ~ Int, [W] a ~ Bool
-During improvement we get [D] Int ~ Bool, and indeed the constraints
-are insoluble, and we want simplifyInfer to see that, even though we
-don't ultimately want to generate an (inexplicable) error message from
-it.
-
-Note [Do not float kind-incompatible equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we have (t::* ~ s::*->*), we'll get a Derived insoluble equality.
-If we float the equality outwards, we'll get *another* Derived
-insoluble equality one level out, so the same error will be reported
-twice.  So we refrain from floating such equalities.
+  1. Try to solve them; unflattening may lead to improvement that
+     was not exploitable during solving
+  2. Try the plugin
+  3. If step 1 did improvement during unflattening; or if the plugin
+     wants to run again, go back to step 1
+
+Non-obviously, improvement can also take place during
+the unflattening that takes place in step (1). See TcFlatten,
+See Note [Unflattening can force the solver to iterate]
 -}
 
 -- The main solver loop implements Note [Basic Simplifier Plan]
 ---------------------------------------------------------------
 solveSimples :: Cts -> TcS ()
 -- Returns the final InertSet in TcS
--- Has no effect on work-list or residual-iplications
+-- Has no effect on work-list or residual-implications
 -- The constraints are initially examined in left-to-right order
 
 solveSimples cts
@@ -447,14 +244,9 @@ solveSimples cts
       = {-# SCC "solve_loop" #-}
         do { sel <- selectNextWorkItem
            ; case sel of
-              NoWorkRemaining     -- Done, successfuly (modulo frozen)
-                -> return ()
-              MaxDepthExceeded ct -- Failure, depth exceeded
-                -> wrapErrTcS $ solverDepthErrorTcS (ctLoc ct) (ctPred ct)
-              NextWorkItem ct     -- More work, loop around!
-                -> do { runSolverPipeline thePipeline ct
-                      ; solve_loop } }
-
+              Nothing -> return ()
+              Just ct -> do { runSolverPipeline thePipeline ct
+                            ; solve_loop } }
 
 -- | Extract the (inert) givens and invoke the plugins on them.
 -- Remove solved givens from the inert set and emit insolubles, but
@@ -505,7 +297,7 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl =
   where
     setEv :: (EvTerm,Ct) -> TcS ()
     setEv (ev,ct) = case ctEvidence ct of
-      CtWanted {ctev_evar = evar} -> setWantedEvBind evar ev
+      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest ev
       _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
 
 -- | A triple of (given, derived, wanted) constraints to pass to plugins
@@ -574,11 +366,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
@@ -593,55 +382,30 @@ runTcPlugins plugins all_cts
 type WorkItem = Ct
 type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
 
-data SelectWorkItem
-       = NoWorkRemaining      -- No more work left (effectively we're done!)
-       | MaxDepthExceeded Ct
-                              -- More work left to do but this constraint has exceeded
-                              -- the maximum depth and we must stop
-       | NextWorkItem Ct      -- More work left, here's the next item to look at
-
-selectNextWorkItem :: TcS SelectWorkItem
-selectNextWorkItem
-  = do { dflags <- getDynFlags
-       ; updWorkListTcS_return (pick_next dflags) }
-  where
-    pick_next :: DynFlags -> WorkList -> (SelectWorkItem, WorkList)
-    pick_next dflags wl
-      = case selectWorkItem wl of
-          (Nothing,_)
-              -> (NoWorkRemaining,wl)           -- No more work
-          (Just ct, new_wl)
-              | subGoalDepthExceeded dflags (ctLocDepth (ctLoc ct))
-              -> (MaxDepthExceeded ct,new_wl)   -- Depth exceeded
-
-              | otherwise
-              -> (NextWorkItem ct, new_wl)      -- New workitem and worklist
-
 runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
                   -> WorkItem                   -- The work item
                   -> TcS ()
 -- Run this item down the pipeline, leaving behind new work and inerts
 runSolverPipeline pipeline workItem
-  = do { initial_is <- getTcSInerts
+  = do { wl <- getWorkList
+       ; inerts <- getTcSInerts
+       ; traceTcS "----------------------------- " empty
        ; traceTcS "Start solver pipeline {" $
-                  vcat [ ptext (sLit "work item = ") <+> ppr workItem
-                       , ptext (sLit "inerts    = ") <+> ppr initial_is]
+                  vcat [ 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) }"
-                                       (ptext (sLit "inerts =") <+> ppr final_is)
+                                 ; traceTcS "End solver pipeline (discharged) }" empty
                                  ; return () }
-           ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (ptext (sLit "Kept as inert"))
-                                 ; traceTcS "End solver pipeline (not discharged) }" $
-                                       vcat [ ptext (sLit "final_item =") <+> ppr ct
-                                            , pprTvBndrs (varSetElems $ tyVarsOfCt ct)
-                                            , ptext (sLit "inerts     =") <+> ppr final_is]
-                                 ; insertInertItemTcS ct }
+           ContinueWith ct -> do { addInertCan ct
+                                 ; traceFireTcS (ctEvidence ct) (text "Kept as inert")
+                                 ; traceTcS "End solver pipeline (kept as inert) }" $
+                                            (text "final_item =" <+> ppr ct) }
        }
   where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
                      -> TcS (StopOrContinue Ct)
@@ -743,41 +507,43 @@ data InteractResult
    | IRDelete    -- Delete the existing inert constraint from the inert set
 
 instance Outputable InteractResult where
-  ppr IRKeep    = ptext (sLit "keep")
-  ppr IRReplace = ptext (sLit "replace")
-  ppr IRDelete  = ptext (sLit "delete")
+  ppr IRKeep    = text "keep"
+  ppr IRReplace = text "replace"
+  ppr IRDelete  = text "delete"
 
 solveOneFromTheOther :: CtEvidence  -- Inert
                      -> CtEvidence  -- WorkItem
                      -> TcS (InteractResult, StopNowFlag)
 -- Preconditions:
 -- 1) inert and work item represent evidence for the /same/ predicate
--- 2) ip/class/irred evidence (no coercions) only
+-- 2) ip/class/irred constraints only; not used for equalities
 solveOneFromTheOther ev_i ev_w
-  | isDerived ev_w
+  | isDerived ev_w         -- Work item is Derived; just discard it
   = return (IRKeep, True)
 
-  | isDerived ev_i -- The inert item is Derived, we can just throw it away,
-                   -- The ev_w is inert wrt earlier inert-set items,
-                   -- so it's safe to continue on from this point
-  = return (IRDelete, False)
+  | 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
 
   | CtWanted { ctev_loc = loc_w } <- ev_w
   , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
-  = return (IRDelete, False)
+  = do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
+       ; return (IRDelete, False) }
 
-  | CtWanted { ctev_evar = ev_id } <- ev_w   -- Inert is Given or Wanted
-  = do { setWantedEvBind ev_id (ctEvTerm ev_i)
+  | CtWanted { ctev_dest = dest } <- ev_w
+       -- Inert is Given or Wanted
+  = do { setWantedEvTerm dest (ctEvTerm ev_i)
        ; return (IRKeep, True) }
 
   | CtWanted { ctev_loc = loc_i } <- ev_i   -- Work item is Given
   , 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 (IRKeep, False) } -- Just discard the un-usable Given
+                                  -- This never actually happens because
+                                  -- Givens get processed first
 
-  | CtWanted { ctev_evar = ev_id } <- ev_i   -- Work item is Given
-  = do { setWantedEvBind ev_id (ctEvTerm ev_w)
+  | CtWanted { ctev_dest = dest } <- ev_i
+  = do { setWantedEvTerm dest (ctEvTerm ev_w)
        ; return (IRReplace, True) }
 
   -- So they are both Given
@@ -818,15 +584,6 @@ solveOneFromTheOther ev_i ev_w
 
      has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
 
-prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
--- See Note [Solving superclass constraints] in TcInstDcls
-prohibitedSuperClassSolve from_loc solve_loc
-  | GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
-  , ScOrigin wanted_size <- ctLocOrigin solve_loc
-  = given_size >= wanted_size
-  | otherwise
-  = False
-
 {-
 Note [Replacement vs keeping]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -848,7 +605,7 @@ we keep?  More subtle than you might think!
         8% performance improvement in nofib cryptarithm2, compared to
         just rolling the dice.  I didn't investigate why.
 
-  * Constaints coming from the same level (i.e. same implication)
+  * 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
@@ -856,18 +613,19 @@ we keep?  More subtle than you might think!
          See Note [Solving superclass constraints] in TcInstDcls
 
        - Keep the one that has a non-trivial evidence binding.
-         Note [Tracking redundant constraints] again.
             Example:  f :: (Eq a, Ord a) => blah
-            then we may find [G] sc_sel (d1::Ord a) :: Eq a
+            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 unnecesary munging of the inert set.
+    IRReplace, to avoid unnecessary munging of the inert set.
 
 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 }
 
@@ -901,8 +659,9 @@ 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 `tcEqType` pred)
-                                                 (inert_irreds inerts)
+        (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 )
@@ -914,7 +673,7 @@ interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
                          -- These const upd's assume that solveOneFromTheOther
                          -- has no side effects on InertCans
        ; if stop_now then
-            return (Stop ev_w (ptext (sLit "Irred equal") <+> parens (ppr inert_effect)))
+            return (Stop ev_w (text "Irred equal" <+> parens (ppr inert_effect)))
        ; else
             continueWith workItem }
 
@@ -929,60 +688,311 @@ interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
                    interactDict
 *                                                                               *
 *********************************************************************************
+
+Note [Solving from instances when interacting Dicts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+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#) }
+
+However, 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)
+
+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`.
+
+It is important to emphasize that failure means that we don't produce more
+efficient code, NOT that we fail to typecheck at all! This is purely an
+an optimization: exactly the same programs should typecheck with or without this
+procedure.
 -}
 
 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
-  -- don't ever try to solve CallStack IPs directly from other dicts,
-  -- we always build new dicts instead.
-  -- See Note [Overview of implicit CallStacks]
-  | [_ip, ty] <- tys
-  , isWanted ev_w
-  , Just mkEvCs <- isCallStackIP (ctEvLoc ev_w) cls ty
-  = do let ev_cs =
-             case lookupInertDict inerts cls tys of
-               Just ev | isGiven ev -> mkEvCs (ctEvTerm ev)
-               _ -> mkEvCs (EvCallStack EvCsEmpty)
-
-       -- now we have 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`
-       let ip_ty = mkClassPred cls tys
-       let ev_tm = mkEvCast (EvCallStack ev_cs) (TcCoercion $ wrapIP ip_ty)
-       addSolvedDict ev_w cls tys
-       setWantedEvBind (ctEvId ev_w) ev_tm
-       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 (ptext (sLit "Dict equal") <+> parens (ppr inert_effect)))
-         else
-            continueWith workItem }
-
-  | cls `hasKey` ipClassNameKey
+  | Just ctev_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 [Solving from instances when interacting Dicts]
+         dflags <- getDynFlags
+       ; try_inst_res <- trySolveFromInstance dflags ev_w ctev_i
+       ; case try_inst_res of
+           Just evs -> do
+             { flip mapM_ evs $ \(ev_t, ct_ev, cls, typ) -> do
+               { setWantedEvBind (ctEvId ct_ev) ev_t
+               ; addSolvedDict ct_ev cls typ }
+             ; stopWith ev_w "interactDict/solved from instance" }
+
+           -- We were unable to solve the [W] constraint from in-scope instances
+           -- so we solve it from the matching inert we found
+           Nothing ->  do
+             { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
+             ; traceTcS "lookupInertDict" (ppr inert_effect <+> ppr stop_now)
+             ; 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))
+               else
+                 continueWith workItem } }
+
+  | cls `hasKey` ipClassKey
   , isGiven ev_w
   = interactGivenIP inerts workItem
 
   | otherwise
-  = do { -- Try improvement via functional dependencies;
-         -- but only for Givens and Deriveds
-         -- See Note [When improvement happens during solving]
-         unless (isWanted ev_w) $
-                mapBagM_ (addFunDepWork workItem)
-                         (findDictsByClass (inert_dicts inerts) cls)
+  = do { addFunDepWork inerts ev_w cls
+       ; continueWith workItem  }
+
+interactDict _ wi = pprPanic "interactDict" (ppr wi)
+
+-- See Note [Solving from instances when interacting Dicts]
+trySolveFromInstance :: DynFlags
+                     -> CtEvidence -- Work item
+                     -> CtEvidence -- Inert we want to try to replace
+                     -> TcS (Maybe [(EvTerm, CtEvidence, Class, [TcPredType])])
+                     -- Everything we need to bind a solution for the work item
+                     -- and add the solved Dict to the cache in the main solver.
+trySolveFromInstance dflags ev_w ctev_i
+  | isWanted ev_w
+ && isGiven ctev_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 [Solving from instances when interacting Dicts]
+ && 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.
+ && gopt Opt_SolveConstantDicts dflags
+ -- Enabled by the -fsolve-constant-dicts flag
+  = runMaybeT $ try_solve_from_instance emptyDictMap ev_w
+
+  | otherwise = return Nothing
+  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
+
+    -- 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 :: DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
+    new_wanted_cached cache pty
+      | ClassPred cls tys <- classifyPredType pty
+      = lift $ case findDict cache loc_w cls tys of
+          Just ctev -> return $ Cached (ctEvTerm ctev)
+          Nothing -> Fresh <$> newWantedNC loc_w pty
+      | otherwise = mzero
+
+    -- MaybeT manages early failure if we find a subgoal that cannot be solved
+    -- from instances.
+    -- Why do we need a local cache here?
+    -- 1. We can't use the global cache because it contains givens that
+    --    we specifically don't want to use to solve.
+    -- 2. We need to be able to handle recursive super classes. The
+    --    cache ensures that we remember what we have already tried to
+    --    solve to avoid looping.
+    try_solve_from_instance
+      :: DictMap CtEvidence -> CtEvidence
+      -> MaybeT TcS [(EvTerm, CtEvidence, Class, [TcPredType])]
+    try_solve_from_instance cache ev
+      | ClassPred cls tys <- classifyPredType (ctEvPred ev) = do
+      -- 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.
+      { let cache' = addDict cache cls tys ev
+      ; inst_res <- lift $ match_class_inst dflags cls tys loc_w
+      ; case inst_res of
+          GenInst { lir_new_theta = preds
+                  , lir_mk_ev = mk_ev
+                  , lir_safe_over = safeOverlap }
+            | safeOverlap -> do
+              -- emit work for subgoals but use our local cache so that we can
+              -- solve recursive dictionaries.
+              { evc_vs <- mapM (new_wanted_cached cache') preds
+              ; subgoalBinds <- mapM (try_solve_from_instance cache')
+                                     (freshGoals evc_vs)
+              ; return $ (mk_ev (map getEvTerm evc_vs), ev, cls, preds)
+                       : concat subgoalBinds }
+
+            | otherwise -> mzero
+          _ -> mzero }
+      | 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
+      | isImprovable inert_ev
+      = 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_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 }
 
-       ; continueWith workItem  }
-
-interactDict _ wi = pprPanic "interactDict" (ppr wi)
+{-
+**********************************************************************
+*                                                                    *
+                   Implicit parameters
+*                                                                    *
+**********************************************************************
+-}
 
 interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 -- Work item is Given (?x:ty)
@@ -1004,27 +1014,8 @@ interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
 
 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
 
-addFunDepWork :: Ct -> Ct -> TcS ()
--- Add derived constraints from type-class functional dependencies.
-addFunDepWork work_ct inert_ct
-  = 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
-                -- Also see Note [When improvement happens during solving]
-  where
-    work_pred  = ctPred work_ct
-    inert_pred = ctPred inert_ct
-    work_loc   = ctLoc work_ct
-    inert_loc  = ctLoc inert_ct
-    derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred  work_loc
-                                                        inert_pred inert_loc }
-
-{-
-Note [Shadowing of Implicit Parameters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Shadowing of Implicit Parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider the following example:
 
 f :: (?x :: Char) => Char
@@ -1047,9 +1038,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
@@ -1059,12 +1060,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.
 
@@ -1073,84 +1074,200 @@ I can think of two ways to fix this:
      error if we get multiple givens for the same implicit parameter.
 
 
-*********************************************************************************
-*                                                                               *
+**********************************************************************
+*                                                                    *
                    interactFunEq
-*                                                                               *
-*********************************************************************************
+*                                                                    *
+**********************************************************************
 -}
 
 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 `canRewriteOrSame` 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 `canRewriteOrSame` 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" }
-
-  | not (isWanted ev)  -- Try improvement only for Given/Derived
-                       -- See Note [When improvement happens during solving]
-  , Just ops <- isBuiltInSynFamTyCon_maybe tc
-  = do { let matching_funeqs = findFunEqsByTyCon funeqs tc
-       ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk)
-             do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev })
-                = mapM_ (unifyDerived (ctEvLoc iev) Nominal)
-                        (interact iargs (lookupFlattenTyVar eqs ifsk))
-             do_one ct = pprPanic "interactFunEq" (ppr ct)
-       ; mapM_ do_one matching_funeqs
-       ; traceTcS "builtInCandidates 1: " $ vcat [ ptext (sLit "Candidates:") <+> ppr matching_funeqs
-                                                 , ptext (sLit "TvEqs:") <+> ppr eqs ]
-       ; return (ContinueWith workItem) }
+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 ev inerts tc args fsk
+       ; continueWith work_item }
+
+interactFunEq _ work_item = pprPanic "interactFunEq" (ppr work_item)
+
+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 :: 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'
+--
+-- 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 "Inert eqs:" <+> ppr ieqs ]
+       ; emitFunDepDeriveds improvement_eqns }
 
   | otherwise
-  = return (ContinueWith workItem)
+  = return ()
+
   where
-    eqs    = inert_eqs inerts
-    funeqs = inert_funeqs inerts
-    matching_inerts = findFunEqs funeqs tc args
-
-interactFunEq _ wi = pprPanic "interactFunEq" (ppr wi)
-
-lookupFlattenTyVar :: TyVarEnv EqualCtList -> TcTyVar -> TcType
--- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
--- this is used only when dealing with a CFunEqCan
-lookupFlattenTyVar inert_eqs ftv
-  = case lookupVarEnv inert_eqs ftv of
-      Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _) -> rhs
-      _                                                       -> mkTyVarTy ftv
-
-reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F tys ~ fsk1
-           -> CtEvidence -> TcTyVar    -- Solve this :: F tys ~ fsk2
+    ieqs          = inert_eqs inerts
+    funeqs        = inert_funeqs inerts
+    funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
+    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 <- fam_inj_info
+      =    -- Try improvement from type families with injectivity annotations
+        concatMap (do_one_injective injective_args) funeqs_for_tc
+
+      | otherwise
+      = []
+
+    --------------------
+    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 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)
+
+    --------------------
+    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 (CtGiven { ctev_evar = evar, ctev_loc = loc }) fsk2
-  = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar)
-                         `mkTcTransCo` ctEvCoercion from_this
+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 = mkTcEqPred (mkTyVarTy fsk2) (mkTyVarTy 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] }
 
-reactFunEq from_this fuv1 ev fuv2
-  = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fuv1 $$ ppr ev $$ ppr fuv2)
-       ; dischargeFmv ev fuv2 (ctEvCoercion from_this) (mkTyVarTy fuv1)
-       ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fuv1 $$ ppr ev $$ ppr fuv2) }
+  | CtDerived { ctev_loc = loc } <- solve_this
+  = do { traceTcS "reactFunEq (Derived)" (ppr from_this $$ ppr fsk1 $$
+                                          ppr solve_this $$ ppr fsk2)
+       ; emitNewDerivedEq loc Nominal (mkTyVarTy fsk1) (mkTyVarTy fsk2) }
+              -- FunEqs are always at Nominal role
+
+  | otherwise  -- Wanted
+  = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fsk1 $$
+                                ppr solve_this $$ ppr fsk2)
+       ; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
+       ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
+                                     ppr solve_this $$ ppr fsk2) }
+
+{- 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
+
+Then if we have two CFunEqCan constraints for F with the same RHS
+   F s1 t1 ~ rhs
+   F s2 t2 ~ rhs
+then we can use the injectivity to get a new Derived constraint on
+the injective argument
+  [D] t1 ~ t2
+
+That in turn can help GHC solve constraints that would otherwise require
+guessing.  For example, consider the ambiguity check for
+   f :: F Int b -> Int
+We get the constraint
+   [W] F Int b ~ F Int beta
+where beta is a unification variable.  Injectivity lets us pick beta ~ b.
+
+Injectivity information is also used at the call sites. For example:
+   g = f True
+gives rise to
+   [W] F Int b ~ Bool
+from which we can derive b.  This requires looking at the defining equations of
+a type family, ie. finding equation with a matching RHS (Bool in this example)
+and infering values of type variables (b in this example) from the LHS patterns
+of the matching equation.  For closed type families we have to perform
+additional apartness check for the selected equation to check that the selected
+is guaranteed to fire for given LHS arguments.
+
+These new constraints are simply *Derived* constraints; they have no evidence.
+We could go further and offer evidence from decomposing injective type-function
+applications, but that would require new evidence forms, and an extension to
+FC, so we don't do that right now (Dec 14).
+
+See also Note [Injective type families] in TyCon
+
 
-{-
 Note [Cache-caused loops]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
@@ -1233,99 +1350,101 @@ The second is the right thing to do.  Hence the isMetaTyVarTy
 test when solving pairwise CFunEqCan.
 
 
-*********************************************************************************
-*                                                                               *
+**********************************************************************
+*                                                                    *
                    interactTyVarEq
-*                                                                               *
-*********************************************************************************
+*                                                                    *
+**********************************************************************
 -}
 
-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 })
+inertsCanDischarge :: InertCans -> TcTyVar -> TcType -> CtEvidence
+                   -> 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 ev
   | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
                              <- findTyEqs inerts tv
-                         , ev_i `canRewriteOrSame` ev
+                         , ev_i `eqCanDischarge` ev
                          , rhs_i `tcEqType` rhs ]
-  =  -- Inert:     a ~ b
-     -- Work item: a ~ b
-    do { setEvBindIfWanted ev (ctEvTerm ev_i)
-       ; stopWith ev "Solved from inert" }
+  =  -- Inert:     a ~ ty
+     -- Work item: a ~ ty
+    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 }
                              <- findTyEqs inerts tv_rhs
-                         , ev_i `canRewriteOrSame` ev
+                         , ev_i `eqCanDischarge` ev
                          , rhs_i `tcEqType` mkTyVarTy tv ]
   =  -- Inert:     a ~ b
      -- Work item: b ~ a
-    do { setEvBindIfWanted ev
-                   (EvCoercion (mkTcSymCo (ctEvCoercion ev_i)))
-       ; stopWith ev "Solved from inert (r)" }
+     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 <- ctEvFlavour ev    -- 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 ev
+  = 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" }
+
+  | ReprEq <- eq_rel   -- We never solve representational
+  = unsolved_inert     -- equalities by unification
+
+  | isGiven ev         -- See Note [Touchables and givens]
+  = unsolved_inert
 
   | 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 <- kickOutRewritable Given NomEq tv
-                               -- Given because the tv := xi is given
-                               -- NomEq because only nom. equalities are solved
-                               -- by unification
-                 ; return (Stop ev (ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked)) }
-
-         else do { traceTcS "Can't solve tyvar equality"
-                       (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 ])
-                 ; n_kicked <- kickOutRewritable (ctEvFlavour ev)
-                                                 (ctEvEqRel ev)
-                                                 tv
-                 ; updInertCans (\ ics -> addInertCan ics workItem)
-                 ; return (Stop ev (ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked)) } }
+                 ; n_kicked <- kickOutAfterUnification tv
+                 ; return (Stop ev (text "Solved by unification" <+> ppr_kicked n_kicked)) }
 
-interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
+         else unsolved_inert }
 
--- @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
+    unsolved_inert
+      = 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) ])
+           ; addInertEq workItem
+           ; stopWith ev "Kept as inert" }
+
+interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
 
 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
 -- Solve with the identity coercion
--- Precondition: kind(xi) is a sub-kind of kind(tv)
+-- Precondition: kind(xi) equals kind(tv)
 -- Precondition: CtEvidence is Wanted or Derived
 -- Precondition: CtEvidence is nominal
 -- Returns: workItem where
@@ -1341,174 +1460,20 @@ solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
 solveByUnification wd tv xi
   = do { let tv_ty = mkTyVarTy tv
        ; traceTcS "Sneaky unification:" $
-                       vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
+                       vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr xi,
                              text "Coercion:" <+> pprEq tv_ty xi,
                              text "Left Kind is:" <+> ppr (typeKind tv_ty),
                              text "Right Kind is:" <+> ppr (typeKind xi) ]
 
-       ; let xi' = defaultKind xi
-               -- We only instantiate kind unification variables
-               -- with simple kinds like *, not OpenKind or ArgKind
-               -- cf TcUnify.uUnboundKVar
-
-       ; unifyTyVar tv xi'
-       ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi')) }
-
+       ; unifyTyVar tv xi
+       ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi)) }
 
 ppr_kicked :: Int -> SDoc
 ppr_kicked 0 = empty
-ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
-
-kickOutRewritable :: CtFlavour    -- Flavour of the equality that is
-                                  -- being added to the inert set
-                  -> EqRel        -- of the new equality
-                  -> TcTyVar      -- The new equality is tv ~ ty
-                  -> TcS Int
-kickOutRewritable new_flavour new_eq_rel new_tv
-  | not ((new_flavour, new_eq_rel) `eqCanRewriteFR` (new_flavour, new_eq_rel))
-  = return 0  -- If new_flavour can't rewrite itself, it can't rewrite
-              -- anything else, so no need to kick out anything
-              -- This is a common case: wanteds can't rewrite wanteds
-
-  | otherwise
-  = do { ics <- getInertCans
-       ; let (kicked_out, ics') = kick_out new_flavour new_eq_rel new_tv ics
-       ; setInertCans ics'
-       ; updWorkListTcS (appendWorkList kicked_out)
-
-       ; unless (isEmptyWorkList kicked_out) $
-         csTraceTcS $
-         hang (ptext (sLit "Kick out, tv =") <+> ppr new_tv)
-            2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
-                    , text "n-kept fun-eqs =" <+> int (sizeFunEqMap (inert_funeqs ics'))
-                    , ppr kicked_out ])
-       ; return (workListSize kicked_out) }
-
-kick_out :: CtFlavour -> EqRel -> TcTyVar -> InertCans -> (WorkList, InertCans)
-kick_out new_flavour new_eq_rel new_tv (IC { inert_eqs      = tv_eqs
-                                           , inert_dicts    = dictmap
-                                           , inert_safehask = safehask
-                                           , inert_funeqs   = funeqmap
-                                           , inert_irreds   = irreds
-                                           , inert_insols   = insols })
-  = (kicked_out, inert_cans_in)
-  where
-                -- NB: Notice that don't rewrite
-                -- inert_solved_dicts, and inert_solved_funeqs
-                -- optimistically. But when we lookup we have to
-                -- take the substitution into account
-    inert_cans_in = IC { inert_eqs      = tv_eqs_in
-                       , inert_dicts    = dicts_in
-                       , inert_safehask = safehask
-                       , inert_funeqs   = feqs_in
-                       , inert_irreds   = irs_in
-                       , inert_insols   = insols_in }
-
-    kicked_out = WL { wl_eqs    = tv_eqs_out
-                    , wl_funeqs = feqs_out
-                    , wl_rest   = bagToList (dicts_out `andCts` irs_out
-                                             `andCts` insols_out)
-                    , wl_implics = emptyBag }
-
-    (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
-    (feqs_out,   feqs_in)   = partitionFunEqs  kick_out_ct funeqmap
-    (dicts_out,  dicts_in)  = partitionDicts   kick_out_ct dictmap
-    (irs_out,    irs_in)    = partitionBag     kick_out_irred irreds
-    (insols_out, insols_in) = partitionBag     kick_out_ct    insols
-      -- Kick out even insolubles; see Note [Kick out insolubles]
-
-    can_rewrite :: CtEvidence -> Bool
-    can_rewrite = ((new_flavour, new_eq_rel) `eqCanRewriteFR`) . ctEvFlavourRole
-
-    kick_out_ct :: Ct -> Bool
-    kick_out_ct ct = kick_out_ctev (ctEvidence ct)
-
-    kick_out_ctev :: CtEvidence -> Bool
-    kick_out_ctev ev =  can_rewrite ev
-                     && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
-         -- See Note [Kicking out inert constraints]
-
-    kick_out_irred :: Ct -> Bool
-    kick_out_irred ct =  can_rewrite (cc_ev ct)
-                      && new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct)
-          -- See Note [Kicking out Irreds]
-
-    kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList)
-                 -> ([Ct], TyVarEnv EqualCtList)
-    kick_out_eqs eqs (acc_out, acc_in)
-      = (eqs_out ++ acc_out, case eqs_in of
-                               []      -> acc_in
-                               (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in)
-      where
-        (eqs_in, eqs_out) = partition keep_eq eqs
-
-    -- implements criteria K1-K3 in Note [The inert equalities] in TcFlatten
-    keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
-                      , cc_eq_rel = eq_rel })
-      | tv == new_tv
-      = not (can_rewrite ev)  -- (K1)
+ppr_kicked n = parens (int n <+> text "kicked out")
 
-      | otherwise
-      = check_k2 && check_k3
-      where
-        check_k2 = not (ev `eqCanRewrite` ev)
-                || not (can_rewrite ev)
-                || not (new_tv `elemVarSet` tyVarsOfType rhs_ty)
-
-        check_k3
-          | can_rewrite ev
-          = case eq_rel of
-              NomEq  -> not (rhs_ty `eqType` mkTyVarTy new_tv)
-              ReprEq -> not (isTyVarExposed new_tv rhs_ty)
-
-          | otherwise
-          = True
-
-    keep_eq ct = pprPanic "keep_eq" (ppr ct)
-
-{-
-Note [Kicking out inert constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Given a new (a -> ty) inert, we want to kick out an existing inert
-constraint if
-  a) the new constraint can rewrite the inert one
-  b) 'a' is free in the inert constraint (so that it *will*)
-     rewrite it if we kick it out.
-
-For (b) we use tyVarsOfCt, which returns the type variables /and
-the kind variables/ that are directly visible in the type. Hence we
-will have exposed all the rewriting we care about to make the most
-precise kinds visible for matching classes etc. No need to kick out
-constraints that mention type variables whose kinds contain this
-variable!  (Except see Note [Kicking out Irreds].)
-
-Note [Kicking out Irreds]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-There is an awkward special case for Irreds.  When we have a
-kind-mis-matched equality constraint (a:k1) ~ (ty:k2), we turn it into
-an Irred (see Note [Equalities with incompatible kinds] in
-TcCanonical). So in this case the free kind variables of k1 and k2
-are not visible.  More precisely, the type looks like
-   (~) k1 (a:k1) (ty:k2)
-because (~) has kind forall k. k -> k -> Constraint.  So the constraint
-itself is ill-kinded.  We can "see" k1 but not k2.  That's why we use
-closeOverKinds to make sure we see k2.
-
-This is not pretty. Maybe (~) should have kind
-   (~) :: forall k1 k1. k1 -> k2 -> Constraint
-
-Note [Kick out insolubles]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have an insoluble alpha ~ [alpha], which is insoluble
-because an occurs check.  And then we unify alpha := [Int].
-Then we really want to rewrite the insouluble to [Int] ~ [[Int]].
-Now it can be decomposed.  Otherwise we end up with a "Can't match
-[Int] ~ [[Int]]" which is true, but a bit confusing because the
-outer type constructors match.
-
-
-Note [Avoid double unifications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Avoid double unifications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The spontaneous solver has to return a given which mentions the unified unification
 variable *on the left* of the equality. Here is what happens if not:
   Original wanted:  (a ~ alpha),  (alpha ~ Int)
@@ -1547,37 +1512,108 @@ 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)
+          ; mapM_ (unifyDerived loc Nominal) eqs }
      | otherwise
-     = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
+     = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ 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)
        = unifyDerived loc Nominal $
-         Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
+         Pair (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2)
 
 {-
-*********************************************************************************
-*                                                                               *
+**********************************************************************
+*                                                                    *
                        The top-reaction Stage
-*                                                                               *
-*********************************************************************************
+*                                                                    *
+**********************************************************************
 -}
 
 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
 topReactionsStage wi
  = do { tir <- doTopReact wi
       ; case tir of
-          ContinueWith wi -> return (ContinueWith wi)
-          Stop ev s       -> return (Stop ev (ptext (sLit "Top react:") <+> s)) }
+          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
@@ -1594,226 +1630,216 @@ doTopReact work_item
                               ; doTopReactDict inerts work_item }
            CFunEqCan {} -> doTopReactFunEq work_item
            _  -> -- Any other work item does not react with any top-level equations
-                 return (ContinueWith work_item)  }
+                 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 preds _ s -> do { mapM_ (emitNewDerived dict_loc) preds
-                                       ; unless s $
-                                           insertSafeOverlapFailureTcS work_item
-                                       ; stopWith fl "Dict/Top (solved)" }
+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         -> 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 }
 
-               NoInstance        -> do { -- If there is no instance, try improvement
-                                         try_fundep_improvement
-                                       ; continueWith work_item } }
+doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
 
-  | otherwise  -- Wanted, but not cached
-   = do { dflags <- getDynFlags
-        ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
-        ; case lkup_inst_res of
-               GenInst theta mk_ev s -> do { addSolvedDict fl cls xis
-                                           ; unless s $
-                                               insertSafeOverlapFailureTcS work_item
-                                           ; solve_from_instance theta mk_ev }
-               NoInstance            -> 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)
+reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
+                  -> TcS (StopOrContinue Ct)
+-- We have found an applicable top-level axiom: use it to reduce
+-- Precondition: fsk is not free in rhs_ty
+--               old_ev is not Derived
+reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
+  | isDerived old_ev
+  = do { emitNewDerivedEq loc Nominal (mkTyVarTy fsk) rhs_ty
+       ; stopWith old_ev "Fun/Top (derived)" }
+
+  | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
+  , isTypeFamilyTyCon tc
+  , tc_args `lengthIs` tyConArity tc    -- Short-cut
+  = -- RHS is another type-family application
+    -- Try shortcut; see Note [Top-level reductions for type functions]
+    shortCutReduction old_ev fsk ax_co tc tc_args
+
+  | 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)" }
+
+  | otherwise   -- So old_ev is Wanted (cannot be Derived)
+  = ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
+           , ppr old_ev $$ ppr rhs_ty )
+           -- Guaranteed by Note [FunEq occurs-check principle]
+    do { dischargeFmv 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)" }
 
-     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] -> ([EvId] -> 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 (newWantedEvVar deeper_loc) theta
-             ; setWantedEvBind (ctEvId fl) (mk_ev (map (ctEvId . fst) evc_vars))
-             ; emitWorkNC (freshGoals evc_vars)
-             ; stopWith fl "Dict/Top (solved, more work)" }
+  where
+    loc = ctEvLoc old_ev
+    deeper_loc = bumpCtLocDepth loc
 
-     -- We didn't solve it; so try functional dependencies with
-     -- the instance environment, and return
-     -- We just land here for Given and Derived;
-     -- See Note [When improvement happens during solving]
-     -- See also Note [Weird fundeps]
-     try_fundep_improvement
-        = do { instEnvs <- getInstEnvs
-             ; emitFunDepDeriveds $
-               improveFromInstEnv instEnvs mk_ct_loc dict_pred }
+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 ()
 
-     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 }
+  | otherwise
+  = do { ieqs <- getInertEqs
+       ; fam_envs <- getFamInstEnvs
+       ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
+                                    (lookupFlattenTyVar ieqs fsk)
+       ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr fsk
+                                          , ppr eqns ])
+       ; mapM_ (unifyDerived loc Nominal) eqns }
+  where
+    loc = ctEvLoc ev
+
+improve_top_fun_eqs :: FamInstEnvs
+                    -> TyCon -> [TcType] -> TcType
+                    -> 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 <- 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.
+    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 <- tyConInjectivityInfo fam_tc
+  = concatMapM (injImproveEqns injective_args) $
+    buildImprovementData (fromBranches (co_ax_branches ax))
+                         cab_tvs cab_lhs cab_rhs Just
 
-doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
+  | otherwise
+  = return []
 
---------------------
-doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
--- Note [Short cut for top-level reaction]
-doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
-                                     , cc_tyargs = args , cc_fsk = fsk })
-  = ASSERT(isTypeFamilyTyCon fam_tc) -- No associated data families
-                                     -- have reached this far
-    -- Look up in top-level instances, or built-in axiom
-    do { match_res <- matchFam fam_tc args   -- See Note [MATCHING-SYNONYMS]
-       ; case match_res of {
-           Nothing -> do { try_improve
-                         ; continueWith work_item } ;
-           Just (ax_co, rhs_ty)
-
-    -- Found a top-level instance
-
-    | 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 (mkTcEqPred (mkTyVarTy fsk) rhs_ty,
-                                                EvCoercion final_co)
-          ; emitWorkNC [new_ev]   -- Non-canonical; that will mean we flatten rhs_ty
-          ; stopWith old_ev "Fun/Top (given)" }
-
-    | not (fsk `elemVarSet` tyVarsOfType rhs_ty)
-    -> do { dischargeFmv 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 <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
-          ; emitWorkNC [new_ev]
-              -- By emitting this as non-canonical, we deal with all
-              -- flattening, occurs-check, and ufsk := ufsk issues
-          ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
-              --    ax_co :: fam_tc args ~ rhs_ty
-              --   new_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
-
-    try_improve
-      | not (isWanted old_ev)  -- Try improvement only for Given/Derived constraints
-                               -- See Note [When improvement happens during solving]
-      , Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
-      = do { inert_eqs <- getInertEqs
-           ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk)
-           ; mapM_ (unifyDerived loc Nominal) eqns }
-      | otherwise
-      = return ()
+      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, [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 axiomTVs axiomLHS axiomRHS wrap =
+          [ (ax_args, subst, unsubstTvs, wrap axiom)
+          | axiom <- axioms
+          , let ax_args = axiomLHS axiom
+                ax_rhs  = axiomRHS axiom
+                ax_tvs  = axiomTVs axiom
+          , Just subst <- [tcUnifyTyWithTFs False ax_rhs rhs_ty]
+          , 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, [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 ] }
 
-doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
 
 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
                   -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
 -- See Note [Top-level reductions for type functions]
 shortCutReduction old_ev fsk ax_co fam_tc tc_args
-  | isGiven old_ev
-  = ASSERT( ctEvEqRel old_ev == NomEq )
+  = 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 <- newGivenEvVar deeper_loc
-                         ( mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
+       ; 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) )
 
-       ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
-       ; emitWorkCt new_ct
-       ; stopWith old_ev "Fun/Top (given, shortcut)" }
-
-  | otherwise
-  = ASSERT( not (isDerived old_ev) )   -- Caller ensures this
-    ASSERT( ctEvEqRel old_ev == NomEq )
-    do { (xis, cos) <- flattenManyNom old_ev tc_args
-               -- ax_co :: F args ~ G tc_args
-               -- cos   :: xis ~ tc_args
-               -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
-               -- new_ev :: G xis ~ fsk
-               -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
-
-       ; new_ev <- newWantedEvVarNC deeper_loc
-                                    (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
-       ; setWantedEvBind (ctEvId old_ev)
-                   (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
-                                      `mkTcTransCo` ctEvCoercion new_ev))
-
-       ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
-       ; emitWorkCt new_ct
-       ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
+           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
+                ; 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)" }
   where
-    loc = ctEvLoc old_ev
-    deeper_loc = bumpCtLocDepth loc
+    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
+-- Precondition: fmv is not filled, and fmv `notElem` xi
+--               ev is Wanted
 --
 -- Then set fmv := xi,
---      set ev := co
+--      set ev  := co
 --      kick out any inert things that are now rewritable
-dischargeFmv ev fmv co xi
-  = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
-    do { case ev of
-           CtWanted { ctev_evar = evar } -> setWantedEvBind evar (EvCoercion co)
-           CtDerived {}                  -> return ()  -- Happens during improvement
-           CtGiven {}                    -> pprPanic "dischargeFmv" (ppr ev)
-       ; unifyTyVar fmv xi
-       ; n_kicked <- kickOutRewritable Given NomEq fmv
-       ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
+--
+-- Does not evaluate 'co' if 'ev' is Derived
+dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
+  = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
+    do { setWantedEvTerm dest (EvCoercion co)
+       ; unflattenFmv fmv xi
+       ; n_kicked <- kickOutAfterUnification fmv
+       ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
+dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev)
 
 {- Note [Top-level reductions for type functions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1827,15 +1853,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
@@ -1867,12 +1892,42 @@ 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
 to see if we have reduced (FunExpensive big-type) before, lest we
 simply repeat it.  Hence the lookup in inert_solved_funeqs.  Moreover
-we must use `canRewriteOrSame` because both uses might (say) be Wanteds,
+we must use `funEqCanDischarge` because both uses might (say) be Wanteds,
 and we *still* want to save the re-computation.
 
 Note [MATCHING-SYNONYMS]
@@ -1881,144 +1936,196 @@ 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!  Infnite loop.
+
+This all sesms 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
-
-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 [When improvement happens during solving]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Improvement for functional dependencies or type-function injectivity
-means emitting a Derived equality constraint by interacting the work
-item with an inert item, or with the top-level instances.  e.g.
-
-       class C a b | a -> b
-       [W] C a b, [W] C a c  ==>  [D] b ~ c
-
-We fire the fundep improvement if the "work item" is Given or Derived,
-but not Wanted.  Reason:
-
- * Given: we want to spot Given/Given inconsistencies because that means
-          unreachable code.  See typecheck/should_fail/FDsFromGivens
-
- * Derived: during the improvement phase (i.e. when handling Derived
-            constraints) we also do improvement for functional dependencies. e.g.
-            And similarly wrt top-level instances.
-
- * Wanted: spotting fundep improvements is somewhat inefficient, and
-           and if we can solve without improvement so much the better.
-           So we don't bother to do this when solving Wanteds, instead
-           leaving it for the try_improvement loop
-
-Example (tcfail138)
-    class L a b | a -> b
-    class (G a, L a b) => C a b
-
-    instance C a b' => G (Maybe a)
-    instance C a b  => C (Maybe a) a
-    instance L (Maybe a) a
+{- *******************************************************************
+*                                                                    *
+         Top-level reaction for class constraints (CDictCan)
+*                                                                    *
+**********************************************************************-}
 
-When solving the superclasses of the (C (Maybe a) a) instance, we get
-  [G] C a b, and hance by superclasses, [G] G a, [G] L a b
-  [W] G (Maybe a)
-Use the instance decl to get
-  [W] C a beta
+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 }
 
-During improvement (see Note [The improvement story]) we generate the superclasses
-of (C a beta): [D] L a beta.  Now using fundeps, combine with [G] L a b to get
-[D] beta ~ b, which is what we want.
+  | Just ev <- lookupSolvedDict inerts dict_loc cls xis   -- Cached
+  = do { setEvBindIfWanted fl (ctEvTerm ev)
+       ; stopWith fl "Dict/Top (cached)" }
 
+  | otherwise  -- Wanted or Derived, 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 { traceTcS "doTopReact/found instance for" $ ppr fl
+                    ; checkReductionDepth deeper_loc dict_pred
+                    ; unless s $ insertSafeOverlapFailureTcS work_item
+                    ; if isDerived fl then finish_derived theta
+                                      else finish_wanted  theta mk_ev }
+               NoInstance ->
+                 do { when (isImprovable fl) $
+                      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)
 
-Note [Weird fundeps]
-~~~~~~~~~~~~~~~~~~~~
-Consider   class Het a b | a -> b where
-              het :: m (f c) -> a -> m b
+     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
 
-           class GHet (a :: * -> *) (b :: * -> *) | a -> b
-           instance            GHet (K a) (K [a])
-           instance Het a b => GHet (K a) (K b)
+     finish_wanted :: [TcPredType]
+                   -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct)
+      -- Precondition: evidence term matches the predicate workItem
+     finish_wanted theta mk_ev
+        = do { addSolvedDict fl cls xis
+             ; 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 wanted)" }
 
-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.
+     finish_derived 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 deeper_loc theta
+            ; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc))
+            ; stopWith fl "Dict/Top (solved derived)" }
 
-Trac #7875 is a case in point.
+     -- 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 }
 
-Note [Overriding implicit parameters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-   f :: (?x::a) -> Bool -> a
+     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 }
 
-   g v = let ?x::Int = 3
-         in (f v, let ?x::Bool = True in f v)
+doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
 
-This should probably be well typed, with
-   g :: Bool -> (Int, Bool)
 
-So the inner binding for ?x::Bool *overrides* the outer one.
-Hence a work-item Given overrides an inert-item Given.
--}
+{- *******************************************************************
+*                                                                    *
+                       Class lookup
+*                                                                    *
+**********************************************************************-}
 
 -- | Indicates if Instance met the Safe Haskell overlapping instances safety
 -- check.
@@ -2029,137 +2136,63 @@ type SafeOverlapping = Bool
 
 data LookupInstResult
   = NoInstance
-  | GenInst [TcPredType] ([EvId] -> EvTerm) SafeOverlapping
+  | GenInst { lir_new_theta :: [TcPredType]
+            , lir_mk_ev     :: [EvTerm] -> EvTerm
+            , lir_safe_over :: SafeOverlapping }
 
 instance Outputable LookupInstResult where
-  ppr NoInstance       = text "NoInstance"
-  ppr (GenInst ev _ s) = text "GenInst" <+> ppr ev <+> ss
+  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 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]
-matchClassInst dflags inerts clas tys loc
-  | not (xopt Opt_IncoherentInstances dflags)
+  | not (xopt LangExt.IncoherentInstances dflags)
+  , not (naturallyCoherentClass clas)
+  , let matchable_givens = matchableGivens loc pred inerts
   , not (isEmptyBag matchable_givens)
   = do { traceTcS "Delaying instance application" $
-              vcat [ text "Work item=" <+> pprType (mkClassPred clas tys)
-                   , text "Relevant given dictionaries="
-                           <+> ppr matchable_givens ]
+           vcat [ text "Work item=" <+> pprClassPred clas tys
+                , text "Potential matching givens:" <+> ppr matchable_givens ]
        ; return NoInstance }
   where
-     matchable_givens :: Cts
-     matchable_givens = filterBag matchable_given $
-                        findDictsByClass (inert_dicts $ inert_cans inerts) clas
-
-     matchable_given ct
-       | CDictCan { cc_class = clas_g, cc_tyargs = sys, cc_ev = fl } <- ct
-       , CtGiven { ctev_loc = loc_g } <- fl
-       , Just {} <- tcUnifyTys bind_meta_tv tys sys
-       , not (prohibitedSuperClassSolve loc_g loc)
-       = ASSERT( clas_g == clas ) True
-     matchable_given _ = False
-
-     bind_meta_tv :: TcTyVar -> BindFlag
-     -- Any meta tyvar may be unified later, so we treat it as
-     -- bindable when unifying with givens. That ensures that we
-     -- conservatively assume that a meta tyvar might get unified with
-     -- something that matches the 'given', until demonstrated
-     -- otherwise.
-     bind_meta_tv tv | isMetaTyVar tv = BindMe
-                     | otherwise      = Skolem
-
-matchClassInst _ _ clas [ ty ] _
-  | className clas == knownNatClassName
-  , Just n <- isNumLitTy ty = makeDict (EvNum n)
-
-  | className clas == knownSymbolClassName
-  , Just s <- isStrLitTy ty = makeDict (EvStr s)
-
-  where
-  {- This 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
-  -}
-  makeDict 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 [] (\_ -> ev_tm) True
-
-    | otherwise
-    = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
-                     $$ vcat (map (ppr . idType) (classMethods clas)))
-
-matchClassInst _ _ clas ts _
-  | isCTupleClass clas
-  , let data_con = tyConSingleDataCon (classTyCon clas)
-        tuple_ev = EvDFunApp (dataConWrapId data_con) ts
-  = return (GenInst ts tuple_ev True)
-            -- The dfun is the data constructor!
-
-matchClassInst _ _ clas [k,t] _
-  | className clas == typeableClassName
-  = matchTypeableClass clas k t
-
-matchClassInst dflags _ clas tys loc
-   = do { traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred ]
-        ; 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 theta (EvDFunApp dfun_id tys) so }
-
+matchClassInst dflags _ clas tys loc
+ = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr (mkClassPred clas tys) <+> char '{'
+      ; 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
+  | cls_name == hasFieldClassName     = matchHasField dflags clas tys loc
+  | otherwise                         = matchInstEnv dflags clas tys loc
+  where
+    cls_name = className clas
+
+-- | If a class is "naturally coherent", then we needn't worry at all, in any
+-- way, about overlapping/incoherent instances. Just solve the thing!
+naturallyCoherentClass :: Class -> Bool
+-- See also Note [The equality class story] in TysPrim.
+naturallyCoherentClass cls
+  = isCTupleClass cls ||   -- See "Tuple classes" in Note [Instance and Given overlap]
+    cls `hasKey` heqTyConKey ||
+    cls `hasKey` eqTyConKey ||
+    cls `hasKey` coercibleTyConKey ||
+    cls `hasKey` typeableClassKey
 
 {- Note [Instance and Given overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2172,21 +2205,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
@@ -2201,6 +2235,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
@@ -2208,6 +2249,15 @@ Other notes:
 
 * Another "live" example is Trac #10195; another is #10177.
 
+* 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 the "instance"
+  for class tuples is bidirectional: the Given can also be decomposed
+  to provide the pieces.
+
 * We ignore the overlap problem if -XIncoherentInstances is in force:
   see Trac #6002 for a worked-out example where this makes a
   difference.
@@ -2222,85 +2272,241 @@ Other notes:
 
   But for the Given Overlap check our goal is just related to completeness of
   constraint solving.
+
+* 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].
 -}
 
--- | Is the constraint for an implicit CallStack parameter?
-isCallStackIP :: CtLoc -> Class -> Type -> Maybe (EvTerm -> EvCallStack)
-isCallStackIP loc cls ty
-  | Just (tc, []) <- splitTyConApp_maybe ty
-  , cls `hasKey` ipClassNameKey && tc `hasKey` callStackTyConKey
-  = occOrigin (ctLocOrigin loc)
+
+{- *******************************************************************
+*                                                                    *
+                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
-  -- We only want to grab constraints that arose due to the use of an IP or a
-  -- function call. See Note [Overview of implicit CallStacks]
-  occOrigin (OccurrenceOf n)
-    = Just (EvCsPushCall n locSpan)
-  occOrigin (IPOccOrigin n)
-    = Just (EvCsTop ('?' `consFS` hsIPNameFS n) locSpan)
-  occOrigin _
-    = Nothing
-  locSpan
-    = ctLocSpan loc
-isCallStackIP _ _ _
-  = Nothing
+     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.
-matchTypeableClass :: Class -> Kind -> Type -> TcS LookupInstResult
-matchTypeableClass clas _k t
-
-  -- See Note [No Typeable for qualified types]
-  | isForAllTy t                               = return NoInstance
-  -- Is the type of the form `C => t`?
-  | Just (t1,_) <- splitFunTy_maybe t,
-    isConstraintKind (typeKind t1)             = return NoInstance
-
-  | Just (tc, ks) <- splitTyConApp_maybe t
-  , all isKind ks                              = doTyCon tc ks
-  | Just (f,kt)       <- splitAppTy_maybe t    = doTyApp f kt
-  | Just _            <- isNumLitTy t          = mkSimpEv (EvTypeableTyLit t)
-  | Just _            <- isStrLitTy t          = mkSimpEv (EvTypeableTyLit t)
-  | otherwise                                  = return NoInstance
+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
+  | isConstraintKind t                     = doTyConApp clas t constraintKindTyCon []
+  | Just (arg,ret) <- splitFunTy_maybe t   = doFunTy    clas t arg ret
+  | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
+  , onlyNamedBndrsApplied tc ks            = doTyConApp clas t tc ks
+  | Just (f,kt)   <- splitAppTy_maybe t    = doTyApp    clas t f kt
+
+matchTypeable _ _ = return NoInstance
+
+-- | Representation for a type @ty@ of the form @arg -> ret@.
+doFunTy :: Class -> Type -> Type -> Type -> TcS LookupInstResult
+doFunTy clas ty arg_ty ret_ty
+  = do { let preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
+             build_ev [arg_ev, ret_ev] =
+                 EvTypeable ty $ EvTypeableTrFun arg_ev ret_ev
+             build_ev _ = panic "TcInteract.doFunTy"
+       ; return $ GenInst preds build_ev True
+       }
 
-  where
-  -- Representation for type constructor applied to some kinds
-  doTyCon tc ks =
-    case mapM kindRep ks of
-      Nothing    -> return NoInstance
-      Just kReps -> mkSimpEv (EvTypeableTyCon tc kReps)
-
-  {- 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 f tk
-    | isKind tk
-    = return NoInstance -- We can't solve until we know the ctr.
-    | otherwise
-    = return $ GenInst [mk_typeable_pred f, mk_typeable_pred tk]
-                       (\[t1,t2] -> EvTypeable $ EvTypeableTyApp (EvId t1,f) (EvId t2,tk))
-                       True
+-- | Representation for type constructor applied to some kinds.
+-- 'onlyNamedBndrsApplied' has ensured that this application results in a type
+-- of monomorphic kind (e.g. all kind variables have been instantiated).
+doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcS LookupInstResult
+doTyConApp clas ty tc kind_args
+  = return $ GenInst (map (mk_typeable_pred clas) kind_args)
+                     (\kinds -> EvTypeable ty $ EvTypeableTyCon tc kinds)
+                     True
+
+-- | Representation for TyCon applications of a concrete kind. 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 isNamedTyConBinder used_bndrs &&
+   not (any isNamedTyConBinder 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 (map (mk_typeable_pred clas) [f, 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,
+via doTyApp, until we get to a *kind* instantiation.  Example
+   Proxy :: forall k. k -> *
 
-  -- Representation for concrete kinds.  We just use the kind itself,
-  -- but first check to make sure that it is "simple" (i.e., made entirely
-  -- out of kind constructors).
-  kindRep ki = do (_,ks) <- splitTyConApp_maybe ki
-                  mapM_ kindRep ks
-                  return ki
+To solve Typeable (Proxy (* -> *) Maybe) we
+  - First decompose with doTyApp,
+    to get (Typeable (Proxy (* -> *))) and Typeable Maybe
+  - Then solve (Typeable (Proxy (* -> *))) with doTyConApp
 
-  -- Emit a `Typeable` constraint for the given type.
-  mk_typeable_pred ty = mkClassPred clas [ typeKind ty, ty ]
+If we attempt to short-cut by solving it all at once, via
+doTyConApp
 
-  mkSimpEv ev = return $ GenInst [] (\_ -> EvTypeable ev) True
+(this note is sadly truncated FIXME)
 
-{- Note [No Typeable for polytype or for constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+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)
@@ -2314,9 +2520,152 @@ a TypeRep for them.  For qualified but not polymorphic types, like
  * 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.
+ * 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.
+-}
+
+{- ********************************************************************
+*                                                                     *
+                   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 })
+  where
+    args' = [k, k, t1, t2]
+matchLiftedCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
+
+
+{- ********************************************************************
+*                                                                     *
+              Class lookup for overloaded record fields
+*                                                                     *
+***********************************************************************-}
+
+{-
+Note [HasField instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+
+    data T y = MkT { foo :: [y] }
+
+and `foo` is in scope.  Then GHC will automatically solve a constraint like
+
+    HasField "foo" (T Int) b
+
+by emitting a new wanted
+
+    T alpha -> [alpha] ~# T Int -> b
+
+and building a HasField dictionary out of the selector function `foo`,
+appropriately cast.
+
+The HasField class is defined (in GHC.Records) thus:
+
+    class HasField (x :: k) r a | x r -> a where
+      getField :: r -> a
+
+Since this is a one-method class, it is represented as a newtype.
+Hence we can solve `HasField "foo" (T Int) b` by taking an expression
+of type `T Int -> b` and casting it using the newtype coercion.
+Note that
+
+    foo :: forall y . T y -> [y]
+
+so the expression we construct is
+
+    foo @alpha |> co
+
+where
+
+    co :: (T alpha -> [alpha]) ~# HasField "foo" (T Int) b
+
+is built from
+
+    co1 :: (T alpha -> [alpha]) ~# (T Int -> b)
+
+which is the new wanted, and
+
+    co2 :: (T Int -> b) ~# HasField "foo" (T Int) b
+
+which can be derived from the newtype coercion.
+
+If `foo` is not in scope, or has a higher-rank or existentially
+quantified type, then the constraint is not solved automatically, but
+may be solved by a user-supplied HasField instance.  Similarly, if we
+encounter a HasField constraint where the field is not a literal
+string, or does not belong to the type, then we fall back on the
+normal constraint solver behaviour.
 -}
+
+-- See Note [HasField instances]
+matchHasField :: DynFlags -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
+matchHasField dflags clas tys loc
+  = do { fam_inst_envs <- getFamInstEnvs
+       ; rdr_env       <- getGlobalRdrEnvTcS
+       ; case tys of
+           -- We are matching HasField {k} x r a...
+           [_k_ty, x_ty, r_ty, a_ty]
+               -- x should be a literal string
+             | Just x <- isStrLitTy x_ty
+               -- r should be an applied type constructor
+             , Just (tc, args) <- tcSplitTyConApp_maybe r_ty
+               -- use representation tycon (if data family); it has the fields
+             , let r_tc = fstOf3 (tcLookupDataFamInst fam_inst_envs tc args)
+               -- x should be a field of r
+             , Just fl <- lookupTyConFieldLabel x r_tc
+               -- the field selector should be in scope
+             , Just gre <- lookupGRE_FieldLabel rdr_env fl
+
+             -> do { sel_id <- tcLookupId (flSelector fl)
+                   ; (tv_prs, preds, sel_ty) <- tcInstType newMetaTyVars sel_id
+
+                         -- The first new wanted constraint equates the actual
+                         -- type of the selector with the type (r -> a) within
+                         -- the HasField x r a dictionary.  The preds will
+                         -- typically be empty, but if the datatype has a
+                         -- "stupid theta" then we have to include it here.
+                   ; let theta = mkPrimEqPred sel_ty (mkFunTy r_ty a_ty) : preds
+
+                         -- Use the equality proof to cast the selector Id to
+                         -- type (r -> a), then use the newtype coercion to cast
+                         -- it to a HasField dictionary.
+                         mk_ev (ev1:evs) = EvSelector sel_id tvs evs `EvCast` co
+                           where
+                             co = mkTcSubCo (evTermCoercion ev1)
+                                      `mkTcTransCo` mkTcSymCo co2
+                         mk_ev [] = panic "matchHasField.mk_ev"
+
+                         Just (_, co2) = tcInstNewTyCon_maybe (classTyCon clas)
+                                                              tys
+
+                         tvs = mkTyVarTys (map snd tv_prs)
+
+                     -- The selector must not be "naughty" (i.e. the field
+                     -- cannot have an existentially quantified type), and
+                     -- it must not be higher-rank.
+                   ; if not (isNaughtyRecordSelector sel_id) && isTauTy sel_ty
+                     then do { addUsedGRE True gre
+                             ; return GenInst { lir_new_theta = theta
+                                              , lir_mk_ev     = mk_ev
+                                              , lir_safe_over = True
+                                              } }
+                     else matchInstEnv dflags clas tys loc }
+
+           _ -> matchInstEnv dflags clas tys loc }