A collection of type-inference refactorings.
[ghc.git] / compiler / typecheck / TcSMonad.hs
index ffdfb27..0174b4a 100644 (file)
 -- Type definitions for the constraint solver
 module TcSMonad (
 
-       -- Canonical constraints, definition is now in TcRnTypes
-
+    -- The work list
     WorkList(..), isEmptyWorkList, emptyWorkList,
-    extendWorkListFunEq,
-    extendWorkListNonEq, extendWorkListCt,
-    extendWorkListCts, appendWorkList, selectWorkItem,
-    workListSize,
-
-    updWorkListTcS, updWorkListTcS_return,
-
-    updInertTcS, updInertCans, updInertDicts, updInertIrreds, updInertFunEqs,
-
-    Ct(..), Xi, tyVarsOfCt, tyVarsOfCts,
-    emitInsoluble, emitWorkNC,
-
-    isWanted, isDerived,
-    isGivenCt, isWantedCt, isDerivedCt,
-
-    mkGivenLoc,
-
-    TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality
+    extendWorkListNonEq, extendWorkListCt, extendWorkListDerived,
+    extendWorkListCts, extendWorkListEq, extendWorkListFunEq,
+    appendWorkList,
+    selectNextWorkItem,
+    workListSize, workListWantedCount,
+    getWorkList, updWorkListTcS,
+
+    -- The TcS monad
+    TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
+    failTcS, warnTcS, addErrTcS,
+    runTcSEqualities,
+    nestTcS, nestImplicTcS, setEvBindsTcS,
+
+    runTcPluginTcS, addUsedGREs, deferTcSForAllEq,
+
+    -- Tracing etc
+    panicTcS, traceTcS,
     traceFireTcS, bumpStepCountTcS, csTraceTcS,
-    tryTcS, nestTcS, nestImplicTcS, recoverTcS,
     wrapErrTcS, wrapWarnTcS,
-    runTcPluginTcS,
 
-    -- Getting and setting the flattening cache
-    addSolvedDict,
+    -- Evidence creation and transformation
+    MaybeNew(..), freshGoals, isFresh, getEvTerm,
 
-    -- Marking stuff as used
-    addUsedRdrNamesTcS,
+    newTcEvBinds,
+    newWantedEq,
+    newWanted, newWantedEvVar, newWantedEvVarNC, newDerivedNC,
+    newBoundEvVarId,
+    unifyTyVar, unflattenFmv, reportUnifications,
+    setEvBind, setWantedEq, setEqIfWanted,
+    setWantedEvTerm, setWantedEvBind, setEvBindIfWanted,
+    newEvVar, newGivenEvVar, newGivenEvVars,
+    emitNewDerived, emitNewDeriveds, emitNewDerivedEq,
+    checkReductionDepth,
 
-    deferTcSForAllEq,
-
-    setEvBind,
-    XEvTerm(..),
-    Freshness(..), freshGoals,
-
-    StopOrContinue(..), continueWith, stopWith, andWhenContinue,
+    getInstEnvs, getFamInstEnvs,                -- Getting the environments
+    getTopEnv, getGblEnv, getLclEnv,
+    getTcEvBindsVar, getTcLevel,
+    getTcEvBindsAndTCVs, getTcEvBindsMap,
+    tcLookupClass,
 
-    xCtEvidence,        -- Transform a CtEvidence during a step
-    rewriteEvidence,    -- Specialized version of xCtEvidence for coercions
-    rewriteEqEvidence,  -- Yet more specialised, for equality coercions
-    maybeSym,
+    -- Inerts
+    InertSet(..), InertCans(..),
+    updInertTcS, updInertCans, updInertDicts, updInertIrreds,
+    getNoGivenEqs, setInertCans,
+    getInertEqs, getInertCans, getInertModel, getInertGivens,
+    emptyInert, getTcSInerts, setTcSInerts, takeGivenInsolubles,
+    matchableGivens, prohibitedSuperClassSolve,
+    getUnsolvedInerts,
+    removeInertCts, getPendingScDicts,
+    addInertCan, addInertEq, insertFunEq,
+    emitInsoluble, emitWorkNC, emitWork,
 
-    newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
-    newEvVar, newGivenEvVar,
-    emitNewDerived, emitNewDerivedEq,
-    instDFunConstraints,
+    -- The Model
+    InertModel, kickOutAfterUnification,
 
-       -- Creation of evidence variables
-    setWantedTyBind, reportUnifications,
+    -- Inert Safe Haskell safe-overlap failures
+    addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
+    getSafeOverlapFailures,
 
-    getInstEnvs, getFamInstEnvs,                -- Getting the environments
-    getTopEnv, getGblEnv, getTcEvBinds, getTcLevel,
-    getTcEvBindsMap,
+    -- Inert CDictCans
+    lookupInertDict, findDictsByClass, addDict, addDictsByClass,
+    delDict, foldDicts, filterDicts,
 
-    lookupFlatCache, newFlattenSkolem,            -- Flatten skolems
+    -- Inert CTyEqCans
+    EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
 
-        -- Deque
-    Deque(..), insertDeque, emptyDeque,
+    -- Inert solved dictionaries
+    addSolvedDict, lookupSolvedDict,
 
-        -- Inerts
-    InertSet(..), InertCans(..),
-    getNoGivenEqs, setInertCans, getInertEqs, getInertCans,
-    emptyInert, getTcSInerts, setTcSInerts,
-    getUnsolvedInerts, checkAllSolved,
-    splitInertCans, removeInertCts,
-    prepareInertsForImplications,
-    addInertCan, insertInertItemTcS, insertFunEq,
-    EqualCtList,
-    lookupSolvedDict, extendFlatCache,
+    -- Irreds
+    foldIrreds,
 
-    lookupInertDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
+    -- The flattening cache
+    lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems
 
-    findFunEq, findTyEqs,
-    findFunEqsByTyCon, findFunEqs, partitionFunEqs,
-    sizeFunEqMap,
+    -- Inert CFunEqCans
+    updInertFunEqs, findFunEq, sizeFunEqMap,
+    findFunEqsByTyCon,
 
     instDFunType,                              -- Instantiation
-    newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
+
+    -- MetaTyVars
+    newFlexiTcSTy, instFlexiTcS,
     cloneMetaTyVar, demoteUnfilledFmv,
 
     TcLevel, isTouchableMetaTyVarTcS,
     isFilledMetaTyVar_maybe, isFilledMetaTyVar,
-    zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkFlats,
+    zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
+    zonkTyCoVarsAndFVList,
+    zonkSimples, zonkWC,
 
-    getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
+    -- References
+    newTcRef, readTcRef, updTcRef,
 
-    matchFam,
+    -- Misc
+    getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
+    matchFam, matchFamTcM,
     checkWellStagedDFun,
     pprEq                                    -- Smaller utils, re-exported from TcM
                                              -- TODO (DV): these are only really used in the
@@ -105,7 +114,7 @@ module TcSMonad (
 
 import HscTypes
 
-import Inst
+import qualified Inst as TcM
 import InstEnv
 import FamInst
 import FamInstEnv
@@ -113,43 +122,45 @@ import FamInstEnv
 import qualified TcRnMonad as TcM
 import qualified TcMType as TcM
 import qualified TcEnv as TcM
-       ( checkWellStaged, topIdLvl, tcGetDefaultTys )
+       ( checkWellStaged, topIdLvl, tcGetDefaultTys, tcLookupClass )
 import Kind
 import TcType
 import DynFlags
 import Type
-import CoAxiom(sfMatchFam)
+import Coercion
+import Unify
 
 import TcEvidence
 import Class
 import TyCon
+import TcErrors   ( solverDepthErrorTcS )
 
 import Name
-import RdrName (RdrName, GlobalRdrEnv)
-import RnEnv (addUsedRdrNames)
+import RdrName ( GlobalRdrEnv, GlobalRdrElt )
+import qualified RnEnv as TcM
 import Var
 import VarEnv
 import VarSet
 import Outputable
 import Bag
 import UniqSupply
-
-import FastString
 import Util
-import Id
 import TcRnTypes
 
-import BasicTypes
 import Unique
 import UniqFM
-import Maybes ( orElse, firstJusts )
+import UniqDFM
+import Maybes
 
+import StaticFlags( opt_PprStyle_Debug )
 import TrieMap
-import Control.Monad( ap, when, unless )
+import Control.Monad
+#if __GLASGOW_HASKELL__ > 710
+import qualified Control.Monad.Fail as MonadFail
+#endif
 import MonadUtils
 import Data.IORef
-import Data.List ( partition, foldl' )
-import Pair
+import Data.List ( foldl', partition )
 
 #ifdef DEBUG
 import Digraph
@@ -176,87 +187,80 @@ 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.
--}
-
-data Deque a = DQ [a] [a]   -- Insert in RH field, remove from LH field
-                            -- First to remove is at head of LH field
-
-instance Outputable a => Outputable (Deque a) where
-  ppr q = ppr (dequeList q)
-
-dequeList :: Deque a -> [a]
-dequeList (DQ as bs) = as ++ reverse bs  -- First one to come out at the start
-
-emptyDeque :: Deque a
-emptyDeque = DQ [] []
-
-isEmptyDeque :: Deque a -> Bool
-isEmptyDeque (DQ as bs) = null as && null bs
-
-dequeSize :: Deque a -> Int
-dequeSize (DQ as bs) = length as + length bs
 
-insertDeque :: a -> Deque a -> Deque a
-insertDeque b (DQ as bs) = DQ as (b:bs)
+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.
 
-appendDeque :: Deque a -> Deque a -> Deque a
-appendDeque (DQ as1 bs1) (DQ as2 bs2) = DQ (as1 ++ reverse bs1 ++ as2) bs2
-
-extractDeque :: Deque a -> Maybe (Deque a, a)
-extractDeque (DQ [] [])     = Nothing
-extractDeque (DQ (a:as) bs) = Just (DQ as bs, a)
-extractDeque (DQ [] bs)     = case reverse bs of
-                                (a:as) -> Just (DQ as [], a)
-                                [] -> panic "extractDeque"
+-}
 
 -- See Note [WorkList priorities]
 data WorkList
   = WL { wl_eqs     :: [Ct]
-       , wl_funeqs  :: Deque Ct
+       , wl_funeqs  :: [Ct]  -- LIFO stack of goals
        , 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_implics = implics1 })
-    (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2, wl_implics = implics2 })
-   = WL { wl_eqs     = eqs1     ++            eqs2
-        , wl_funeqs  = funeqs1  `appendDeque` funeqs2
-        , wl_rest    = rest1    ++            rest2
+    (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1
+        , wl_deriv = ders1, wl_implics = implics1 })
+    (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2
+        , wl_deriv = ders2, 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_rest = rest })
-  = length eqs + dequeSize funeqs + length rest
+workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_deriv = ders, wl_rest = rest })
+  = length eqs + length funeqs + length rest + length ders
+
+workListWantedCount :: WorkList -> Int
+workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest })
+  = count isWantedCt eqs + count isWantedCt rest
 
 extendWorkListEq :: Ct -> WorkList -> WorkList
-extendWorkListEq ct wl
-  = wl { wl_eqs = ct : wl_eqs wl }
+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 = insertDeque ct (wl_funeqs wl) }
+extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl }
 
 extendWorkListNonEq :: Ct -> WorkList -> WorkList
 -- Extension by non equality
-extendWorkListNonEq ct wl
-  = wl { wl_rest = ct : wl_rest wl }
+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 :: 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 implic wl = wl { wl_implics = implic `consBag` wl_implics wl }
 
 extendWorkListCt :: Ct -> WorkList -> WorkList
 -- Agnostic
 extendWorkListCt ct wl
  = case classifyPredType (ctPred ct) of
-     EqPred ty1 _
+     EqPred NomEq ty1 _
        | Just (tc,_) <- tcSplitTyConApp_maybe ty1
        , isTypeFamilyTyCon tc
        -> extendWorkListFunEq ct wl
-       | otherwise
+     EqPred {}
        -> extendWorkListEq ct wl
 
      _ -> extendWorkListNonEq ct wl
@@ -267,47 +271,342 @@ extendWorkListCts cts wl = foldr extendWorkListCt wl cts
 
 isEmptyWorkList :: WorkList -> Bool
 isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
-                    , wl_rest = rest, wl_implics = implics })
-  = null eqs && null rest && isEmptyDeque funeqs && isEmptyBag implics
+                    , wl_rest = rest, wl_deriv = ders, wl_implics = implics })
+  = null eqs && null rest && null funeqs && isEmptyBag implics && null ders
 
 emptyWorkList :: WorkList
 emptyWorkList = WL { wl_eqs  = [], wl_rest = []
-                   , wl_funeqs = emptyDeque, wl_implics = emptyBag }
+                   , wl_funeqs = [], wl_deriv = [], wl_implics = emptyBag }
+
+selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
+selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs
+                      , wl_rest = rest })
+  | ct:cts <- eqs  = Just (ct, wl { wl_eqs    = cts })
+  | ct:fes <- feqs = Just (ct, wl { wl_funeqs = fes })
+  | ct:cts <- rest = Just (ct, wl { wl_rest   = cts })
+  | otherwise      = Nothing
+
+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)
+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
 
-selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
-selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
-  = case (eqs,feqs,rest) of
-      (ct:cts,_,_)     -> (Just ct, wl { wl_eqs    = cts })
-      (_,fun_eqs,_)    | Just (fun_eqs', ct) <- extractDeque fun_eqs
-                       -> (Just ct, wl { wl_funeqs = fun_eqs' })
-      (_,_,(ct:cts))   -> (Just ct, wl { wl_rest   = cts })
-      (_,_,_)          -> (Nothing,wl)
+       ; 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) } }
 
 -- Pretty printing
 instance Outputable WorkList where
   ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
