Break up TcRnTypes, among other modules.
[ghc.git] / compiler / typecheck / TcSMonad.hs
index fa4b169..ca6022f 100644 (file)
@@ -1,13 +1,13 @@
-{-# LANGUAGE CPP, TypeFamilies #-}
+{-# LANGUAGE CPP, DeriveFunctor, TypeFamilies #-}
 
 -- Type definitions for the constraint solver
 module TcSMonad (
 
     -- The work list
     WorkList(..), isEmptyWorkList, emptyWorkList,
-    extendWorkListNonEq, extendWorkListCt, extendWorkListDerived,
+    extendWorkListNonEq, extendWorkListCt,
     extendWorkListCts, extendWorkListEq, extendWorkListFunEq,
-    appendWorkList,
+    appendWorkList, extendWorkListImplic,
     selectNextWorkItem,
     workListSize, workListWantedCount,
     getWorkList, updWorkListTcS,
@@ -17,8 +17,12 @@ module TcSMonad (
     failTcS, warnTcS, addErrTcS,
     runTcSEqualities,
     nestTcS, nestImplicTcS, setEvBindsTcS,
+    checkConstraintsTcS, checkTvConstraintsTcS,
 
-    runTcPluginTcS, addUsedGREs, deferTcSForAllEq,
+    runTcPluginTcS, addUsedGRE, addUsedGREs, keepAlive,
+    matchGlobalInst, TcM.ClsInstResult(..),
+
+    QCInst(..),
 
     -- Tracing etc
     panicTcS, traceTcS,
@@ -26,50 +30,56 @@ module TcSMonad (
     wrapErrTcS, wrapWarnTcS,
 
     -- Evidence creation and transformation
-    MaybeNew(..), freshGoals, isFresh, getEvTerm,
+    MaybeNew(..), freshGoals, isFresh, getEvExpr,
 
-    newTcEvBinds,
-    newWantedEq,
-    newWanted, newWantedEvVar, newWantedEvVarNC, newDerivedNC,
+    newTcEvBinds, newNoTcEvBinds,
+    newWantedEq, newWantedEq_SI, emitNewWantedEq,
+    newWanted, newWanted_SI, newWantedEvVar,
+    newWantedNC, newWantedEvVarNC,
+    newDerivedNC,
     newBoundEvVarId,
     unifyTyVar, unflattenFmv, reportUnifications,
-    setEvBind, setWantedEq, setEqIfWanted,
-    setWantedEvTerm, setWantedEvBind, setEvBindIfWanted,
+    setEvBind, setWantedEq,
+    setWantedEvTerm, setEvBindIfWanted,
     newEvVar, newGivenEvVar, newGivenEvVars,
-    emitNewDerived, emitNewDeriveds, emitNewDerivedEq,
+    emitNewDeriveds, emitNewDerivedEq,
     checkReductionDepth,
+    getSolvedDicts, setSolvedDicts,
 
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
     getTopEnv, getGblEnv, getLclEnv,
-    getTcEvBinds, getTcEvBindsFromVar, getTcLevel,
-    getTcEvBindsMap,
-    tcLookupClass,
+    getTcEvBindsVar, getTcLevel,
+    getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
+    tcLookupClass, tcLookupId,
 
     -- Inerts
     InertSet(..), InertCans(..),
     updInertTcS, updInertCans, updInertDicts, updInertIrreds,
     getNoGivenEqs, setInertCans,
-    getInertEqs, getInertCans, getInertModel, getInertGivens,
-    emptyInert, getTcSInerts, setTcSInerts, takeGivenInsolubles,
-    matchableGivens, prohibitedSuperClassSolve,
+    getInertEqs, getInertCans, getInertGivens,
+    getInertInsols,
+    getTcSInerts, setTcSInerts,
+    matchableGivens, prohibitedSuperClassSolve, mightMatchLater,
     getUnsolvedInerts,
-    removeInertCts, getPendingScDicts,
-    addInertCan, addInertEq, insertFunEq,
-    emitInsoluble, emitWorkNC, emitWork,
+    removeInertCts, getPendingGivenScs,
+    addInertCan, insertFunEq, addInertForAll,
+    emitWorkNC, emitWork,
+    isImprovable,
 
     -- The Model
-    InertModel, kickOutAfterUnification,
+    kickOutAfterUnification,
 
     -- Inert Safe Haskell safe-overlap failures
     addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
     getSafeOverlapFailures,
 
     -- Inert CDictCans
-    lookupInertDict, findDictsByClass, addDict, addDictsByClass,
-    delDict, foldDicts, filterDicts,
+    DictMap, emptyDictMap, lookupInertDict, findDictsByClass, addDict,
+    addDictsByClass, delDict, foldDicts, filterDicts, findDict,
 
     -- Inert CTyEqCans
     EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
+    lookupFlattenTyVar, lookupInertTyVar,
 
     -- Inert solved dictionaries
     addSolvedDict, lookupSolvedDict,
@@ -79,25 +89,28 @@ module TcSMonad (
 
     -- The flattening cache
     lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems
+    dischargeFunEq, pprKicked,
 
     -- Inert CFunEqCans
-    updInertFunEqs, findFunEq, sizeFunEqMap,
+    updInertFunEqs, findFunEq,
     findFunEqsByTyCon,
 
     instDFunType,                              -- Instantiation
 
     -- MetaTyVars
-    newFlexiTcSTy, instFlexiTcS,
+    newFlexiTcSTy, instFlexi, instFlexiX,
     cloneMetaTyVar, demoteUnfilledFmv,
+    tcInstSkolTyVarsX,
 
-    TcLevel, isTouchableMetaTyVarTcS,
+    TcLevel,
     isFilledMetaTyVar_maybe, isFilledMetaTyVar,
     zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
     zonkTyCoVarsAndFVList,
     zonkSimples, zonkWC,
+    zonkTyCoVarKind,
 
     -- References
-    newTcRef, readTcRef, updTcRef,
+    newTcRef, readTcRef, writeTcRef, updTcRef,
 
     -- Misc
     getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
@@ -112,6 +125,8 @@ module TcSMonad (
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import HscTypes
 
 import qualified Inst as TcM
@@ -121,8 +136,10 @@ import FamInstEnv
 
 import qualified TcRnMonad as TcM
 import qualified TcMType as TcM
+import qualified ClsInst as TcM( matchGlobalInst, ClsInstResult(..) )
 import qualified TcEnv as TcM
-       ( checkWellStaged, topIdLvl, tcGetDefaultTys, tcLookupClass )
+       ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl )
+import ClsInst( InstanceWhat(..), safeOverlap, instanceReturnsDictCon )
 import Kind
 import TcType
 import DynFlags
@@ -136,6 +153,7 @@ import TyCon
 import TcErrors   ( solverDepthErrorTcS )
 
 import Name
+import Module ( HasModule, getModule )
 import RdrName ( GlobalRdrEnv, GlobalRdrElt )
 import qualified RnEnv as TcM
 import Var
@@ -146,24 +164,25 @@ import Bag
 import UniqSupply
 import Util
 import TcRnTypes
+import TcOrigin
+import Constraint
+import Predicate
 
 import Unique
 import UniqFM
 import UniqDFM
 import Maybes
 
-import StaticFlags( opt_PprStyle_Debug )
-import TrieMap
+import CoreMap
 import Control.Monad
-#if __GLASGOW_HASKELL__ > 710
 import qualified Control.Monad.Fail as MonadFail
-#endif
 import MonadUtils
 import Data.IORef
-import Data.List ( foldl', partition )
+import Data.List ( partition, mapAccumL )
 
-#ifdef DEBUG
+#if defined(DEBUG)
 import Digraph
+import UniqSet
 #endif
 
 {-
@@ -183,55 +202,109 @@ Notice that each Ct now has a simplification depth. We may
 consider using this depth for prioritization as well in the future.
 
 As a simple form of priority queue, our worklist separates out
-equalities (wl_eqs) from the rest of the canonical constraints,
-so that it's easier to deal with them first, but the separation
-is not strictly necessary. Notice that non-canonical constraints
-are also parts of the worklist.
 
-Note [Process derived items last]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We can often solve all goals without processing *any* derived constraints.
-The derived constraints are just there to help us if we get stuck.  So
-we keep them in a separate list.
+* equalities (wl_eqs); see Note [Prioritise equalities]
+* type-function equalities (wl_funeqs)
+* all the rest (wl_rest)
+
+Note [Prioritise equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's very important to process equalities /first/:
+
+* (Efficiency)  The general reason to do so is that if we process a
+  class constraint first, we may end up putting it into the inert set
+  and then kicking it out later.  That's extra work compared to just
+  doing the equality first.
+
+* (Avoiding fundep iteration) As #14723 showed, it's possible to
+  get non-termination if we
+      - Emit the Derived fundep equalities for a class constraint,
+        generating some fresh unification variables.
+      - That leads to some unification
+      - Which kicks out the class constraint
+      - Which isn't solved (because there are still some more Derived
+        equalities in the work-list), but generates yet more fundeps
+  Solution: prioritise derived equalities over class constraints
+
+* (Class equalities) We need to prioritise equalities even if they
+  are hidden inside a class constraint;
+  see Note [Prioritise class equalities]
+
+* (Kick-out) We want to apply this priority scheme to kicked-out
+  constraints too (see the call to extendWorkListCt in kick_out_rewritable
+  E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
+  homo-kinded when kicked out, and hence we want to priotitise it.
+
+* (Derived equalities) Originally we tried to postpone processing
+  Derived equalities, in the hope that we might never need to deal
+  with them at all; but in fact we must process Derived equalities
+  eagerly, partly for the (Efficiency) reason, and more importantly
+  for (Avoiding fundep iteration).
+
+Note [Prioritise class equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We prioritise equalities in the solver (see selectWorkItem). But class
+constraints like (a ~ b) and (a ~~ b) are actually equalities too;
+see Note [The equality types story] in TysPrim.
+
+Failing to prioritise these is inefficient (more kick-outs etc).
+But, worse, it can prevent us spotting a "recursive knot" among
+Wanted constraints.  See comment:10 of #12734 for a worked-out
+example.
 
+So we arrange to put these particular class constraints in the wl_eqs.
+
+  NB: since we do not currently apply the substitution to the
+  inert_solved_dicts, the knot-tying still seems a bit fragile.
+  But this makes it better.
 -}
 
 -- See Note [WorkList priorities]
 data WorkList
-  = WL { wl_eqs     :: [Ct]
-       , wl_funeqs  :: [Ct]  -- LIFO stack of goals
+  = WL { wl_eqs     :: [Ct]  -- CTyEqCan, CDictCan, CIrredCan
+                             -- Given, Wanted, and Derived
+                       -- Contains both equality constraints and their
+                       -- class-level variants (a~b) and (a~~b);
+                       -- See Note [Prioritise equalities]
+                       -- See Note [Prioritise class equalities]
+
+       , wl_funeqs  :: [Ct]
+
        , wl_rest    :: [Ct]
-       , wl_deriv   :: [CtEvidence]  -- Implicitly non-canonical
-                                     -- See Note [Process derived items last]
+
        , wl_implics :: Bag Implication  -- See Note [Residual implications]
     }
 
 appendWorkList :: WorkList -> WorkList -> WorkList
 appendWorkList
     (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1
-        , wl_deriv = ders1, wl_implics = implics1 })
+        , wl_implics = implics1 })
     (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2
-        , wl_deriv = ders2, wl_implics = implics2 })
+        , wl_implics = implics2 })
    = WL { wl_eqs     = eqs1     ++ eqs2
         , wl_funeqs  = funeqs1  ++ funeqs2
         , wl_rest    = rest1    ++ rest2
-        , wl_deriv   = ders1    ++ ders2
         , wl_implics = implics1 `unionBags`   implics2 }
 
 workListSize :: WorkList -> Int
-workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_deriv = ders, wl_rest = rest })
-  = length eqs + length funeqs + length rest + length ders
+workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
+  = length eqs + length funeqs + length rest
 
 workListWantedCount :: WorkList -> Int
+-- Count the things we need to solve
+-- excluding the insolubles (c.f. inert_count)
 workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest })
-  = count isWantedCt eqs + count isWantedCt rest
+  = count isWantedCt eqs + count is_wanted rest
+  where
+    is_wanted ct
+     | CIrredCan { cc_ev = ev, cc_insol = insol } <- ct
+     = not insol && isWanted ev
+     | otherwise
+     = isWantedCt ct
 
 extendWorkListEq :: Ct -> WorkList -> WorkList
 extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }
 
-extendWorkListEqs :: [Ct] -> WorkList -> WorkList
-extendWorkListEqs cts wl = wl { wl_eqs = cts ++ wl_eqs wl }
-
 extendWorkListFunEq :: Ct -> WorkList -> WorkList
 extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl }
 
@@ -239,30 +312,29 @@ extendWorkListNonEq :: Ct -> WorkList -> WorkList
 -- Extension by non equality
 extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }
 
-extendWorkListDerived :: CtLoc -> CtEvidence -> WorkList -> WorkList
-extendWorkListDerived loc ev wl
-  | isDroppableDerivedLoc loc = wl { wl_deriv = ev : wl_deriv wl }
-  | otherwise                 = extendWorkListEq (mkNonCanonical ev) wl
+extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList
+extendWorkListDeriveds evs wl
+  = extendWorkListCts (map mkNonCanonical evs) wl
 
-extendWorkListDeriveds :: CtLoc -> [CtEvidence] -> WorkList -> WorkList
-extendWorkListDeriveds loc evs wl
-  | isDroppableDerivedLoc loc = wl { wl_deriv = evs ++ wl_deriv wl }
-  | otherwise                 = extendWorkListEqs (map mkNonCanonical evs) wl
-
-extendWorkListImplic :: Implication -> WorkList -> WorkList
-extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl }
+extendWorkListImplic :: Bag Implication -> WorkList -> WorkList
+extendWorkListImplic implics wl = wl { wl_implics = implics `unionBags` wl_implics wl }
 
 extendWorkListCt :: Ct -> WorkList -> WorkList
 -- Agnostic
 extendWorkListCt ct wl
  = case classifyPredType (ctPred ct) of
      EqPred NomEq ty1 _
-       | Just (tc,_) <- tcSplitTyConApp_maybe ty1
+       | Just tc <- tcTyConAppTyCon_maybe ty1
        , isTypeFamilyTyCon tc
        -> extendWorkListFunEq ct wl
+
      EqPred {}
        -> extendWorkListEq ct wl
 
+     ClassPred cls _  -- See Note [Prioritise class equalities]
+       |  isEqPredClass cls
+       -> extendWorkListEq ct wl
+
      _ -> extendWorkListNonEq ct wl
 
 extendWorkListCts :: [Ct] -> WorkList -> WorkList
@@ -271,14 +343,15 @@ extendWorkListCts cts wl = foldr extendWorkListCt wl cts
 
 isEmptyWorkList :: WorkList -> Bool
 isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
-                    , wl_rest = rest, wl_deriv = ders, wl_implics = implics })
-  = null eqs && null rest && null funeqs && isEmptyBag implics && null ders
+                    , wl_rest = rest, wl_implics = implics })
+  = null eqs && null rest && null funeqs && isEmptyBag implics
 
 emptyWorkList :: WorkList
 emptyWorkList = WL { wl_eqs  = [], wl_rest = []
-                   , wl_funeqs = [], wl_deriv = [], wl_implics = emptyBag }
+                   , wl_funeqs = [], wl_implics = emptyBag }
 
 selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
+-- See Note [Prioritise equalities]
 selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs
                       , wl_rest = rest })
   | ct:cts <- eqs  = Just (ct, wl { wl_eqs    = cts })
@@ -290,37 +363,24 @@ getWorkList :: TcS WorkList
 getWorkList = do { wl_var <- getTcSWorkListRef
                  ; wrapTcS (TcM.readTcRef wl_var) }
 
-selectDerivedWorkItem  :: WorkList -> Maybe (Ct, WorkList)
-selectDerivedWorkItem wl@(WL { wl_deriv = ders })
-  | ev:evs <- ders = Just (mkNonCanonical ev, wl { wl_deriv  = evs })
-  | otherwise      = Nothing
-
 selectNextWorkItem :: TcS (Maybe Ct)
+-- Pick which work item to do next
+-- See Note [Prioritise equalities]
 selectNextWorkItem
   = do { wl_var <- getTcSWorkListRef
-       ; wl <- wrapTcS (TcM.readTcRef wl_var)
-
-       ; let try :: Maybe (Ct,WorkList) -> TcS (Maybe Ct) -> TcS (Maybe Ct)
-             try mb_work do_this_if_fail
-                | Just (ct, new_wl) <- mb_work
-                = do { checkReductionDepth (ctLoc ct) (ctPred ct)
-                     ; wrapTcS (TcM.writeTcRef wl_var new_wl)
-                     ; return (Just ct) }
-                | otherwise
-                = do_this_if_fail
-
-       ; try (selectWorkItem wl) $
-
-    do { ics <- getInertCans
-       ; solve_deriveds <- keepSolvingDeriveds
-       ; if inert_count ics == 0 && not solve_deriveds
-         then return Nothing
-         else try (selectDerivedWorkItem wl) (return Nothing) } }
+       ; wl <- readTcRef wl_var
+       ; case selectWorkItem wl of {
+           Nothing -> return Nothing ;
+           Just (ct, new_wl) ->
+    do { -- checkReductionDepth (ctLoc ct) (ctPred ct)
+         -- This is done by TcInteract.chooseInstance
+       ; writeTcRef wl_var new_wl
+       ; return (Just ct) } } }
 
 -- Pretty printing
 instance Outputable WorkList where
   ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
-          , wl_rest = rest, wl_implics = implics, wl_deriv = ders })
+          , wl_rest = rest, wl_implics = implics })
    = text "WL" <+> (braces $
      vcat [ ppUnless (null eqs) $
             text "Eqs =" <+> vcat (map ppr eqs)
@@ -328,12 +388,9 @@ instance Outputable WorkList where
             text "Funeqs =" <+> vcat (map ppr feqs)
           , ppUnless (null rest) $
             text "Non-eqs =" <+> vcat (map ppr rest)
-          , ppUnless (null ders) $
-            text "Derived =" <+> vcat (map ppr ders)
           , ppUnless (isEmptyBag implics) $
-            if opt_PprStyle_Debug  -- Typically we only want the work list for this level
-            then text "Implics =" <+> vcat (map ppr (bagToList implics))
-            else text "(Implics omitted)"
+            ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics)))
+                       (text "(Implics omitted)")
           ])
 
 
@@ -346,13 +403,24 @@ instance Outputable WorkList where
 
 data InertSet
   = IS { inert_cans :: InertCans
-              -- Canonical Given, Wanted, Derived (no Solved)
+              -- Canonical Given, Wanted, Derived
               -- Sometimes called "the inert set"
 
+       , inert_fsks :: [(TcTyVar, TcType)]
+              -- A list of (fsk, ty) pairs; we add one element when we flatten
+              -- a function application in a Given constraint, creating
+              -- a new fsk in newFlattenSkolem.  When leaving a nested scope,
+              -- unflattenGivens unifies fsk := ty
+              --
+              -- We could also get this info from inert_funeqs, filtered by
+              -- level, but it seems simpler and more direct to capture the
+              -- fsk as we generate them.
+
        , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
               -- See Note [Type family equations]
-              -- If    F tys :-> (co, ty, ev),
-              -- then  co :: F tys ~ ty
+              -- If    F tys :-> (co, rhs, flav),
+              -- then  co :: F tys ~ rhs
+              --       flav is [G] or [WD]
               --
               -- Just a hash-cons cache for use when flattening only
               -- These include entirely un-processed goals, so don't use
@@ -364,32 +432,43 @@ data InertSet
               -- NB: An ExactFunEqMap -- this doesn't match via loose types!
 
        , inert_solved_dicts   :: DictMap CtEvidence
-              -- Of form ev :: C t1 .. tn
+              -- All Wanteds, of form ev :: C t1 .. tn
               -- See Note [Solved dictionaries]
               -- and Note [Do not add superclasses of solved dictionaries]
        }
 
 instance Outputable InertSet where