-          , wl_rest = rest, wl_implics = implics })
+          , wl_rest = rest, wl_implics = implics, wl_deriv = ders })
    = text "WL" <+> (braces $
      vcat [ ppUnless (null eqs) $
-            ptext (sLit "Eqs =") <+> vcat (map ppr eqs)
-          , ppUnless (isEmptyDeque feqs) $
-            ptext (sLit "Funeqs =") <+> vcat (map ppr (dequeList feqs))
+            text "Eqs =" <+> vcat (map ppr eqs)
+          , ppUnless (null feqs) $
+            text "Funeqs =" <+> vcat (map ppr feqs)
           , ppUnless (null rest) $
-            ptext (sLit "Non-eqs =") <+> vcat (map ppr rest)
+            text "Non-eqs =" <+> vcat (map ppr rest)
+          , ppUnless (null ders) $
+            text "Derived =" <+> vcat (map ppr ders)
           , ppUnless (isEmptyBag implics) $
-            ptext (sLit "Implics =") <+> vcat (map ppr (bagToList 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)"
           ])
 
-{-
-************************************************************************
+
+{- *********************************************************************
 *                                                                      *
-*                            Inert Sets                                *
+                InertSet: the inert set
 *                                                                      *
 *                                                                      *
-************************************************************************
+********************************************************************* -}
 
-Note [Detailed InertCans Invariants]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+data InertSet
+  = IS { inert_cans :: InertCans
+              -- Canonical Given, Wanted, Derived (no Solved)
+              -- Sometimes called "the inert set"
+
+       , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
+              -- See Note [Type family equations]
+              -- If    F tys :-> (co, ty, ev),
+              -- then  co :: F tys ~ ty
+              --
+              -- Just a hash-cons cache for use when flattening only
+              -- These include entirely un-processed goals, so don't use
+              -- them to solve a top-level goal, else you may end up solving
+              -- (w:F ty ~ a) by setting w:=w!  We just use the flat-cache
+              -- when allocating a new flatten-skolem.
+              -- Not necessarily inert wrt top-level equations (or inert_cans)
+
+              -- NB: An ExactFunEqMap -- this doesn't match via loose types!
+
+       , inert_solved_dicts   :: DictMap CtEvidence
+              -- 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)))) ]
+
+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 }
+
+
+{- Note [Solved dictionaries]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we apply a top-level instance declararation, 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.
+
+But in particular, we can use it to create *recursive* dictionaries.
+The simplest, degnerate case is
+    instance C [a] => C [a] where ...
+If we have
+    [W] d1 :: C [x]
+then we can apply the instance to get
+    d1 = $dfCList d
+    [W] d2 :: C [x]
+Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
+    d1 = $dfCList d
+    d2 = d1
+
+See Note [Example of recursive dictionaries]
+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.
+
+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.
+Consider
+
+        class Ord a => C a where
+        instance Ord [a] => C [a] where ...
+
+Suppose we are trying to solve
+  [G] d1 : Ord a
+  [W] d2 : C [a]
+
+Then we'll use the instance decl to give
+
+  [G] d1 : Ord a     Solved: d2 : C [a] = $dfCList d3
+  [W] d3 : Ord [a]
+
+We must not add d4 : Ord [a] to the 'solved' set (by taking the
+superclass of d2), otherwise we'll use it to solve d3, without ever
+using d1, which would be a catastrophe.
+
+Solution: when extending the solved dictionaries, do not add superclasses.
+That's why each element of the inert_solved_dicts is the result of applying
+a dictionary function.
+
+Note [Example of recursive dictionaries]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--- Example 1
+
+    data D r = ZeroD | SuccD (r (D r));
+
+    instance (Eq (r (D r))) => Eq (D r) where
+        ZeroD     == ZeroD     = True
+        (SuccD a) == (SuccD b) = a == b
+        _         == _         = False;
+
+    equalDC :: D [] -> D [] -> Bool;
+    equalDC = (==);
+
+We need to prove (Eq (D [])). Here's how we go:
+
+   [W] d1 : Eq (D [])
+By instance decl of Eq (D r):
+   [W] d2 : Eq [D []]      where   d1 = dfEqD d2
+By instance decl of Eq [a]:
+   [W] d3 : Eq (D [])      where   d2 = dfEqList d3
+                                   d1 = dfEqD d2
+Now this wanted can interact with our "solved" d1 to get:
+    d3 = d1
+
+-- Example 2:
+This code arises in the context of "Scrap Your Boilerplate with Class"
+
+    class Sat a
+    class Data ctx a
+    instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
+    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2
+
+    class Data Maybe a => Foo a
+
+    instance Foo t => Sat (Maybe t)                             -- dfunSat
+
+    instance Data Maybe a => Foo a                              -- dfunFoo1
+    instance Foo a        => Foo [a]                            -- dfunFoo2
+    instance                 Foo [Char]                         -- dfunFoo3
+
+Consider generating the superclasses of the instance declaration
+         instance Foo a => Foo [a]
+
+So our problem is this
+    [G] d0 : Foo t
+    [W] d1 : Data Maybe [t]   -- Desired superclass
+
+We may add the given in the inert set, along with its superclasses
+  Inert:
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  WorkList
+    [W] d1 : Data Maybe [t]
+
+Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
+  Inert:
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+  WorkList:
+    [W] d2 : Sat (Maybe [t])
+    [W] d3 : Data Maybe t
+
+Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
+  Inert:
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+        d2 : Sat (Maybe [t])
+  WorkList:
+    [W] d3 : Data Maybe t
+    [W] d4 : Foo [t]
+
+Now, we can just solve d3 from d01; d3 := d01
+  Inert
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+        d2 : Sat (Maybe [t])
+  WorkList
+    [W] d4 : Foo [t]
+
+Now, solve d4 using dfunFoo2;  d4 := dfunFoo2 d5
+  Inert
+    [G] d0  : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+        d2 : Sat (Maybe [t])
+        d4 : Foo [t]
+  WorkList:
+    [W] d5 : Foo t
+
+Now, d5 can be solved! d5 := d0
+
+Result
+   d1 := dfunData2 d2 d3
+   d2 := dfunSat d4
+   d3 := d01
+   d4 := dfunFoo2 d5
+   d5 := d0
+-}
+
+{- *********************************************************************
+*                                                                      *
+                InertCans: the canonical inerts
+*                                                                      *
+*                                                                      *
+********************************************************************* -}
+
+data InertCans   -- See Note [Detailed InertCans Invariants] for more
+  = IC { inert_model :: InertModel
+              -- See Note [inert_model: the inert model]
+
+       , inert_eqs :: DTyVarEnv EqualCtList
+              -- See Note [inert_eqs: the inert equalities]
+              -- All Given/Wanted CTyEqCans; index is the LHS tyvar
+
+       , 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
+
+       , inert_dicts :: DictMap Ct
+              -- Dictionaries only
+              -- All fully rewritten (modulo flavour constraints)
+              --     wrt inert_eqs/inert_model
+
+       , inert_safehask :: DictMap Ct
+              -- Failed dictionary resolution due to Safe Haskell overlapping
+              -- instances restriction. We keep this seperate from inert_dicts
+              -- as it doesn't cause compilation failure, just safe inference
+              -- failure.
+              --
+              -- ^ See Note [Safe Haskell Overlapping Instances Implementation]
+              -- in TcSimplify
+
+       , inert_irreds :: Cts
+              -- Irreducible predicates
+
+       , inert_insols :: Cts
+              -- Frozen errors (as non-canonicals)
+
+       , 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
+       }
+
+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
+
+
+{- Note [Detailed InertCans Invariants]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The InertCans represents a collection of constraints with the following properties:
 
   * All canonical
@@ -347,137 +646,961 @@ Type-family equations, of form (ev : F tys ~ ty), live in three places
     using w3 itself!
 
   * The inert_funeqs are un-solved but fully processed and in the InertCans.
--}
 