-  ppr is = vcat [ ppr $ inert_cans is
-                , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ]
+  ppr (IS { inert_cans = ics
+          , inert_fsks = ifsks
+          , inert_solved_dicts = solved_dicts })
+      = vcat [ ppr ics
+             , text "Inert fsks =" <+> ppr ifsks
+             , ppUnless (null dicts) $
+               text "Solved dicts =" <+> vcat (map ppr dicts) ]
+         where
+           dicts = bagToList (dictsToBag solved_dicts)
+
+emptyInertCans :: InertCans
+emptyInertCans
+  = IC { inert_count    = 0
+       , inert_eqs      = emptyDVarEnv
+       , inert_dicts    = emptyDicts
+       , inert_safehask = emptyDicts
+       , inert_funeqs   = emptyFunEqs
+       , inert_insts    = []
+       , inert_irreds   = emptyCts }
 
 emptyInert :: InertSet
 emptyInert
-  = IS { inert_cans = IC { inert_count    = 0
-                         , inert_eqs      = emptyDVarEnv
-                         , inert_dicts    = emptyDicts
-                         , inert_safehask = emptyDicts
-                         , inert_funeqs   = emptyFunEqs
-                         , inert_irreds   = emptyCts
-                         , inert_insols   = emptyCts
-                         , inert_model    = emptyDVarEnv }
-       , inert_flat_cache    = emptyExactFunEqs
-       , inert_solved_dicts  = emptyDictMap }
+  = IS { inert_cans         = emptyInertCans
+       , inert_fsks         = []
+       , inert_flat_cache   = emptyExactFunEqs
+       , inert_solved_dicts = emptyDictMap }
 
 
 {- Note [Solved dictionaries]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we apply a top-level instance declararation, we add the "solved"
+When we apply a top-level instance declaration, we add the "solved"
 dictionary to the inert_solved_dicts.  In general, we use it to avoid
 creating a new EvVar when we have a new goal that we have solved in
 the past.
@@ -407,17 +486,82 @@ Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
     d2 = d1
 
 See Note [Example of recursive dictionaries]
+
+VERY IMPORTANT INVARIANT:
+
+ (Solved Dictionary Invariant)
+    Every member of the inert_solved_dicts is the result
+    of applying an instance declaration that "takes a step"
+
+    An instance "takes a step" if it has the form
+        dfunDList d1 d2 = MkD (...) (...) (...)
+    That is, the dfun is lazy in its arguments, and guarantees to
+    immediately return a dictionary constructor.  NB: all dictionary
+    data constructors are lazy in their arguments.
+
+    This property is crucial to ensure that all dictionaries are
+    non-bottom, which in turn ensures that the whole "recursive
+    dictionary" idea works at all, even if we get something like
+        rec { d = dfunDList d dx }
+    See Note [Recursive superclasses] in TcInstDcls.
+
+ Reason:
+   - All instances, except two exceptions listed below, "take a step"
+     in the above sense
+
+   - Exception 1: local quantified constraints have no such guarantee;
+     indeed, adding a "solved dictionary" when appling a quantified
+     constraint led to the ability to define unsafeCoerce
+     in #17267.
+
+   - Exception 2: the magic built-in instace for (~) has no
+     such guarantee.  It behaves as if we had
+         class    (a ~# b) => (a ~ b) where {}
+         instance (a ~# b) => (a ~ b) where {}
+     The "dfun" for the instance is strict in the coercion.
+     Anyway there's no point in recording a "solved dict" for
+     (t1 ~ t2); it's not going to allow a recursive dictionary
+     to be constructed.  Ditto (~~) and Coercible.
+
+THEREFORE we only add a "solved dictionary"
+  - when applying an instance declaration
+  - subject to Exceptions 1 and 2 above
+
+In implementation terms
+  - TcSMonad.addSolvedDict adds a new solved dictionary,
+    conditional on the kind of instance
+
+  - It is only called when applying an instance decl,
+    in TcInteract.doTopReactDict
+
+  - ClsInst.InstanceWhat says what kind of instance was
+    used to solve the constraint.  In particular
+      * LocalInstance identifies quantified constraints
+      * BuiltinEqInstance identifies the strange built-in
+        instances for equality.
+
+  - ClsInst.instanceReturnsDictCon says which kind of
+    instance guarantees to return a dictionary constructor
+
 Other notes about solved dictionaries
 
 * See also Note [Do not add superclasses of solved dictionaries]
 
-* The inert_solved_dicts field is not rewritten by equalities, so it may
-  get out of date.
+* The inert_solved_dicts field is not rewritten by equalities,
+  so it may get out of date.
+
+* The inert_solved_dicts are all Wanteds, never givens
+
+* We only cache dictionaries from top-level instances, not from
+  local quantified constraints.  Reason: if we cached the latter
+  we'd need to purge the cache when bringing new quantified
+  constraints into scope, because quantified constraints "shadow"
+  top-level instances.
 
 Note [Do not add superclasses of solved dictionaries]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Every member of inert_solved_dicts is the result of applying a dictionary
-function, NOT of applying superclass selection to anything.
+Every member of inert_solved_dicts is the result of applying a
+dictionary function, NOT of applying superclass selection to anything.
 Consider
 
         class Ord a => C a where
@@ -555,30 +699,29 @@ Result
 ********************************************************************* -}
 
 data InertCans   -- See Note [Detailed InertCans Invariants] for more
-  = IC { inert_model :: InertModel
-              -- See Note [inert_model: the inert model]
-
-       , inert_eqs :: DTyVarEnv EqualCtList
+  = IC { inert_eqs :: InertEqs
               -- See Note [inert_eqs: the inert equalities]
-              -- All Given/Wanted CTyEqCans; index is the LHS tyvar
+              -- All CTyEqCans; index is the LHS tyvar
+              -- Domain = skolems and untouchables; a touchable would be unified
 
        , inert_funeqs :: FunEqMap Ct
               -- All CFunEqCans; index is the whole family head type.
               -- All Nominal (that's an invarint of all CFunEqCans)
               -- LHS is fully rewritten (modulo eqCanRewrite constraints)
-              --     wrt inert_eqs/inert_model
-              -- We can get Derived ones from e.g.
-              --   (a) flattening derived equalities
-              --   (b) emitDerivedShadows
+              --     wrt inert_eqs
+              -- Can include all flavours, [G], [W], [WD], [D]
+              -- See Note [Type family equations]
 
        , inert_dicts :: DictMap Ct
               -- Dictionaries only
               -- All fully rewritten (modulo flavour constraints)
-              --     wrt inert_eqs/inert_model
+              --     wrt inert_eqs
+
+       , inert_insts :: [QCInst]
 
        , inert_safehask :: DictMap Ct
               -- Failed dictionary resolution due to Safe Haskell overlapping
-              -- instances restriction. We keep this seperate from inert_dicts
+              -- instances restriction. We keep this separate from inert_dicts
               -- as it doesn't cause compilation failure, just safe inference
               -- failure.
               --
@@ -586,27 +729,22 @@ data InertCans   -- See Note [Detailed InertCans Invariants] for more
               -- in TcSimplify
 
        , inert_irreds :: Cts
-              -- Irreducible predicates
-
-       , inert_insols :: Cts
-              -- Frozen errors (as non-canonicals)
+              -- Irreducible predicates that cannot be made canonical,
+              --     and which don't interact with others (e.g.  (c a))
+              -- and insoluble predicates (e.g.  Int ~ Bool, or a ~ [a])
 
        , inert_count :: Int
               -- Number of Wanted goals in
               --     inert_eqs, inert_dicts, inert_safehask, inert_irreds
               -- Does not include insolubles
-              -- When non-zero, keep trying to solved
+              -- When non-zero, keep trying to solve
        }
 
-type InertModel  = DTyVarEnv Ct
-     -- If a -> ct, then ct is a
-     --    nominal, Derived, canonical CTyEqCan for [D] (a ~N rhs)
-     -- The index of the TyVarEnv is the 'a'
-     -- All saturated info for Given, Wanted, Derived is here
-
+type InertEqs    = DTyVarEnv EqualCtList
+type EqualCtList = [Ct]  -- See Note [EqualCtList invariants]
 
 {- Note [Detailed InertCans Invariants]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The InertCans represents a collection of constraints with the following properties:
 
   * All canonical
@@ -628,69 +766,58 @@ The InertCans represents a collection of constraints with the following properti
   * CTyEqCan equalities: see Note [Applying the inert substitution]
                          in TcFlatten
 
+Note [EqualCtList invariants]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    * All are equalities
+    * All these equalities have the same LHS
+    * The list is never empty
+    * No element of the list can rewrite any other
+    * Derived before Wanted
+
+From the fourth invariant it follows that the list is
+   - A single [G], or
+   - Zero or one [D] or [WD], followd by any number of [W]
+
+The Wanteds can't rewrite anything which is why we put them last
+
 Note [Type family equations]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Type-family equations, of form (ev : F tys ~ ty), live in three places
+Type-family equations, CFunEqCans, of form (ev : F tys ~ ty),
+live in three places
 
   * The work-list, of course
 
+  * The inert_funeqs are un-solved but fully processed, and in
+    the InertCans. They can be [G], [W], [WD], or [D].
+
   * The inert_flat_cache.  This is used when flattening, to get maximal
-    sharing.  It contains lots of things that are still in the work-list.
+    sharing. Everthing in the inert_flat_cache is [G] or [WD]
+
+    It contains lots of things that are still in the work-list.
     E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
         work list.  Then we flatten w1, dumping (w3: G a ~ f1) in the work
         list.  Now if we flatten w2 before we get to w3, we still want to
         share that (G a).
-
     Because it contains work-list things, DO NOT use the flat cache to solve
     a top-level goal.  Eg in the above example we don't want to solve w3
     using w3 itself!
 
-  * The inert_funeqs are un-solved but fully processed and in the InertCans.
-
-Note [inert_model: the inert model]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-* Part of the inert set is the “model”
-
-   * The “Model” is an non-idempotent but no-occurs-check
-     substitution, reflecting *all* *Nominal* equalities (a ~N ty)
-     that are not immediately soluble by unification.
-
-   * All the constraints in the model are Derived CTyEqCans
-     That is if (a -> ty) is in the model, then
-     we have an inert constraint [D] a ~N ty.
-
-   * There are two sources of constraints in the model:
-
-     - Derived constraints arising from functional dependencies, or
-       decomposing injective arguments of type functions, and
-       suchlike.
-
-     - A Derived "shadow copy" for every Wanted (a ~N ty) in
-       inert_eqs.  (Originally included every Given too; but
-       see Note [Add derived shadows only for Wanteds])
-
-   * The model is not subject to "kicking-out". Reason: we make a Derived
-     shadow copy of any Wanted (a ~ ty), and that Derived copy will
-     be fully rewritten by the model before it is added
+The CFunEqCan Ownership Invariant:
 
-   * The principal reason for maintaining the model is to generate
-     equalities that tell us how to unify a variable: that is, what
-     Mark Jones calls "improvement". The same idea is sometimes also
-     called "saturation"; find all the equalities that must hold in
-     any solution.
+  * Each [G/W/WD] CFunEqCan has a distinct fsk or fmv
+    It "owns" that fsk/fmv, in the sense that:
+      - reducing a [W/WD] CFunEqCan fills in the fmv
+      - unflattening a [W/WD] CFunEqCan fills in the fmv
+      (in both cases unless an occurs-check would result)
 
-   * Domain of the model = skolems + untouchables.
-     A touchable unification variable would have been unified first.
+  * In contrast a [D] CFunEqCan does not "own" its fmv:
+      - reducing a [D] CFunEqCan does not fill in the fmv;
+        it just generates an equality
+      - unflattening ignores [D] CFunEqCans altogether
 
-   * The inert_eqs are all Given/Wanted.  The Derived ones are in the
-     inert_model only.
-
-   * However inert_dicts, inert_funeqs, inert_irreds
-     may well contain derived constraints.
 
 Note [inert_eqs: the inert equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 Definition [Can-rewrite relation]
 A "can-rewrite" relation between flavours, written f1 >= f2, is a
 binary relation with the following properties
@@ -749,39 +876,41 @@ guarantee that this recursive use will terminate.
 
 Note [Extending the inert equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Theorem [Stability under extension]
-   This is the main theorem!
+Main Theorem [Stability under extension]
    Suppose we have a "work item"
        a -fw-> t
    and an inert generalised substitution S,
-   such that
+   THEN the extended substitution T = S+(a -fw-> t)
+        is an inert generalised substitution
+   PROVIDED
       (T1) S(fw,a) = a     -- LHS of work-item is a fixpoint of S(fw,_)
       (T2) S(fw,t) = t     -- RHS of work-item is a fixpoint of S(fw,_)
       (T3) a not in t      -- No occurs check in the work item
 
-      (K1) for every (a -fs-> s) in S, then not (fw >= fs)
-           Reason: the work item is fully rewritten by S, hence not (fs >= fw)
-                   but if (fw >= fs) then the work item could rewrite
-                   the inert item
+      AND, for every (b -fs-> s) in S:
+           (K0) not (fw >= fs)
+                Reason: suppose we kick out (a -fs-> s),
+                        and add (a -fw-> t) to the inert set.
+                        The latter can't rewrite the former,
+                        so the kick-out achieved nothing
 
-      (K2) for every (b -fs-> s) in S, where b /= a, then
-              (K2a) not (fs >= fs)
-           or (K2b) fs >= fw
-           or (K2c) not (fw >= fs)
-           or (K2d) a not in s
+           OR { (K1) not (a = b)
+                     Reason: if fw >= fs, WF1 says we can't have both
+                             a -fw-> t  and  a -fs-> s
 
-      (K3) See Note [K3: completeness of solving]
-           If (b -fs-> s) is in S with (fw >= fs), then
-        (K3a) If the role of fs is nominal: s /= a
-        (K3b) If the role of fs is representational: EITHER
-                a not in s, OR
-                the path from the top of s to a includes at least one non-newtype
+                AND (K2): guarantees inertness of the new substitution
+                    {  (K2a) not (fs >= fs)
+                    OR (K2b) fs >= fw
+                    OR (K2d) a not in s }
+
+                AND (K3) See Note [K3: completeness of solving]
+                    { (K3a) If the role of fs is nominal: s /= a
+                      (K3b) If the role of fs is representational:
+                            s is not of form (a t1 .. tn) } }
 
-   then the extended substition T = S+(a -fw-> t)
-   is an inert generalised substitution.
 
 Conditions (T1-T3) are established by the canonicaliser
-Conditions (K1-K3) are established by TcSMonad.kickOutRewriteable
+Conditions (K1-K3) are established by TcSMonad.kickOutRewritable
 
 The idea is that
 * (T1-2) are guaranteed by exhaustively rewriting the work-item
@@ -806,11 +935,12 @@ The idea is that
   us to kick out an inert wanted that mentions a, because of (K2a).  This
   is a common case, hence good not to kick out.
 
-* Lemma (L2): if not (fw >= fw), then K1-K3 all hold.
+* Lemma (L2): if not (fw >= fw), then K0 holds and we kick out nothing
   Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
-         and so K1-K3 hold.  Intuitively, since fw can't rewrite anything,
+         and so K0 holds.  Intuitively, since fw can't rewrite anything,
          adding it cannot cause any loops
   This is a common case, because Wanteds cannot rewrite Wanteds.
+  It's used to avoid even looking for constraint to kick out.
 
 * Lemma (L1): The conditions of the Main Theorem imply that there is no
               (a -fs-> t) in S, s.t.  (fs >= fw).
@@ -823,9 +953,9 @@ The idea is that
   - (T3) guarantees (WF2).
 
 * (K2) is about inertness.  Intuitively, any infinite chain T^0(f,t),
-  T^1(f,t), T^2(f,T).... must pass through the new work item infnitely
-  often, since the substution without the work item is inert; and must
-  pass through at least one of the triples in S infnitely often.
+  T^1(f,t), T^2(f,T).... must pass through the new work item infinitely
+  often, since the substitution without the work item is inert; and must
+  pass through at least one of the triples in S infinitely often.
 
   - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f),
     and hence this triple never plays a role in application S(f,a).
@@ -834,12 +964,12 @@ The idea is that
     (NB: we could strengten K1) in this way too, but see K3.
 
   - (K2b): If this holds then, by (T2), b is not in t.  So applying the
-    work item does not genenerate any new opportunities for applying S
+    work item does not generate any new opportunities for applying S
 
   - (K2c): If this holds, we can't pass through this triple infinitely
     often, because if we did then fs>=f, fw>=f, hence by (R2)
       * either fw>=fs, contradicting K2c
-      * or fs>=fw; so by the agument in K2b we can't have a loop
+      * or fs>=fw; so by the argument in K2b we can't have a loop
 
   - (K2d): if a not in s, we hae no further opportunity to apply the
     work item, similar to (K2b)
@@ -887,46 +1017,35 @@ is somewhat accidental.
 
 When considering roles, we also need the second clause (K3b). Consider
 
-  inert-item   a -W/R-> b c
   work-item    c -G/N-> a
+  inert-item   a -W/R-> b c
 
 The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
-We've satisfied conditions (T1)-(T3) and (K1) and (K2). If all we had were
-condition (K3a), then we would keep the inert around and add the work item.
-But then, consider if we hit the following:
-
-  work-item2   b -G/N-> Id
+But we don't kick out the inert item because not (W/R >= W/R).  So we just
+add the work item. But then, consider if we hit the following:
 
+  work-item    b -G/N-> Id
+  inert-items  a -W/R-> b c
+               c -G/N-> a
 where
-
   newtype Id x = Id x
 
 For similar reasons, if we only had (K3a), we wouldn't kick the
 representational inert out. And then, we'd miss solving the inert, which
-now reduced to reflexivity. The solution here is to kick out representational
-inerts whenever the tyvar of a work item is "exposed", where exposed means
-not under some proper data-type constructor, like [] or Maybe. See
-isTyVarExposed in TcType. This is encoded in (K3b).
+now reduced to reflexivity.
 
-Note [Stability of flattening]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The inert_eqs and inert_model, *considered separately* are each stable;
-that is, substituting using them will terminate.  Considered *together*
-they are not.  E.g.
-
-  Add: [G] a~[b] to inert set with model  [D] b~[a]
-
-  We add [G] a~[b] to inert_eqs, and emit [D] a~[b]. At this point
-  the combination of inert_eqs and inert_model is not stable.
-
-  Then we canonicalise [D] a~[b] to [D] a~[[a]], and add that to
-  insolubles as an occurs check.
-
-* When canonicalizing, the flattener respects flavours. In particular,
-  when flattening a type variable 'a':
-    * Derived:      look up 'a' in the inert_model
-    * Given/Wanted: look up 'a' in the inert_eqs
+The solution here is to kick out representational inerts whenever the
+tyvar of a work item is "exposed", where exposed means being at the
+head of the top-level application chain (a t1 .. tn).  See
+TcType.isTyVarHead. This is encoded in (K3b).
 
+Beware: if we make this test succeed too often, we kick out too much,
+and the solver might loop.  Consider (#14363)
+  work item:   [G] a ~R f b
+  inert item:  [G] b ~R f a
+In GHC 8.2 the completeness tests more aggressive, and kicked out
+the inert item; but no rewriting happened and there was an infinite
+loop.  All we need is to have the tyvar at the head.
 
 Note [Flavours with roles]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -950,129 +1069,14 @@ T Int Bool. The reason is that T's first parameter has a nominal role, and
 thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of
 substitution means that the proof in Note [The inert equalities] may need
 to be revisited, but we don't think that the end conclusion is wrong.
-
-Note [Examples of how the inert_model helps completeness]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
------------ 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 awe appear to be stuck, since we don't rewrite Wanteds with
-  Wanteds. But inert_model to the rescue.  In the model we first added
-           fmv -> Maybe e
-  Then when adding [W] fmv -> Maybe ee to the inert set, we noticed
-  that the model can rewrite the constraint, and so emit [D] fmv ~ Maybe ee.
-  That canonicalises to
-           [D] Maybe e ~ Maybe ee
-  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.
-
-  And that is exactly what happens, in the *Derived* constraints.
-  In effect we get
-
-    [D] F alpha ~ fmv
-    [D] C fmv alpha
-    [D] fmv ~ Bool
-
-  and now we can rewrite (C fmv alpha) with (fmv ~ Bool), ane
-  we are off to the races.
-
------------ 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: beta ~ fmv2
-      [W] w5: fmv1 ~ fsk1   -- From F a ~ F beta using flat-cache
-                            -- and re-orient to put meta-var on left
-
-  Unify beta := fmv2
-      [W] w1: F fmv2 ~ fmv1
-      [W] w2: UnF fmv1 ~ fmv2
-      [W] w5: fmv1 ~ fsk1
-
-  In the model, we have the shadow Deriveds of w1 and w2
-  (I name them for convenience even though they are anonymous)
-      [D] d1: F fmv2 ~ fmv1d
-      [D] d2: fmv1d ~ fmv1
-      [D] d3: UnF fmv1 ~ fmv2d
-      [D] d4: fmv2d ~ fmv2
-
-  Now we can rewrite d3 with w5, and match with g2, to get
-      fmv2d := fsk2
-      [D] d1: F fmv2 ~ fmv1d
-      [D] d2: fmv1d ~ fmv1
-      [D] d4: fmv2 ~ fsk2
-
-  Use g2 to rewrite fsk2 to a.
-      [D] d1: F fmv2 ~ fmv1d
-      [D] d2: fmv1d ~ fmv1
-      [D] d4: fmv2 ~ a
-
-  Use d4 to rewrite d1, rewrite with g3,
-  match with g1, to get
-      fmv1d := fsk1
-      [D] d2: fmv1 ~ fsk1
-      [D] d4: fmv2 ~ a
-
-  At this point we are stuck so we unflatten this set:
-  See Note [Orientation of equalities with fmvs] in TcFlatten
-      [W] w1: F fmv2 ~ fmv1
-      [W] w2: UnF fmv1 ~ fmv2
-      [W] w5: fmv1 ~ fsk1
-      [D] d4: fmv2 ~ a
-
-  Unflattening will discharge w1: fmv1 := F fmv2
-  It can't discharge w2, so it is kept.  But we can
-  unify fmv2 := fsk2, and that is "progress". Result
-      [W] w2: UnF (F a) ~ a
-      [W] w5: F a ~ fsk1
-
-  And now both of these are easily proved in the next iteration.  Phew!
 -}
 
 instance Outputable InertCans where
-  ppr (IC { inert_model = model, inert_eqs = eqs
+  ppr (IC { inert_eqs = eqs
           , inert_funeqs = funeqs, inert_dicts = dicts
           , inert_safehask = safehask, inert_irreds = irreds
-          , inert_insols = insols, inert_count = count })
+          , inert_insts = insts
+          , inert_count = count })
     = braces $ vcat
       [ ppUnless (isEmptyDVarEnv eqs) $
         text "Equalities:"
@@ -1085,220 +1089,266 @@ instance Outputable InertCans where
         text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
       , ppUnless (isEmptyCts irreds) $
         text "Irreds =" <+> pprCts irreds
-      , ppUnless (isEmptyCts insols) $
-        text "Insolubles =" <+> pprCts insols
-      , ppUnless (isEmptyDVarEnv model) $
-        text "Model =" <+> pprCts (foldDVarEnv consCts emptyCts model)
+      , ppUnless (null insts) $
+        text "Given instances =" <+> vcat (map ppr insts)
       , text "Unsolved goals =" <+> int count
       ]
 
 {- *********************************************************************
 *                                                                      *
-                  Adding an inert
+             Shadow constraints and improvement
 *                                                                      *
 ************************************************************************
 
-Note [Adding an inert canonical constraint the InertCans]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-* Adding any constraint c *other* than a CTyEqCan (TcSMonad.addInertCan):
-
-    * If c can be rewritten by model, emit the shadow constraint [D] c
-      as NonCanonical.   See Note [Emitting shadow constraints]
-
-    * Reason for non-canonical: a CFunEqCan has a unique fmv on the RHS,
-      so we must not duplicate it.
-
-* Adding a *nominal* CTyEqCan (a ~N ty) to the inert set (TcSMonad.addInertEq).
-
-    (A) Always (G/W/D) kick out constraints that can be rewritten
-        (respecting flavours) by the new constraint. This is done
-        by kickOutRewritable.
-
-    (B) Applies only to nominal equalities: a ~ ty.  Four cases:
-
-        [Representational]   [G/W/D] a ~R ty:
-          Just add it to inert_eqs
-
-        [Derived Nominal]  [D] a ~N ty:
-          1. Add (a~ty) to the model
-             NB: 'a' cannot be in fv(ty), because the constraint is canonical.
-
-          2. (DShadow) Do emitDerivedShadows
-               For every inert [W] constraint c, st
-                (a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]),
-                    and
-                (b) the model cannot rewrite c
-               kick out a Derived *copy*, leaving the original unchanged.
-               Reason for (b) if the model can rewrite c, then we have already
-               generated a shadow copy
-               See Note [Add derived shadows only for Wanteds]
-
-       [Given/Wanted Nominal]  [G/W] a ~N ty:
-          1. Add it to inert_eqs
-          2. For [W], Emit [D] a~ty
-             Step (2) is needed to allow the current model to fully
-             rewrite [D] a~ty before adding it using the [Derived Nominal]
-             steps above.
-             See Note [Add derived shadows only for Wanteds]
-
-* Unifying a:=ty, is like adding [G] a~ty, but we can't make a [D]
-  a~ty, as in step (1) of the [G/W] case above.  So instead, do
-  kickOutAfterUnification:
-    - Kick out from the model any equality (b~ty2) that mentions 'a'
-      (i.e. a=b or a in ty2).  Example:
-            [G] a ~ [b],    model [D] b ~ [a]
-
-Note [Emitting shadow constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- * Given a new model element [D] a ~ ty, we want to emit shadow
-   [D] constraints for any inert constraints 'c' that can be
-   rewritten [D] a-> ty
+Note [The improvement story and derived shadows]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Because Wanteds cannot rewrite Wanteds (see Note [Wanteds do not
+rewrite Wanteds] in Constraint), we may miss some opportunities for
+solving.  Here's a classic example (indexed-types/should_fail/T4093a)
 
- * And similarly given a new Given/Wanted 'c', we want to emit a
-   shadow 'c' if the model can rewrite [D] c
+    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 appear to be stuck, since we don't rewrite Wanteds with
+    Wanteds.  This is silly because we can see that ee := e is the
+    only solution.
+
+The basic plan is
+  * generate Derived constraints that shadow Wanted constraints
+  * allow Derived to rewrite Derived
+  * in order to cause some unifications to take place
+  * that in turn solve the original Wanteds
+
+The ONLY reason for all these Derived equalities is to tell us how to
+unify a variable: that is, what Mark Jones calls "improvement".
+
+The same idea is sometimes also called "saturation"; find all the
+equalities that must hold in any solution.
+
+Or, equivalently, you can think of the derived shadows as implementing
+the "model": a non-idempotent but no-occurs-check substitution,
+reflecting *all* *Nominal* equalities (a ~N ty) that are not
+immediately soluble by unification.
+
+More specifically, here's how it works (Oct 16):
+
+* Wanted constraints are born as [WD]; this behaves like a
+  [W] and a [D] paired together.
+
+* When we are about to add a [WD] to the inert set, if it can
+  be rewritten by a [D] a ~ ty, then we split it into [W] and [D],
+  putting the latter into the work list (see maybeEmitShadow).
+
+In the example above, we get to the point where we are stuck:
+    [WD] Foo ee ~ fmv
+    [WD] fmv ~ Maybe e
+    [WD] fmv ~ Maybe ee
+
+But now when [WD] fmv ~ Maybe ee is about to be added, we'll
+split it into [W] and [D], since the inert [WD] fmv ~ Maybe e
+can rewrite it.  Then:
+    work item: [D] fmv ~ Maybe ee
+    inert:     [W] fmv ~ Maybe ee
+               [WD] fmv ~ Maybe e   -- (C)
+               [WD] Foo ee ~ fmv
+
+See Note [Splitting WD constraints].  Now the work item is rewritten
+by (C) and we soon get ee := e.
+
+Additional notes:
+
+  * The derived shadow equalities live in inert_eqs, along with
+    the Givens and Wanteds; see Note [EqualCtList invariants].
+
+  * We make Derived shadows only for Wanteds, not Givens.  So we
+    have only [G], not [GD] and [G] plus splitting.  See
+    Note [Add derived shadows only for Wanteds]
+
+  * We also get Derived equalities from functional dependencies
+    and type-function injectivity; see calls to unifyDerived.
+
+  * This splitting business applies to CFunEqCans too; and then
+    we do apply type-function reductions to the [D] CFunEqCan.
+    See Note [Reduction for Derived CFunEqCans]
+
+  * It's worth having [WD] rather than just [W] and [D] because
+    * efficiency: silly to process the same thing twice
+    * inert_funeqs, inert_dicts is a finite map keyed by
+      the type; it's inconvenient for it to map to TWO constraints
+
+Note [Splitting WD constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We are about to add a [WD] constraint to the inert set; and we
+know that the inert set has fully rewritten it.  Should we split
+it into [W] and [D], and put the [D] in the work list for further
+work?
+
+* CDictCan (C tys) or CFunEqCan (F tys ~ fsk):
+  Yes if the inert set could rewrite tys to make the class constraint,
+  or type family, fire.  That is, yes if the inert_eqs intersects
+  with the free vars of tys.  For this test we use
+  (anyRewritableTyVar True) which ignores casts and coercions in tys,
+  because rewriting the casts or coercions won't make the thing fire
+  more often.
+
+* CTyEqCan (a ~ ty): Yes if the inert set could rewrite 'a' or 'ty'.
+  We need to check both 'a' and 'ty' against the inert set:
+    - Inert set contains  [D] a ~ ty2
+      Then we want to put [D] a ~ ty in the worklist, so we'll
+      get [D] ty ~ ty2 with consequent good things
+
+    - Inert set contains [D] b ~ a, where b is in ty.
+      We can't just add [WD] a ~ ty[b] to the inert set, because
+      that breaks the inert-set invariants.  If we tried to
+      canonicalise another [D] constraint mentioning 'a', we'd
+      get an infinite loop
+
+  Moreover we must use (anyRewritableTyVar False) for the RHS,
+  because even tyvars in the casts and coercions could give
+  an infinite loop if we don't expose it
+
+* CIrredCan: Yes if the inert set can rewrite the constraint.
+  We used to think splitting irreds was unnecessary, but
+  see Note [Splitting Irred WD constraints]
+
+* Others: nothing is gained by splitting.
+
+Note [Splitting Irred WD constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Splitting Irred constraints can make a difference. Here is the
+scenario:
 
-See modelCanRewrite.
+  a[sk] :: F v     -- F is a type family
+  beta :: alpha
 
-NB the use of rewritableTyVars. You might wonder whether, given the new
-constraint [D] fmv ~ ty and the inert [W] F alpha ~ fmv, do we want to
-emit a shadow constraint [D] F alpha ~ fmv?  No, we don't, because
-it'll literally be a duplicate (since we do not rewrite the RHS of a
-CFunEqCan) and hence immediately eliminated again.  Insetad we simply
-want to *kick-out* the [W] F alpha ~ fmv, so that it is reconsidered
-from a fudep point of view.  See Note [Kicking out CFunEqCan for
-fundeps]
+  work item: [WD] a ~ beta
 
-Note [Kicking out CFunEqCan for fundeps]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider:
-   New:    [D] fmv1 ~ fmv2
-   Inert:  [W] F alpha ~ fmv1
-           [W] F beta  ~ fmv2
+This is heterogeneous, so we try flattening the kinds.
 
-The new (derived) equality certainly can't rewrite the inerts. But we
-*must* kick out the first one, to get:
+  co :: F v ~ fmv
+  [WD] (a |> co) ~ beta
 
-   New:   [W] F alpha ~ fmv1
-   Inert: [W] F beta ~ fmv2
-   Model: [D] fmv1 ~ fmv2
+This is still hetero, so we emit a kind equality and make the work item an
+inert Irred.
 
-and now improvement will discover [D] alpha ~ beta. This is important;
-eg in Trac #9587.
--}
+  work item: [D] fmv ~ alpha
+  inert: [WD] (a |> co) ~ beta (CIrredCan)
 
-addInertEq :: Ct -> TcS ()
--- This is a key function, because of the kick-out stuff
--- Precondition: item /is/ canonical
-addInertEq ct@(CTyEqCan { cc_tyvar = tv })
-  = do { traceTcS "addInertEq {" $
-         text "Adding new inert equality:" <+> ppr ct
-       ; ics <- getInertCans
+Can't make progress on the work item. Add to inert set. This kicks out the
+old inert, because a [D] can rewrite a [WD].
 
-       ; let (kicked_out, ics1) = kickOutRewritable (ctFlavourRole ct) tv ics
-       ; ics2 <- add_inert_eq ics1 ct
+  work item: [WD] (a |> co) ~ beta
+  inert: [D] fmv ~ alpha (CTyEqCan)
 
-       ; setInertCans ics2
+Can't make progress on this work item either (although GHC tries by
+decomposing the cast and reflattening... but that doesn't make a difference),
+which is still hetero. Emit a new kind equality and add to inert set. But,
+critically, we split the Irred.
 
-       ; unless (isEmptyWorkList kicked_out) $
-         do { updWorkListTcS (appendWorkList kicked_out)
-            ; csTraceTcS $
-               hang (text "Kick out, tv =" <+> ppr tv)
-                  2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
-                          , ppr kicked_out ]) }
-
-       ; traceTcS "addInertEq }" $ empty }
-addInertEq ct = pprPanic "addInertEq" (ppr ct)
-
-add_inert_eq :: InertCans -> Ct -> TcS InertCans
-add_inert_eq ics@(IC { inert_count = n
-                     , inert_eqs = old_eqs
-                     , inert_model = old_model })
-             ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv
-                          , cc_rhs = _rhs })
-  | ReprEq <- eq_rel
-  = return new_ics
-
-  | isDerived ev
-  = do { emitDerivedShadows ics tv
-       ; return (ics { inert_model = extendDVarEnv old_model tv ct }) }
-
-  | otherwise   -- Given/Wanted Nominal equality [W] tv ~N ty
-  = do { emitNewDerived loc pred
-       ; return new_ics }
-  where
-    loc     = ctEvLoc ev
-    pred    = ctEvPred ev
-    new_ics = ics { inert_eqs   = addTyEq old_eqs tv ct
-                  , inert_count = bumpUnsolvedCount ev n }
-
-add_inert_eq _ ct = pprPanic "addInertEq" (ppr ct)
-
-emitDerivedShadows :: InertCans -> TcTyVar -> TcS ()
-emitDerivedShadows IC { inert_eqs      = tv_eqs
-                      , inert_dicts    = dicts
-                      , inert_safehask = safehask
-                      , inert_funeqs   = funeqs
-                      , inert_irreds   = irreds
-                      , inert_model    = model } new_tv
-  | null shadows
-  = return ()
-  | otherwise
-  = do { traceTcS "Emit derived shadows:" $
-         vcat [ text "tyvar =" <+> ppr new_tv
-              , text "shadows =" <+> vcat (map ppr shadows) ]
-       ; emitWork shadows }
-  where
-    shadows = foldDicts  get_ct dicts    $
-              foldDicts  get_ct safehask $
-              foldFunEqs get_ct funeqs   $
-              foldIrreds get_ct irreds   $
-              foldTyEqs  get_ct tv_eqs []
-      -- Ignore insolubles
-
-    get_ct ct cts | want_shadow ct = mkShadowCt ct : cts
-                  | otherwise      = cts
-
-    want_shadow ct
-      =  isWantedCt ct                     -- See Note [Add shadows only for Wanteds]
-      && (new_tv `elemVarSet` rw_tvs)      -- New tv can rewrite ct, yielding a
-                                           -- different ct
-      && not (modelCanRewrite model rw_tvs)-- We have not already created a
-                                           -- shadow
-      where
-        rw_tvs = rewritableTyCoVars ct
-
-mkShadowCt :: Ct -> Ct
--- Produce a Derived shadow constraint from the input
--- If it is a CFunEqCan, make it NonCanonical, to avoid
---   duplicating the flatten-skolems
--- Otherwise keep the canonical shape.  This just saves work, but
--- is sometimes important; see Note [Keep CDictCan shadows as CDictCan]
-mkShadowCt ct
-  | CFunEqCan {} <- ct = CNonCanonical { cc_ev = derived_ev }
-  | otherwise          = ct { cc_ev = derived_ev }
-  where
-    ev = ctEvidence ct
-    derived_ev = CtDerived { ctev_pred = ctEvPred ev
-                           , ctev_loc  = ctEvLoc ev }
-
-{- Note [Add derived shadows only for Wanteds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We now only add shadows for Wanted constraints.  Why add derived
-shadows for Givens?  After all, Givens can rewrite Deriveds.  But
-Deriveds can't rewrite Givens.  So in principle, if we created a
-Derived shadow of a Given, it could be rewritten by other Deriveds,
-and that could, conceivably, lead to a useful unification.
+  work list:
+   [D] fmv ~ alpha (CTyEqCan)
+   [D] (a |> co) ~ beta (CIrred) -- this one was split off
+  inert:
+   [W] (a |> co) ~ beta
+   [D] fmv ~ alpha
+
+We quickly solve the first work item, as it's the same as an inert.
+
+  work item: [D] (a |> co) ~ beta
+  inert:
+   [W] (a |> co) ~ beta
+   [D] fmv ~ alpha
+
+We decompose the cast, yielding
+
+  [D] a ~ beta
+
+We then flatten the kinds. The lhs kind is F v, which flattens to fmv which
+then rewrites to alpha.
+
+  co' :: F v ~ alpha
+  [D] (a |> co') ~ beta
+
+Now this equality is homo-kinded. So we swizzle it around to
+
+  [D] beta ~ (a |> co')
+
+and set beta := a |> co', and go home happy.
+
+If we don't split the Irreds, we loop. This is all dangerously subtle.
+
+This is triggered by test case typecheck/should_compile/SplitWD.
+
+Note [Examples of how Derived shadows helps completeness]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+#10009, a very 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
+               [WD] UnF (F beta) ~ beta
+               [WD] 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
+
+      [WD] w1: F beta ~ fmv1
+      [WD] w2: UnF fmv1 ~ fmv2
+      [WD] w3: fmv2 ~ beta
+      [WD] w4: fmv1 ~ fsk1   -- From F a ~ F beta using flat-cache
+                             -- and re-orient to put meta-var on left
+
+Rewrite w2 with w4: [D] d1: UnF fsk1 ~ fmv2
+React that with g2: [D] d2: fmv2 ~ fsk2
+React that with w3: [D] beta ~ fsk2
+            and g3: [D] beta ~ a -- Hooray beta := a
+And that is enough to solve everything
+
+Note [Add derived shadows only for Wanteds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We only add shadows for Wanted constraints. That is, we have
+[WD] but not [GD]; and maybeEmitShaodw looks only at [WD]
+constraints.
+
+It does just possibly make sense ot add a derived shadow for a
+Given. If we created a Derived shadow of a Given, it could be
+rewritten by other Deriveds, and that could, conceivably, lead to a
+useful unification.
 
 But (a) I have been unable to come up with an example of this
-happening and (b) see Trac #12660 for how adding the derived shadows
-of a Given led to an infinite loop.  For (b) there may be other
-ways to solve the loop, but simply reraining from adding
-derived shadows of Givens is particularly simple.  And it's more
-efficient too!
+        happening
+    (b) see #12660 for how adding the derived shadows
+        of a Given led to an infinite loop.
+    (c) It's unlikely that rewriting derived Givens will lead
+        to a unification because Givens don't mention touchable
+        unification variables
+
+For (b) there may be other ways to solve the loop, but simply
+reraining from adding derived shadows of Givens is particularly
+simple.  And it's more efficient too!
 
 Still, here's one possible reason for adding derived shadows
 for Givens.  Consider
-           work-item [G] a ~ [b], model has [D] b ~ a.
+           work-item [G] a ~ [b], inerts has [D] b ~ a.
 If we added the derived shadow (into the work list)
          [D] a ~ [b]
 When we process it, we'll rewrite to a ~ [a] and get an
@@ -1326,53 +1376,284 @@ because we've already added its superclasses.  So we won't re-add
 them.  If we forget the pend_sc flag, our cunning scheme for avoiding
 generating superclasses repeatedly will fail.
 
-See Trac #11379 for a case of this.
+See #11379 for a case of this.
+
+Note [Do not do improvement for WOnly]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We do improvement between two constraints (e.g. for injectivity
+or functional dependencies) only if both are "improvable". And
+we improve a constraint wrt the top-level instances only if
+it is improvable.
+
+Improvable:     [G] [WD] [D}
+Not improvable: [W]
+
+Reasons:
+
+* It's less work: fewer pairs to compare
+
+* Every [W] has a shadow [D] so nothing is lost
+
+* Consider [WD] C Int b,  where 'b' is a skolem, and
+    class C a b | a -> b
+    instance C Int Bool
+  We'll do a fundep on it and emit [D] b ~ Bool
+  That will kick out constraint [WD] C Int b
+  Then we'll split it to [W] C Int b (keep in inert)
+                     and [D] C Int b (in work list)
+  When processing the latter we'll rewrite it to
+        [D] C Int Bool
+  At that point it would be /stupid/ to interact it
+  with the inert [W] C Int b in the inert set; after all,
+  it's the very constraint from which the [D] C Int Bool
+  was split!  We can avoid this by not doing improvement
+  on [W] constraints. This came up in #12860.
 -}
 
-modelCanRewrite :: InertModel -> TcTyCoVarSet -> Bool
--- See Note [Emitting shadow constraints]
--- True if there is any intersection between dom(model) and tvs
-modelCanRewrite model tvs = not (disjointUdfmUfm model tvs)
-     -- The low-level use of disjointUFM might e surprising.
-     -- InertModel = TyVarEnv Ct, and we want to see if its domain
-     -- is disjoint from that of a TcTyCoVarSet.  So we drop down
-     -- to the underlying UniqFM.  A bit yukky, but efficient.
+maybeEmitShadow :: InertCans -> Ct -> TcS Ct
+-- See Note [The improvement story and derived shadows]
+maybeEmitShadow ics ct
+  | let ev = ctEvidence ct
+  , CtWanted { ctev_pred = pred, ctev_loc = loc
+             , ctev_nosh = WDeriv } <- ev
+  , shouldSplitWD (inert_eqs ics) ct
+  = do { traceTcS "Emit derived shadow" (ppr ct)
+       ; let derived_ev = CtDerived { ctev_pred = pred
+                                    , ctev_loc  = loc }
+             shadow_ct = ct { cc_ev = derived_ev }
+               -- Te shadow constraint keeps the canonical shape.
+               -- This just saves work, but is sometimes important;
+               -- see Note [Keep CDictCan shadows as CDictCan]
+       ; emitWork [shadow_ct]
+
+       ; let ev' = ev { ctev_nosh = WOnly }
+             ct' = ct { cc_ev = ev' }
+                 -- Record that it now has a shadow
+                 -- This is /the/ place we set the flag to WOnly
+       ; return ct' }
 
-rewritableTyCoVars :: Ct -> TcTyVarSet
--- The tyvars of a Ct that can be rewritten
-rewritableTyCoVars (CFunEqCan { cc_tyargs = tys }) = tyCoVarsOfTypes tys
-rewritableTyCoVars ct                              = tyCoVarsOfType (ctPred ct)
+  | otherwise
+  = return ct
+
+shouldSplitWD :: InertEqs -> Ct -> Bool
+-- Precondition: 'ct' is [WD], and is inert
+-- True <=> we should split ct ito [W] and [D] because
+--          the inert_eqs can make progress on the [D]
+-- See Note [Splitting WD constraints]
+
+shouldSplitWD inert_eqs (CFunEqCan { cc_tyargs = tys })
+  = should_split_match_args inert_eqs tys
+    -- We don't need to split if the tv is the RHS fsk
+
+shouldSplitWD inert_eqs (CDictCan { cc_tyargs = tys })
+  = should_split_match_args inert_eqs tys
+    -- NB True: ignore coercions
+    -- See Note [Splitting WD constraints]
+
+shouldSplitWD inert_eqs (CTyEqCan { cc_tyvar = tv, cc_rhs = ty
+                                  , cc_eq_rel = eq_rel })
+  =  tv `elemDVarEnv` inert_eqs
+  || anyRewritableTyVar False eq_rel (canRewriteTv inert_eqs) ty
+  -- NB False: do not ignore casts and coercions
+  -- See Note [Splitting WD constraints]
+
+shouldSplitWD inert_eqs (CIrredCan { cc_ev = ev })
+  = anyRewritableTyVar False (ctEvEqRel ev) (canRewriteTv inert_eqs) (ctEvPred ev)
+
+shouldSplitWD _ _ = False   -- No point in splitting otherwise
+
+should_split_match_args :: InertEqs -> [TcType] -> Bool
+-- True if the inert_eqs can rewrite anything in the argument
+-- types, ignoring casts and coercions
+should_split_match_args inert_eqs tys
+  = any (anyRewritableTyVar True NomEq (canRewriteTv inert_eqs)) tys
+    -- NB True: ignore casts coercions
+    -- See Note [Splitting WD constraints]
+
+canRewriteTv :: InertEqs -> EqRel -> TyVar -> Bool
+canRewriteTv inert_eqs eq_rel tv
+  | Just (ct : _) <- lookupDVarEnv inert_eqs tv
+  , CTyEqCan { cc_eq_rel = eq_rel1 } <- ct
+  = eq_rel1 `eqCanRewrite` eq_rel
+  | otherwise
+  = False
+
+isImprovable :: CtEvidence -> Bool
+-- See Note [Do not do improvement for WOnly]
+isImprovable (CtWanted { ctev_nosh = WOnly }) = False
+isImprovable _                                = True
+
+
+{- *********************************************************************
+*                                                                      *
+                   Inert equalities
+*                                                                      *
+********************************************************************* -}
+
+addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
+addTyEq old_eqs tv ct
+  = extendDVarEnv_C add_eq old_eqs tv [ct]
+  where
+    add_eq old_eqs _
+      | isWantedCt ct
+      , (eq1 : eqs) <- old_eqs
+      = eq1 : ct : eqs
+      | otherwise
+      = ct : old_eqs
+
+foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
+foldTyEqs k eqs z
+  = foldDVarEnv (\cts z -> foldr k z cts) z eqs
+
+findTyEqs :: InertCans -> TyVar -> EqualCtList
+findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` []
+
+delTyEq :: InertEqs -> TcTyVar -> TcType -> InertEqs
+delTyEq m tv t = modifyDVarEnv (filter (not . isThisOne)) m tv
+  where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
+        isThisOne _                          = False
+
+lookupInertTyVar :: InertEqs -> TcTyVar -> Maybe TcType
+lookupInertTyVar ieqs tv
+  = case lookupDVarEnv ieqs tv of
+      Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _ ) -> Just rhs
+      _                                                        -> Nothing
+
+lookupFlattenTyVar :: InertEqs -> TcTyVar -> TcType
+-- See Note [lookupFlattenTyVar]
+lookupFlattenTyVar ieqs ftv
+  = lookupInertTyVar ieqs ftv `orElse` mkTyVarTy ftv
+
+{- Note [lookupFlattenTyVar]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have an injective function F and
+  inert_funeqs:   F t1 ~ fsk1
+                  F t2 ~ fsk2
+  inert_eqs:      fsk1 ~ fsk2
+
+We never rewrite the RHS (cc_fsk) of a CFunEqCan.  But we /do/ want to
+get the [D] t1 ~ t2 from the injectiveness of F.  So we look up the
+cc_fsk of CFunEqCans in the inert_eqs when trying to find derived
+equalities arising from injectivity.
+-}
+
+
+{- *********************************************************************
+*                                                                      *
+                   Inert instances: inert_insts
+*                                                                      *
+********************************************************************* -}
+
+addInertForAll :: QCInst -> TcS ()
+-- Add a local Given instance, typically arising from a type signature
+addInertForAll new_qci
+  = updInertCans $ \ics ->
+    ics { inert_insts = add_qci (inert_insts ics) }
+  where
+    add_qci :: [QCInst] -> [QCInst]
+    -- See Note [Do not add duplicate quantified instances]
+    add_qci qcis | any same_qci qcis = qcis
+                 | otherwise         = new_qci : qcis
+
+    same_qci old_qci = tcEqType (ctEvPred (qci_ev old_qci))
+                                (ctEvPred (qci_ev new_qci))
+
+{- Note [Do not add duplicate quantified instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this (#15244):
+
+  f :: (C g, D g) => ....
+  class S g => C g where ...
+  class S g => D g where ...
+  class (forall a. Eq a => Eq (g a)) => S g where ...
+
+Then in f's RHS there are two identical quantified constraints
+available, one via the superclasses of C and one via the superclasses
+of D.  The two are identical, and it seems wrong to reject the program
+because of that. But without doing duplicate-elimination we will have
+two matching QCInsts when we try to solve constraints arising from f's
+RHS.
+
+The simplest thing is simply to eliminate duplicattes, which we do here.
+-}
+
+{- *********************************************************************
+*                                                                      *
+                  Adding an inert
+*                                                                      *
+************************************************************************
+
+Note [Adding an equality to the InertCans]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When adding an equality to the inerts:
+
+* Split [WD] into [W] and [D] if the inerts can rewrite the latter;
+  done by maybeEmitShadow.
+
+* Kick out any constraints that can be rewritten by the thing
+  we are adding.  Done by kickOutRewritable.
+
+* Note that unifying a:=ty, is like adding [G] a~ty; just use
+  kickOutRewritable with Nominal, Given.  See kickOutAfterUnification.
+
+Note [Kicking out CFunEqCan for fundeps]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider:
+   New:    [D] fmv1 ~ fmv2
+   Inert:  [W] F alpha ~ fmv1
+           [W] F beta  ~ fmv2
+
+where F is injective. The new (derived) equality certainly can't
+rewrite the inerts. But we *must* kick out the first one, to get:
+
+   New:   [W] F alpha ~ fmv1
+   Inert: [W] F beta ~ fmv2
+          [D] fmv1 ~ fmv2
+
+and now improvement will discover [D] alpha ~ beta. This is important;
+eg in #9587.
+
+So in kickOutRewritable we look at all the tyvars of the
+CFunEqCan, including the fsk.
+-}
 
---------------
 addInertCan :: Ct -> TcS ()  -- Constraints *other than* equalities
+-- Precondition: item /is/ canonical
+-- See Note [Adding an equality to the InertCans]
 addInertCan ct
   = do { traceTcS "insertInertCan {" $
          text "Trying to insert new inert item:" <+> ppr ct
 
        ; ics <- getInertCans
+       ; ct  <- maybeEmitShadow ics ct
+       ; ics <- maybeKickOut ics ct
        ; setInertCans (add_item ics ct)
 
-       -- Emit shadow derived if necessary
-       -- See Note [Emitting shadow constraints]
-       ; let rw_tvs = rewritableTyCoVars ct
-       ; when (isWantedCt ct && modelCanRewrite (inert_model ics) rw_tvs)
-              -- See Note [Add shadows only for Wanteds]
-              (emitWork [mkShadowCt ct])
-
        ; traceTcS "addInertCan }" $ empty }
 
+maybeKickOut :: InertCans -> Ct -> TcS InertCans
+-- For a CTyEqCan, kick out any inert that can be rewritten by the CTyEqCan
+maybeKickOut ics ct
+  | CTyEqCan { cc_tyvar = tv, cc_ev = ev, cc_eq_rel = eq_rel } <- ct
+  = do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) tv ics
+       ; return ics' }
+  | otherwise
+  = return ics
+
 add_item :: InertCans -> Ct -> InertCans
 add_item ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
   = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
 
-add_item ics item@(CIrredEvCan { cc_ev = ev })
-  = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item
+add_item ics item@(CTyEqCan { cc_tyvar = tv, cc_ev = ev })
+  = ics { inert_eqs   = addTyEq (inert_eqs ics) tv item
         , inert_count = bumpUnsolvedCount ev (inert_count ics) }
-       -- The 'False' is because the irreducible constraint might later instantiate
-       -- to an equality.
-       -- But since we try to simplify first, if there's a constraint function FC with
-       --    type instance FC Int = Show
-       -- we'll reduce a constraint (FC Int a) to Show a, and never add an inert irreducible
+
+add_item ics@(IC { inert_irreds = irreds, inert_count = count })
+         item@(CIrredCan { cc_ev = ev, cc_insol = insoluble })
+  = ics { inert_irreds = irreds `Bag.snocBag` item
+        , inert_count  = if insoluble
+                         then count  -- inert_count does not include insolubles
+                         else bumpUnsolvedCount ev count }
 
 add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
   = ics { inert_dicts = addDict (inert_dicts ics) cls tys item
@@ -1380,9 +1661,8 @@ add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
 
 add_item _ item
   = pprPanic "upd_inert set: can't happen! Inserting " $
-    ppr item   -- CTyEqCan is dealt with by addInertEq
-               -- Can't be CNonCanonical, CHoleCan,
-               -- because they only land in inert_insols
+    ppr item   -- Can't be CNonCanonical, CHoleCan,
+               -- because they only land in inert_irreds
 
 bumpUnsolvedCount :: CtEvidence -> Int -> Int
 bumpUnsolvedCount ev n | isWanted ev = n+1
@@ -1390,21 +1670,40 @@ bumpUnsolvedCount ev n | isWanted ev = n+1
 
 
 -----------------------------------------
-kickOutRewritable :: CtFlavourRole  -- Flavour/role of the equality that
-                                    -- is being added to the inert set
-                  -> TcTyVar        -- The new equality is tv ~ ty
-                  -> InertCans
-                  -> (WorkList, InertCans)
+kickOutRewritable  :: CtFlavourRole  -- Flavour/role of the equality that
+                                      -- is being added to the inert set
+                    -> TcTyVar        -- The new equality is tv ~ ty
+                    -> InertCans
+                    -> TcS (Int, InertCans)
+kickOutRewritable new_fr new_tv ics
+  = do { let (kicked_out, ics') = kick_out_rewritable new_fr new_tv ics
+             n_kicked = workListSize kicked_out
+
+       ; unless (n_kicked == 0) $
+         do { updWorkListTcS (appendWorkList kicked_out)
+            ; csTraceTcS $
+              hang (text "Kick out, tv =" <+> ppr new_tv)
+                 2 (vcat [ text "n-kicked =" <+> int n_kicked
+                         , text "kicked_out =" <+> ppr kicked_out
+                         , text "Residual inerts =" <+> ppr ics' ]) }
+
+       ; return (n_kicked, ics') }
+
+kick_out_rewritable :: CtFlavourRole  -- Flavour/role of the equality that
+                                      -- is being added to the inert set
+                    -> TcTyVar        -- The new equality is tv ~ ty
+                    -> InertCans
+                    -> (WorkList, InertCans)
 -- See Note [kickOutRewritable]
-kickOutRewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
-                                        , inert_dicts    = dictmap
-                                        , inert_safehask = safehask
-                                        , inert_funeqs   = funeqmap
-                                        , inert_irreds   = irreds
-                                        , inert_insols   = insols
-                                        , inert_count    = n
-                                        , inert_model    = model })
-  | not (new_fr `eqCanRewriteFR` new_fr)
+kick_out_rewritable new_fr new_tv
+                    ics@(IC { inert_eqs      = tv_eqs
+                            , inert_dicts    = dictmap
+                            , inert_safehask = safehask
+                            , inert_funeqs   = funeqmap
+                            , inert_irreds   = irreds
+                            , inert_insts    = old_insts
+                            , inert_count    = n })
+  | not (new_fr `eqMayRewriteFR` new_fr)
   = (emptyWorkList, ics)
         -- If new_fr can't rewrite itself, it can't rewrite
         -- anything else, so no need to kick out anything.
@@ -1419,44 +1718,71 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
                        , inert_safehask = safehask   -- ??
                        , inert_funeqs   = feqs_in
                        , inert_irreds   = irs_in
-                       , inert_insols   = insols_in
-                       , inert_count    = n - workListWantedCount kicked_out
-                       , inert_model    = model }
-                     -- Leave the model unchanged
-
-    kicked_out = WL { wl_eqs    = tv_eqs_out
-                    , wl_funeqs = feqs_out
-                    , wl_deriv  = []
-                    , wl_rest   = bagToList (dicts_out `andCts` irs_out
-                                             `andCts` insols_out)
-                    , wl_implics = emptyBag }
+                       , inert_insts    = insts_in
+                       , inert_count    = n - workListWantedCount kicked_out }
+
+    kicked_out :: WorkList
+    -- NB: use extendWorkList to ensure that kicked-out equalities get priority
+    -- See Note [Prioritise equality constraints] (Kick-out).
+    -- The irreds may include non-canonical (hetero-kinded) equality
+    -- constraints, which perhaps may have become soluble after new_tv
+    -- is substituted; ditto the dictionaries, which may include (a~b)
+    -- or (a~~b) constraints.
+    kicked_out = foldr extendWorkListCt
+                          (emptyWorkList { wl_eqs    = tv_eqs_out
+                                         , wl_funeqs = feqs_out })
+                          ((dicts_out `andCts` irs_out)
+                            `extendCtsList` insts_out)
 
     (tv_eqs_out, tv_eqs_in) = foldDVarEnv kick_out_eqs ([], emptyDVarEnv) tv_eqs
-    (feqs_out,   feqs_in)   = partitionFunEqs  kick_out_fe funeqmap
+    (feqs_out,   feqs_in)   = partitionFunEqs  kick_out_ct funeqmap
+           -- See Note [Kicking out CFunEqCan for fundeps]
     (dicts_out,  dicts_in)  = partitionDicts   kick_out_ct dictmap
     (irs_out,    irs_in)    = partitionBag     kick_out_ct irreds
-    (insols_out, insols_in) = partitionBag     kick_out_ct insols
-      -- Kick out even insolubles; see Note [Kick out insolubles]
+      -- Kick out even insolubles: See Note [Rewrite insolubles]
+      -- Of course we must kick out irreducibles like (c a), in case
+      -- we can rewrite 'c' to something more useful
+
+    -- Kick-out for inert instances
+    -- See Note [Quantified constraints] in TcCanonical
+    insts_out :: [Ct]
+    insts_in  :: [QCInst]
+    (insts_out, insts_in)
+       | fr_may_rewrite (Given, NomEq)  -- All the insts are Givens
+       = partitionWith kick_out_qci old_insts
+       | otherwise
+       = ([], old_insts)
+    kick_out_qci qci
+      | let ev = qci_ev qci
+      , fr_can_rewrite_ty NomEq (ctEvPred (qci_ev qci))
+      = Left (mkNonCanonical ev)
+      | otherwise
+      = Right qci
 
-    fr_can_rewrite :: CtEvidence -> Bool
-    fr_can_rewrite ev = new_fr `eqCanRewriteFR` (ctEvFlavourRole ev)
+    (_, new_role) = new_fr
 
-    kick_out_ct :: Ct -> Bool
-    -- Kick it out if the new CTyEqCan can rewrite the inert
-    -- one. See Note [kickOutRewritable]
-    kick_out_ct ct
-      = fr_can_rewrite ev
-        && new_tv `elemVarSet` tyCoVarsOfType (ctEvPred ev)
-      where
-        ev = ctEvidence ct
+    fr_can_rewrite_ty :: EqRel -> Type -> Bool
+    fr_can_rewrite_ty role ty = anyRewritableTyVar False role
+                                                   fr_can_rewrite_tv ty
+    fr_can_rewrite_tv :: EqRel -> TyVar -> Bool
+    fr_can_rewrite_tv role tv = new_role `eqCanRewrite` role
+                             && tv == new_tv
 
-    kick_out_fe :: Ct -> Bool
-    kick_out_fe (CFunEqCan { cc_ev = ev, cc_tyargs = tys, cc_fsk = fsk })
-      = new_tv == fsk  -- If RHS is new_tvs, kick out /regardless of flavour/
-                       -- See Note [Kicking out CFunEqCan for fundeps]
-        || (fr_can_rewrite ev
-            && new_tv `elemVarSet` tyCoVarsOfTypes tys)
-    kick_out_fe ct = pprPanic "kick_out_fe" (ppr ct)
+    fr_may_rewrite :: CtFlavourRole -> Bool
+    fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs
+        -- Can the new item rewrite the inert item?
+
+    kick_out_ct :: Ct -> Bool
+    -- Kick it out if the new CTyEqCan can rewrite the inert one
+    -- See Note [kickOutRewritable]
+    kick_out_ct ct | let fs@(_,role) = ctFlavourRole ct
+                   = fr_may_rewrite fs
+                   && fr_can_rewrite_ty role (ctPred ct)
+                  -- False: ignore casts and coercions
+                  -- NB: this includes the fsk of a CFunEqCan.  It can't
+                  --     actually be rewritten, but we need to kick it out
+                  --     so we get to take advantage of injectivity
+                  -- See Note [Kicking out CFunEqCan for fundeps]
 
     kick_out_eqs :: EqualCtList -> ([Ct], DTyVarEnv EqualCtList)
                  -> ([Ct], DTyVarEnv EqualCtList)
@@ -1465,73 +1791,45 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
                                []      -> acc_in
                                (eq1:_) -> extendDVarEnv acc_in (cc_tyvar eq1) eqs_in)
       where
-        (eqs_in, eqs_out) = partition keep_eq eqs
+        (eqs_out, eqs_in) = partition kick_out_eq eqs
 
     -- Implements criteria K1-K3 in Note [Extending the inert equalities]
-    keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
-                      , cc_eq_rel = eq_rel })
-      | tv == new_tv
-      = not (fr_can_rewrite ev)  -- (K1)
+    kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty
+                          , cc_ev = ev, cc_eq_rel = eq_rel })
+      | not (fr_may_rewrite fs)
+      = False  -- Keep it in the inert set if the new thing can't rewrite it
+
+      -- Below here (fr_may_rewrite fs) is True
+      | tv == new_tv              = True        -- (K1)
+      | kick_out_for_inertness    = True
+      | kick_out_for_completeness = True
+      | otherwise                 = False
 
-      | otherwise
-      = check_k2 && check_k3
       where
-        fs = ctEvFlavourRole ev
-        check_k2 = not (fs  `eqCanRewriteFR` fs)                   -- (K2a)
-                ||     (fs  `eqCanRewriteFR` new_fr)               -- (K2b)
-                || not (new_fr `eqCanRewriteFR` fs)                -- (K2c)
-                || not (new_tv `elemVarSet` tyCoVarsOfType rhs_ty) -- (K2d)
-
-        check_k3
-          | new_fr `eqCanRewriteFR` fs
+        fs = (ctEvFlavour ev, eq_rel)
+        kick_out_for_inertness
+          =        (fs `eqMayRewriteFR` fs)       -- (K2a)
+            && not (fs `eqMayRewriteFR` new_fr)   -- (K2b)
+            && fr_can_rewrite_ty eq_rel rhs_ty    -- (K2d)
+            -- (K2c) is guaranteed by the first guard of keep_eq
+
+        kick_out_for_completeness
           = case eq_rel of
-              NomEq  -> not (rhs_ty `eqType` mkTyVarTy new_tv)
-              ReprEq -> not (isTyVarExposed new_tv rhs_ty)
-
-          | otherwise
-          = True
+              NomEq  -> rhs_ty `eqType` mkTyVarTy new_tv
+              ReprEq -> isTyVarHead new_tv rhs_ty
 
-    keep_eq ct = pprPanic "keep_eq" (ppr ct)
+    kick_out_eq ct = pprPanic "keep_eq" (ppr ct)
 
 kickOutAfterUnification :: TcTyVar -> TcS Int
 kickOutAfterUnification new_tv
   = do { ics <- getInertCans
-       ; let (kicked_out1, ics1) = kickOutModel new_tv ics
-             (kicked_out2, ics2) = kickOutRewritable (Given,NomEq)
-                                                     new_tv ics1
+       ; (n_kicked, ics2) <- kickOutRewritable (Given,NomEq)
+                                                 new_tv ics
                      -- Given because the tv := xi is given; NomEq because
                      -- only nominal equalities are solved by unification
-             kicked_out = appendWorkList kicked_out1 kicked_out2
-       ; setInertCans ics2
-       ; updWorkListTcS (appendWorkList kicked_out)
-
-       ; unless (isEmptyWorkList kicked_out) $
-         csTraceTcS $
-         hang (text "Kick out (unify), tv =" <+> ppr new_tv)
-            2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
-                    , text "kicked_out =" <+> ppr kicked_out
-                    , text "Residual inerts =" <+> ppr ics2 ])
-       ; return (workListSize kicked_out) }
-
-kickOutModel :: TcTyVar -> InertCans -> (WorkList, InertCans)
-kickOutModel new_tv ics@(IC { inert_model = model, inert_eqs = eqs })
-  = (foldDVarEnv add emptyWorkList der_out, ics { inert_model = new_model })
-  where
-    (der_out, new_model) = partitionDVarEnv kick_out_der model
-
-    kick_out_der :: Ct -> Bool
-    kick_out_der (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs })
-      = new_tv == tv || new_tv `elemVarSet` tyCoVarsOfType rhs
-    kick_out_der _ = False
-
-    add :: Ct -> WorkList -> WorkList
-    -- Don't kick out a Derived if there is a Given or Wanted with
-    -- the same predicate.  The model is just a shadow copy, and the
-    -- Given/Wanted will serve the purpose.
-    add (CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) wl
-      | not (isInInertEqs eqs tv rhs) = extendWorkListDerived (ctEvLoc ev) ev wl
-    add _ wl                          = wl
 
+       ; setInertCans ics2
+       ; return n_kicked }
 
 {- Note [kickOutRewritable]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1553,27 +1851,37 @@ new equality, to maintain the inert-set invariants.
     kick out constraints that mention type variables whose kinds
     contain this variable!
 
-  - We do not need to kick anything out from the model; we only
-    add [D] constraints to the model (in effect) and they are
-    fully rewritten by the model, so (K2b) holds
-
-  - A Derived equality can kick out [D] constraints in inert_dicts,
-    inert_irreds etc.  Nothing in inert_eqs because there are no
-    Derived constraints in inert_eqs (they are in the model)
+  - A Derived equality can kick out [D] constraints in inert_eqs,
+    inert_dicts, inert_irreds etc.
 
   - We don't kick out constraints from inert_solved_dicts, and
     inert_solved_funeqs optimistically. But when we lookup we have to
     take the substitution into account
 
 
-Note [Kick out insolubles]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Rewrite 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 insoluble 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.
+because an occurs check.  And then we unify alpha := [Int].  Then we
+really want to rewrite the insoluble 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.
+
+Similarly, if we have a CHoleCan, we'd like to rewrite it with any
+Givens, to give as informative an error messasge as possible
+(#12468, #11325).
+
+Hence:
+ * In the main simlifier loops in TcSimplify (solveWanteds,
+   simpl_loop), we feed the insolubles in solveSimpleWanteds,
+   so that they get rewritten (albeit not solved).
+
+ * We kick insolubles out of the inert set, if they can be
+   rewritten (see TcSMonad.kick_out_rewritable)
+
+ * We rewrite those insolubles in TcCanonical.
+   See Note [Make sure that insolubles are fully rewritten]
 -}
 
 
@@ -1586,10 +1894,11 @@ addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
 addInertSafehask _ item
   = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item
 
-insertSafeOverlapFailureTcS :: Ct -> TcS ()
+insertSafeOverlapFailureTcS :: InstanceWhat -> Ct -> TcS ()
 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
-insertSafeOverlapFailureTcS item
-  = updInertCans (\ics -> addInertSafehask ics item)
+insertSafeOverlapFailureTcS what item
+  | safeOverlap what = return ()
+  | otherwise        = updInertCans (\ics -> addInertSafehask ics item)
 
 getSafeOverlapFailures :: TcS Cts
 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
@@ -1598,16 +1907,26 @@ getSafeOverlapFailures
       ; return $ foldDicts consCts safehask emptyCts }
 
 --------------
-addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
--- Add a new item in the solved set of the monad
+addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [Type] -> TcS ()
+-- Conditionally add a new item in the solved set of the monad
 -- See Note [Solved dictionaries]
-addSolvedDict item cls tys
-  | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
-  = return ()
-  | otherwise
+addSolvedDict what item cls tys
+  | isWanted item
+  , instanceReturnsDictCon what
   = do { traceTcS "updSolvedSetTcs:" $ ppr item
        ; updInertTcS $ \ ics ->
              ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
+  | otherwise
+  = return ()
+
+getSolvedDicts :: TcS (DictMap CtEvidence)
+getSolvedDicts = do { ics <- getTcSInerts; return (inert_solved_dicts ics) }
+
+setSolvedDicts :: DictMap CtEvidence -> TcS ()
+setSolvedDicts solved_dicts
+  = updInertTcS $ \ ics ->
+    ics { inert_solved_dicts = solved_dicts }
+
 
 {- *********************************************************************
 *                                                                      *
@@ -1628,35 +1947,6 @@ getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }
 setInertCans :: InertCans -> TcS ()
 setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }
 
-takeGivenInsolubles :: TcS Cts
--- See Note [The inert set after solving Givens]
-takeGivenInsolubles
-  = updRetInertCans $ \ cans ->
-    ( inert_insols cans
-    , cans { inert_insols = emptyBag
-           , inert_funeqs = filterFunEqs isGivenCt (inert_funeqs cans) } )
-
-{- Note [The inert set after solving Givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-After solving the Givens we take two things out of the inert set
-
-  a) The insolubles; we return these to report inaccessible code
-     We return these separately.  We don't want to leave them in
-     the inert set, lest we confuse them with insolubles arising from
-     solving wanteds
-
-  b) Any Derived CFunEqCans.  Derived CTyEqCans are in the
-     inert_model and do no harm.  In contrast, Derived CFunEqCans
-     get mixed up with the Wanteds later and confuse the
-     post-solve-wanted unflattening (Trac #10507).
-     E.g.  From   [G] 1 <= m, [G] m <= n
-           We get [D] 1 <= n, and we must remove it!
-         Otherwise we unflatten it more then once, and assign
-         to its fmv more than once...disaster.
-     It's ok to remove them because they turned out not to
-     yield an insoluble, and hence have now done their work.
--}
-
 updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
 -- Modify the inert set with the supplied function
 updRetInertCans upd_fn
@@ -1694,8 +1984,11 @@ updInertIrreds upd_fn
 getInertEqs :: TcS (DTyVarEnv EqualCtList)
 getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
 
-getInertModel :: TcS InertModel
-getInertModel = do { inert <- getInertCans; return (inert_model inert) }
+getInertInsols :: TcS Cts
+-- Returns insoluble equality constraints
+-- specifically including Givens
+getInertInsols = do { inert <- getInertCans
+                    ; return (filterBag insolubleEqCt (inert_irreds inert)) }
 
 getInertGivens :: TcS [Ct]
 -- Returns the Given constraints in the inert set,
@@ -1707,34 +2000,57 @@ getInertGivens
                      $ concat (dVarEnvElts (inert_eqs inerts))
        ; return (filter isGivenCt all_cts) }
 
-getPendingScDicts :: TcS [Ct]
--- Find all inert Given dictionaries whose cc_pend_sc flag is True
--- Set the flag to False in the inert set, and return that Ct
-getPendingScDicts = updRetInertCans get_sc_dicts
+getPendingGivenScs :: TcS [Ct]
+-- Find all inert Given dictionaries, or quantified constraints,
+--     whose cc_pend_sc flag is True
+--     and that belong to the current level
+-- Set their cc_pend_sc flag to False in the inert set, and return that Ct
+getPendingGivenScs = do { lvl <- getTcLevel
+                        ; updRetInertCans (get_sc_pending lvl) }
+
+get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans)
+get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts })
+  = ASSERT2( all isGivenCt sc_pending, ppr sc_pending )
+       -- When getPendingScDics is called,
+       -- there are never any Wanteds in the inert set
+    (sc_pending, ic { inert_dicts = dicts', inert_insts = insts' })
   where
-    get_sc_dicts ic@(IC { inert_dicts = dicts })
-      = (sc_pend_dicts, ic')
-      where
-        ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts }
+    sc_pending = sc_pend_insts ++ sc_pend_dicts
+
+    sc_pend_dicts = foldDicts get_pending dicts []
+    dicts' = foldr add dicts sc_pend_dicts
 
-        sc_pend_dicts :: [Ct]
-        sc_pend_dicts = foldDicts get_pending dicts []
+    (sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
 
     get_pending :: Ct -> [Ct] -> [Ct]  -- Get dicts with cc_pend_sc = True
                                        -- but flipping the flag
     get_pending dict dicts
-        | Just dict' <- isPendingScDict dict = dict' : dicts
-        | otherwise                          = dicts
+        | Just dict' <- isPendingScDict dict
+        , belongs_to_this_level (ctEvidence dict)
+        = dict' : dicts
+        | otherwise
+        = dicts
 
     add :: Ct -> DictMap Ct -> DictMap Ct
     add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
         = addDict dicts cls tys ct
     add ct _ = pprPanic "getPendingScDicts" (ppr ct)
 
+    get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
+    get_pending_inst cts qci@(QCI { qci_ev = ev })
+       | Just qci' <- isPendingScInst qci
+       , belongs_to_this_level ev
+       = (CQuantCan qci' : cts, qci')
+       | otherwise
+       = (cts, qci)
+
+    belongs_to_this_level ev = ctLocLevel (ctEvLoc ev) == this_lvl
+    -- We only want Givens from this level; see (3a) in
+    -- Note [The superclass story] in TcCanonical
+
 getUnsolvedInerts :: TcS ( Bag Implication
                          , Cts     -- Tyvar eqs: a ~ ty
                          , Cts     -- Fun eqs:   F a ~ ty
-                         , Cts     -- Insoluble
                          , Cts )   -- All others
 -- Return all the unsolved [Wanted] or [Derived] constraints
 --
@@ -1746,43 +2062,39 @@ getUnsolvedInerts
            , inert_funeqs = fun_eqs
            , inert_irreds = irreds
            , inert_dicts  = idicts
-           , inert_insols = insols
-           , inert_model  = model } <- getInertCans
-      ; keep_derived <- keepSolvingDeriveds
-
-      ; let der_tv_eqs       = foldDVarEnv (add_der_eq keep_derived tv_eqs)
-                                          emptyCts model
-            unsolved_tv_eqs  = foldTyEqs add_if_unsolved tv_eqs der_tv_eqs
-            unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts
+           } <- getInertCans
+
+      ; let unsolved_tv_eqs  = foldTyEqs add_if_unsolved tv_eqs emptyCts
+            unsolved_fun_eqs = foldFunEqs add_if_wanted fun_eqs emptyCts
             unsolved_irreds  = Bag.filterBag is_unsolved irreds
             unsolved_dicts   = foldDicts add_if_unsolved idicts emptyCts
-            others           = unsolved_irreds `unionBags` unsolved_dicts
+            unsolved_others  = unsolved_irreds `unionBags` unsolved_dicts
 
       ; implics <- getWorkListImplics
 
       ; traceTcS "getUnsolvedInerts" $
         vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
              , text "fun eqs =" <+> ppr unsolved_fun_eqs
-             , text "insols =" <+> ppr insols
-             , text "others =" <+> ppr others
+             , text "others =" <+> ppr unsolved_others
              , text "implics =" <+> ppr implics ]
 
-      ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) }
-              -- Keep even the given insolubles
-              -- so that we can report dead GADT pattern match branches
+      ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, unsolved_others) }
   where
-    add_der_eq keep_derived tv_eqs ct cts
-       -- See Note [Unsolved Derived equalities]
-       | CTyEqCan { cc_tyvar = tv, cc_rhs = rhs } <- ct
-       , isMetaTyVar tv || keep_derived
-       , not (isInInertEqs tv_eqs tv rhs) = ct `consBag` cts
-       | otherwise                        = cts
     add_if_unsolved :: Ct -> Cts -> Cts
     add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
                            | otherwise      = cts
 
     is_unsolved ct = not (isGivenCt ct)   -- Wanted or Derived
 
+    -- For CFunEqCans we ignore the Derived ones, and keep
+    -- only the Wanteds for flattening.  The Derived ones
+    -- share a unification variable with the corresponding
+    -- Wanted, so we definitely don't want to participate
+    -- in unflattening
+    -- See Note [Type family equations]
+    add_if_wanted ct cts | isWantedCt ct = ct `consCts` cts
+                         | otherwise     = cts
+
 isInInertEqs :: DTyVarEnv EqualCtList -> TcTyVar -> TcType -> Bool
 -- True if (a ~N ty) is in the inert set, in either Given or Wanted
 isInInertEqs eqs tv rhs
@@ -1798,46 +2110,45 @@ isInInertEqs eqs tv rhs
 
 getNoGivenEqs :: TcLevel          -- TcLevel of this implication
                -> [TcTyVar]       -- Skolems of this implication
-               -> Cts             -- Given insolubles from solveGivens
-               -> TcS Bool        -- True <=> definitely no residual given equalities
+               -> TcS ( Bool      -- True <=> definitely no residual given equalities
+                      , Cts )     -- Insoluble equalities arising from givens
 -- See Note [When does an implication have given equalities?]
-getNoGivenEqs tclvl skol_tvs given_insols
-  = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds
-                    , inert_funeqs = funeqs })
-             <- getInertCans
-       ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
-
-             has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
-                                      (iirreds `unionBags` given_insols)
-                          || anyDVarEnv (eqs_given_here local_fsks) ieqs
-
-       ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
-                                        , ppr given_insols])
-       ; return (not has_given_eqs) }
+getNoGivenEqs tclvl skol_tvs
+  = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = irreds })
+              <- getInertCans
+       ; let has_given_eqs = foldr ((||) . ct_given_here) False irreds
+                          || anyDVarEnv eqs_given_here ieqs
+             insols = filterBag insolubleEqCt irreds
+                      -- Specifically includes ones that originated in some
+                      -- outer context but were refined to an insoluble by
+                      -- a local equality; so do /not/ add ct_given_here.
+
+       ; traceTcS "getNoGivenEqs" $
+         vcat [ if has_given_eqs then text "May have given equalities"
+                                 else text "No given equalities"
+              , text "Skols:" <+> ppr skol_tvs
+              , text "Inerts:" <+> ppr inerts
+              , text "Insols:" <+> ppr insols]
+       ; return (not has_given_eqs, insols) }
   where
-    eqs_given_here :: VarSet -> EqualCtList -> Bool
-    eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
+    eqs_given_here :: EqualCtList -> Bool
+    eqs_given_here [ct@(CTyEqCan { cc_tyvar = tv })]
                               -- Givens are always a sigleton
-      = not (skolem_bound_here local_fsks tv) && ev_given_here ev
-    eqs_given_here _ = False
+      = not (skolem_bound_here tv) && ct_given_here ct
+    eqs_given_here _ = False
 
-    ev_given_here :: CtEvidence -> Bool
-    -- True for a Given bound by the curent implication,
+    ct_given_here :: Ct -> Bool
+    -- True for a Given bound by the current implication,
     -- i.e. the current level
-    ev_given_here ev
-      =  isGiven ev
-      && tclvl == ctLocLevel (ctEvLoc ev)
-
-    add_fsk :: Ct -> VarSet -> VarSet
-    add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
-                    , isGiven ev = extendVarSet fsks tv
-                    | otherwise  = fsks
+    ct_given_here ct =  isGiven ev
+                     && tclvl == ctLocLevel (ctEvLoc ev)
+        where
+          ev = ctEvidence ct
 
     skol_tv_set = mkVarSet skol_tvs
-    skolem_bound_here local_fsks tv -- See Note [Let-bound skolems]
+    skolem_bound_here tv -- See Note [Let-bound skolems]
       = case tcTyVarDetails tv of
           SkolemTv {} -> tv `elemVarSet` skol_tv_set
-          FlatSkol {} -> not (tv `elemVarSet` local_fsks)
           _           -> False
 
 -- | Returns Given constraints that might,
@@ -1845,7 +2156,7 @@ getNoGivenEqs tclvl skol_tvs given_insols
 -- Given might overlap with an instance. See Note [Instance and Given overlap]
 -- in TcInteract.
 matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
-matchableGivens loc_w pred (IS { inert_cans = inert_cans })
+matchableGivens loc_w pred_w (IS { inert_cans = inert_cans })
   = filterBag matchable_given all_relevant_givens
   where
     -- just look in class constraints and irreds. matchableGivens does get called
@@ -1854,7 +2165,7 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans })
     -- non-canonical -- that is, irreducible -- equalities.
     all_relevant_givens :: Cts
     all_relevant_givens
-      | Just (clas, _) <- getClassPredTys_maybe pred
+      | Just (clas, _) <- getClassPredTys_maybe pred_w
       = findDictsByClass (inert_dicts inert_cans) clas
         `unionBags` inert_irreds inert_cans
       | otherwise
@@ -1862,24 +2173,27 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans })
 
     matchable_given :: Ct -> Bool
     matchable_given ct
-      | CtGiven { ctev_loc = loc_g } <- ctev
-      , Just _ <- tcUnifyTys bind_meta_tv [ctEvPred ctev] [pred]
-      , not (prohibitedSuperClassSolve loc_g loc_w)
-      = True
+      | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct
+      = mightMatchLater pred_g loc_g pred_w loc_w
 
       | otherwise
       = False
-      where
-        ctev = cc_ev ct
 
+mightMatchLater :: TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
+mightMatchLater given_pred given_loc wanted_pred wanted_loc
+  =  not (prohibitedSuperClassSolve given_loc wanted_loc)
+  && isJust (tcUnifyTys bind_meta_tv [given_pred] [wanted_pred])
+  where
     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
+    -- otherwise.  More info in Note [Instance and Given overlap]
+    -- in TcInteract
+    bind_meta_tv tv | isMetaTyVar tv
+                    , not (isFskTyVar tv) = BindMe
+                    | otherwise           = Skolem
 
 prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
 -- See Note [Solving superclass constraints] in TcInstDcls
@@ -1892,17 +2206,10 @@ prohibitedSuperClassSolve from_loc solve_loc
 
 {- Note [Unsolved Derived equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In getUnsolvedInerts, we return a derived equality from the model
-for two possible reasons:
-
-  * Because it is a candidate for floating out of this implication.
-    We only float equalities with a meta-tyvar on the left, so we only
-    pull those out here.
-
-  * If we are only solving derived constraints (i.e. tcs_need_derived
-    is true; see Note [Solving for Derived constraints]), then we
-    those Derived constraints are effectively unsolved, and we need
-    them!
+In getUnsolvedInerts, we return a derived equality from the inert_eqs
+because it is a candidate for floating out of this implication.  We
+only float equalities with a meta-tyvar on the left, so we only pull
+those out here.
 
 Note [When does an implication have given equalities?]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1912,7 +2219,7 @@ where beta is a unification variable that has already been unified
 to () in an outer scope.  Then we can float the (alpha ~ Int) out
 just fine. So when deciding whether the givens contain an equality,
 we should canonicalise first, rather than just looking at the original
-givens (Trac #8644).
+givens (#8644).
 
 So we simply look at the inert, canonical Givens and see if there are
 any equalities among them, the calculation of has_given_eqs.  There
@@ -1950,7 +2257,7 @@ are some wrinkles:
 Note [Let-bound skolems]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 If   * the inert set contains a canonical Given CTyEqCan (a ~ ty)
-and  * 'a' is a skolem bound in this very implication, b
+and  * 'a' is a skolem bound in this very implication,
 
 then:
 a) The Given is pretty much a let-binding, like
@@ -1964,7 +2271,36 @@ b) 'a' will have been completely substituted out in the inert set,
    so we can safely discard it.  Notably, it doesn't need to be
    returned as part of 'fsks'
 
-For an example, see Trac #9211.
+For an example, see #9211.
+
+See also TcUnify Note [Deeper level on the left] for how we ensure
+that the right variable is on the left of the equality when both are
+tyvars.
+
+You might wonder whether the skokem really needs to be bound "in the
+very same implication" as the equuality constraint.
+(c.f. #15009) Consider this:
+
+  data S a where
+    MkS :: (a ~ Int) => S a
+
+  g :: forall a. S a -> a -> blah
+  g x y = let h = \z. ( z :: Int
+                      , case x of
+                           MkS -> [y,z])
+          in ...
+
+From the type signature for `g`, we get `y::a` .  Then when when we
+encounter the `\z`, we'll assign `z :: alpha[1]`, say.  Next, from the
+body of the lambda we'll get
+
+  [W] alpha[1] ~ Int                             -- From z::Int
+  [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a   -- From [y,z]
+
+Now, suppose we decide to float `alpha ~ a` out of the implication
+and then unify `alpha := a`.  Now we are stuck!  But if treat
+`alpha ~ Int` first, and unify `alpha := Int`, all is fine.
+But we absolutely cannot float that equality or we will get stuck.
 -}
 
 removeInertCts :: [Ct] -> InertCans -> InertCans
@@ -1985,7 +2321,8 @@ removeInertCt is ct =
     CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty } ->
       is { inert_eqs    = delTyEq (inert_eqs is) x ty }
 
-    CIrredEvCan {}   -> panic "removeInertCt: CIrredEvCan"
+    CQuantCan {}     -> panic "removeInertCt: CQuantCan"
+    CIrredCan {}     -> panic "removeInertCt: CIrredEvCan"
     CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
     CHoleCan {}      -> panic "removeInertCt: CHoleCan"
 
@@ -2000,7 +2337,7 @@ lookupFlatCache fam_tc tys
     lookup_inerts inert_funeqs
       | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk, cc_tyargs = xis })
            <- findFunEq inert_funeqs fam_tc tys
-      , tys `eqTypes` xis   -- the lookup might find a near-match; see
+      , tys `eqTypes` xis   -- The lookup might find a near-match; see
                             -- Note [Use loose types in inert set]
       = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
       | otherwise = Nothing
@@ -2008,30 +2345,30 @@ lookupFlatCache fam_tc tys
     lookup_flats flat_cache = findExactFunEq flat_cache fam_tc tys
 
 
-lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
+lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
-lookupInInerts pty
+lookupInInerts loc pty
   | ClassPred cls tys <- classifyPredType pty
   = do { inerts <- getTcSInerts
-       ; return (lookupSolvedDict inerts cls tys `mplus`
-                 lookupInertDict (inert_cans inerts) cls tys) }
+       ; return (lookupSolvedDict inerts loc cls tys `mplus`
+                 lookupInertDict (inert_cans inerts) loc cls tys) }
   | otherwise -- NB: No caching for equalities, IPs, holes, or errors
   = return Nothing
 
 -- | Look up a dictionary inert. NB: the returned 'CtEvidence' might not
 -- match the input exactly. Note [Use loose types in inert set].
-lookupInertDict :: InertCans -> Class -> [Type] -> Maybe CtEvidence
-lookupInertDict (IC { inert_dicts = dicts }) cls tys
-  = case findDict dicts cls tys of
+lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
+lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
+  = case findDict dicts loc cls tys of
       Just ct -> Just (ctEvidence ct)
       _       -> Nothing
 
 -- | Look up a solved inert. NB: the returned 'CtEvidence' might not
 -- match the input exactly. See Note [Use loose types in inert set].
-lookupSolvedDict :: InertSet -> Class -> [Type] -> Maybe CtEvidence
+lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
 -- Returns just if exactly this predicate type exists in the solved.
-lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
-  = case findDict solved cls tys of
+lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
+  = case findDict solved loc cls tys of
       Just ev -> Just ev
       _       -> Nothing
 
@@ -2042,44 +2379,8 @@ lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
 ********************************************************************* -}
 
 foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
-foldIrreds k irreds z = foldrBag k z irreds
-
-
-{- *********************************************************************
-*                                                                      *
-                   Type equalities
-*                                                                      *
-********************************************************************* -}
-
-type EqualCtList = [Ct]
-
-{- Note [EqualCtList invariants]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-    * All are equalities
-    * All these equalities have the same LHS
-    * The list is never empty
-    * No element of the list can rewrite any other
-
- From the fourth invariant it follows that the list is
-   - A single Given, or
-   - Any number of Wanteds and/or Deriveds
--}
-
-addTyEq :: DTyVarEnv EqualCtList -> TcTyVar -> Ct -> DTyVarEnv EqualCtList
-addTyEq old_list tv it = extendDVarEnv_C (\old_eqs _new_eqs -> it : old_eqs)
-                                        old_list tv [it]
+foldIrreds k irreds z = foldr k z irreds
 
-foldTyEqs :: (Ct -> b -> b) -> DTyVarEnv EqualCtList -> b -> b
-foldTyEqs k eqs z
-  = foldDVarEnv (\cts z -> foldr k z cts) z eqs
-
-findTyEqs :: InertCans -> TyVar -> EqualCtList
-findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` []
-
-delTyEq :: DTyVarEnv EqualCtList -> TcTyVar -> TcType -> DTyVarEnv EqualCtList
-delTyEq m tv t = modifyDVarEnv (filter (not . isThisOne)) m tv
-  where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
-        isThisOne _                          = False
 
 {- *********************************************************************
 *                                                                      *
@@ -2094,7 +2395,7 @@ solvable from the other. So, we do lookup in the inert set using
 loose types, which omit the kind-check.
 
 We must be careful when using the result of a lookup because it may
-not match the requsted info exactly!
+not match the requested info exactly!
 
 -}
 
@@ -2154,16 +2455,66 @@ foldTcAppMap k m z = foldUDFM (foldTM k) z m
 *                                                                      *
 ********************************************************************* -}
 
+
+{- Note [Tuples hiding implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   f,g :: (?x::Int, C a) => a -> a
+   f v = let ?x = 4 in g v
+
+The call to 'g' gives rise to a Wanted constraint (?x::Int, C a).
+We must /not/ solve this from the Given (?x::Int, C a), because of
+the intervening binding for (?x::Int).  #14218.
+
+We deal with this by arranging that we always fail when looking up a
+tuple constraint that hides an implicit parameter. Not that this applies
+  * both to the inert_dicts (lookupInertDict)
+  * and to the solved_dicts (looukpSolvedDict)
+An alternative would be not to extend these sets with such tuple
+constraints, but it seemed more direct to deal with the lookup.
+
+Note [Solving CallStack constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose f :: HasCallStack => blah.  Then
+
+* Each call to 'f' gives rise to
+    [W] s1 :: IP "callStack" CallStack    -- CtOrigin = OccurrenceOf f
+  with a CtOrigin that says "OccurrenceOf f".
+  Remember that HasCallStack is just shorthand for
+    IP "callStack CallStack
+  See Note [Overview of implicit CallStacks] in TcEvidence
+
+* We cannonicalise such constraints, in TcCanonical.canClassNC, by
+  pushing the call-site info on the stack, and changing the CtOrigin
+  to record that has been done.
+   Bind:  s1 = pushCallStack <site-info> s2
+   [W] s2 :: IP "callStack" CallStack   -- CtOrigin = IPOccOrigin
+
+* Then, and only then, we can solve the constraint from an enclosing
+  Given.
+
+So we must be careful /not/ to solve 's1' from the Givens.  Again,
+we ensure this by arranging that findDict always misses when looking
+up souch constraints.
+-}
+
 type DictMap a = TcAppMap a
 
 emptyDictMap :: DictMap a
 emptyDictMap = emptyTcAppMap
 
--- sizeDictMap :: DictMap a -> Int
--- sizeDictMap m = foldDicts (\ _ x -> x+1) m 0
+findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
+findDict m loc cls tys
+  | isCTupleClass cls
+  , any hasIPPred tys   -- See Note [Tuples hiding implicit parameters]
+  = Nothing
+
+  | Just {} <- isCallStackPred cls tys
+  , OccurrenceOf {} <- ctLocOrigin loc
+  = Nothing             -- See Note [Solving CallStack constraints]
 
-findDict :: DictMap a -> Class -> [Type] -> Maybe a
-findDict m cls tys = findTcApp m (getUnique cls) tys
+  | otherwise
+  = findTcApp m (getUnique cls) tys
 
 findDictsByClass :: DictMap a -> Class -> Bag a
 findDictsByClass m cls
@@ -2178,7 +2529,7 @@ addDict m cls tys item = insertTcApp m (getUnique cls) tys item
 
 addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
 addDictsByClass m cls items
-  = addToUDFM m cls (foldrBag add emptyTM items)
+  = addToUDFM m cls (foldr add emptyTM items)
   where
     add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
     add ct _ = pprPanic "addDictsByClass" (ppr ct)
@@ -2216,9 +2567,6 @@ type FunEqMap a = TcAppMap a  -- A map whose key is a (TyCon, [Type]) pair
 emptyFunEqs :: TcAppMap a
 emptyFunEqs = emptyTcAppMap
 
-sizeFunEqMap :: FunEqMap a -> Int
-sizeFunEqMap m = foldFunEqs (\ _ x -> x+1) m 0
-
 findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
 findFunEq m tc tys = findTcApp m (getUnique tc) tys
 
@@ -2240,8 +2588,8 @@ foldFunEqs = foldTcAppMap
 -- mapFunEqs :: (a -> b) -> FunEqMap a -> FunEqMap b
 -- mapFunEqs = mapTcApp
 
-filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
-filterFunEqs = filterTcAppMap
+-- filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
+-- filterFunEqs = filterTcAppMap
 
 insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
 insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
@@ -2295,23 +2643,11 @@ All you can do is
 Filling in a dictionary evidence variable means to create a binding
 for it, so TcS carries a mutable location where the binding can be
 added.  This is initialised from the innermost implication constraint.
-
-Note [Solving for Derived constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Sometimes we invoke the solver on a bunch of Derived constraints, not to
-generate any evidence, but just to cause unification side effects or to
-produce a simpler set of constraints.  If that is what we are doing, we
-should do two things differently:
-  a) Don't stop when you've solved all the Wanteds; instead keep going
-     if there are any Deriveds in the work queue.
-  b) In getInertUnsolved, include Derived ones
 -}
 
 data TcSEnv
   = TcSEnv {
-      tcs_ev_binds    :: Maybe EvBindsVar,
-          -- this could be Nothing if we can't deal with non-equality
-          -- constraints, because, say, we're in a top-level type signature
+      tcs_ev_binds    :: EvBindsVar,
 
       tcs_unified     :: IORef Int,
          -- The number of unification variables we have filled
@@ -2323,39 +2659,34 @@ data TcSEnv
 
       -- The main work-list and the flattening worklist
       -- See Note [Work list priorities] and
-      tcs_worklist  :: IORef WorkList, -- Current worklist
-
-      tcs_used_tcvs :: IORef TyCoVarSet,
-        -- these variables were used when filling holes. Don't discard!
-        -- See also Note [Tracking redundant constraints] in TcSimplify
-
-      tcs_need_deriveds :: Bool
-        -- Keep solving, even if all the unsolved constraints are Derived
-        -- See Note [Solving for Derived constraints]
+      tcs_worklist  :: IORef WorkList -- Current worklist
     }
 
 ---------------
-newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
-
-instance Functor TcS where
-  fmap f m = TcS $ fmap f . unTcS m
+newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } deriving (Functor)
 
 instance Applicative TcS where
   pure x = TcS (\_ -> return x)
   (<*>) = ap
 
 instance Monad TcS where
-  fail err  = TcS (\_ -> fail err)
+#if !MIN_VERSION_base(4,13,0)
+  fail = MonadFail.fail
+#endif
   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
 
-#if __GLASGOW_HASKELL__ > 710
 instance MonadFail.MonadFail TcS where
   fail err  = TcS (\_ -> fail err)
-#endif
 
 instance MonadUnique TcS where
    getUniqueSupplyM = wrapTcS getUniqueSupplyM
 
+instance HasModule TcS where
+   getModule = wrapTcS getModule
+
+instance MonadThings TcS where
+   lookupThing n = wrapTcS (lookupThing n)
+
 -- Basic functionality
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 wrapTcS :: TcM a -> TcS a
@@ -2386,7 +2717,7 @@ traceTcS :: String -> SDoc -> TcS ()
 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
 
 runTcPluginTcS :: TcPluginM a -> TcS a
-runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBinds
+runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBindsVar
 
 instance HasDynFlags TcS where
     getDynFlags = wrapTcS getDynFlags
@@ -2399,43 +2730,36 @@ bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
                                     ; n <- TcM.readTcRef ref
                                     ; TcM.writeTcRef ref (n+1) }
 
--- | Mark variables as used filling a coercion hole
-useVars :: TyCoVarSet -> TcS ()
-useVars vars = TcS $ \env -> useVarsTcM (tcs_used_tcvs env) vars
-
--- | Like 'useVars' but in the TcM monad
-useVarsTcM :: IORef TyCoVarSet -> TyCoVarSet -> TcM ()
-useVarsTcM ref vars = TcM.updTcRef ref (`unionVarSet` vars)
-
 csTraceTcS :: SDoc -> TcS ()
 csTraceTcS doc
-  = wrapTcS $ csTraceTcM (return doc)
+  = wrapTcS $ csTraceTcM (return doc)
 
 traceFireTcS :: CtEvidence -> SDoc -> TcS ()
 -- Dump a rule-firing trace
 traceFireTcS ev doc
-  = TcS $ \env -> csTraceTcM $
+  = TcS $ \env -> csTraceTcM $
     do { n <- TcM.readTcRef (tcs_count env)
        ; tclvl <- TcM.getTcLevel
-       ; return (hang (int n <> brackets (text "U:" <> ppr tclvl
-                                          <> ppr (ctLocDepth (ctEvLoc ev)))
+       ; return (hang (text "Step" <+> int n
+                       <> brackets (text "l:" <> ppr tclvl <> comma <>
+                                    text "d:" <> ppr (ctLocDepth (ctEvLoc ev)))
                        <+> doc <> colon)
                      4 (ppr ev)) }
 
-csTraceTcM :: Int -> TcM SDoc -> TcM ()
+csTraceTcM :: TcM SDoc -> TcM ()
 -- Constraint-solver tracing, -ddump-cs-trace
-csTraceTcM trace_level mk_doc
+csTraceTcM mk_doc
   = do { dflags <- getDynFlags
-       ; when (  (dopt Opt_D_dump_cs_trace dflags || dopt Opt_D_dump_tc_trace dflags)
-              && trace_level <= traceLevel dflags ) $
-         do { msg <- mk_doc
-            ; TcM.traceTcRn Opt_D_dump_cs_trace msg } }
+       ; when (  dopt Opt_D_dump_cs_trace dflags
+                  || dopt Opt_D_dump_tc_trace dflags )
+              ( do { msg <- mk_doc
+                   ; TcM.traceTcRn Opt_D_dump_cs_trace msg }) }
 
 runTcS :: TcS a                -- What to run
        -> TcM (a, EvBindMap)
 runTcS tcs
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; res <- runTcSWithEvBinds False (Just ev_binds_var) tcs
+       ; res <- runTcSWithEvBinds ev_binds_var tcs
        ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
        ; return (res, ev_binds) }
 
@@ -2445,50 +2769,48 @@ runTcS tcs
 runTcSDeriveds :: TcS a -> TcM a
 runTcSDeriveds tcs
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; runTcSWithEvBinds True (Just ev_binds_var) tcs }
+       ; runTcSWithEvBinds ev_binds_var tcs }
 
 -- | This can deal only with equality constraints.
 runTcSEqualities :: TcS a -> TcM a
-runTcSEqualities = runTcSWithEvBinds False Nothing
+runTcSEqualities thing_inside
+  = do { ev_binds_var <- TcM.newNoTcEvBinds
+       ; runTcSWithEvBinds ev_binds_var thing_inside }
 
-runTcSWithEvBinds :: Bool  -- ^ keep running even if only Deriveds are left?
-                  -> Maybe EvBindsVar
+runTcSWithEvBinds :: EvBindsVar
                   -> TcS a
                   -> TcM a
-runTcSWithEvBinds solve_deriveds ev_binds_var tcs
+runTcSWithEvBinds ev_binds_var tcs
   = do { unified_var <- TcM.newTcRef 0
        ; step_count <- TcM.newTcRef 0
        ; inert_var <- TcM.newTcRef emptyInert
        ; wl_var <- TcM.newTcRef emptyWorkList
-       ; used_var <- TcM.newTcRef emptyVarSet -- never read from, but see
-                                              -- nestImplicTcS
-
        ; let env = TcSEnv { tcs_ev_binds      = ev_binds_var
                           , tcs_unified       = unified_var
                           , tcs_count         = step_count
                           , tcs_inerts        = inert_var
-                          , tcs_worklist      = wl_var
-                          , tcs_used_tcvs     = used_var
-                          , tcs_need_deriveds = solve_deriveds }
+                          , tcs_worklist      = wl_var }
 
              -- Run the computation
        ; res <- unTcS tcs env
 
        ; count <- TcM.readTcRef step_count
        ; when (count > 0) $
-         csTraceTcM 0 $ return (text "Constraint solver steps =" <+> int count)
+         csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
+
+       ; unflattenGivens inert_var
 
-#ifdef DEBUG
-       ; whenIsJust ev_binds_var $ \ebv ->
-         do { ev_binds <- TcM.getTcEvBinds ebv
-            ; checkForCyclicBinds ev_binds }
+#if defined(DEBUG)
+       ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
+       ; checkForCyclicBinds ev_binds
 #endif
 
        ; return res }
 
-#ifdef DEBUG
-checkForCyclicBinds :: Bag EvBind -> TcM ()
-checkForCyclicBinds ev_binds
+----------------------------
+#if defined(DEBUG)
+checkForCyclicBinds :: EvBindMap -> TcM ()
+checkForCyclicBinds ev_binds_map
   | null cycles
   = return ()
   | null coercion_cycles
@@ -2496,14 +2818,16 @@ checkForCyclicBinds ev_binds
   | otherwise
   = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
   where
+    ev_binds = evBindMapBinds ev_binds_map
+
     cycles :: [[EvBind]]
     cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
 
     coercion_cycles = [c | c <- cycles, any is_co_bind c]
-    is_co_bind (EvBind { eb_lhs = b }) = isEqPred (varType b)
+    is_co_bind (EvBind { eb_lhs = b }) = isEqPrimPred (varType b)
 
-    edges :: [(EvBind, EvVar, [EvVar])]
-    edges = [ (bind, bndr, nonDetEltsUFM (evVarsOfTerm rhs))
+    edges :: [ Node EvVar EvBind ]
+    edges = [ DigraphNode bind bndr (nonDetEltsUniqSet (evVarsOfTerm rhs))
             | bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs}) <- bagToList ev_binds ]
             -- It's OK to use nonDetEltsUFM here as
             -- stronglyConnCompFromEdgedVertices is still deterministic even
@@ -2511,56 +2835,42 @@ checkForCyclicBinds ev_binds
             -- Note [Deterministic SCC] in Digraph.
 #endif
 
-setEvBindsTcS :: Maybe EvBindsVar -> TcS a -> TcS a
-setEvBindsTcS m_ref (TcS thing_inside)
- = TcS $ \ env -> thing_inside (env { tcs_ev_binds = m_ref })
+----------------------------
+setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
+setEvBindsTcS ref (TcS thing_inside)
+ = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
 
-nestImplicTcS :: Maybe EvBindsVar -> TyCoVarSet -- bound in this implication
+nestImplicTcS :: EvBindsVar
               -> TcLevel -> TcS a
-              -> TcS (a, TyCoVarSet)  -- also returns any vars used when filling
-                                      -- coercion holes (for redundant-constraint
-                                      -- tracking)
-nestImplicTcS m_ref bound_tcvs inner_tclvl (TcS thing_inside)
+              -> TcS a
+nestImplicTcS ref inner_tclvl (TcS thing_inside)
   = TcS $ \ TcSEnv { tcs_unified       = unified_var
                    , tcs_inerts        = old_inert_var
                    , tcs_count         = count
-                   , tcs_used_tcvs     = used_var
-                   , tcs_need_deriveds = solve_deriveds
                    } ->
     do { inerts <- TcM.readTcRef old_inert_var
-       ; let nest_inert = inerts { inert_flat_cache = emptyExactFunEqs }
-                                     -- See Note [Do not inherit the flat cache]
+       ; let nest_inert = emptyInert
+                            { inert_cans = inert_cans inerts
+                            , inert_solved_dicts = inert_solved_dicts inerts }
+                              -- See Note [Do not inherit the flat cache]
        ; new_inert_var <- TcM.newTcRef nest_inert
        ; new_wl_var    <- TcM.newTcRef emptyWorkList
-       ; new_used_var  <- TcM.newTcRef emptyVarSet
-       ; let nest_env = TcSEnv { tcs_ev_binds      = m_ref
+       ; let nest_env = TcSEnv { tcs_ev_binds      = ref
                                , tcs_unified       = unified_var
                                , tcs_count         = count
                                , tcs_inerts        = new_inert_var
-                               , tcs_worklist      = new_wl_var
-                               , tcs_used_tcvs     = new_used_var
-                               , tcs_need_deriveds = solve_deriveds }
+                               , tcs_worklist      = new_wl_var }
        ; res <- TcM.setTcLevel inner_tclvl $
                 thing_inside nest_env
 
-#ifdef DEBUG
+       ; unflattenGivens new_inert_var
+
+#if defined(DEBUG)
        -- Perform a check that the thing_inside did not cause cycles
-       ; whenIsJust m_ref $ \ ref ->
-         do { ev_binds <- TcM.getTcEvBinds ref
-            ; checkForCyclicBinds ev_binds }
+       ; ev_binds <- TcM.getTcEvBindsMap ref
+       ; checkForCyclicBinds ev_binds
 #endif
-       ; used_tcvs <- TcM.readTcRef new_used_var
-
-       ; local_ev_vars <- case m_ref of
-           Nothing  -> return emptyVarSet
-           Just ref -> do { binds <- TcM.getTcEvBinds ref
-                          ; return $ mkVarSet $ map evBindVar $ bagToList binds }
-       ; let all_locals = bound_tcvs `unionVarSet` local_ev_vars
-             (inner_used_tcvs, outer_used_tcvs)
-               = partitionVarSet (`elemVarSet` all_locals) used_tcvs
-       ; useVarsTcM used_var outer_used_tcvs
-
-       ; return (res, inner_used_tcvs) }
+       ; return res }
 
 {- Note [Do not inherit the flat cache]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2602,6 +2912,82 @@ nestTcS (TcS thing_inside)
 
        ; return res }
 