--- All Given (fully known) or Wanted or Derived
--- See Note [Detailed InertCans Invariants] for more
-data InertCans
-  = IC { inert_eqs :: TyVarEnv EqualCtList
-              -- All CTyEqCans; index is the LHS tyvar
+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 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.
+
+   * Domain of the model = skolems + untouchables.
+     A touchable unification variable would have been unified first.
+
+   * 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
+
+  (R1) >= is transitive
+  (R2) If f1 >= f, and f2 >= f,
+       then either f1 >= f2 or f2 >= f1
+
+Lemma.  If f1 >= f then f1 >= f1
+Proof.  By property (R2), with f1=f2
+
+Definition [Generalised substitution]
+A "generalised substitution" S is a set of triples (a -f-> t), where
+  a is a type variable
+  t is a type
+  f is a flavour
+such that
+  (WF1) if (a -f1-> t1) in S
+           (a -f2-> t2) in S
+        then neither (f1 >= f2) nor (f2 >= f1) hold
+  (WF2) if (a -f-> t) is in S, then t /= a
+
+Definition [Applying a generalised substitution]
+If S is a generalised substitution
+   S(f,a) = t,  if (a -fs-> t) in S, and fs >= f
+          = a,  otherwise
+Application extends naturally to types S(f,t), modulo roles.
+See Note [Flavours with roles].
+
+Theorem: S(f,a) is well defined as a function.
+Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S,
+               and  f1 >= f and f2 >= f
+       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
+
+Notation: repeated application.
+  S^0(f,t)     = t
+  S^(n+1)(f,t) = S(f, S^n(t))
+
+Definition: inert generalised substitution
+A generalised substitution S is "inert" iff
+
+  (IG1) there is an n such that
+        for every f,t, S^n(f,t) = S^(n+1)(f,t)
+
+By (IG1) we define S*(f,t) to be the result of exahaustively
+applying S(f,_) to t.
+
+----------------------------------------------------------------
+Our main invariant:
+   the inert CTyEqCans should be an inert generalised substitution
+----------------------------------------------------------------
+
+Note that inertness is not the same as idempotence.  To apply S to a
+type, you may have to apply it recursive.  But inertness does
+guarantee that this recursive use will terminate.
+
+Note [Extending the inert equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Theorem [Stability under extension]
+   This is the main theorem!
+   Suppose we have a "work item"
+       a -fw-> t
+   and an inert generalised substitution S,
+   such that
+      (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
+
+      (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
+
+      (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
+
+   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
+
+The idea is that
+* (T1-2) are guaranteed by exhaustively rewriting the work-item
+  with S(fw,_).
+
+* T3 is guaranteed by a simple occurs-check on the work item.
+  This is done during canonicalisation, in canEqTyVar;
+  (invariant: a CTyEqCan never has an occurs check).
+
+* (K1-3) are the "kick-out" criteria.  (As stated, they are really the
+  "keep" criteria.) If the current inert S contains a triple that does
+  not satisfy (K1-3), then we remove it from S by "kicking it out",
+  and re-processing it.
+
+* Note that kicking out is a Bad Thing, because it means we have to
+  re-process a constraint.  The less we kick out, the better.
+  TODO: Make sure that kicking out really *is* a Bad Thing. We've assumed
+  this but haven't done the empirical study to check.
+
+* Assume we have  G>=G, G>=W and that's all.  Then, when performing
+  a unification we add a new given  a -G-> ty.  But doing so does NOT require
+  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.
+  Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
+         and so K1-K3 hold.  Intuitively, since fw can't rewrite anything,
+         adding it cannot cause any loops
+  This is a common case, because Wanteds cannot rewrite Wanteds.
+
+* Lemma (L1): The conditions of the Main Theorem imply that there is no
+              (a -fs-> t) in S, s.t.  (fs >= fw).
+  Proof. Suppose the contrary (fs >= fw).  Then because of (T1),
+  S(fw,a)=a.  But since fs>=fw, S(fw,a) = s, hence s=a.  But now we
+  have (a -fs-> a) in S, which contradicts (WF2).
+
+* The extended substitution satisfies (WF1) and (WF2)
+  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
+  - (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.
+
+  - (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).
+    It is always safe to extend S with such a triple.
+
+    (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
+
+  - (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
+
+  - (K2d): if a not in s, we hae no further opportunity to apply the
+    work item, similar to (K2b)
+
+  NB: Dimitrios has a PDF that does this in more detail
+
+Key lemma to make it watertight.
+  Under the conditions of the Main Theorem,
+  forall f st fw >= f, a is not in S^k(f,t), for any k
+
+Also, consider roles more carefully. See Note [Flavours with roles]
+
+Note [K3: completeness of solving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(K3) is not necessary for the extended substitution
+to be inert.  In fact K1 could be made stronger by saying
+   ... then (not (fw >= fs) or not (fs >= fs))
+But it's not enough for S to be inert; we also want completeness.
+That is, we want to be able to solve all soluble wanted equalities.
+Suppose we have
 
-       , inert_funeqs :: FunEqMap Ct
-              -- All CFunEqCans; index is the whole family head type.
+   work-item   b -G-> a
+   inert-item  a -W-> b
 
-       , inert_dicts :: DictMap Ct
-              -- Dictionaries only, index is the class
-              -- NB: index is /not/ the whole type because FD reactions
-              -- need to match the class but not necessarily the whole type.
+Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
+so we could extend the inerts, thus:
 
-       , inert_irreds :: Cts
-              -- Irreducible predicates
+   inert-items   b -G-> a
+                 a -W-> b
 
-       , inert_insols :: Cts
-              -- Frozen errors (as non-canonicals)
-       }
+But if we kicked-out the inert item, we'd get
 
-type EqualCtList = [Ct]
--- 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
---   - Multiple Wanteds, or
---   - Multiple Deriveds
+   work-item     a -W-> b
+   inert-item    b -G-> a
 
--- The Inert Set
-data InertSet
-  = IS { inert_cans :: InertCans
-              -- Canonical Given, Wanted, Derived (no Solved)
-              -- Sometimes called "the inert set"
+Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
+So we add one more clause to the kick-out criteria
 
-       , inert_flat_cache :: FunEqMap (TcCoercion, TcTyVar)
-              -- See Note [Type family equations]
-              -- If    F tys :-> (co, fsk),
-              -- then  co :: F tys ~ fsk
-              -- Just a hash-cons cache for use when flattening only
-              -- These include entirely un-processed goals, so don't use
-              -- them to solve a top-level goal, else you may end up solving
-              -- (w:F ty ~ a) by setting w:=w!  We just use the flat-cache
-              -- when allocating a new flatten-skolem.
-              -- Not necessarily inert wrt top-level equations (or inert_cans)
+Another way to understand (K3) is that we treat an inert item
+        a -f-> b
+in the same way as
+        b -f-> a
+So if we kick out one, we should kick out the other.  The orientation
+is somewhat accidental.
 
-       , inert_solved_dicts   :: DictMap CtEvidence
-              -- Of form ev :: C t1 .. tn
-              -- Always the result of using a top-level instance declaration
-              -- See Note [Solved constraints]
-              -- - Used to avoid creating a new EvVar when we have a new goal
-              --   that we have solved in the past
-              -- - Stored not necessarily as fully rewritten
-              --   (ToDo: rewrite lazily when we lookup)
-       }
+When considering roles, we also need the second clause (K3b). Consider
+
+  inert-item   a -W/R-> b c
+  work-item    c -G/N-> a
+
+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
+
+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).
+
+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
+
+
+Note [Flavours with roles]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+The system described in Note [inert_eqs: the inert equalities]
+discusses an abstract
+set of flavours. In GHC, flavours have two components: the flavour proper,
+taken from {Wanted, Derived, Given} and the equality relation (often called
+role), taken from {NomEq, ReprEq}.
+When substituting w.r.t. the inert set,
+as described in Note [inert_eqs: the inert equalities],
+we must be careful to respect all components of a flavour.
+For example, if we have
+
+  inert set: a -G/R-> Int
+             b -G/R-> Bool
+
+  type role T nominal representational
+
+and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT
+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 ics = vcat [ ptext (sLit "Equalities:")
-                   <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest)
-                                          emptyCts (inert_eqs ics))
-                 , ptext (sLit "Type-function equalities:")
-                   <+> pprCts (funEqsToBag (inert_funeqs ics))
-                 , ptext (sLit "Dictionaries:")
-                   <+> pprCts (dictsToBag (inert_dicts ics))
-                 , ptext (sLit "Irreds:")
-                   <+> pprCts (inert_irreds ics)
-                 , text "Insolubles =" <+> -- Clearly print frozen errors
-                    braces (vcat (map ppr (Bag.bagToList $ inert_insols ics)))
-                 ]
+  ppr (IC { inert_model = model, inert_eqs = eqs
+          , inert_funeqs = funeqs, inert_dicts = dicts
+          , inert_safehask = safehask, inert_irreds = irreds
+          , inert_insols = insols, inert_count = count })
+    = braces $ vcat
+      [ ppUnless (isEmptyDVarEnv eqs) $
+        text "Equalities:"
+          <+> pprCts (foldDVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
+      , ppUnless (isEmptyTcAppMap funeqs) $
+        text "Type-function equalities =" <+> pprCts (funEqsToBag funeqs)
+      , ppUnless (isEmptyTcAppMap dicts) $
+        text "Dictionaries =" <+> pprCts (dictsToBag dicts)
+      , ppUnless (isEmptyTcAppMap safehask) $
+        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)
+      , text "Unsolved goals =" <+> int count
+      ]
+
+{- *********************************************************************
+*                                                                      *
+                  Adding an inert
+*                                                                      *
+************************************************************************
 
-instance Outputable InertSet where
-  ppr is = vcat [ ppr $ inert_cans is
-                , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ]
+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
 
-emptyInert :: InertSet
-emptyInert
-  = IS { inert_cans = IC { inert_eqs     = emptyVarEnv
-                         , inert_dicts   = emptyDicts
-                         , inert_funeqs  = emptyFunEqs
-                         , inert_irreds  = emptyCts
-                         , inert_insols  = emptyCts
-                         }
-       , inert_flat_cache    = emptyFunEqs
-       , inert_solved_dicts  = emptyDictMap }
+ * And similarly given a new Given/Wanted 'c', we want to emit a
+   shadow 'c' if the model can rewrite [D] c
 
----------------
-addInertCan :: InertCans -> Ct -> InertCans
+See modelCanRewrite.
+
+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]
+
+Note [Kicking out CFunEqCan for fundeps]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider:
+   New:    [D] fmv1 ~ fmv2
+   Inert:  [W] F alpha ~ fmv1
+           [W] F beta  ~ fmv2
+
+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
+   Model: [D] fmv1 ~ fmv2
+
+and now improvement will discover [D] alpha ~ beta. This is important;
+eg in Trac #9587.
+-}
+
+addInertEq :: Ct -> TcS ()
+-- This is a key function, because of the kick-out stuff
 -- Precondition: item /is/ canonical
-addInertCan ics item@(CTyEqCan {})
-  = ics { inert_eqs = extendVarEnv_C (\eqs _ -> item : eqs)
-                              (inert_eqs ics)
-                              (cc_tyvar item) [item] }
+addInertEq ct@(CTyEqCan { cc_tyvar = tv })
+  = do { traceTcS "addInertEq {" $
+         text "Adding new inert equality:" <+> ppr ct
+       ; ics <- getInertCans
+
+       ; let (kicked_out, ics1) = kickOutRewritable (ctFlavourRole ct) tv ics
+       ; ics2 <- add_inert_eq ics1 ct
+
+       ; setInertCans ics2
+
+       ; 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.
+
+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!
+
+Still, here's one possible reason for adding derived shadows
+for Givens.  Consider
+           work-item [G] a ~ [b], model 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
+occurs check.  Without it we'll miss the occurs check (reporting
+inaccessible code); but that's probably OK.
+
+Note [Keep CDictCan shadows as CDictCan]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+  class C a => D a b
+and [G] D a b, [G] C a in the inert set.  Now we insert
+[D] b ~ c.  We want to kick out a derived shadow for [D] D a b,
+so we can rewrite it with the new constraint, and perhaps get
+instance reduction or other consequences.
+
+BUT we do not want to kick out a *non-canonical* (D a b). If we
+did, we would do this:
+  - rewrite it to [D] D a c, with pend_sc = True
+  - use expandSuperClasses to add C a
+  - go round again, which solves C a from the givens
+This loop goes on for ever and triggers the simpl_loop limit.
+
+Solution: kick out the CDictCan which will have pend_sc = False,
+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.
+-}
+
+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.
+
+rewritableTyCoVars :: Ct -> TcTyVarSet
+-- The tyvars of a Ct that can be rewritten
+rewritableTyCoVars (CFunEqCan { cc_tyargs = tys }) = tyCoVarsOfTypes tys
+rewritableTyCoVars ct                              = tyCoVarsOfType (ctPred ct)
 
-addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
+--------------
+addInertCan :: Ct -> TcS ()  -- Constraints *other than* equalities
+addInertCan ct
+  = do { traceTcS "insertInertCan {" $
+         text "Trying to insert new inert item:" <+> ppr ct
+
+       ; ics <- getInertCans
+       ; 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 }
+
+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 }
 
-addInertCan ics item@(CIrredEvCan {})
-  = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
+add_item ics item@(CIrredEvCan { cc_ev = ev })
+  = ics { inert_irreds = inert_irreds ics `Bag.snocBag` 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
 
-addInertCan ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
-  = ics { inert_dicts = addDict (inert_dicts ics) cls tys item }
+add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
+  = ics { inert_dicts = addDict (inert_dicts ics) cls tys item
+        , inert_count = bumpUnsolvedCount ev (inert_count ics) }
 
-addInertCan _ item
+add_item _ item
   = pprPanic "upd_inert set: can't happen! Inserting " $
-    ppr item   -- Can't be CNonCanonical, CHoleCan,
+    ppr item   -- CTyEqCan is dealt with by addInertEq
+               -- Can't be CNonCanonical, CHoleCan,
                -- because they only land in inert_insols
 
+bumpUnsolvedCount :: CtEvidence -> Int -> Int
+bumpUnsolvedCount ev n | isWanted ev = n+1
+                       | otherwise   = n
+
+
+-----------------------------------------
+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)
+-- 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)
+  = (emptyWorkList, ics)
+        -- If new_fr can't rewrite itself, it can't rewrite
+        -- anything else, so no need to kick out anything.
+        -- (This is a common case: wanteds can't rewrite wanteds)
+        -- Lemma (L2) in Note [Extending the inert equalities]
+
+  | otherwise
+  = (kicked_out, inert_cans_in)
+  where
+    inert_cans_in = IC { inert_eqs      = tv_eqs_in
+                       , inert_dicts    = dicts_in
+                       , inert_safehask = safehask   -- ??
+                       , inert_funeqs   = feqs_in
+                       , inert_irreds   = irs_in
+                       , inert_insols   = insols_in
+                       , 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 }
+
+    (tv_eqs_out, tv_eqs_in) = foldDVarEnv kick_out_eqs ([], emptyDVarEnv) tv_eqs
+    (feqs_out,   feqs_in)   = partitionFunEqs  kick_out_fe funeqmap
+    (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]
+
+    fr_can_rewrite :: CtEvidence -> Bool
+    fr_can_rewrite ev = new_fr `eqCanRewriteFR` (ctEvFlavourRole ev)
+
+    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
+
+    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)
+
+    kick_out_eqs :: EqualCtList -> ([Ct], DTyVarEnv EqualCtList)
+                 -> ([Ct], DTyVarEnv EqualCtList)
+    kick_out_eqs eqs (acc_out, acc_in)
+      = (eqs_out ++ acc_out, case eqs_in of
+                               []      -> acc_in
+                               (eq1:_) -> extendDVarEnv acc_in (cc_tyvar eq1) eqs_in)
+      where
+        (eqs_in, eqs_out) = partition keep_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)
+
+      | 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
+          = case eq_rel of
+              NomEq  -> not (rhs_ty `eqType` mkTyVarTy new_tv)
+              ReprEq -> not (isTyVarExposed new_tv rhs_ty)
+
+          | otherwise
+          = True
+
+    keep_eq ct = pprPanic "keep_eq" (ppr ct)
+
+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
+                     -- 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
+
+
+{- Note [kickOutRewritable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [inert_eqs: the inert equalities].
+
+When we add a new inert equality (a ~N ty) to the inert set,
+we must kick out any inert items that could be rewritten by the
+new equality, to maintain the inert-set invariants.
+
+  - We want to kick out an existing inert constraint if
+    a) the new constraint can rewrite the inert one
+    b) 'a' is free in the inert constraint (so that it *will*)
+       rewrite it if we kick it out.
+
+    For (b) we use tyCoVarsOfCt, which returns the type variables /and
+    the kind variables/ that are directly visible in the type. Hence
+    we will have exposed all the rewriting we care about to make the
+    most precise kinds visible for matching classes etc. No need to
+    kick out constraints that mention type variables whose kinds
+    contain this variable!
+
+  - 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)
+
+  - 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]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+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.
+-}
+
+
+
 --------------
-insertInertItemTcS :: Ct -> TcS ()
--- Add a new item in the inerts of the monad
-insertInertItemTcS item
-  = do { traceTcS "insertInertItemTcS {" $
-         text "Trying to insert new inert item:" <+> ppr item
+addInertSafehask :: InertCans -> Ct -> InertCans
+addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
+  = ics { inert_safehask = addDict (inert_dicts ics) cls tys item }
+
+addInertSafehask _ item
+  = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item
 
-       ; updInertCans (\ics -> addInertCan ics item)
+insertSafeOverlapFailureTcS :: Ct -> TcS ()
+-- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
+insertSafeOverlapFailureTcS item
+  = updInertCans (\ics -> addInertSafehask ics item)
 
-       ; traceTcS "insertInertItemTcS }" $ empty }
+getSafeOverlapFailures :: TcS Cts
+-- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
+getSafeOverlapFailures
+ = do { IC { inert_safehask = safehask } <- getInertCans
+      ; return $ foldDicts consCts safehask emptyCts }
 
+--------------
 addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
 -- 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 ()
@@ -486,6 +1609,12 @@ addSolvedDict item cls tys
        ; updInertTcS $ \ ics ->
              ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
 
+{- *********************************************************************
+*                                                                      *
+                  Other inert-set operations
+*                                                                      *
+********************************************************************* -}
+
 updInertTcS :: (InertSet -> InertSet) -> TcS ()
 -- Modify the inert set with the supplied function
 updInertTcS upd_fn