+checkTvConstraintsTcS :: SkolemInfo
+                      -> [TcTyVar]        -- Skolems
+                      -> TcS (result, Cts)
+                      -> TcS result
+-- Just like TcUnify.checkTvConstraints, but
+--   - In the TcS monnad
+--   - The thing-inside should not put things in the work-list
+--     Instead, it returns the Wanted constraints it needs
+--   - No 'givens', and no TcEvBinds; this is type-level constraints only
+checkTvConstraintsTcS skol_info skol_tvs (TcS thing_inside)
+  = TcS $ \ tcs_env ->
+    do { let wl_panic  = pprPanic "TcSMonad.buildImplication" $
+                         ppr skol_info $$ ppr skol_tvs
+                         -- This panic checks that the thing-inside
+                         -- does not emit any work-list constraints
+             new_tcs_env = tcs_env { tcs_worklist = wl_panic }
+
+       ; (new_tclvl, (res, wanteds)) <- TcM.pushTcLevelM $
+                                        thing_inside new_tcs_env
+
+       ; unless (null wanteds) $
+         do { ev_binds_var <- TcM.newNoTcEvBinds
+            ; imp <- TcM.newImplication
+            ; let wc = emptyWC { wc_simple = wanteds }
+                  imp' = imp { ic_tclvl  = new_tclvl
+                             , ic_skols  = skol_tvs
+                             , ic_wanted = wc
+                             , ic_binds  = ev_binds_var
+                             , ic_info   = skol_info }
+
+           -- Add the implication to the work-list
+           ; TcM.updTcRef (tcs_worklist tcs_env)
+                          (extendWorkListImplic (unitBag imp')) }
+
+      ; return res }
+
+checkConstraintsTcS :: SkolemInfo
+                    -> [TcTyVar]        -- Skolems
+                    -> [EvVar]          -- Givens
+                    -> TcS (result, Cts)
+                    -> TcS (result, TcEvBinds)
+-- Just like checkConstraintsTcS, but
+--   - In the TcS monnad
+--   - The thing-inside should not put things in the work-list
+--     Instead, it returns the Wanted constraints it needs
+--   - I did not bother to put in the fast-path for
+--     empty-skols/empty-givens, or for empty-wanteds, because
+--     this function is used only for "quantified constraints" in
+--     with both tests are pretty much guaranteed to fail
+checkConstraintsTcS skol_info skol_tvs given (TcS thing_inside)
+  = TcS $ \ tcs_env ->
+    do { let wl_panic  = pprPanic "TcSMonad.buildImplication" $
+                         ppr skol_info $$ ppr skol_tvs
+                         -- This panic checks that the thing-inside
+                         -- does not emit any work-list constraints
+             new_tcs_env = tcs_env { tcs_worklist = wl_panic }
+
+       ; (new_tclvl, (res, wanteds)) <- TcM.pushTcLevelM $
+                                        thing_inside new_tcs_env
+
+       ; ev_binds_var <- TcM.newTcEvBinds
+       ; imp <- TcM.newImplication
+       ; let wc = emptyWC { wc_simple = wanteds }
+             imp' = imp { ic_tclvl  = new_tclvl
+                        , ic_skols  = skol_tvs
+                        , ic_given  = given
+                        , ic_wanted = wc
+                        , ic_binds  = ev_binds_var
+                        , ic_info   = skol_info }
+
+           -- Add the implication to the work-list
+       ; TcM.updTcRef (tcs_worklist tcs_env)
+                      (extendWorkListImplic (unitBag imp'))
+
+       ; return (res, TcEvBinds ev_binds_var) }
+
 {-
 Note [Propagate the solved dictionaries]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2627,27 +3013,21 @@ getTcSWorkListRef :: TcS (IORef WorkList)
 getTcSWorkListRef = TcS (return . tcs_worklist)
 
 getTcSInerts :: TcS InertSet
-getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
+getTcSInerts = getTcSInertsRef >>= readTcRef
 
 setTcSInerts :: InertSet -> TcS ()
-setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) }
+setTcSInerts ics = do { r <- getTcSInertsRef; writeTcRef r ics }
 
 getWorkListImplics :: TcS (Bag Implication)
 getWorkListImplics
   = do { wl_var <- getTcSWorkListRef
-       ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
+       ; wl_curr <- readTcRef wl_var
        ; return (wl_implics wl_curr) }
 
 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
 updWorkListTcS f
   = do { wl_var <- getTcSWorkListRef
-       ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
-       ; let new_work = f wl_curr
-       ; wrapTcS (TcM.writeTcRef wl_var new_work) }
-
--- | Should we keep solving even only deriveds are left?
-keepSolvingDeriveds :: TcS Bool
-keepSolvingDeriveds = TcS (return . tcs_need_deriveds)
+       ; updTcRef wl_var f }
 
 emitWorkNC :: [CtEvidence] -> TcS ()
 emitWorkNC evs
@@ -2661,44 +3041,35 @@ emitWork cts
   = do { traceTcS "Emitting fresh work" (vcat (map ppr cts))
        ; updWorkListTcS (extendWorkListCts cts) }
 
-emitInsoluble :: Ct -> TcS ()
--- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
-emitInsoluble ct
-  = do { traceTcS "Emit insoluble" (ppr ct $$ pprCtLoc (ctLoc ct))
-       ; updInertTcS add_insol }
-  where
-    this_pred = ctPred ct
-    add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
-      | already_there = is
-      | otherwise     = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } }
-      where
-        already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
-             -- See Note [Do not add duplicate derived insolubles]
-
 newTcRef :: a -> TcS (TcRef a)
 newTcRef x = wrapTcS (TcM.newTcRef x)
 
 readTcRef :: TcRef a -> TcS a
 readTcRef ref = wrapTcS (TcM.readTcRef ref)
 