@@ -499,6 +1628,44 @@ 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
+  = do { is_var <- getTcSInertsRef
+       ; wrapTcS (do { inerts <- TcM.readTcRef is_var
+                     ; let (res, cans') = upd_fn (inert_cans inerts)
+                     ; TcM.writeTcRef is_var (inerts { inert_cans = cans' })
+                     ; return res }) }
+
 updInertCans :: (InertCans -> InertCans) -> TcS ()
 -- Modify the inert set with the supplied function
 updInertCans upd_fn
@@ -509,6 +1676,11 @@ updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
 updInertDicts upd_fn
   = updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }
 
+updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
+-- Modify the inert set with the supplied function
+updInertSafehask upd_fn
+  = updInertCans $ \ ics -> ics { inert_safehask = upd_fn (inert_safehask ics) }
+
 updInertFunEqs :: (FunEqMap Ct -> FunEqMap Ct) -> TcS ()
 -- Modify the inert set with the supplied function
 updInertFunEqs upd_fn
@@ -519,106 +1691,128 @@ updInertIrreds :: (Cts -> Cts) -> TcS ()
 updInertIrreds upd_fn
   = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
 
-
-prepareInertsForImplications :: InertSet -> (InertSet)
--- See Note [Preparing inert set for implications]
-prepareInertsForImplications is@(IS { inert_cans = cans })
-  = is { inert_cans       = getGivens cans
-       , inert_flat_cache = emptyFunEqs }  -- See Note [Do not inherit the flat cache]
+getInertEqs :: TcS (DTyVarEnv EqualCtList)
+getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
+
+getInertModel :: TcS InertModel
+getInertModel = do { inert <- getInertCans; return (inert_model inert) }
+
+getInertGivens :: TcS [Ct]
+-- Returns the Given constraints in the inert set,
+-- with type functions *not* unflattened
+getInertGivens
+  = do { inerts <- getInertCans
+       ; let all_cts = foldDicts (:) (inert_dicts inerts)
+                     $ foldFunEqs (:) (inert_funeqs inerts)
+                     $ 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
   where
-    getGivens (IC { inert_eqs    = eqs
-                  , inert_irreds = irreds
-                  , inert_funeqs = funeqs
-                  , inert_dicts  = dicts })
-      = IC { inert_eqs     = filterVarEnv  is_given_ecl eqs
-           , inert_funeqs  = filterFunEqs  isGivenCt funeqs
-           , inert_irreds  = Bag.filterBag isGivenCt irreds
-           , inert_dicts   = filterDicts   isGivenCt dicts
-           , inert_insols  = emptyCts }
-
-    is_given_ecl :: EqualCtList -> Bool
-    is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True
-    is_given_ecl _                        = False
-
-{-
-Note [Do not inherit the flat cache]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We do not want to inherit the flat cache when processing nested
-implications.  Consider
-   a ~ F b, forall c. b~Int => blah
-If we have F b ~ fsk in the flat-cache, and we push that into the
-nested implication, we might miss that F b can be rewritten to F Int,
-and hence perhpas solve it.  Moreover, the fsk from outside is
-flattened out after solving the outer level, but and we don't
-do that flattening recursively.
-
-Note [Preparing inert set for implications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Before solving the nested implications, we trim the inert set,
-retaining only Givens.  These givens can be used when solving
-the inner implications.
-
-There might be cases where interactions between wanteds at different levels
-could help to solve a constraint. For example
-
-        class C a b | a -> b
-        (C Int alpha), (forall d. C d blah => C Int a)
+    get_sc_dicts ic@(IC { inert_dicts = dicts })
+      = (sc_pend_dicts, ic')
+      where
+        ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts }
 
-If we pushed the (C Int alpha) inwards, as a given, it can produce a
-fundep (alpha~a) and this can float out again and be used to fix
-alpha.  (In general we can't float class constraints out just in case
-(C d blah) might help to solve (C Int a).)  But we ignore this possiblity.
+        sc_pend_dicts :: [Ct]
+        sc_pend_dicts = foldDicts get_pending dicts []
 
-For Derived constraints we don't have evidence, so we do not turn
-them into Givens.  There can *be* deriving CFunEqCans; see Trac #8129.
--}
+    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
 
-getInertEqs :: TcS (TyVarEnv EqualCtList)
-getInertEqs = do { inert <- getTcSInerts
-                 ; return (inert_eqs (inert_cans inert)) }
+    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)
 
 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
+--
+-- Post-condition: the returned simple constraints are all fully zonked
+--                     (because they come from the inert set)
+--                 the unsolved implics may not be
 getUnsolvedInerts
- = do { IC { inert_eqs = tv_eqs, inert_funeqs = fun_eqs
-           , inert_irreds = irreds, inert_dicts = idicts
-           , inert_insols = insols } <- getInertCans
-
-      ; let unsolved_tv_eqs  = foldVarEnv (\cts rest -> foldr add_if_unsolved rest cts)
-                                          emptyCts tv_eqs
+ = do { IC { inert_eqs    = tv_eqs
+           , 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
             unsolved_irreds  = Bag.filterBag is_unsolved irreds
             unsolved_dicts   = foldDicts add_if_unsolved idicts emptyCts
-            others = unsolved_irreds `unionBags` unsolved_dicts
+            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 "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
   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
 
-getNoGivenEqs :: TcLevel     -- TcLevel of this implication
+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
+  = case lookupDVarEnv eqs tv of
+      Nothing  -> False
+      Just cts -> any (same_pred rhs) cts
+  where
+    same_pred rhs ct
+      | CTyEqCan { cc_rhs = rhs2, cc_eq_rel = eq_rel } <- ct
+      , NomEq <- eq_rel
+      , rhs `eqType` rhs2 = True
+      | otherwise         = False
+
+getNoGivenEqs :: TcLevel          -- TcLevel of this implication
                -> [TcTyVar]       -- Skolems of this implication
+               -> Cts             -- Given insolubles from solveGivens
                -> TcS Bool        -- True <=> definitely no residual given equalities
 -- See Note [When does an implication have given equalities?]
-getNoGivenEqs tclvl skol_tvs
-  = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds, inert_funeqs = funeqs })
+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
-                          || foldVarEnv ((||) . eqs_given_here local_fsks) False ieqs
+             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])
+       ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
+                                        , ppr given_insols])
        ; return (not has_given_eqs) }
   where
     eqs_given_here :: VarSet -> EqualCtList -> Bool
@@ -632,7 +1826,7 @@ getNoGivenEqs tclvl skol_tvs
     -- i.e. the current level
     ev_given_here ev
       =  isGiven ev
-      && tclvl == tcl_tclvl (ctl_env (ctEvLoc ev))
+      && tclvl == ctLocLevel (ctEvLoc ev)
 
     add_fsk :: Ct -> VarSet -> VarSet
     add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
@@ -646,7 +1840,70 @@ getNoGivenEqs tclvl skol_tvs
           FlatSkol {} -> not (tv `elemVarSet` local_fsks)
           _           -> False
 
-{-
+-- | Returns Given constraints that might,
+-- potentially, match the given pred. This is used when checking to see if a
+-- 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 })
+  = filterBag matchable_given all_relevant_givens
+  where
+    -- just look in class constraints and irreds. matchableGivens does get called
+    -- for ~R constraints, but we don't need to look through equalities, because
+    -- canonical equalities are used for rewriting. We'll only get caught by
+    -- non-canonical -- that is, irreducible -- equalities.
+    all_relevant_givens :: Cts
+    all_relevant_givens
+      | Just (clas, _) <- getClassPredTys_maybe pred
+      = findDictsByClass (inert_dicts inert_cans) clas
+        `unionBags` inert_irreds inert_cans
+      | otherwise
+      = inert_irreds 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
+
+      | otherwise
+      = False
+      where
+        ctev = cc_ev ct
+
+    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
+
+prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
+-- See Note [Solving superclass constraints] in TcInstDcls
+prohibitedSuperClassSolve from_loc solve_loc
+  | GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
+  , ScOrigin wanted_size <- ctLocOrigin solve_loc
+  = given_size >= wanted_size
+  | otherwise
+  = False
+
+{- Note [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!
+
 Note [When does an implication have given equalities?]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider an implication
@@ -687,6 +1944,9 @@ are some wrinkles:
 
  * See Note [Let-bound skolems] for another wrinkle
 
+ * We do *not* need to worry about representational equalities, because
+   these do not affect the ability to float constraints.
+
 Note [Let-bound skolems]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 If   * the inert set contains a canonical Given CTyEqCan (a ~ ty)
@@ -707,17 +1967,6 @@ b) 'a' will have been completely substituted out in the inert set,
 For an example, see Trac #9211.
 -}
 
-splitInertCans :: InertCans -> ([Ct], [Ct], [Ct])
--- ^ Extract the (given, derived, wanted) inert constraints
-splitInertCans iCans = (given,derived,wanted)
-  where
-    allCts   = foldDicts  (:) (inert_dicts iCans)
-             $ foldFunEqs (:) (inert_funeqs iCans)
-             $ concat (varEnvElts (inert_eqs iCans))
-
-    (derived,other) = partition isDerivedCt allCts
-    (wanted,given)  = partition isWantedCt  other
-
 removeInertCts :: [Ct] -> InertCans -> InertCans
 -- ^ Remove inert constraints from the 'InertCans', for use when a
 -- typechecker plugin wishes to discard a given.
@@ -733,31 +1982,15 @@ removeInertCt is ct =
     CFunEqCan { cc_fun  = tf,  cc_tyargs = tys } ->
       is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }
 
-    CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty  } ->
-      is { inert_eqs = delTyEq (inert_eqs is) x ty }
+    CTyEqCan  { cc_tyvar = x,  cc_rhs    = ty } ->
+      is { inert_eqs    = delTyEq (inert_eqs is) x ty }
 
     CIrredEvCan {}   -> panic "removeInertCt: CIrredEvCan"
     CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
     CHoleCan {}      -> panic "removeInertCt: CHoleCan"
 
 
-checkAllSolved :: TcS Bool
--- True if there are no unsolved wanteds
--- Ignore Derived for this purpose, unless in insolubles
-checkAllSolved
- = do { is <- getTcSInerts
-
-      ; let icans = inert_cans is
-            unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans)
-            unsolved_dicts  = foldDicts ((||)  . isWantedCt) (inert_dicts icans)  False
-            unsolved_funeqs = foldFunEqs ((||) . isWantedCt) (inert_funeqs icans) False
-            unsolved_eqs    = foldVarEnv ((||) . any isWantedCt) False (inert_eqs icans)
-
-      ; return (not (unsolved_eqs || unsolved_irreds
-                     || unsolved_dicts || unsolved_funeqs
-                     || not (isEmptyBag (inert_insols icans)))) }
-
-lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcTyVar))
+lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
 lookupFlatCache fam_tc tys
   = do { IS { inert_flat_cache = flat_cache
             , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
@@ -765,94 +1998,138 @@ lookupFlatCache fam_tc tys
                              lookup_flats flat_cache]) }
   where
     lookup_inerts inert_funeqs
-      | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk })
-           <- findFunEqs inert_funeqs fam_tc tys
-      = Just (ctEvCoercion ctev, fsk)
+      | 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
+                            -- Note [Use loose types in inert set]
+      = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
       | otherwise = Nothing
 
-    lookup_flats flat_cache = findFunEq flat_cache fam_tc tys
+    lookup_flats flat_cache = findExactFunEq flat_cache fam_tc tys
 
 
-lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
+lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
-lookupInInerts loc pty
+lookupInInerts pty
+  | ClassPred cls tys <- classifyPredType pty
   = do { inerts <- getTcSInerts
-       ; return $ case (classifyPredType pty) of
-           ClassPred cls tys
-              | Just ev <- lookupSolvedDict inerts loc cls tys
-              -> Just ev
-              | otherwise
-              -> lookupInertDict (inert_cans inerts) loc cls tys
-
-           _other -> Nothing -- NB: No caching for equalities, IPs, holes, or errors
-      }
-
-lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
-lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
+       ; return (lookupSolvedDict inerts cls tys `mplus`
+                 lookupInertDict (inert_cans inerts) 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
-      Just ct | let ev = ctEvidence ct
-              , ctEvCheckDepth cls loc ev
-              -> Just ev
+      Just ct -> Just (ctEvidence ct)
       _       -> Nothing
 
-lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
+-- | 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
 -- Returns just if exactly this predicate type exists in the solved.
-lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
+lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
   = case findDict solved cls tys of
-      Just ev | ctEvCheckDepth cls loc ev -> Just ev
-      _                                   -> Nothing
+      Just ev -> Just ev
+      _       -> Nothing
 
-{-
-************************************************************************
+{- *********************************************************************
 *                                                                      *
-                   TyEqMap
+                   Irreds
 *                                                                      *
-************************************************************************
+********************************************************************* -}
+
+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
 -}
 
-type TyEqMap a = TyVarEnv a
+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]
+
+foldTyEqs :: (Ct -> b -> b) -> DTyVarEnv EqualCtList -> b -> b
+foldTyEqs k eqs z
+  = foldDVarEnv (\cts z -> foldr k z cts) z eqs
 