+writeTcRef :: TcRef a -> a -> TcS ()
+writeTcRef ref val = wrapTcS (TcM.writeTcRef ref val)
+
 updTcRef :: TcRef a -> (a->a) -> TcS ()
 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
 
-getTcEvBinds :: TcS (Maybe EvBindsVar)
-getTcEvBinds = TcS (return . tcs_ev_binds)
-
-getTcEvBindsFromVar :: EvBindsVar -> TcS (Bag EvBind)
-getTcEvBindsFromVar = wrapTcS . TcM.getTcEvBinds
+getTcEvBindsVar :: TcS EvBindsVar
+getTcEvBindsVar = TcS (return . tcs_ev_binds)
 
 getTcLevel :: TcS TcLevel
 getTcLevel = wrapTcS TcM.getTcLevel
 
-getTcEvBindsMap :: TcS EvBindMap
-getTcEvBindsMap
-  = do { ev_binds <- getTcEvBinds
-       ; case ev_binds of
-           Just (EvBindsVar ev_ref _) -> wrapTcS $ TcM.readTcRef ev_ref
-           Nothing                    -> return emptyEvBindMap }
+getTcEvTyCoVars :: EvBindsVar -> TcS TyCoVarSet
+getTcEvTyCoVars ev_binds_var
+  = wrapTcS $ TcM.getTcEvTyCoVars ev_binds_var
+
+getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
+getTcEvBindsMap ev_binds_var
+  = wrapTcS $ TcM.getTcEvBindsMap ev_binds_var
+
+setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS ()
+setTcEvBindsMap ev_binds_var binds
+  = wrapTcS $ TcM.setTcEvBindsMap ev_binds_var binds
 
 unifyTyVar :: TcTyVar -> TcType -> TcS ()
 -- Unify a meta-tyvar with a type
@@ -2712,15 +3083,6 @@ unifyTyVar tv ty
        ; TcM.writeMetaTyVar tv ty
        ; TcM.updTcRef (tcs_unified env) (+1) }
 
-unflattenFmv :: TcTyVar -> TcType -> TcS ()
--- Fill a flatten-meta-var, simply by unifying it.
--- This does NOT count as a unification in tcs_unified.
-unflattenFmv tv ty
-  = ASSERT2( isMetaTyVar tv, ppr tv )
-    TcS $ \ _ ->
-    do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty)
-       ; TcM.writeMetaTyVar tv ty }
-
 reportUnifications :: TcS a -> TcS (Int, a)
 reportUnifications (TcS thing_inside)
   = TcS $ \ env ->
@@ -2754,41 +3116,48 @@ getLclEnv = wrapTcS $ TcM.getLclEnv
 tcLookupClass :: Name -> TcS Class
 tcLookupClass c = wrapTcS $ TcM.tcLookupClass c
 
+tcLookupId :: Name -> TcS Id
+tcLookupId n = wrapTcS $ TcM.tcLookupId n
+
 -- Setting names as used (used in the deriving of Coercible evidence)
 -- Too hackish to expose it to TcS? In that case somehow extract the used
 -- constructors from the result of solveInteract
 addUsedGREs :: [GlobalRdrElt] -> TcS ()
 addUsedGREs gres = wrapTcS  $ TcM.addUsedGREs gres
 