-findTyEqs :: TyEqMap EqualCtList -> TyVar -> EqualCtList
-findTyEqs m tv = lookupVarEnv m tv `orElse` []
+findTyEqs :: InertCans -> TyVar -> EqualCtList
+findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` []
 
-delTyEq :: TyEqMap EqualCtList -> TcTyVar -> TcType -> TyEqMap EqualCtList
-delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
+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
 
-{-
-************************************************************************
+{- *********************************************************************
 *                                                                      *
-                   TcAppMap, DictMap, FunEqMap
+                   TcAppMap
 *                                                                      *
 ************************************************************************
+
+Note [Use loose types in inert set]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Say we know (Eq (a |> c1)) and we need (Eq (a |> c2)). One is clearly
+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!
+
 -}
 
-type TcAppMap a = UniqFM (ListMap TypeMap a)
-    -- Indexed by tycon then the arg types
-    -- Used for types and classes; hence UniqFM
+type TcAppMap a = UniqDFM (ListMap LooseTypeMap a)
+    -- Indexed by tycon then the arg types, using "loose" matching, where
+    -- we don't require kind equality. This allows, for example, (a |> co)
+    -- to match (a).
+    -- See Note [Use loose types in inert set]
+    -- Used for types and classes; hence UniqDFM
+    -- See Note [foldTM determinism] for why we use UniqDFM here
+
+isEmptyTcAppMap :: TcAppMap a -> Bool
+isEmptyTcAppMap m = isNullUDFM m
 
 emptyTcAppMap :: TcAppMap a
-emptyTcAppMap = emptyUFM
+emptyTcAppMap = emptyUDFM
 
 findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
-findTcApp m u tys = do { tys_map <- lookupUFM m u
+findTcApp m u tys = do { tys_map <- lookupUDFM m u
                        ; lookupTM tys tys_map }
 
 delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
-delTcApp m cls tys = adjustUFM (deleteTM tys) m cls
+delTcApp m cls tys = adjustUDFM (deleteTM tys) m cls
 
 insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
-insertTcApp m cls tys ct = alterUFM alter_tm m cls
+insertTcApp m cls tys ct = alterUDFM alter_tm m cls
   where
     alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
 
 -- mapTcApp :: (a->b) -> TcAppMap a -> TcAppMap b
--- mapTcApp f = mapUFM (mapTM f)
+-- mapTcApp f = mapUDFM (mapTM f)
 
 filterTcAppMap :: (Ct -> Bool) -> TcAppMap Ct -> TcAppMap Ct
 filterTcAppMap f m
-  = mapUFM do_tm m
+  = mapUDFM do_tm m
   where
     do_tm tm = foldTM insert_mb tm emptyTM
     insert_mb ct tm
@@ -868,9 +2145,15 @@ tcAppMapToBag :: TcAppMap a -> Bag a
 tcAppMapToBag m = foldTcAppMap consBag m emptyBag
 
 foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
-foldTcAppMap k m z = foldUFM (foldTM k) z m
+foldTcAppMap k m z = foldUDFM (foldTM k) z m
+
+
+{- *********************************************************************
+*                                                                      *
+                   DictMap
+*                                                                      *
+********************************************************************* -}
 
--------------------------
 type DictMap a = TcAppMap a
 
 emptyDictMap :: DictMap a
@@ -884,7 +2167,7 @@ findDict m cls tys = findTcApp m (getUnique cls) tys
 
 findDictsByClass :: DictMap a -> Class -> Bag a
 findDictsByClass m cls
-  | Just tm <- lookupUFM m cls = foldTM consBag tm emptyBag
+  | Just tm <- lookupUDFM m cls = foldTM consBag tm emptyBag
   | otherwise                  = emptyBag
 
 delDict :: DictMap a -> Class -> [Type] -> DictMap a
@@ -895,7 +2178,7 @@ addDict m cls tys item = insertTcApp m (getUnique cls) tys item
 
 addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
 addDictsByClass m cls items
-  = addToUFM m cls (foldrBag add emptyTM items)
+  = addToUDFM m cls (foldrBag add emptyTM items)
   where
     add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
     add ct _ = pprPanic "addDictsByClass" (ppr ct)
@@ -921,7 +2204,13 @@ foldDicts = foldTcAppMap
 emptyDicts :: DictMap a
 emptyDicts = emptyTcAppMap
 
-------------------------
+
+{- *********************************************************************
+*                                                                      *
+                   FunEqMap
+*                                                                      *
+********************************************************************* -}
+
 type FunEqMap a = TcAppMap a  -- A map whose key is a (TyCon, [Type]) pair
 
 emptyFunEqs :: TcAppMap a
@@ -933,9 +2222,6 @@ sizeFunEqMap m = foldFunEqs (\ _ x -> x+1) m 0
 findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
 findFunEq m tc tys = findTcApp m (getUnique tc) tys
 
-findFunEqs :: FunEqMap a -> TyCon -> [Type] -> Maybe a
-findFunEqs m tc tys = findTcApp m (getUnique tc) tys
-
 funEqsToBag :: FunEqMap a -> Bag a
 funEqsToBag m = foldTcAppMap consBag m emptyBag
 
@@ -945,7 +2231,7 @@ findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
 -- We use this to check for derived interactions with built-in type-function
 -- constructors.
 findFunEqsByTyCon m tc
-  | Just tm <- lookupUFM m tc = foldTM (:) tm []
+  | Just tm <- lookupUDFM m tc = foldTM (:) tm []
   | otherwise                 = []
 
 foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
@@ -960,19 +2246,14 @@ filterFunEqs = filterTcAppMap
 insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
 insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
 
--- insertFunEqCt :: FunEqMap Ct -> Ct -> FunEqMap Ct
--- insertFunEqCt m ct@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
---  = insertFunEq m tc tys ct
--- insertFunEqCt _ ct = pprPanic "insertFunEqCt" (ppr ct)
-
-partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> (Bag Ct, FunEqMap Ct)
+partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> ([Ct], FunEqMap Ct)
 -- Optimise for the case where the predicate is false
 -- partitionFunEqs is called only from kick-out, and kick-out usually
 -- kicks out very few equalities, so we want to optimise for that case
-partitionFunEqs f m = (yeses, foldrBag del m yeses)
+partitionFunEqs f m = (yeses, foldr del m yeses)
   where
-    yeses = foldTcAppMap k m emptyBag
-    k ct yeses | f ct      = yeses `snocBag` ct
+    yeses = foldTcAppMap k m []
+    k ct yeses | f ct      = ct : yeses
                | otherwise = yeses
     del (CFunEqCan { cc_fun = tc, cc_tyargs = tys }) m
         = delFunEq m tc tys
@@ -981,6 +2262,20 @@ partitionFunEqs f m = (yeses, foldrBag del m yeses)
 delFunEq :: FunEqMap a -> TyCon -> [Type] -> FunEqMap a
 delFunEq m tc tys = delTcApp m (getUnique tc) tys
 
+------------------------------
+type ExactFunEqMap a = UniqFM (ListMap TypeMap a)
+
+emptyExactFunEqs :: ExactFunEqMap a
+emptyExactFunEqs = emptyUFM
+
+findExactFunEq :: ExactFunEqMap a -> TyCon -> [Type] -> Maybe a
+findExactFunEq m tc tys = do { tys_map <- lookupUFM m (getUnique tc)
+                             ; lookupTM tys tys_map }
+
+insertExactFunEq :: ExactFunEqMap a -> TyCon -> [Type] -> a -> ExactFunEqMap a
+insertExactFunEq m tc tys val = alterUFM alter_tm m (getUnique tc)
+  where alter_tm mb_tm = Just (insertTM tys val (mb_tm `orElse` emptyTM))
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1000,20 +2295,37 @@ 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    :: EvBindsVar,
 
-      tcs_unified :: IORef Bool,
-          -- The "dirty-flag" Bool is set True when
-          -- we unify a unification variable
+      tcs_unified     :: IORef Int,
+         -- The number of unification variables we have filled
+         -- The important thing is whether it is non-zero
+
+      tcs_count     :: IORef Int, -- Global step count
+
+      tcs_inerts    :: IORef InertSet, -- Current inert set
 
-      tcs_count    :: IORef Int, -- Global step count
+      -- The main work-list and the flattening worklist
+      -- See Note [Work list priorities] and
+      tcs_worklist  :: IORef WorkList, -- Current worklist
 
-      tcs_inerts   :: IORef InertSet, -- Current inert set
-      tcs_worklist :: IORef WorkList  -- Current worklist
+      tcs_need_deriveds :: Bool
+        -- Keep solving, even if all the unsolved constraints are Derived
+        -- See Note [Solving for Derived constraints]
     }
 
 ---------------
@@ -1023,14 +2335,18 @@ instance Functor TcS where
   fmap f m = TcS $ fmap f . unTcS m
 
 instance Applicative TcS where
-  pure  = return
+  pure x = TcS (\_ -> return x)
   (<*>) = ap
 
 instance Monad TcS where
-  return x  = TcS (\_ -> return x)
   fail err  = TcS (\_ -> fail err)
   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
 
@@ -1052,15 +2368,19 @@ wrapWarnTcS :: TcM a -> TcS a
 -- There's no static check; it's up to the user
 wrapWarnTcS = wrapTcS
 
-failTcS, panicTcS :: SDoc -> TcS a
+failTcS, panicTcS  :: SDoc -> TcS a
+warnTcS   :: WarningFlag -> SDoc -> TcS ()
+addErrTcS :: SDoc -> TcS ()
 failTcS      = wrapTcS . TcM.failWith
+warnTcS flag = wrapTcS . TcM.addWarn (Reason flag)
+addErrTcS    = wrapTcS . TcM.addErr
 panicTcS doc = pprPanic "TcCanonical" doc
 
 traceTcS :: String -> SDoc -> TcS ()
 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
 
 runTcPluginTcS :: TcPluginM a -> TcS a
-runTcPluginTcS = wrapTcS . runTcPluginM
+runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBindsVar
 
 instance HasDynFlags TcS where
     getDynFlags = wrapTcS getDynFlags
@@ -1083,7 +2403,7 @@ traceFireTcS ev doc
   = TcS $ \env -> csTraceTcM 1 $
     do { n <- TcM.readTcRef (tcs_count env)
        ; tclvl <- TcM.getTcLevel
-       ; return (hang (int n <> brackets (ptext (sLit "U:") <> ppr tclvl
+       ; return (hang (int n <> brackets (text "U:" <> ppr tclvl
                                           <> ppr (ctLocDepth (ctEvLoc ev)))
                        <+> doc <> colon)
                      4 (ppr ev)) }
@@ -1098,47 +2418,60 @@ csTraceTcM trace_level mk_doc
             ; TcM.traceTcRn Opt_D_dump_cs_trace msg } }
 
 runTcS :: TcS a                -- What to run
-       -> TcM (a, Bag EvBind)
+       -> TcM (a, EvBindMap)
 runTcS tcs
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; res <- runTcSWithEvBinds ev_binds_var tcs
-       ; ev_binds <- TcM.getTcEvBinds ev_binds_var
+       ; res <- runTcSWithEvBinds False ev_binds_var tcs
+       ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
        ; return (res, ev_binds) }
 
-runTcSWithEvBinds :: EvBindsVar
+-- | This variant of 'runTcS' will keep solving, even when only Deriveds
+-- are left around. It also doesn't return any evidence, as callers won't
+-- need it.
+runTcSDeriveds :: TcS a -> TcM a
+runTcSDeriveds tcs
+  = do { ev_binds_var <- TcM.newTcEvBinds
+       ; runTcSWithEvBinds True ev_binds_var tcs }
+
+-- | This can deal only with equality constraints.
+runTcSEqualities :: TcS a -> TcM a
+runTcSEqualities thing_inside
+  = do { ev_binds_var <- TcM.newTcEvBinds
+       ; runTcSWithEvBinds False ev_binds_var thing_inside }
+
+runTcSWithEvBinds :: Bool  -- ^ keep running even if only Deriveds are left?
+                  -> EvBindsVar
                   -> TcS a
                   -> TcM a
-runTcSWithEvBinds ev_binds_var tcs
-  = do { unified_var <- TcM.newTcRef False
+runTcSWithEvBinds solve_deriveds ev_binds_var tcs
+  = do { unified_var <- TcM.newTcRef 0
        ; step_count <- TcM.newTcRef 0
-       ; inert_var <- TcM.newTcRef is
+       ; inert_var <- TcM.newTcRef emptyInert
        ; wl_var <- TcM.newTcRef emptyWorkList
-
-       ; 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 }
+       ; 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_need_deriveds = solve_deriveds }
 
              -- Run the computation
        ; res <- unTcS tcs env
 
        ; count <- TcM.readTcRef step_count
        ; when (count > 0) $
-         csTraceTcM 0 $ return (ptext (sLit "Constraint solver steps =") <+> int count)
+         csTraceTcM 0 $ return (text "Constraint solver steps =" <+> int count)
 
 #ifdef DEBUG
-       ; ev_binds <- TcM.getTcEvBinds ev_binds_var
+       ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
        ; checkForCyclicBinds ev_binds
 #endif
 
        ; return res }
-  where
-    is = emptyInert
 
 #ifdef DEBUG
-checkForCyclicBinds :: Bag EvBind -> TcM ()
-checkForCyclicBinds ev_binds
+checkForCyclicBinds :: EvBindMap -> TcM ()
+checkForCyclicBinds ev_binds_map
   | null cycles
   = return ()
   | null coercion_cycles
@@ -1146,52 +2479,74 @@ 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 <- stronglyConnCompFromEdgedVertices edges]
+    cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
 
     coercion_cycles = [c | c <- cycles, any is_co_bind c]
-    is_co_bind (EvBind b _) = isEqVar b
+    is_co_bind (EvBind { eb_lhs = b }) = isEqPred (varType b)
 
     edges :: [(EvBind, EvVar, [EvVar])]
-    edges = [(bind, bndr, varSetElems (evVarsOfTerm rhs)) | bind@(EvBind bndr rhs) <- bagToList ev_binds]
+    edges = [ (bind, bndr, nonDetEltsUFM (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
+            -- if the edges are in nondeterministic order as explained in
+            -- Note [Deterministic SCC] in Digraph.
 #endif
 
-nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a
+setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
+setEvBindsTcS ref (TcS thing_inside)
+ = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
+
+nestImplicTcS :: EvBindsVar
+              -> TcLevel -> TcS a
+              -> TcS a
 nestImplicTcS ref inner_tclvl (TcS thing_inside)
-  = TcS $ \ TcSEnv { tcs_unified = unified_var
-                   , tcs_inerts = old_inert_var
-                   , tcs_count = count } ->
+  = TcS $ \ TcSEnv { tcs_unified       = unified_var
+                   , tcs_inerts        = old_inert_var
+                   , tcs_count         = count
+                   , tcs_need_deriveds = solve_deriveds
+                   } ->
     do { inerts <- TcM.readTcRef old_inert_var
-       ; let nest_inert = inerts { inert_flat_cache = emptyFunEqs }
-                                   -- See Note [Do not inherit the flat cache]
+       ; let nest_inert = inerts { inert_flat_cache = emptyExactFunEqs }
+                                     -- See Note [Do not inherit the flat cache]
        ; new_inert_var <- TcM.newTcRef nest_inert
        ; new_wl_var    <- TcM.newTcRef emptyWorkList
-       ; 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 }
+       ; 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_need_deriveds = solve_deriveds }
        ; res <- TcM.setTcLevel inner_tclvl $
                 thing_inside nest_env
 
 #ifdef DEBUG
        -- Perform a check that the thing_inside did not cause cycles
-       ; ev_binds <- TcM.getTcEvBinds ref
+       ; ev_binds <- TcM.getTcEvBindsMap ref
        ; checkForCyclicBinds ev_binds
 #endif
-
        ; return res }
 
-recoverTcS :: TcS a -> TcS a -> TcS a
-recoverTcS (TcS recovery_code) (TcS thing_inside)
-  = TcS $ \ env ->
-    TcM.recoverM (recovery_code env) (thing_inside env)
+{- Note [Do not inherit the flat cache]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We do not want to inherit the flat cache when processing nested
+implications.  Consider
+   a ~ F b, forall c. b~Int => blah
+If we have F b ~ fsk in the flat-cache, and we push that into the
+nested implication, we might miss that F b can be rewritten to F Int,
+and hence perhpas solve it.  Moreover, the fsk from outside is
+flattened out after solving the outer level, but and we don't
+do that flattening recursively.
+-}
 
 nestTcS ::  TcS a -> TcS a
 -- Use the current untouchables, augmenting the current
 -- evidence bindings, and solved dictionaries
 -- But have no effect on the InertCans, or on the inert_flat_cache
---  (the latter because the thing inside a nestTcS does unflattening)
+-- (we want to inherit the latter from processing the Givens)
 nestTcS (TcS thing_inside)
   = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
     do { inerts <- TcM.readTcRef inerts_var
@@ -1203,27 +2558,18 @@ nestTcS (TcS thing_inside)
        ; res <- thing_inside nest_env
 
        ; new_inerts <- TcM.readTcRef new_inert_var
+
+       -- we want to propogate the safe haskell failures
+       ; let old_ic = inert_cans inerts
+             new_ic = inert_cans new_inerts
+             nxt_ic = old_ic { inert_safehask = inert_safehask new_ic }
+
        ; TcM.writeTcRef inerts_var  -- See Note [Propagate the solved dictionaries]
-                        (inerts { inert_solved_dicts = inert_solved_dicts new_inerts })
+                        (inerts { inert_solved_dicts = inert_solved_dicts new_inerts
+                                , inert_cans = nxt_ic })
 
        ; return res }
 
-tryTcS :: TcS a -> TcS a
--- Like runTcS, but from within the TcS monad
--- Completely fresh inerts and worklist, be careful!
--- Moreover, we will simply throw away all the evidence generated.
-tryTcS (TcS thing_inside)
-  = TcS $ \env ->
-    do { is_var <- TcM.newTcRef emptyInert
-       ; unified_var <- TcM.newTcRef False
-       ; ev_binds_var <- TcM.newTcEvBinds
-       ; wl_var <- TcM.newTcRef emptyWorkList
-       ; let nest_env = env { tcs_ev_binds = ev_binds_var
-                            , tcs_unified  = unified_var
-                            , tcs_inerts   = is_var
-                            , tcs_worklist = wl_var }
-       ; thing_inside nest_env }
-
 {-
 Note [Propagate the solved dictionaries]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1232,7 +2578,7 @@ dictionaries from the thing_inside.
 Consider
    Eq [a]
    forall b. empty =>  Eq [a]
-We solve the flat (Eq [a]), under nestTcS, and then turn our attention to
+We solve the simple (Eq [a]), under nestTcS, and then turn our attention to
 the implications.  It's definitely fine to use the solved dictionaries on
 the inner implications, and it can make a signficant performance difference
 if you do so.
@@ -1267,29 +2613,26 @@ updWorkListTcS f
        ; let new_work = f wl_curr
        ; wrapTcS (TcM.writeTcRef wl_var new_work) }
 
-updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
--- Process the work list, returning a depleted work list,
--- plus a value extracted from it (typically a work item removed from it)
-updWorkListTcS_return f
-  = do { wl_var <- getTcSWorkListRef
-       ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
-       ; traceTcS "updWorkList" (ppr wl_curr)
-       ; let (res,new_work) = f wl_curr
-       ; wrapTcS (TcM.writeTcRef wl_var new_work)
-       ; return res }
+-- | Should we keep solving even only deriveds are left?
+keepSolvingDeriveds :: TcS Bool
+keepSolvingDeriveds = TcS (return . tcs_need_deriveds)
 
 emitWorkNC :: [CtEvidence] -> TcS ()
 emitWorkNC evs
   | null evs
   = return ()
   | otherwise
-  = do { traceTcS "Emitting fresh work" (vcat (map ppr evs))
-       ; updWorkListTcS (extendWorkListCts (map mkNonCanonical evs)) }
+  = emitWork (map mkNonCanonical evs)
+
+emitWork :: [Ct] -> TcS ()
+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)
+  = do { traceTcS "Emit insoluble" (ppr ct $$ pprCtLoc (ctLoc ct))
        ; updInertTcS add_insol }
   where
     this_pred = ctPred ct
@@ -1300,41 +2643,61 @@ emitInsoluble ct
         already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
              -- See Note [Do not add duplicate derived insolubles]
 
-getTcEvBinds :: TcS EvBindsVar
-getTcEvBinds = TcS (return . tcs_ev_binds)
+newTcRef :: a -> TcS (TcRef a)
+newTcRef x = wrapTcS (TcM.newTcRef x)
+
+readTcRef :: TcRef a -> TcS a
+readTcRef ref = wrapTcS (TcM.readTcRef ref)
+
+updTcRef :: TcRef a -> (a->a) -> TcS ()
+updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
+
+getTcEvBindsVar :: TcS EvBindsVar
+getTcEvBindsVar = TcS (return . tcs_ev_binds)
 
 getTcLevel :: TcS TcLevel
 getTcLevel = wrapTcS TcM.getTcLevel
 
+getTcEvBindsAndTCVs :: EvBindsVar -> TcS (EvBindMap, TyCoVarSet)
+getTcEvBindsAndTCVs ev_binds_var
+  = wrapTcS $ do { bnds <- TcM.getTcEvBindsMap ev_binds_var
+                 ; tcvs <- TcM.getTcEvTyCoVars ev_binds_var
+                 ; return (bnds, tcvs) }
+
 getTcEvBindsMap :: TcS EvBindMap
 getTcEvBindsMap
-  = do { EvBindsVar ev_ref _ <- getTcEvBinds
-       ; wrapTcS $ TcM.readTcRef ev_ref }
-
-setWantedTyBind :: TcTyVar -> TcType -> TcS ()
--- Add a type binding
--- We never do this twice!
-setWantedTyBind tv ty
-  | ASSERT2( isMetaTyVar tv, ppr tv )
-    isFmvTyVar tv
-  = ASSERT2( isMetaTyVar tv, ppr tv )
-    wrapTcS (TcM.writeMetaTyVar tv ty)
-           -- Write directly into the mutable tyvar
-           -- Flatten meta-vars are born and die locally
+  = do { ev_binds_var <- getTcEvBindsVar
+       ; wrapTcS $ TcM.getTcEvBindsMap ev_binds_var }
 
-  | otherwise
-  = TcS $ \ env ->
-    do { TcM.traceTc "setWantedTyBind" (ppr tv <+> text ":=" <+> ppr ty)
+unifyTyVar :: TcTyVar -> TcType -> TcS ()
+-- Unify a meta-tyvar with a type
+-- We keep track of how many unifications have happened in tcs_unified,
+--
+-- We should never unify the same variable twice!
+unifyTyVar tv ty
+  = ASSERT2( isMetaTyVar tv, ppr tv )
+    TcS $ \ env ->
+    do { TcM.traceTc "unifyTyVar" (ppr tv <+> text ":=" <+> ppr ty)
        ; TcM.writeMetaTyVar tv ty
-       ; TcM.writeTcRef (tcs_unified env) True }
+       ; 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 (Bool, a)
+reportUnifications :: TcS a -> TcS (Int, a)
 reportUnifications (TcS thing_inside)
   = TcS $ \ env ->
-    do { inner_unified <- TcM.newTcRef False
+    do { inner_unified <- TcM.newTcRef 0
        ; res <- thing_inside (env { tcs_unified = inner_unified })
-       ; dirty <- TcM.readTcRef inner_unified
-       ; return (dirty, res) }
+       ; n_unifs <- TcM.readTcRef inner_unified
+       ; TcM.updTcRef (tcs_unified env) (+ n_unifs)
+       ; return (n_unifs, res) }
 
 getDefaultInfo ::  TcS ([Type], (Bool, Bool))
 getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
@@ -1343,7 +2706,7 @@ getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 getInstEnvs :: TcS InstEnvs
-getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs
+getInstEnvs = wrapTcS $ TcM.tcGetInstEnvs
 
 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
@@ -1354,22 +2717,28 @@ getTopEnv = wrapTcS $ TcM.getTopEnv
 getGblEnv :: TcS TcGblEnv
 getGblEnv = wrapTcS $ TcM.getGblEnv
 
+getLclEnv :: TcS TcLclEnv
+getLclEnv = wrapTcS $ TcM.getLclEnv
+
+tcLookupClass :: Name -> TcS Class
+tcLookupClass c = wrapTcS $ TcM.tcLookupClass c
+
 -- 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
-addUsedRdrNamesTcS :: [RdrName] -> TcS ()
-addUsedRdrNamesTcS names = wrapTcS  $ addUsedRdrNames names
+addUsedGREs :: [GlobalRdrElt] -> TcS ()
+addUsedGREs gres = wrapTcS  $ TcM.addUsedGREs gres
 
 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
 checkWellStagedDFun pred dfun_id loc
-  = wrapTcS $ TcM.setCtLoc loc $
+  = wrapTcS $ TcM.setCtLocM loc $
     do { use_stage <- TcM.getStage
        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
   where
-    pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
+    pp_thing = text "instance for" <+> quotes (ppr pred)
     bind_lvl = TcM.topIdLvl dfun_id
 
 pprEq :: TcType -> TcType -> SDoc
@@ -1382,8 +2751,7 @@ isTouchableMetaTyVarTcS tv
 
 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
 isFilledMetaTyVar_maybe tv
- = ASSERT2( isTcTyVar tv, ppr tv )
-   case tcTyVarDetails tv of
+ = case tcTyVarDetails tv of
      MetaTv { mtv_ref = ref }
         -> do { cts <- wrapTcS (TcM.readTcRef ref)
               ; case cts of
@@ -1394,17 +2762,29 @@ isFilledMetaTyVar_maybe tv
 isFilledMetaTyVar :: TcTyVar -> TcS Bool
 isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
 
-zonkTyVarsAndFV :: TcTyVarSet -> TcS TcTyVarSet
-zonkTyVarsAndFV tvs = wrapTcS (TcM.zonkTyVarsAndFV tvs)
+zonkTyCoVarsAndFV :: TcTyCoVarSet -> TcS TcTyCoVarSet
+zonkTyCoVarsAndFV tvs = wrapTcS (TcM.zonkTyCoVarsAndFV tvs)
+
+zonkTyCoVarsAndFVList :: [TcTyCoVar] -> TcS [TcTyCoVar]
+zonkTyCoVarsAndFVList tvs = wrapTcS (TcM.zonkTyCoVarsAndFVList tvs)
+
+zonkCo :: Coercion -> TcS Coercion
+zonkCo = wrapTcS . TcM.zonkCo
 
 zonkTcType :: TcType -> TcS TcType
 zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
 
+zonkTcTypes :: [TcType] -> TcS [TcType]
+zonkTcTypes tys = wrapTcS (TcM.zonkTcTypes tys)
+
 zonkTcTyVar :: TcTyVar -> TcS TcType
 zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
 
-zonkFlats :: Cts -> TcS Cts
-zonkFlats cts = wrapTcS (TcM.zonkFlats cts)
+zonkSimples :: Cts -> TcS Cts
+zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
+
+zonkWC :: WantedConstraints -> TcS WantedConstraints
+zonkWC wc = wrapTcS (TcM.zonkWC wc)
 
 {-
 Note [Do not add duplicate derived insolubles]
@@ -1416,7 +2796,7 @@ sites.  Not only do we want an error message for each, but with
 *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 sucessively rewritten.
+    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.
@@ -1436,11 +2816,11 @@ Example of (b): assume a top-level class and instance declaration:
 
 Assume we have started with an implication:
 
-  forall c. Eq c => { wc_flat = D [c] c [W] }
+  forall c. Eq c => { wc_simple = D [c] c [W] }
 
 which we have simplified to:
 
-  forall c. Eq c => { wc_flat = D [c] c [W]
+  forall c. Eq c => { wc_simple = D [c] c [W]
                     , wc_insols = (c ~ [c]) [D] }
 
 For some reason, e.g. because we floated an equality somewhere else,
@@ -1453,67 +2833,49 @@ constraints the second time:
 
 which will result in two Deriveds to end up in the insoluble set:
 
-  wc_flat   = D [c] c [W]
+  wc_simple   = D [c] c [W]
   wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
 -}
 
 -- Flatten skolems
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-newFlattenSkolem :: CtEvidence -> TcType         -- F xis
-                 -> TcS (CtEvidence, TcTyVar)    -- [W] x:: F xis ~ fsk
-newFlattenSkolem ctxt_ev fam_ty
-  | isGiven ctxt_ev   -- Make a given
-  =  do { fsk <- wrapTcS $
-                 do { uniq <- TcM.newUnique
-                    ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk")
-                    ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
-        ; let ev = CtGiven { ctev_pred = mkTcEqPred fam_ty (mkTyVarTy fsk)
-                           , ctev_evtm = EvCoercion (mkTcNomReflCo fam_ty)
-                           , ctev_loc  = loc }
-        ; return (ev, fsk) }
-
-  | otherwise        -- Make a wanted
-  = do { fuv <- wrapTcS $
-                 do { uniq <- TcM.newUnique
-                    ; ref  <- TcM.newMutVar Flexi
-                    ; let details = MetaTv { mtv_info  = FlatMetaTv
-                                           , mtv_ref   = ref
-                                           , mtv_tclvl = fskTcLevel }
-                          name = TcM.mkTcTyVarName uniq (fsLit "s")
-                    ; return (mkTcTyVar name (typeKind fam_ty) details) }
-       ; ev <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fuv))
-       ; return (ev, fuv) }
-  where
-    loc = ctEvLoc ctxt_ev
-
-extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcTyVar) -> TcS ()
-extendFlatCache tc xi_args (co, fsk)
+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)
+
+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 = insertFunEq fc tc xi_args (co, fsk) } }
+            is { inert_flat_cache = insertExactFunEq fc tc xi_args stuff } }
 
 -- Instantiations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcType)
-instDFunType dfun_id mb_inst_tys
-  = wrapTcS $ go dfun_tvs mb_inst_tys (mkTopTvSubst [])
-  where
-    (dfun_tvs, dfun_phi) = tcSplitForAllTys (idType dfun_id)
-
-    go :: [TyVar] -> [DFunInstType] -> TvSubst -> TcM ([TcType], TcType)
-    go [] [] subst = return ([], substTy subst dfun_phi)
-    go (tv:tvs) (Just ty : mb_tys) subst
-      = do { (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
-           ; return (ty : tys, phi) }
-    go (tv:tvs) (Nothing : mb_tys) subst
-      = do { ty <- instFlexiTcSHelper (tyVarName tv) (substTy subst (tyVarKind tv))
-                         -- Don't forget to instantiate the kind!
-                         -- cf TcMType.tcInstTyVarX
-           ; (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
-           ; return (ty : tys, phi) }
-    go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr mb_inst_tys)
+instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
+instDFunType dfun_id inst_tys
+  = wrapTcS $ TcM.instDFunType dfun_id inst_tys
 
 newFlexiTcSTy :: Kind -> TcS TcType
 newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
@@ -1530,45 +2892,82 @@ demoteUnfilledFmv fmv
                    do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
                       ; TcM.writeMetaTyVar fmv tv_ty } }
 
-instFlexiTcS :: [TKVar] -> TcS (TvSubst, [TcType])
-instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTvSubst tvs)
+instFlexiTcS :: [TKVar] -> TcS (TCvSubst, [TcType])
+instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTCvSubst tvs)
   where
      inst_one subst tv
          = do { ty' <- instFlexiTcSHelper (tyVarName tv)
-                                          (substTy subst (tyVarKind tv))
+                                          (substTyUnchecked subst (tyVarKind tv))
               ; return (extendTvSubst subst tv ty', ty') }
 
 instFlexiTcSHelper :: Name -> Kind -> TcM TcType
 instFlexiTcSHelper tvname kind
   = do { uniq <- TcM.newUnique
-       ; details <- TcM.newMetaDetails (TauTv False)
+       ; details <- TcM.newMetaDetails TauTv
        ; let name = setNameUnique tvname uniq
        ; return (mkTyVarTy (mkTcTyVar name kind details)) }
 
-instFlexiTcSHelperTcS :: Name -> Kind -> TcS TcType
-instFlexiTcSHelperTcS n k = wrapTcS (instFlexiTcSHelper n k)
 
 
 -- Creating and setting evidence variables and CtFlavors
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-data XEvTerm
-  = XEvTerm { ev_preds  :: [PredType]           -- New predicate types
-            , ev_comp   :: [EvTerm] -> EvTerm   -- How to compose evidence
-            , ev_decomp :: EvTerm -> [EvTerm]   -- How to decompose evidence
-            -- In both ev_comp and ev_decomp, the [EvTerm] is 1-1 with ev_preds
-            -- and each EvTerm has type of the corresponding EvPred
-            }
-
-data Freshness = Fresh | Cached
-
-freshGoals :: [(CtEvidence, Freshness)] -> [CtEvidence]
-freshGoals mns = [ ctev | (ctev, Fresh) <- mns ]
-
-setEvBind :: EvVar -> EvTerm -> TcS ()
-setEvBind the_ev tm
-  = do { tc_evbinds <- getTcEvBinds
-       ; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev tm }
+data MaybeNew = Fresh CtEvidence | Cached EvTerm
+
+isFresh :: MaybeNew -> Bool
+isFresh (Fresh {})  = True
+isFresh (Cached {}) = False
+
+freshGoals :: [MaybeNew] -> [CtEvidence]
+freshGoals mns = [ ctev | Fresh ctev <- mns ]
+
+getEvTerm :: MaybeNew -> EvTerm
+getEvTerm (Fresh ctev) = ctEvTerm ctev
+getEvTerm (Cached evt) = evt
+
+setEvBind :: EvBind -> TcS ()
+setEvBind ev_bind
+  = do { evb <- getTcEvBindsVar
+       ; wrapTcS $ TcM.addTcEvBind evb ev_bind }
+
+-- | Mark variables as used filling a coercion hole
+useVars :: TyCoVarSet -> TcS ()
+useVars vars
+  = do { EvBindsVar { ebv_tcvs = ref } <- getTcEvBindsVar
+       ; wrapTcS $
+         do { tcvs <- TcM.readTcRef ref
+            ; let tcvs' = tcvs `unionVarSet` vars
+            ; TcM.writeTcRef ref tcvs' } }
+
+-- | Equalities only
+setWantedEq :: TcEvDest -> Coercion -> TcS ()
+setWantedEq (HoleDest hole) co
+  = do { useVars (tyCoVarsOfCo 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
+setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
+setWantedEvTerm (HoleDest hole) tm
+  = do { let co = evTermCoercion tm
+       ; useVars (tyCoVarsOfCo co)
+       ; wrapTcS $ TcM.fillCoercionHole hole co }
+setWantedEvTerm (EvVarDest ev) tm = setWantedEvBind ev tm
+
+setWantedEvBind :: EvVar -> EvTerm -> TcS ()
+setWantedEvBind 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 ()
 
 newTcEvBinds :: TcS EvBindsVar
 newTcEvBinds = wrapTcS TcM.newTcEvBinds
@@ -1580,354 +2979,122 @@ 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
 newGivenEvVar loc (pred, rhs)
+  = do { new_ev <- newBoundEvVarId pred rhs
+       ; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) }
+
+-- | Make a new 'Id' of the given type, bound (in the monad's EvBinds) to the
+-- given term
+newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar
+newBoundEvVarId pred rhs
   = do { new_ev <- newEvVar pred
-       ; setEvBind new_ev rhs
-       ; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev, ctev_loc = loc }) }
+       ; setEvBind (mkGivenEvBind new_ev rhs)
+       ; return new_ev }
+
+newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
+newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
+
+-- | Make a new equality CtEvidence
+newWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion)
+newWantedEq loc role ty1 ty2
+  = do { hole <- wrapTcS $ TcM.newCoercionHole
+       ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
+       ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
+                           , ctev_loc = loc}
+                , mkHoleCo hole role ty1 ty2 ) }
+  where
+    pty = mkPrimEqPredRole role ty1 ty2
 
+-- no equalities here. Use newWantedEqNC instead
 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
 -- Don't look up in the solved/inerts; we know it's not there
 newWantedEvVarNC loc pty
-  = do { new_ev <- newEvVar pty
-       ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
-
-newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
+  = do { -- checkReductionDepth loc pty
+       ; 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_loc = loc })}
+
+newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
+-- For anything except ClassPred, this is the same as newWantedEvVarNC
 newWantedEvVar loc pty
-  = do { mb_ct <- lookupInInerts loc pty
+  = do { mb_ct <- lookupInInerts pty
        ; case mb_ct of
-            Just ctev | not (isDerived ctev)
-                      -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
-                            ; return (ctev, Cached) }
+            Just ctev
+              | not (isDerived ctev)
+              -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
+                    ; return $ Cached (ctEvTerm ctev) }
             _ -> do { ctev <- newWantedEvVarNC loc pty
-                    ; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
-                    ; return (ctev, Fresh) } }
-
-emitNewDerivedEq :: CtLoc -> Pair TcType -> TcS ()
--- Create new Derived and put it in the work list
-emitNewDerivedEq loc (Pair ty1 ty2)
-  | ty1 `tcEqType` ty2   -- Quite common!
-  = return ()
+                    ; 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
+  | Just (role, ty1, ty2) <- getEqPredTys_maybe pty
+  = Fresh . fst <$> newWantedEq loc role ty1 ty2
   | otherwise
-  = emitNewDerived loc (mkTcEqPred ty1 ty2)
+  = newWantedEvVar loc pty
 
 emitNewDerived :: CtLoc -> TcPredType -> TcS ()
--- Create new Derived and put it in the work list
 emitNewDerived loc pred
-  = do { mb_ev <- newDerived loc pred
-       ; case mb_ev of
-           Nothing -> return ()
-           Just ev -> do { traceTcS "Emitting [D]" (ppr ev)
-                         ; updWorkListTcS (extendWorkListCt (mkNonCanonical ev)) } }
-
-newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
--- Returns Nothing    if cached,
---         Just pred  if not cached
-newDerived loc pred
-  = do { mb_ct <- lookupInInerts loc pred
-       ; return (case mb_ct of
-                    Just {} -> Nothing
-                    Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
-
-instDFunConstraints :: CtLoc -> TcThetaType -> TcS [(CtEvidence, Freshness)]
-instDFunConstraints loc = mapM (newWantedEvVar loc)
-
-{-
-Note [xCtEvidence]
-~~~~~~~~~~~~~~~~~~
-A call might look like this:
-
-    xCtEvidence ev evidence-transformer
-
-  ev is Given   => use ev_decomp to create new Givens for ev_preds,
-                   and return them
-
-  ev is Wanted  => create new wanteds for ev_preds,
-                   use ev_comp to bind ev,
-                   return fresh wanteds (ie ones not cached in inert_cans or solved)
-
-  ev is Derived => create new deriveds for ev_preds
-                      (unless cached in inert_cans or solved)
-
-Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
-      Ones that are already cached are not returned
-
-Example
-    ev : Tree a b ~ Tree c d
-    xCtEvidence ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. <Tree> c1 c2
-                                       , ev_decomp = \c. [nth 1 c, nth 2 c] })
-              (\fresh-goals.  stuff)
-
-Note [Bind new Givens immediately]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For Givens we make new EvVars and bind them immediately. We don't worry
-about caching, but we don't expect complicated calculations among Givens.
-It is important to bind each given:
-      class (a~b) => C a b where ....
-      f :: C a b => ....
-Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
-But that superclass selector can't (yet) appear in a coercion
-(see evTermCoercion), so the easy thing is to bind it to an Id.
-
-See Note [Coercion evidence terms] in TcEvidence.
-
-Note [Do not create Given kind equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We do not want to create a Given kind equality like
-
-   [G]  kv ~ k   -- kv is a skolem kind variable
-                 -- Reason we don't yet support non-Refl kind equalities
-
-This showed up in Trac #8566, where we had a data type
-   data I (u :: U *) (r :: [*]) :: * where
-        A :: I (AA t as) r                  -- Existential k
-so A has type
-   A :: forall (u:U *) (r:[*])                  Universal
-        (k:BOX) (t:k) (as:[U *]).        Existential
-        (u ~ AA * k t as) => I u r
-
-There is no direct kind equality, but in a pattern match where 'u' is
-instantiated to, say, (AA * kk (t1:kk) as1), we'd decompose to get
-   k ~ kk, t ~ t1, as ~ as1
-This is bad.  We "fix" this by simply ignoring the Given kind equality
-But the Right Thing is to add kind equalities!
-
-But note (Trac #8705) that we *do* create Given (non-canonical) equalities
-with un-equal kinds, e.g.
-   [G]  t1::k1 ~ t2::k2   -- k1 and k2 are un-equal kinds
-Reason: k1 or k2 might be unification variables that have already been
-unified (at this point we have not canonicalised the types), so we want
-to emit this t1~t2 as a (non-canonical) Given in the work-list. If k1/k2
-have been unified, we'll find that when we canonicalise it, and the
-t1~t2 information may be crucial (Trac #8705 is an example).
-
-If it turns out that k1 and k2 are really un-equal, then it'll end up
-as an Irreducible (see Note [Equalities with incompatible kinds] in
-TcCanonical), and will do no harm.
--}
-
-xCtEvidence :: CtEvidence            -- Original evidence
-            -> XEvTerm               -- Instructions about how to manipulate evidence
-            -> TcS ()
-
-xCtEvidence (CtWanted { ctev_evar = evar, ctev_loc = loc })
-            (XEvTerm { ev_preds = ptys, ev_comp = comp_fn })
-  = do { new_evars <- mapM (newWantedEvVar loc) ptys
-       ; setEvBind evar (comp_fn (map (ctEvTerm . fst) new_evars))
-       ; emitWorkNC (freshGoals new_evars) }
-         -- Note the "NC": these are fresh goals, not necessarily canonical
-
-xCtEvidence (CtGiven { ctev_evtm = tm, ctev_loc = loc })
-            (XEvTerm { ev_preds = ptys, ev_decomp = decomp_fn })
-  = ASSERT( equalLength ptys (decomp_fn tm) )
-    do { given_evs <- mapM (newGivenEvVar loc) $    -- See Note [Bind new Givens immediately]
-                      filterOut bad_given_pred (ptys `zip` decomp_fn tm)
-       ; emitWorkNC given_evs }
-  where
-    -- See Note [Do not create Given kind equalities]
-    bad_given_pred (pred_ty, _)
-      | EqPred t1 _ <- classifyPredType pred_ty
-      = isKind t1
-      | otherwise
-      = False
-
-xCtEvidence (CtDerived { ctev_loc = loc })
-            (XEvTerm { ev_preds = ptys })
-  = mapM_ (emitNewDerived loc) ptys
-
------------------------------
-data StopOrContinue a
-  = ContinueWith a    -- The constraint was not solved, although it may have
-                      --   been rewritten
-
-  | Stop CtEvidence   -- The (rewritten) constraint was solved
-         SDoc         -- Tells how it was solved
-                      -- Any new sub-goals have been put on the work list
-
-instance Functor StopOrContinue where
-  fmap f (ContinueWith x) = ContinueWith (f x)
-  fmap _ (Stop ev s)      = Stop ev s
-
-instance Outputable a => Outputable (StopOrContinue a) where
-  ppr (Stop ev s)      = ptext (sLit "Stop") <> parens s <+> ppr ev
-  ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
-
-continueWith :: a -> TcS (StopOrContinue a)
-continueWith = return . ContinueWith
-
-stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
-stopWith ev s = return (Stop ev (text s))
-
-andWhenContinue :: TcS (StopOrContinue a)
-                -> (a -> TcS (StopOrContinue b))
-                -> TcS (StopOrContinue b)
-andWhenContinue tcs1 tcs2
-  = do { r <- tcs1
-       ; case r of
-           Stop ev s       -> return (Stop ev s)
-           ContinueWith ct -> tcs2 ct }
-
-rewriteEvidence :: CtEvidence   -- old evidence
-                -> TcPredType   -- new predicate
-                -> TcCoercion   -- Of type :: new predicate ~ <type of old evidence>
-                -> TcS (StopOrContinue CtEvidence)
--- Returns Just new_ev iff either (i)  'co' is reflexivity
---                             or (ii) 'co' is not reflexivity, and 'new_pred' not cached
--- In either case, there is nothing new to do with new_ev
-{-
-     rewriteEvidence old_ev new_pred co
-Main purpose: create new evidence for new_pred;
-              unless new_pred is cached already
-* Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
-* If old_ev was wanted, create a binding for old_ev, in terms of new_ev
-* If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
-* Returns Nothing if new_ev is already cached
-
-        Old evidence    New predicate is               Return new evidence
-        flavour                                        of same flavor
-        -------------------------------------------------------------------
-        Wanted          Already solved or in inert     Nothing
-        or Derived      Not                            Just new_evidence
-
-        Given           Already in inert               Nothing
-                        Not                            Just new_evidence
-
-Note [Rewriting with Refl]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-If the coercion is just reflexivity then you may re-use the same
-variable.  But be careful!  Although the coercion is Refl, new_pred
-may reflect the result of unification alpha := ty, so new_pred might
-not _look_ the same as old_pred, and it's vital to proceed from now on
-using new_pred.
-
-The flattener preserves type synonyms, so they should appear in new_pred
-as well as in old_pred; that is important for good error messages.
- -}
-
-
-rewriteEvidence old_ev@(CtDerived { ctev_loc = loc }) new_pred _co
-  = -- If derived, don't even look at the coercion.
-    -- This is very important, DO NOT re-order the equations for
-    -- rewriteEvidence to put the isTcReflCo test first!
-    -- Why?  Because for *Derived* constraints, c, the coercion, which
-    -- was produced by flattening, may contain suspended calls to
-    -- (ctEvTerm c), which fails for Derived constraints.
-    -- (Getting this wrong caused Trac #7384.)
-    do { mb_ev <- newDerived loc new_pred
-       ; case mb_ev of
-           Just new_ev -> continueWith new_ev
-           Nothing     -> stopWith old_ev "Cached derived" }
-
-rewriteEvidence old_ev new_pred co
-  | isTcReflCo co -- See Note [Rewriting with Refl]
-  = return (ContinueWith (old_ev { ctev_pred = new_pred }))
-
-rewriteEvidence (CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co
-  = do { new_ev <- newGivenEvVar loc (new_pred, new_tm)  -- See Note [Bind new Givens immediately]
-       ; return (ContinueWith new_ev) }
-  where
-    new_tm = mkEvCast old_tm (mkTcSubCo (mkTcSymCo co))  -- mkEvCast optimises ReflCo
-
-rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
-  = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
-       ; MASSERT( tcCoercionRole co == Nominal )
-       ; setEvBind evar (mkEvCast (ctEvTerm new_ev) (mkTcSubCo co))
-       ; case freshness of
-            Fresh  -> continueWith new_ev
-            Cached -> stopWith ev "Cached wanted" }
-
-
-rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swapped)
-                                        --              or orhs ~ olhs (swapped)
-                  -> SwapFlag
-                  -> TcType -> TcType   -- New predicate  nlhs ~ nrhs
-                                        -- Should be zonked, because we use typeKind on nlhs/nrhs
-                  -> TcCoercion         -- lhs_co, of type :: nlhs ~ olhs
-                  -> TcCoercion         -- rhs_co, of type :: nrhs ~ orhs
-                  -> TcS (StopOrContinue CtEvidence)  -- Of type nlhs ~ nrhs
--- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
--- we generate
--- If not swapped
---      g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
--- If 'swapped'
---      g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
---
--- For (Wanted w) we do the dual thing.
--- New  w1 : nlhs ~ nrhs
--- If not swapped
---      w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
--- If swapped
---      w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
---
--- It's all a form of rewwriteEvidence, specialised for equalities
-rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
-  | CtDerived { ctev_loc = loc } <- old_ev
-  = do { mb <- newDerived loc (mkTcEqPred nlhs nrhs)
-       ; case mb of
-           Just new_ev -> continueWith new_ev
-           Nothing     -> stopWith old_ev "Cached derived" }
-
-  | NotSwapped <- swapped
-  , isTcReflCo lhs_co      -- See Note [Rewriting with Refl]
-  , isTcReflCo rhs_co
-  = return (ContinueWith (old_ev { ctev_pred = new_pred }))
-
-  | CtGiven { ctev_evtm = old_tm , ctev_loc = loc } <- old_ev
-  = do { let new_tm = EvCoercion (lhs_co
-                                  `mkTcTransCo` maybeSym swapped (evTermCoercion old_tm)
-                                  `mkTcTransCo` mkTcSymCo rhs_co)
-       ; new_ev <- newGivenEvVar loc (new_pred, new_tm)  -- See Note [Bind new Givens immediately]
-       ; return (ContinueWith new_ev) }
-
-  | CtWanted { ctev_evar = evar, ctev_loc = loc } <- old_ev
-  = do { new_evar <- newWantedEvVarNC loc new_pred
-                     -- Not much point in seeking exact-match equality evidence
-       ; let co = maybeSym swapped $
-                  mkTcSymCo lhs_co
-                  `mkTcTransCo` ctEvCoercion new_evar
-                  `mkTcTransCo` rhs_co
-       ; setEvBind evar (EvCoercion co)
-       ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
-       ; return (ContinueWith new_evar) }
+  = do { ev <- newDerivedNC loc pred
+       ; traceTcS "Emitting new derived" (ppr ev)
+       ; updWorkListTcS (extendWorkListDerived loc ev) }
 
+emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
+emitNewDeriveds loc preds
+  | null preds
+  = return ()
   | otherwise
-  = panic "rewriteEvidence"
-  where
-    new_pred = mkTcEqPred nlhs nrhs
+  = do { evs <- mapM (newDerivedNC loc) preds
+       ; traceTcS "Emitting new deriveds" (ppr evs)
+       ; updWorkListTcS (extendWorkListDeriveds loc evs) }
+
+emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS ()
+-- Create new equality Derived and put it in the work list
+-- There's no caching, no lookupInInerts
+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) }
+
+newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
+newDerivedNC loc pred
+  = do { -- checkReductionDepth loc pred
+       ; return (CtDerived { ctev_pred = pred, ctev_loc = loc }) }
+
+-- --------- Check done in TcInteract.selectNewWorkItem???? ---------
+-- | Checks if the depth of the given location is too much. Fails if
+-- it's too big, with an appropriate error message.
+checkReductionDepth :: CtLoc -> TcType   -- ^ type being reduced
+                    -> TcS ()
+checkReductionDepth loc ty
+  = do { dflags <- getDynFlags
+       ; when (subGoalDepthExceeded dflags (ctLocDepth loc)) $
+         wrapErrTcS $
+         solverDepthErrorTcS loc ty }
 
-maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
-maybeSym IsSwapped  co = mkTcSymCo co
-maybeSym NotSwapped co = co
+matchFam :: TyCon -> [Type] -> TcS (Maybe (Coercion, TcType))
+matchFam tycon args = wrapTcS $ matchFamTcM tycon args
 
-matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
+matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (Coercion, TcType))
 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
-matchFam tycon args
-  | isOpenTypeFamilyTyCon tycon
-  = do { fam_envs <- getFamInstEnvs
-       ; let mb_match = tcLookupFamInst fam_envs tycon args
-       ; traceTcS "lookupFamInst" $
-                  vcat [ ppr tycon <+> ppr args
-                       , pprTvBndrs (varSetElems (tyVarsOfTypes args))
-                       , ppr mb_match ]
-       ; case mb_match of
-           Nothing -> return Nothing
-           Just (FamInstMatch { fim_instance = famInst
-                              , fim_tys      = inst_tys })
-             -> let co = mkTcUnbranchedAxInstCo Nominal (famInstAxiom famInst) inst_tys
-                    ty = pSnd $ tcCoercionKind co
-                in return $ Just (co, ty) }
-
-  | Just ax <- isClosedSynFamilyTyCon_maybe tycon
-  , Just (ind, inst_tys) <- chooseBranch ax args
-  = let co = mkTcAxInstCo Nominal ax ind inst_tys
-        ty = pSnd (tcCoercionKind co)
-    in return $ Just (co, ty)
-
-  | Just ops <- isBuiltInSynFamTyCon_maybe tycon =
-    return $ do (r,ts,ty) <- sfMatchFam ops args
-                return (mkTcAxiomRuleCo r ts [], ty)
-
-  | otherwise
-  = return Nothing
+matchFamTcM tycon args
+  = 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)
+              , ppr_res match_fam_result ]
+       ; return match_fam_result }
+  where
+    ppr_res Nothing        = text "Match failed"
+    ppr_res (Just (co,ty)) = hang (text "Match succeeded:")
+                                2 (vcat [ text "Rewrites to:" <+> ppr ty
+                                        , text "Coercion:" <+> ppr co ])
 
 {-
 Note [Residual implications]
@@ -1946,43 +3113,41 @@ See TcSMonad.deferTcSForAllEq
 
 deferTcSForAllEq :: Role -- Nominal or Representational
                  -> CtLoc  -- Original wanted equality flavor
-                 -> ([TyVar],TcType)   -- ForAll tvs1 body1
-                 -> ([TyVar],TcType)   -- ForAll tvs2 body2
-                 -> TcS EvTerm
--- Some of this functionality is repeated from TcUnify,
--- consider having a single place where we create fresh implications.
-deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
- = do { (subst1, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
-      ; let tys  = mkTyVarTys skol_tvs
-            phi1 = Type.substTy subst1 body1
-            phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
-            skol_info = UnifyForAllSkol skol_tvs phi1
-            eq_pred   = case role of
-                          Nominal ->          mkTcEqPred      phi1 phi2
-                          Representational -> mkCoerciblePred phi1 phi2
-                          Phantom ->          panic "deferTcSForAllEq Phantom"
-        ; (ctev, freshness) <- newWantedEvVar loc eq_pred
-        ; coe_inside <- case freshness of
-            Cached -> return (ctEvCoercion ctev)
-            Fresh  -> do { ev_binds_var <- newTcEvBinds
-                         ; env <- wrapTcS $ TcM.getLclEnv
-                         ; let ev_binds = TcEvBinds ev_binds_var
-                               new_ct = mkNonCanonical ctev
-                               new_co = ctEvCoercion ctev
-                               new_tclvl = pushTcLevel (tcl_tclvl env)
-                         ; let wc = WC { wc_flat  = singleCt new_ct
-                                       , 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_insol  = False
-                                            , ic_binds  = ev_binds_var
-                                            , ic_env    = env
-                                            , ic_info   = skol_info }
-                         ; updWorkListTcS (extendWorkListImplic imp)
-                         ; return (TcLetCo ev_binds new_co) }
-
-        ; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) }
+                 -> [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
+      ; ev_binds <- newTcEvBinds
+           -- We have nowhere to put these bindings
+           -- but TcSimplify.setImplicationStatus
+           -- checks that we don't actually use them
+      ; 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  = ev_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