+addUsedGRE :: Bool -> GlobalRdrElt -> TcS ()
+addUsedGRE warn_if_deprec gre = wrapTcS $ TcM.addUsedGRE warn_if_deprec gre
+
+keepAlive :: Name -> TcS ()
+keepAlive = wrapTcS . TcM.keepAlive
+
 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
-checkWellStagedDFun pred dfun_id loc
+checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS ()
+-- Check that we do not try to use an instance before it is available.  E.g.
+--    instance Eq T where ...
+--    f x = $( ... (\(p::T) -> p == p)... )
+-- Here we can't use the equality function from the instance in the splice
+
+checkWellStagedDFun loc what pred
+  | TopLevInstance { iw_dfun_id = dfun_id } <- what
+  , let bind_lvl = TcM.topIdLvl dfun_id
+  , bind_lvl > impLevel
   = wrapTcS $ TcM.setCtLocM loc $
     do { use_stage <- TcM.getStage
        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
+
+  | otherwise
+  = return ()    -- Fast path for common case
   where
     pp_thing = text "instance for" <+> quotes (ppr pred)
-    bind_lvl = TcM.topIdLvl dfun_id
 
 pprEq :: TcType -> TcType -> SDoc
 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
 
-isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
-isTouchableMetaTyVarTcS tv
-  = do { tclvl <- getTcLevel
-       ; return $ isTouchableMetaTyVar tclvl tv }
-
 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
-isFilledMetaTyVar_maybe tv
- = case tcTyVarDetails tv of
-     MetaTv { mtv_ref = ref }
-        -> do { cts <- wrapTcS (TcM.readTcRef ref)
-              ; case cts of
-                  Indirect ty -> return (Just ty)
-                  Flexi       -> return Nothing }
-     _ -> return Nothing
+isFilledMetaTyVar_maybe tv = wrapTcS (TcM.isFilledMetaTyVar_maybe tv)
 
 isFilledMetaTyVar :: TcTyVar -> TcS Bool
 isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
@@ -2817,89 +3186,151 @@ zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
 zonkWC :: WantedConstraints -> TcS WantedConstraints
 zonkWC wc = wrapTcS (TcM.zonkWC wc)
 
-{-
-Note [Do not add duplicate derived insolubles]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In general we *must* add an insoluble (Int ~ Bool) even if there is
-one such there already, because they may come from distinct call
-sites.  Not only do we want an error message for each, but with
--fdefer-type-errors we must generate evidence for each.  But for
-*derived* insolubles, we only want to report each one once.  Why?
-
-(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
-    equality many times, as the original constraint is successively rewritten.
-
-(b) Ditto the successive iterations of the main solver itself, as it traverses
-    the constraint tree. See example below.
-
-Also for *given* insolubles we may get repeated errors, as we
-repeatedly traverse the constraint tree.  These are relatively rare
-anyway, so removing duplicates seems ok.  (Alternatively we could take
-the SrcLoc into account.)
-
-Note that the test does not need to be particularly efficient because
-it is only used if the program has a type error anyway.
+zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar
+zonkTyCoVarKind tv = wrapTcS (TcM.zonkTyCoVarKind tv)
 
-Example of (b): assume a top-level class and instance declaration:
-
-  class D a b | a -> b
-  instance D [a] [a]
+{- *********************************************************************
+*                                                                      *
+*                Flatten skolems                                       *
+*                                                                      *
+********************************************************************* -}
 
-Assume we have started with an implication:
+newFlattenSkolem :: CtFlavour -> CtLoc
+                 -> TyCon -> [TcType]                    -- F xis
+                 -> TcS (CtEvidence, Coercion, TcTyVar)  -- [G/WD] x:: F xis ~ fsk
+newFlattenSkolem flav loc tc xis
+  = do { stuff@(ev, co, fsk) <- new_skolem
+       ; let fsk_ty = mkTyVarTy fsk
+       ; extendFlatCache tc xis (co, fsk_ty, ctEvFlavour ev)
+       ; return stuff }
+  where
+    fam_ty = mkTyConApp tc xis
+
+    new_skolem
+      | Given <- flav
+      = do { fsk <- wrapTcS (TcM.newFskTyVar fam_ty)
+
+           -- Extend the inert_fsks list, for use by unflattenGivens
+           ; updInertTcS $ \is -> is { inert_fsks = (fsk, fam_ty) : inert_fsks is }
+
+           -- Construct the Refl evidence
+           ; let pred = mkPrimEqPred fam_ty (mkTyVarTy fsk)
+                 co   = mkNomReflCo fam_ty
+           ; ev  <- newGivenEvVar loc (pred, evCoercion co)
+           ; return (ev, co, fsk) }
+
+      | otherwise  -- Generate a [WD] for both Wanted and Derived
+                   -- See Note [No Derived CFunEqCans]
+      = do { fmv <- wrapTcS (TcM.newFmvTyVar fam_ty)
+           ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv)
+           ; return (ev, hole_co, fmv) }
+
+----------------------------
+unflattenGivens :: IORef InertSet -> TcM ()
+-- Unflatten all the fsks created by flattening types in Given
+-- constraints. We must be sure to do this, else we end up with
+-- flatten-skolems buried in any residual Wanteds
+--
+-- NB: this is the /only/ way that a fsk (MetaDetails = FlatSkolTv)
+--     is filled in. Nothing else does so.
+--
+-- It's here (rather than in TcFlatten) because the Right Places
+-- to call it are in runTcSWithEvBinds/nestImplicTcS, where it
+-- is nicely paired with the creation an empty inert_fsks list.
+unflattenGivens inert_var
+ = do { inerts <- TcM.readTcRef inert_var
+       ; TcM.traceTc "unflattenGivens" (ppr (inert_fsks inerts))
+       ; mapM_ flatten_one (inert_fsks inerts) }
+  where
+    flatten_one (fsk, ty) = TcM.writeMetaTyVar fsk ty
 
-  forall c. Eq c => { wc_simple = D [c] c [W] }
+----------------------------
+extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
+extendFlatCache tc xi_args stuff@(_, ty, fl)
+  | isGivenOrWDeriv fl  -- Maintain the invariant that inert_flat_cache
+                        -- only has [G] and [WD] CFunEqCans
+  = do { dflags <- getDynFlags
+       ; when (gopt Opt_FlatCache dflags) $
+    do { traceTcS "extendFlatCache" (vcat [ ppr tc <+> ppr xi_args
+                                          , ppr fl, ppr ty ])
+            -- 'co' can be bottom, in the case of derived items
+       ; updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
+            is { inert_flat_cache = insertExactFunEq fc tc xi_args stuff } } }
 
-which we have simplified to:
+  | otherwise
+  = return ()
 
-  forall c. Eq c => { wc_simple = D [c] c [W]
-                    , wc_insols = (c ~ [c]) [D] }
+----------------------------
+unflattenFmv :: TcTyVar -> TcType -> TcS ()
+-- Fill a flatten-meta-var, simply by unifying it.
+-- This does NOT count as a unification in tcs_unified.
+unflattenFmv tv ty
+  = ASSERT2( isMetaTyVar tv, ppr tv )
+    TcS $ \ _ ->
+    do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty)
+       ; TcM.writeMetaTyVar tv ty }
 
-For some reason, e.g. because we floated an equality somewhere else,
-we might try to re-solve this implication. If we do not do a
-dropDerivedWC, then we will end up trying to solve the following
-constraints the second time:
+----------------------------
+demoteUnfilledFmv :: TcTyVar -> TcS ()
+-- If a flatten-meta-var is still un-filled,
+-- turn it into an ordinary meta-var
+demoteUnfilledFmv fmv
+  = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
+                 ; unless is_filled $
+                   do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
+                      ; TcM.writeMetaTyVar fmv tv_ty } }
 
-  (D [c] c) [W]
-  (c ~ [c]) [D]
+-----------------------------
+dischargeFunEq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
+-- (dischargeFunEq tv co ty)
+--     Preconditions
+--       - ev :: F tys ~ tv   is a CFunEqCan
+--       - tv is a FlatMetaTv of FlatSkolTv
+--       - co :: F tys ~ xi
+--       - fmv/fsk `notElem` xi
+--       - fmv not filled (for Wanteds)
+--
+-- Then for [W] or [WD], we actually fill in the fmv:
+--      set fmv := xi,
+--      set ev  := co
+--      kick out any inert things that are now rewritable
+--
+-- For [D], we instead emit an equality that must ultimately hold
+--      [D] xi ~ fmv
+--      Does not evaluate 'co' if 'ev' is Derived
+--
+-- For [G], emit this equality
+--     [G] (sym ev; co) :: fsk ~ xi
+
+-- See TcFlatten Note [The flattening story],
+-- especially "Ownership of fsk/fmv"
+dischargeFunEq (CtGiven { ctev_evar = old_evar, ctev_loc = loc }) fsk co xi
+  = do { new_ev <- newGivenEvVar loc ( new_pred, evCoercion new_co  )
+       ; emitWorkNC [new_ev] }
+  where
+    new_pred = mkPrimEqPred (mkTyVarTy fsk) xi
+    new_co   = mkTcSymCo (mkTcCoVarCo old_evar) `mkTcTransCo` co
 
-which will result in two Deriveds to end up in the insoluble set:
+dischargeFunEq 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 $$ pprKicked n_kicked) }
 
-  wc_simple   = D [c] c [W]
-  wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
--}
+dischargeFunEq (CtDerived { ctev_loc = loc }) fmv _co xi
+  = emitNewDerivedEq loc Nominal xi (mkTyVarTy fmv)
+              -- FunEqs are always at Nominal role
 
--- Flatten skolems
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-newFlattenSkolem :: CtFlavour -> CtLoc
-                 -> TcType         -- F xis
-                 -> TcS (CtEvidence, Coercion, TcTyVar)    -- [W] x:: F xis ~ fsk
-newFlattenSkolem Given loc fam_ty
-  = do { fsk <- newFsk fam_ty
-       ; let co = mkNomReflCo fam_ty
-       ; ev  <- newGivenEvVar loc (mkPrimEqPred fam_ty (mkTyVarTy fsk),
-                                   EvCoercion co)
-       ; return (ev, co, fsk) }
-
-newFlattenSkolem Wanted loc fam_ty
-  = do { fmv <- newFmv fam_ty
-       ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv)
-       ; return (ev, hole_co, fmv) }
-
-newFlattenSkolem Derived loc fam_ty
-  = do { fmv <- newFmv fam_ty
-       ; ev <- newDerivedNC loc (mkPrimEqPred fam_ty (mkTyVarTy fmv))
-       ; return (ev, pprPanic "newFlattenSkolem [D]" (ppr fam_ty), fmv) }
-
-newFsk, newFmv :: TcType -> TcS TcTyVar
-newFsk fam_ty = wrapTcS (TcM.newFskTyVar fam_ty)
-newFmv fam_ty = wrapTcS (TcM.newFmvTyVar fam_ty)
+pprKicked :: Int -> SDoc
+pprKicked 0 = empty
+pprKicked n = parens (int n <+> text "kicked out")
 
-extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
-extendFlatCache tc xi_args stuff
-  = do { dflags <- getDynFlags
-       ; when (gopt Opt_FlatCache dflags) $
-         updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
-            is { inert_flat_cache = insertExactFunEq fc tc xi_args stuff } }
+{- *********************************************************************
+*                                                                      *
+*                Instantiation etc.
+*                                                                      *
+********************************************************************* -}
 
 -- Instantiations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2914,36 +3345,37 @@ newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
 
-demoteUnfilledFmv :: TcTyVar -> TcS ()
--- If a flatten-meta-var is still un-filled,
--- turn it into an ordinary meta-var
-demoteUnfilledFmv fmv
-  = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
-                 ; unless is_filled $
-                   do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
-                      ; TcM.writeMetaTyVar fmv tv_ty } }
+instFlexi :: [TKVar] -> TcS TCvSubst
+instFlexi = instFlexiX emptyTCvSubst
 
-instFlexiTcS :: [TKVar] -> TcS (TCvSubst, [TcType])
-instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTCvSubst tvs)
-  where
-     inst_one subst tv
-         = do { ty' <- instFlexiTcSHelper (tyVarName tv)
-                                          (substTyUnchecked subst (tyVarKind tv))
-              ; return (extendTvSubst subst tv ty', ty') }
+instFlexiX :: TCvSubst -> [TKVar] -> TcS TCvSubst
+instFlexiX subst tvs
+  = wrapTcS (foldlM instFlexiHelper subst tvs)
 
-instFlexiTcSHelper :: Name -> Kind -> TcM TcType
-instFlexiTcSHelper tvname kind
+instFlexiHelper :: TCvSubst -> TKVar -> TcM TCvSubst
+instFlexiHelper subst tv
   = do { uniq <- TcM.newUnique
        ; details <- TcM.newMetaDetails TauTv
-       ; let name = setNameUnique tvname uniq
-       ; return (mkTyVarTy (mkTcTyVar name kind details)) }
-
-
+       ; let name = setNameUnique (tyVarName tv) uniq
+             kind = substTyUnchecked subst (tyVarKind tv)
+             ty'  = mkTyVarTy (mkTcTyVar name kind details)
+       ; TcM.traceTc "instFlexi" (ppr ty')
+       ; return (extendTvSubst subst tv ty') }
+
+matchGlobalInst :: DynFlags
+                -> Bool      -- True <=> caller is the short-cut solver
+                             -- See Note [Shortcut solving: overlap]
+                -> Class -> [Type] -> TcS TcM.ClsInstResult
+matchGlobalInst dflags short_cut cls tys
+  = wrapTcS (TcM.matchGlobalInst dflags short_cut cls tys)
+
+tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
+tcInstSkolTyVarsX subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX subst tvs
 
 -- Creating and setting evidence variables and CtFlavors
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-data MaybeNew = Fresh CtEvidence | Cached EvTerm
+data MaybeNew = Fresh CtEvidence | Cached EvExpr
 
 isFresh :: MaybeNew -> Bool
 isFresh (Fresh {})  = True
@@ -2952,50 +3384,58 @@ isFresh (Cached {}) = False
 freshGoals :: [MaybeNew] -> [CtEvidence]
 freshGoals mns = [ ctev | Fresh ctev <- mns ]
 
-getEvTerm :: MaybeNew -> EvTerm
-getEvTerm (Fresh ctev) = ctEvTerm ctev
-getEvTerm (Cached evt) = evt
+getEvExpr :: MaybeNew -> EvExpr
+getEvExpr (Fresh ctev) = ctEvExpr ctev
+getEvExpr (Cached evt) = evt
 
 setEvBind :: EvBind -> TcS ()
 setEvBind ev_bind
-  = do { tc_evbinds <- getTcEvBinds
-       ; case tc_evbinds of
-           Just evb -> wrapTcS $ TcM.addTcEvBind evb ev_bind
-           Nothing  -> pprPanic "setEvBind" (ppr ev_bind) }
+  = do { evb <- getTcEvBindsVar
+       ; wrapTcS $ TcM.addTcEvBind evb ev_bind }
+
+-- | Mark variables as used filling a coercion hole
+useVars :: CoVarSet -> TcS ()
+useVars co_vars
+  = do { ev_binds_var <- getTcEvBindsVar
+       ; let ref = ebv_tcvs ev_binds_var
+       ; wrapTcS $
+         do { tcvs <- TcM.readTcRef ref
+            ; let tcvs' = tcvs `unionVarSet` co_vars
+            ; TcM.writeTcRef ref tcvs' } }
 
 -- | Equalities only
 setWantedEq :: TcEvDest -> Coercion -> TcS ()
 setWantedEq (HoleDest hole) co
-  = do { useVars (tyCoVarsOfCo co)
+  = do { useVars (coVarsOfCo co)
        ; wrapTcS $ TcM.fillCoercionHole hole co }
 setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq" (ppr ev)
 
--- | Equalities only
-setEqIfWanted :: CtEvidence -> Coercion -> TcS ()
-setEqIfWanted (CtWanted { ctev_dest = dest }) co = setWantedEq dest co
-setEqIfWanted _ _ = return ()
-
--- | Good for equalities and non-equalities
+-- | Good for both equalities and non-equalities
 setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
 setWantedEvTerm (HoleDest hole) tm
-  = do { let co = evTermCoercion tm
-       ; useVars (tyCoVarsOfCo co)
+  | Just co <- evTermCoercion_maybe tm
+  = do { useVars (coVarsOfCo co)
        ; wrapTcS $ TcM.fillCoercionHole hole co }
-setWantedEvTerm (EvVarDest ev) tm = setWantedEvBind ev tm
+  | otherwise
+  = do { let co_var = coHoleCoVar hole
+       ; setEvBind (mkWantedEvBind co_var tm)
+       ; wrapTcS $ TcM.fillCoercionHole hole (mkTcCoVarCo co_var) }
 
-setWantedEvBind :: EvVar -> EvTerm -> TcS ()
-setWantedEvBind ev_id tm = setEvBind (mkWantedEvBind ev_id tm)
+setWantedEvTerm (EvVarDest ev_id) tm
+  = setEvBind (mkWantedEvBind ev_id tm)
 
 setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
 setEvBindIfWanted ev tm
   = case ev of
-      CtWanted { ctev_dest = dest }
-        -> setWantedEvTerm dest tm
-      _ -> return ()
+      CtWanted { ctev_dest = dest } -> setWantedEvTerm dest tm
+      _                             -> return ()
 
 newTcEvBinds :: TcS EvBindsVar
 newTcEvBinds = wrapTcS TcM.newTcEvBinds
 
+newNoTcEvBinds :: TcS EvBindsVar
+newNoTcEvBinds = wrapTcS TcM.newNoTcEvBinds
+
 newEvVar :: TcPredType -> TcS EvVar
 newEvVar pred = wrapTcS (TcM.newEvVar pred)
 
@@ -3003,7 +3443,7 @@ newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
 -- Make a new variable of the given PredType,
 -- immediately bind it to the given term
 -- and return its CtEvidence
--- See Note [Bind new Givens immediately] in TcRnTypes
+-- See Note [Bind new Givens immediately] in Constraint
 newGivenEvVar loc (pred, rhs)
   = do { new_ev <- newBoundEvVarId pred rhs
        ; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) }
@@ -3019,54 +3459,79 @@ newBoundEvVarId pred rhs
 newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
 newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
 
+emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion
+-- | Emit a new Wanted equality into the work-list
+emitNewWantedEq loc role ty1 ty2
+  = do { (ev, co) <- newWantedEq loc role ty1 ty2
+       ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev))
+       ; return co }
+
 -- | Make a new equality CtEvidence
-newWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion)
-newWantedEq loc role ty1 ty2
-  = do { hole <- wrapTcS $ TcM.newCoercionHole
+newWantedEq :: CtLoc -> Role -> TcType -> TcType
+            -> TcS (CtEvidence, Coercion)
+newWantedEq = newWantedEq_SI WDeriv
+
+newWantedEq_SI :: ShadowInfo -> CtLoc -> Role
+               -> TcType -> TcType
+               -> TcS (CtEvidence, Coercion)
+newWantedEq_SI si loc role ty1 ty2
+  = do { hole <- wrapTcS $ TcM.newCoercionHole pty
        ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
        ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
+                           , ctev_nosh = si
                            , ctev_loc = loc}
-                , mkHoleCo hole role ty1 ty2 ) }
+                , mkHoleCo hole ) }
   where
     pty = mkPrimEqPredRole role ty1 ty2
 
--- no equalities here. Use newWantedEqNC instead
+-- no equalities here. Use newWantedEq instead
 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
+newWantedEvVarNC = newWantedEvVarNC_SI WDeriv
+
+newWantedEvVarNC_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS CtEvidence
 -- Don't look up in the solved/inerts; we know it's not there
-newWantedEvVarNC loc pty
-  = do { -- checkReductionDepth loc pty
-       ; new_ev <- newEvVar pty
+newWantedEvVarNC_SI si loc pty
+  = do { new_ev <- newEvVar pty
        ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$
                                          pprCtLoc loc)
        ; return (CtWanted { ctev_pred = pty, ctev_dest = EvVarDest new_ev
+                          , ctev_nosh = si
                           , ctev_loc = loc })}
 
 newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
+newWantedEvVar = newWantedEvVar_SI WDeriv
+
+newWantedEvVar_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew
 -- For anything except ClassPred, this is the same as newWantedEvVarNC
-newWantedEvVar loc pty
-  = do { mb_ct <- lookupInInerts pty
+newWantedEvVar_SI si loc pty
+  = do { mb_ct <- lookupInInerts loc pty
        ; case mb_ct of
             Just ctev
               | not (isDerived ctev)
               -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
-                    ; return $ Cached (ctEvTerm ctev) }
-            _ -> do { ctev <- newWantedEvVarNC loc pty
+                    ; return $ Cached (ctEvExpr ctev) }
+            _ -> do { ctev <- newWantedEvVarNC_SI si loc pty
                     ; return (Fresh ctev) } }
 
--- deals with both equalities and non equalities. Tries to look
--- up non-equalities in the cache
 newWanted :: CtLoc -> PredType -> TcS MaybeNew
-newWanted loc pty
+-- Deals with both equalities and non equalities. Tries to look
+-- up non-equalities in the cache
+newWanted = newWanted_SI WDeriv
+
+newWanted_SI :: ShadowInfo -> CtLoc -> PredType -> TcS MaybeNew
+newWanted_SI si loc pty
   | Just (role, ty1, ty2) <- getEqPredTys_maybe pty
-  = Fresh . fst <$> newWantedEq loc role ty1 ty2
+  = Fresh . fst <$> newWantedEq_SI si loc role ty1 ty2
   | otherwise
-  = newWantedEvVar loc pty
+  = newWantedEvVar_SI si loc pty
 
-emitNewDerived :: CtLoc -> TcPredType -> TcS ()
-emitNewDerived loc pred
-  = do { ev <- newDerivedNC loc pred
-       ; traceTcS "Emitting new derived" (ppr ev)
-       ; updWorkListTcS (extendWorkListDerived loc ev) }
+-- deals with both equalities and non equalities. Doesn't do any cache lookups.
+newWantedNC :: CtLoc -> PredType -> TcS CtEvidence
+newWantedNC loc pty
+  | Just (role, ty1, ty2) <- getEqPredTys_maybe pty
+  = fst <$> newWantedEq loc role ty1 ty2
+  | otherwise
+  = newWantedEvVarNC loc pty
 
 emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
 emitNewDeriveds loc preds
@@ -3075,7 +3540,7 @@ emitNewDeriveds loc preds
   | otherwise
   = do { evs <- mapM (newDerivedNC loc) preds
        ; traceTcS "Emitting new deriveds" (ppr evs)
-       ; updWorkListTcS (extendWorkListDeriveds loc evs) }
+       ; updWorkListTcS (extendWorkListDeriveds evs) }
 
 emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS ()
 -- Create new equality Derived and put it in the work list
@@ -3083,7 +3548,9 @@ emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS ()
 emitNewDerivedEq loc role ty1 ty2
   = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2)
        ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc)
-       ; updWorkListTcS (extendWorkListDerived loc ev) }
+       ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) }
+         -- Very important: put in the wl_eqs
+         -- See Note [Prioritise equalities] (Avoiding fundep iteration)
 
 newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
 newDerivedNC loc pred
@@ -3107,7 +3574,8 @@ matchFam tycon args = wrapTcS $ matchFamTcM tycon args
 matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (Coercion, TcType))
 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
 matchFamTcM tycon args
-  = do { let match_fam_result
+  = do { fam_envs <- FamInst.tcGetFamInstEnvs
+       ; let match_fam_result
               = reduceTyFamApp_maybe fam_envs Nominal tycon args
        ; TcM.traceTc "matchFamTcM" $
          vcat [ text "Matching:" <+> ppr (mkTyConApp tycon args)
@@ -3130,43 +3598,3 @@ from which we get the implication
    (forall a. t1 ~ t2)
 See TcSMonad.deferTcSForAllEq
 -}
-
--- Deferring forall equalities as implications
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-deferTcSForAllEq :: Role -- Nominal or Representational
-                 -> CtLoc  -- Original wanted equality flavor
-                 -> [Coercion]        -- among the kinds of the binders
-                 -> ([TyVarBinder],TcType)   -- ForAll tvs1 body1
-                 -> ([TyVarBinder],TcType)   -- ForAll tvs2 body2
-                 -> TcS Coercion
-deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2)
- = do { let tvs1'  = zipWithEqual "deferTcSForAllEq"
-                       mkCastTy (mkTyVarTys tvs1) kind_cos
-            body2' = substTyWithUnchecked tvs2 tvs1' body2
-      ; (subst, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
-      ; let phi1  = Type.substTyUnchecked subst body1
-            phi2  = Type.substTyUnchecked subst body2'
-            skol_info = UnifyForAllSkol phi1
-
-      ; (ctev, hole_co) <- newWantedEq loc role phi1 phi2
-      ; env <- getLclEnv
-      ; let new_tclvl = pushTcLevel (tcl_tclvl env)
-            wc        = WC { wc_simple = singleCt (mkNonCanonical ctev)
-                           , wc_impl   = emptyBag
-                           , wc_insol  = emptyCts }
-            imp       = Implic { ic_tclvl  = new_tclvl
-                               , ic_skols  = skol_tvs
-                               , ic_no_eqs = True
-                               , ic_given  = []
-                               , ic_wanted = wc
-                               , ic_status = IC_Unsolved
-                               , ic_binds  = Nothing -- no place to put binds
-                               , ic_env    = env
-                               , ic_info   = skol_info }
-      ; updWorkListTcS (extendWorkListImplic imp)
-      ; let cobndrs    = zip skol_tvs kind_cos
-      ; return $ mkForAllCos cobndrs hole_co }
-   where
-     tvs1 = binderVars bndrs1
-     tvs2 = binderVars bndrs2