A collection of type-inference refactorings.
[ghc.git] / compiler / typecheck / TcSMonad.hs
index 7f2dd66..0174b4a 100644 (file)
@@ -6,16 +6,19 @@ module TcSMonad (
     -- The work list
     WorkList(..), isEmptyWorkList, emptyWorkList,
     extendWorkListNonEq, extendWorkListCt, extendWorkListDerived,
-    extendWorkListCts, extendWorkListEq, appendWorkList,
+    extendWorkListCts, extendWorkListEq, extendWorkListFunEq,
+    appendWorkList,
     selectNextWorkItem,
     workListSize, workListWantedCount,
-    updWorkListTcS,
+    getWorkList, updWorkListTcS,
 
     -- The TcS monad
-    TcS, runTcS, runTcSWithEvBinds,
-    failTcS, tryTcS, nestTcS, nestImplicTcS, recoverTcS,
+    TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
+    failTcS, warnTcS, addErrTcS,
+    runTcSEqualities,
+    nestTcS, nestImplicTcS, setEvBindsTcS,
 
-    runTcPluginTcS, addUsedDataCons, deferTcSForAllEq,
+    runTcPluginTcS, addUsedGREs, deferTcSForAllEq,
 
     -- Tracing etc
     panicTcS, traceTcS,
@@ -23,18 +26,23 @@ module TcSMonad (
     wrapErrTcS, wrapWarnTcS,
 
     -- Evidence creation and transformation
-    Freshness(..), freshGoals, isFresh,
+    MaybeNew(..), freshGoals, isFresh, getEvTerm,
 
-    newTcEvBinds, newWantedEvVar, newWantedEvVarNC, newDerivedNC,
+    newTcEvBinds,
+    newWantedEq,
+    newWanted, newWantedEvVar, newWantedEvVarNC, newDerivedNC,
+    newBoundEvVarId,
     unifyTyVar, unflattenFmv, reportUnifications,
-    setEvBind, setWantedEvBind, setEvBindIfWanted,
+    setEvBind, setWantedEq, setEqIfWanted,
+    setWantedEvTerm, setWantedEvBind, setEvBindIfWanted,
     newEvVar, newGivenEvVar, newGivenEvVars,
     emitNewDerived, emitNewDeriveds, emitNewDerivedEq,
     checkReductionDepth,
 
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
-    getTopEnv, getGblEnv, getLclEnv, getTcEvBinds, getTcLevel,
-    getTcEvBindsMap,
+    getTopEnv, getGblEnv, getLclEnv,
+    getTcEvBindsVar, getTcLevel,
+    getTcEvBindsAndTCVs, getTcEvBindsMap,
     tcLookupClass,
 
     -- Inerts
@@ -45,9 +53,9 @@ module TcSMonad (
     emptyInert, getTcSInerts, setTcSInerts, takeGivenInsolubles,
     matchableGivens, prohibitedSuperClassSolve,
     getUnsolvedInerts,
-    removeInertCts,
+    removeInertCts, getPendingScDicts,
     addInertCan, addInertEq, insertFunEq,
-    emitInsoluble, emitWorkNC, emitWorkCt,
+    emitInsoluble, emitWorkNC, emitWork,
 
     -- The Model
     InertModel, kickOutAfterUnification,
@@ -58,7 +66,7 @@ module TcSMonad (
 
     -- Inert CDictCans
     lookupInertDict, findDictsByClass, addDict, addDictsByClass,
-    delDict, partitionDicts, foldDicts, filterDicts,
+    delDict, foldDicts, filterDicts,
 
     -- Inert CTyEqCans
     EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
@@ -73,18 +81,20 @@ module TcSMonad (
     lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems
 
     -- Inert CFunEqCans
-    updInertFunEqs, findFunEq, sizeFunEqMap, filterFunEqs,
-    findFunEqsByTyCon, findFunEqs, partitionFunEqs, foldFunEqs,
+    updInertFunEqs, findFunEq, sizeFunEqMap,
+    findFunEqsByTyCon,
 
     instDFunType,                              -- Instantiation
 
     -- MetaTyVars
-    newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
+    newFlexiTcSTy, instFlexiTcS,
     cloneMetaTyVar, demoteUnfilledFmv,
 
     TcLevel, isTouchableMetaTyVarTcS,
     isFilledMetaTyVar_maybe, isFilledMetaTyVar,
-    zonkTyVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkSimples, zonkWC,
+    zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
+    zonkTyCoVarsAndFVList,
+    zonkSimples, zonkWC,
 
     -- References
     newTcRef, readTcRef, updTcRef,
@@ -117,6 +127,7 @@ import Kind
 import TcType
 import DynFlags
 import Type
+import Coercion
 import Unify
 
 import TcEvidence
@@ -125,7 +136,7 @@ import TyCon
 import TcErrors   ( solverDepthErrorTcS )
 
 import Name
-import RdrName ( GlobalRdrEnv)
+import RdrName ( GlobalRdrEnv, GlobalRdrElt )
 import qualified RnEnv as TcM
 import Var
 import VarEnv
@@ -133,17 +144,17 @@ import VarSet
 import Outputable
 import Bag
 import UniqSupply
-import FastString
 import Util
 import TcRnTypes
 
 import Unique
 import UniqFM
-import Maybes ( orElse, firstJusts )
+import UniqDFM
+import Maybes
 
+import StaticFlags( opt_PprStyle_Debug )
 import TrieMap
-import Control.Arrow ( first )
-import Control.Monad( ap, when, unless, MonadPlus(..) )
+import Control.Monad
 #if __GLASGOW_HASKELL__ > 710
 import qualified Control.Monad.Fail as MonadFail
 #endif
@@ -236,7 +247,7 @@ extendWorkListDerived loc 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
+  | otherwise                 = extendWorkListEqs (map mkNonCanonical evs) wl
 
 extendWorkListImplic :: Implication -> WorkList -> WorkList
 extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl }
@@ -275,6 +286,10 @@ selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs
   | 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 })
@@ -297,7 +312,8 @@ selectNextWorkItem
        ; try (selectWorkItem wl) $
 
     do { ics <- getInertCans
-       ; if inert_count ics == 0
+       ; solve_deriveds <- keepSolvingDeriveds
+       ; if inert_count ics == 0 && not solve_deriveds
          then return Nothing
          else try (selectDerivedWorkItem wl) (return Nothing) } }
 
@@ -307,15 +323,17 @@ instance Outputable WorkList where
           , wl_rest = rest, wl_implics = implics, wl_deriv = ders })
    = text "WL" <+> (braces $
      vcat [ ppUnless (null eqs) $
-            ptext (sLit "Eqs =") <+> vcat (map ppr eqs)
+            text "Eqs =" <+> vcat (map ppr eqs)
           , ppUnless (null feqs) $
-            ptext (sLit "Funeqs =") <+> vcat (map ppr 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) $
-            ptext (sLit "Derived =") <+> vcat (map ppr 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)"
           ])
 
 
@@ -331,7 +349,7 @@ data InertSet
               -- Canonical Given, Wanted, Derived (no Solved)
               -- Sometimes called "the inert set"
 
-       , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtFlavour)
+       , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
               -- See Note [Type family equations]
               -- If    F tys :-> (co, ty, ev),
               -- then  co :: F tys ~ ty
@@ -343,6 +361,8 @@ data InertSet
               -- 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]
@@ -356,14 +376,14 @@ instance Outputable InertSet where
 emptyInert :: InertSet
 emptyInert
   = IS { inert_cans = IC { inert_count    = 0
-                         , inert_eqs      = emptyVarEnv
+                         , inert_eqs      = emptyDVarEnv
                          , inert_dicts    = emptyDicts
                          , inert_safehask = emptyDicts
                          , inert_funeqs   = emptyFunEqs
                          , inert_irreds   = emptyCts
                          , inert_insols   = emptyCts
-                         , inert_model    = emptyVarEnv }
-       , inert_flat_cache    = emptyFunEqs
+                         , inert_model    = emptyDVarEnv }
+       , inert_flat_cache    = emptyExactFunEqs
        , inert_solved_dicts  = emptyDictMap }
 
 
@@ -374,7 +394,7 @@ 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* dicationaries.
+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
@@ -536,21 +556,25 @@ Result
 
 data InertCans   -- See Note [Detailed InertCans Invariants] for more
   = IC { inert_model :: InertModel
+              -- See Note [inert_model: the inert model]
 
-       , inert_eqs :: TyVarEnv EqualCtList
+       , 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, 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.
+              -- 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
@@ -574,7 +598,7 @@ data InertCans   -- See Note [Detailed InertCans Invariants] for more
               -- When non-zero, keep trying to solved
        }
 
-type InertModel  = TyVarEnv Ct
+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'
@@ -626,34 +650,43 @@ Type-family equations, of form (ev : F tys ~ ty), live in three places
 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.
 
-   * The principal reason for maintaining the model is to generate equalities
-     that tell us how 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.
+   * 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.
+       decomposing injective arguments of type functions, and
+       suchlike.
 
-     - A "shadow copy" for every Given or Wanted (a ~N ty) in
-       inert_eqs.  We imagine that every G/W immediately generates its shadow
-       constraint, but we refrain from actually generating the constraint itself
-       until necessary.  See (DShadow) and (GWShadow) in
-       Note [Adding an inert canonical constraint the InertCans]
+     - 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])
 
-   * If (a -> ty) is in the model, then it is
-     as if we had an inert constraint [D] a ~N ty.
+   * 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
 
-   * Domain of the model = skolems + untouchables
+   * 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_irreds may well contain derived costraints.
+   * However inert_dicts, inert_funeqs, inert_irreds
+     may well contain derived constraints.
 
 Note [inert_eqs: the inert equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -662,8 +695,8 @@ 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,
+  (R1) >= is transitive
+  (R2) If f1 >= f, and f2 >= f,
        then either f1 >= f2 or f2 >= f1
 
 Lemma.  If f1 >= f then f1 >= f1
@@ -690,7 +723,7 @@ 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 (WF)
+       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
 
 Notation: repeated application.
   S^0(f,t)     = t
@@ -702,8 +735,8 @@ 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)
 
-  (IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t
-        that is, each individual binding is "self-stable"
+By (IG1) we define S*(f,t) to be the result of exahaustively
+applying S(f,_) to t.
 
 ----------------------------------------------------------------
 Our main invariant:
@@ -714,7 +747,10 @@ 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.
 
----------- The main theorem --------------
+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,
@@ -724,6 +760,9 @@ guarantee that this recursive use will terminate.
       (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)
@@ -731,7 +770,8 @@ guarantee that this recursive use will terminate.
            or (K2c) not (fw >= fs)
            or (K2d) a not in s
 
-      (K3) If (b -fs-> s) is in S with (fw >= fs), then
+      (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
@@ -740,11 +780,16 @@ guarantee that this recursive use will terminate.
    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
@@ -756,11 +801,17 @@ The idea is that
   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, D>=D, and that's all.  Then, when performing
+* 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),
@@ -799,11 +850,11 @@ 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].
+Also, consider roles more carefully. See Note [Flavours with roles]
 
-Completeness
-~~~~~~~~~~~~~
-K3: completeness.  (K3) is not necessary for the extended substitution
+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.
@@ -879,12 +930,15 @@ they are not.  E.g.
 
 Note [Flavours with roles]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
-The system described in Note [The inert equalities] discusses an abstract
+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 [The inert equalities], we must be careful to respect
-roles. For example, if we have
+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
@@ -894,7 +948,7 @@ roles. For example, if we have
 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
-subsitution means that the proof in Note [The inert equalities] may need
+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]
@@ -1020,21 +1074,21 @@ instance Outputable InertCans where
           , inert_safehask = safehask, inert_irreds = irreds
           , inert_insols = insols, inert_count = count })
     = braces $ vcat
-      [ ppUnless (isEmptyVarEnv eqs) $
-        ptext (sLit "Equalities:")
-          <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
+      [ ppUnless (isEmptyDVarEnv eqs) $
+        text "Equalities:"
+          <+> pprCts (foldDVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
       , ppUnless (isEmptyTcAppMap funeqs) $
-        ptext (sLit "Type-function equalities =") <+> pprCts (funEqsToBag funeqs)
+        text "Type-function equalities =" <+> pprCts (funEqsToBag funeqs)
       , ppUnless (isEmptyTcAppMap dicts) $
-        ptext (sLit "Dictionaries =") <+> pprCts (dictsToBag dicts)
+        text "Dictionaries =" <+> pprCts (dictsToBag dicts)
       , ppUnless (isEmptyTcAppMap safehask) $
-        ptext (sLit "Safe Haskell unsafe overlap =") <+> pprCts (dictsToBag safehask)
+        text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
       , ppUnless (isEmptyCts irreds) $
-        ptext (sLit "Irreds =") <+> pprCts irreds
+        text "Irreds =" <+> pprCts irreds
       , ppUnless (isEmptyCts insols) $
         text "Insolubles =" <+> pprCts insols
-      , ppUnless (isEmptyVarEnv model) $
-        text "Model =" <+> pprCts (foldVarEnv consCts emptyCts model)
+      , ppUnless (isEmptyDVarEnv model) $
+        text "Model =" <+> pprCts (foldDVarEnv consCts emptyCts model)
       , text "Unsolved goals =" <+> int count
       ]
 
@@ -1056,47 +1110,40 @@ Note [Adding an inert canonical constraint the InertCans]
 
 * Adding a *nominal* CTyEqCan (a ~N ty) to the inert set (TcSMonad.addInertEq).
 
-    * We always (G/W/D) kick out constraints that can be rewritten
-      (respecting flavours) by the new constraint.
-        - This is done by kickOutRewritable;
-          see Note [inert_eqs: the inert equalities].
-
-        - 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)
-
-  Then, when adding:
-
-     * [Derived] a ~N ty
-        1. Add (a~ty) to the model
-           NB: 'a' cannot be in fv(ty), because the constraint is canonical.
-
-        2. (DShadow) Emit shadow-copies (emitDerivedShadows):
-             For every inert G/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
-
-     * [Given/Wanted] a ~N ty
-        1. Add it to inert_eqs
-        2. If the model can rewrite (a~ty)
-           then (GWShadow) emit [D] a~ty
-           else (GWModel)  Use emitDerivedShadows just like (DShadow)
-                           and add a~ty to the model
-                           (Reason:[D] a~ty is inert wrt model, and (K2b) holds)
-
-     * [Given/Wanted] a ~R ty: just add it to inert_eqs
-
-
-* 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:
+    (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]
@@ -1112,7 +1159,7 @@ Note [Emitting shadow constraints]
 
 See modelCanRewrite.
 
-NB the use of rewritableTyVars. ou might wonder whether, given the new
+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
@@ -1142,12 +1189,12 @@ eg in Trac #9587.
 addInertEq :: Ct -> TcS ()
 -- This is a key function, because of the kick-out stuff
 -- Precondition: item /is/ canonical
-addInertEq ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv })
+addInertEq ct@(CTyEqCan { cc_tyvar = tv })
   = do { traceTcS "addInertEq {" $
          text "Adding new inert equality:" <+> ppr ct
        ; ics <- getInertCans
 
-       ; let (kicked_out, ics1) = kickOutRewritable (ctEvFlavour ev, eq_rel) tv ics
+       ; let (kicked_out, ics1) = kickOutRewritable (ctFlavourRole ct) tv ics
        ; ics2 <- add_inert_eq ics1 ct
 
        ; setInertCans ics2
@@ -1155,7 +1202,7 @@ addInertEq ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv })
        ; unless (isEmptyWorkList kicked_out) $
          do { updWorkListTcS (appendWorkList kicked_out)
             ; csTraceTcS $
-               hang (ptext (sLit "Kick out, tv =") <+> ppr tv)
+               hang (text "Kick out, tv =" <+> ppr tv)
                   2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
                           , ppr kicked_out ]) }
 
@@ -1166,33 +1213,23 @@ 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 })
-  | isDerived ev
-  = do { emitDerivedShadows ics tv
-       ; return (ics { inert_model = extendVarEnv old_model tv ct }) }
-
+             ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv
+                          , cc_rhs = _rhs })
   | ReprEq <- eq_rel
   = return new_ics
 
-  -- Nominal equality (tv ~N ty), Given/Wanted
-  -- See Note [Emitting shadow constraints]
-  | modelCanRewrite old_model rw_tvs  -- Shadow of new constraint is
-  = do { emitNewDerivedEq loc pred    -- not inert, so emit it
-       ; return new_ics }
-
-  | otherwise   -- Shadow of new constraint is inert wrt model
-                -- so extend model, and create shadows it can now rewrite
+  | isDerived ev
   = do { emitDerivedShadows ics tv
-       ; return (new_ics { inert_model = new_model }) }
+       ; 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
-    rw_tvs  = tyVarsOfType pred
     new_ics = ics { inert_eqs   = addTyEq old_eqs tv ct
                   , inert_count = bumpUnsolvedCount ev n }
-    new_model = extendVarEnv old_model tv derived_ct
-    derived_ct = ct { cc_ev = CtDerived { ctev_loc = loc, ctev_pred = pred } }
 
 add_inert_eq _ ct = pprPanic "addInertEq" (ppr ct)
 
@@ -1203,14 +1240,14 @@ emitDerivedShadows IC { inert_eqs      = tv_eqs
                       , inert_funeqs   = funeqs
                       , inert_irreds   = irreds
                       , inert_model    = model } new_tv
-  = mapM_ emit_shadow shadows
+  | null shadows
+  = return ()
+  | otherwise
+  = do { traceTcS "Emit derived shadows:" $
+         vcat [ text "tyvar =" <+> ppr new_tv
+              , text "shadows =" <+> vcat (map ppr shadows) ]
+       ; emitWork shadows }
   where
-    emit_shadow ct = emitNewDerived loc pred
-      where
-        ev = ctEvidence ct
-        pred = ctEvPred ev
-        loc  = ctEvLoc  ev
-
     shadows = foldDicts  get_ct dicts    $
               foldDicts  get_ct safehask $
               foldFunEqs get_ct funeqs   $
@@ -1218,31 +1255,93 @@ emitDerivedShadows IC { inert_eqs      = tv_eqs
               foldTyEqs  get_ct tv_eqs []
       -- Ignore insolubles
 
-    get_ct ct cts | want_shadow ct = ct:cts
+    get_ct ct cts | want_shadow ct = mkShadowCt ct : cts
                   | otherwise      = cts
 
     want_shadow ct
-      =  not (isDerivedCt ct)              -- No need for a shadow of a Derived!
+      =  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 alrady created a
+      && not (modelCanRewrite model rw_tvs)-- We have not already created a
                                            -- shadow
       where
-        rw_tvs = rewritableTyVars ct
+        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 -> TcTyVarSet -> Bool
+modelCanRewrite :: InertModel -> TcTyCoVarSet -> Bool
 -- See Note [Emitting shadow constraints]
 -- True if there is any intersection between dom(model) and tvs
-modelCanRewrite model tvs = not (disjointUFM model 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 TcTyVarSet.  So we drop down
+     -- is disjoint from that of a TcTyCoVarSet.  So we drop down
      -- to the underlying UniqFM.  A bit yukky, but efficient.
 
-rewritableTyVars :: Ct -> TcTyVarSet
+rewritableTyCoVars :: Ct -> TcTyVarSet
 -- The tyvars of a Ct that can be rewritten
-rewritableTyVars (CFunEqCan { cc_tyargs = tys }) = tyVarsOfTypes tys
-rewritableTyVars ct                              = tyVarsOfType (ctPred ct)
+rewritableTyCoVars (CFunEqCan { cc_tyargs = tys }) = tyCoVarsOfTypes tys
+rewritableTyCoVars ct                              = tyCoVarsOfType (ctPred ct)
 
 --------------
 addInertCan :: Ct -> TcS ()  -- Constraints *other than* equalities
@@ -1255,12 +1354,10 @@ addInertCan ct
 
        -- Emit shadow derived if necessary
        -- See Note [Emitting shadow constraints]
-       ; let ev     = ctEvidence ct
-             pred   = ctEvPred ev
-             rw_tvs = rewritableTyVars ct
-
-       ; when (not (isDerived ev) && modelCanRewrite (inert_model ics) rw_tvs)
-              (emitNewDerived (ctEvLoc ev) pred)
+       ; 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 }
 
@@ -1293,43 +1390,28 @@ bumpUnsolvedCount ev n | isWanted ev = n+1
 
 
 -----------------------------------------
-kickOutRewritable :: CtFlavourRole  -- Flavour and role of the equality that is
-                                    -- being added to the inert set
+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)
-   -- NB: Notice that 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
-kickOutRewritable new_fr new_tv ics@(IC { inert_funeqs = funeqmap })
+-- 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)
-  = if isFlattenTyVar new_tv
-    then (emptyWorkList { wl_funeqs = feqs_out }, ics { inert_funeqs = feqs_in })
-    else (emptyWorkList,                          ics)
+  = (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)
-        --
-        -- ExCEPT (tiresomely) that we should kick out any CFunEqCans
-        -- that we should re-examine for their fundeps, even though
-        -- they can't be *rewrittten*.
-        -- See Note [Kicking out CFunEqCan for fundeps]
-  where
-    (feqs_out, feqs_in) = partitionFunEqs kick_out_fe funeqmap
+        -- Lemma (L2) in Note [Extending the inert equalities]
 
-    kick_out_fe :: Ct -> Bool
-    kick_out_fe (CFunEqCan { cc_fsk = fsk }) = fsk == new_tv
-    kick_out_fe _ = False  -- Can't happen
-
-kickOutRewritable new_fr new_tv (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 })
+  | otherwise
   = (kicked_out, inert_cans_in)
   where
     inert_cans_in = IC { inert_eqs      = tv_eqs_in
@@ -1349,60 +1431,59 @@ kickOutRewritable new_fr new_tv (IC { inert_eqs      = tv_eqs
                                              `andCts` insols_out)
                     , wl_implics = emptyBag }
 
-    (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
+    (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_irred irreds
-    (insols_out, insols_in) = partitionBag     kick_out_ct    insols
+    (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]
 
-    can_rewrite :: CtEvidence -> Bool
-    can_rewrite = (new_fr `eqCanRewriteFR`) . ctEvFlavourRole
+    fr_can_rewrite :: CtEvidence -> Bool
+    fr_can_rewrite ev = new_fr `eqCanRewriteFR` (ctEvFlavourRole ev)
 
     kick_out_ct :: Ct -> Bool
-    kick_out_ct ct = kick_out_ctev (ctEvidence ct)
+    -- 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_fsk = fsk })
-      =  kick_out_ctev ev || fsk == new_tv
-    kick_out_fe _ = False  -- Can't happen
-
-    kick_out_ctev :: CtEvidence -> Bool
-    kick_out_ctev ev =  can_rewrite ev
-                     && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
-         -- See Note [Kicking out inert constraints]
-
-    kick_out_irred :: Ct -> Bool
-    kick_out_irred ct =  can_rewrite (cc_ev ct)
-                      && new_tv `elemVarSet` closeOverKinds (TcM.tyVarsOfCt ct)
-          -- See Note [Kicking out Irreds]
-
-    kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList)
-                 -> ([Ct], TyVarEnv EqualCtList)
+    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:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_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 [The inert equalities] in TcFlatten
+    -- 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 (can_rewrite ev)  -- (K1)
+      = not (fr_can_rewrite ev)  -- (K1)
 
       | otherwise
       = check_k2 && check_k3
       where
-        ev_fr = ctEvFlavourRole ev
-        check_k2 = not (ev_fr  `eqCanRewriteFR` ev_fr)
-                || not (new_fr `eqCanRewriteFR` ev_fr)
-                ||     (ev_fr  `eqCanRewriteFR` new_fr)
-                || not (new_tv `elemVarSet` tyVarsOfType rhs_ty)
+        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` ev_fr
+          | new_fr `eqCanRewriteFR` fs
           = case eq_rel of
               NomEq  -> not (rhs_ty `eqType` mkTyVarTy new_tv)
               ReprEq -> not (isTyVarExposed new_tv rhs_ty)
@@ -1416,7 +1497,8 @@ 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
+             (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
@@ -1425,7 +1507,7 @@ kickOutAfterUnification new_tv
 
        ; unless (isEmptyWorkList kicked_out) $
          csTraceTcS $
-         hang (ptext (sLit "Kick out (unify), tv =") <+> ppr new_tv)
+         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 ])
@@ -1433,13 +1515,13 @@ kickOutAfterUnification new_tv
 
 kickOutModel :: TcTyVar -> InertCans -> (WorkList, InertCans)
 kickOutModel new_tv ics@(IC { inert_model = model, inert_eqs = eqs })
-  = (foldVarEnv add emptyWorkList der_out, ics { inert_model = new_model })
+  = (foldDVarEnv add emptyWorkList der_out, ics { inert_model = new_model })
   where
-    (der_out, new_model) = partitionVarEnv kick_out_der model
+    (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` tyVarsOfType rhs
+      = new_tv == tv || new_tv `elemVarSet` tyCoVarsOfType rhs
     kick_out_der _ = False
 
     add :: Ct -> WorkList -> WorkList
@@ -1450,35 +1532,39 @@ kickOutModel new_tv ics@(IC { inert_model = model, inert_eqs = eqs })
       | not (isInInertEqs eqs tv rhs) = extendWorkListDerived (ctEvLoc ev) ev wl
     add _ wl                          = wl
 
-{- Note [Kicking out inert constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Given a new (a -> ty) inert, we want to kick out an existing inert
-constraint if
-  a) the new constraint can rewrite the inert one
-  b) 'a' is free in the inert constraint (so that it *will*)
-     rewrite it if we kick it out.
-
-For (b) we use tyVarsOfCt, which returns the type variables /and
-the kind variables/ that are directly visible in the type. Hence we
-will have exposed all the rewriting we care about to make the most
-precise kinds visible for matching classes etc. No need to kick out
-constraints that mention type variables whose kinds contain this
-variable!  (Except see Note [Kicking out Irreds].)
-
-Note [Kicking out Irreds]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-There is an awkward special case for Irreds.  When we have a
-kind-mis-matched equality constraint (a:k1) ~ (ty:k2), we turn it into
-an Irred (see Note [Equalities with incompatible kinds] in
-TcCanonical). So in this case the free kind variables of k1 and k2
-are not visible.  More precisely, the type looks like
-   (~) k1 (a:k1) (ty:k2)
-because (~) has kind forall k. k -> k -> Constraint.  So the constraint
-itself is ill-kinded.  We can "see" k1 but not k2.  That's why we use
-closeOverKinds to make sure we see k2.
-
-This is not pretty. Maybe (~) should have kind
-   (~) :: forall k1 k1. k1 -> k2 -> Constraint
+
+{- Note [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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1501,10 +1587,12 @@ addInertSafehask _ item
   = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item
 
 insertSafeOverlapFailureTcS :: Ct -> TcS ()
+-- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
 insertSafeOverlapFailureTcS item
   = updInertCans (\ics -> addInertSafehask ics item)
 
 getSafeOverlapFailures :: TcS Cts
+-- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
 getSafeOverlapFailures
  = do { IC { inert_safehask = safehask } <- getInertCans
       ; return $ foldDicts consCts safehask emptyCts }
@@ -1554,7 +1642,7 @@ 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 onfuse them with insolubles arising from
+     the inert set, lest we confuse them with insolubles arising from
      solving wanteds
 
   b) Any Derived CFunEqCans.  Derived CTyEqCans are in the
@@ -1565,7 +1653,7 @@ After solving the Givens we take two things out of the inert set
            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 not not to
+     It's ok to remove them because they turned out not to
      yield an insoluble, and hence have now done their work.
 -}
 
@@ -1603,8 +1691,7 @@ updInertIrreds :: (Cts -> Cts) -> TcS ()
 updInertIrreds upd_fn
   = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
 
-
-getInertEqs :: TcS (TyVarEnv EqualCtList)
+getInertEqs :: TcS (DTyVarEnv EqualCtList)
 getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
 
 getInertModel :: TcS InertModel
@@ -1617,14 +1704,40 @@ getInertGivens
   = do { inerts <- getInertCans
        ; let all_cts = foldDicts (:) (inert_dicts inerts)
                      $ foldFunEqs (:) (inert_funeqs inerts)
-                     $ concat (varEnvElts (inert_eqs 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
+    get_sc_dicts ic@(IC { inert_dicts = dicts })
+      = (sc_pend_dicts, ic')
+      where
+        ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts }
+
+        sc_pend_dicts :: [Ct]
+        sc_pend_dicts = foldDicts get_pending dicts []
+
+    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
+
+    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
@@ -1635,8 +1748,10 @@ getUnsolvedInerts
            , inert_dicts  = idicts
            , inert_insols = insols
            , inert_model  = model } <- getInertCans
+      ; keep_derived <- keepSolvingDeriveds
 
-      ; let der_tv_eqs       = foldVarEnv (add_der tv_eqs) emptyCts model  -- Want to float these
+      ; 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
@@ -1656,8 +1771,10 @@ getUnsolvedInerts
               -- Keep even the given insolubles
               -- so that we can report dead GADT pattern match branches
   where
-    add_der tv_eqs ct cts
+    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
@@ -1666,10 +1783,10 @@ getUnsolvedInerts
 
     is_unsolved ct = not (isGivenCt ct)   -- Wanted or Derived
 
-isInInertEqs :: TyVarEnv EqualCtList -> TcTyVar -> TcType -> Bool
+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 lookupVarEnv eqs tv of
+  = case lookupDVarEnv eqs tv of
       Nothing  -> False
       Just cts -> any (same_pred rhs) cts
   where
@@ -1679,19 +1796,23 @@ isInInertEqs eqs tv rhs
       , rhs `eqType` rhs2 = True
       | otherwise         = False
 
-getNoGivenEqs :: TcLevel     -- TcLevel of this implication
+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
@@ -1769,7 +1890,20 @@ prohibitedSuperClassSolve from_loc solve_loc
   | 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
@@ -1864,12 +1998,14 @@ 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 (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 :: TcPredType -> TcS (Maybe CtEvidence)
@@ -1882,12 +2018,16 @@ lookupInInerts pty
   | 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 -> Just (ctEvidence ct)
       _       -> Nothing
 
+-- | Look up a solved inert. NB: the returned 'CtEvidence' might not
+-- match the input exactly. See Note [Use loose types in inert set].
 lookupSolvedDict :: InertSet -> Class -> [Type] -> Maybe CtEvidence
 -- Returns just if exactly this predicate type exists in the solved.
 lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
@@ -1895,7 +2035,6 @@ lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
       Just ev -> Just ev
       _       -> Nothing
 
-
 {- *********************************************************************
 *                                                                      *
                    Irreds
@@ -1926,19 +2065,19 @@ type EqualCtList = [Ct]
    - Any number of Wanteds and/or Deriveds
 -}
 
-addTyEq :: TyVarEnv EqualCtList -> TcTyVar -> Ct -> TyVarEnv EqualCtList
-addTyEq old_list tv it = extendVarEnv_C (\old_eqs _new_eqs -> it : old_eqs)
+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) -> TyVarEnv EqualCtList -> b -> b
+foldTyEqs :: (Ct -> b -> b) -> DTyVarEnv EqualCtList -> b -> b
 foldTyEqs k eqs z
-  = foldVarEnv (\cts z -> foldr k z cts) z eqs
+  = foldDVarEnv (\cts z -> foldr k z cts) z eqs
 
 findTyEqs :: InertCans -> TyVar -> EqualCtList
-findTyEqs icans tv = lookupVarEnv (inert_eqs icans) tv `orElse` []
+findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` []
 
-delTyEq :: TyVarEnv EqualCtList -> TcTyVar -> TcType -> TyVarEnv 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
 
@@ -1946,36 +2085,51 @@ delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
 *                                                                      *
                    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.
 
-type TcAppMap a = UniqFM (ListMap TypeMap a)
-    -- Indexed by tycon then the arg types
-    -- Used for types and classes; hence UniqFM
+We must be careful when using the result of a lookup because it may
+not match the requsted info exactly!
+
+-}
+
+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 = isNullUFM m
+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
@@ -1991,7 +2145,7 @@ 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
 
 
 {- *********************************************************************
@@ -2013,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
@@ -2024,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)
@@ -2068,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
 
@@ -2080,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
@@ -2095,11 +2246,6 @@ 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 -> ([Ct], FunEqMap Ct)
 -- Optimise for the case where the predicate is false
 -- partitionFunEqs is called only from kick-out, and kick-out usually
@@ -2116,6 +2262,20 @@ partitionFunEqs f m = (yeses, foldr 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))
+
 {-
 ************************************************************************
 *                                                                      *
@@ -2135,23 +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 Int,
-          -- The number of unification variables we have filled
-          -- The important thing is whether it is non-zero
+      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_count     :: IORef Int, -- Global step count
 
       tcs_inerts    :: IORef InertSet, -- Current inert set
 
       -- The main work-list and the flattening worklist
       -- See Note [Work list priorities] and
-      tcs_worklist  :: IORef WorkList -- Current worklist
+      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]
     }
 
 ---------------
@@ -2165,7 +2339,6 @@ instance Applicative TcS where
   (<*>) = ap
 
 instance Monad TcS where
-  return = pure
   fail err  = TcS (\_ -> fail err)
   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
 
@@ -2195,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 m = wrapTcS . runTcPluginM m . Just =<< getTcEvBinds
+runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBindsVar
 
 instance HasDynFlags TcS where
     getDynFlags = wrapTcS getDynFlags
@@ -2226,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)) }
@@ -2241,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
+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
@@ -2289,41 +2479,55 @@ 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 { eb_lhs = 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 { eb_lhs = bndr, eb_rhs = 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 }
 
 {- Note [Do not inherit the flat cache]
@@ -2338,17 +2542,11 @@ flattened out after solving the outer level, but and we don't
 do that flattening recursively.
 -}
 
-
-recoverTcS :: TcS a -> TcS a -> TcS a
-recoverTcS (TcS recovery_code) (TcS thing_inside)
-  = TcS $ \ env ->
-    TcM.recoverM (recovery_code env) (thing_inside env)
-
 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
@@ -2372,22 +2570,6 @@ nestTcS (TcS thing_inside)
 
        ; 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 0
-       ; 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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2431,18 +2613,21 @@ updWorkListTcS f
        ; let new_work = f wl_curr
        ; wrapTcS (TcM.writeTcRef wl_var new_work) }
 
+-- | Should we keep solving even only deriveds are left?
+keepSolvingDeriveds :: TcS Bool
+keepSolvingDeriveds = TcS (return . tcs_need_deriveds)
+
 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)
 
-emitWorkCt :: Ct -> TcS ()
-emitWorkCt ct
-  = do { traceTcS "Emitting fresh (canonical) work" (ppr ct)
-       ; updWorkListTcS (extendWorkListCt ct) }
+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.
@@ -2467,16 +2652,22 @@ readTcRef ref = wrapTcS (TcM.readTcRef ref)
 updTcRef :: TcRef a -> (a->a) -> TcS ()
 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
 
-getTcEvBinds :: TcS EvBindsVar
-getTcEvBinds = TcS (return . tcs_ev_binds)
+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 }
+  = do { ev_binds_var <- getTcEvBindsVar
+       ; wrapTcS $ TcM.getTcEvBindsMap ev_binds_var }
 
 unifyTyVar :: TcTyVar -> TcType -> TcS ()
 -- Unify a meta-tyvar with a type
@@ -2488,7 +2679,7 @@ unifyTyVar tv ty
     TcS $ \ env ->
     do { TcM.traceTc "unifyTyVar" (ppr tv <+> text ":=" <+> ppr ty)
        ; TcM.writeMetaTyVar tv ty
-       ; TcM.updTcRef (tcs_unified env) (+ 1) }
+       ; TcM.updTcRef (tcs_unified env) (+1) }
 
 unflattenFmv :: TcTyVar -> TcType -> TcS ()
 -- Fill a flatten-meta-var, simply by unifying it.
@@ -2505,8 +2696,8 @@ reportUnifications (TcS thing_inside)
     do { inner_unified <- TcM.newTcRef 0
        ; res <- thing_inside (env { tcs_unified = inner_unified })
        ; n_unifs <- TcM.readTcRef inner_unified
-       ; TcM.updTcRef (tcs_unified env) (+ n_unifs)  -- Inner unifications affect
-       ; return (n_unifs, res) }                     -- the outer scope too
+       ; TcM.updTcRef (tcs_unified env) (+ n_unifs)
+       ; return (n_unifs, res) }
 
 getDefaultInfo ::  TcS ([Type], (Bool, Bool))
 getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
@@ -2535,8 +2726,8 @@ 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
-addUsedDataCons :: GlobalRdrEnv -> TyCon -> TcS ()
-addUsedDataCons rdr_env tycon = wrapTcS  $ TcM.addUsedDataCons rdr_env tycon
+addUsedGREs :: [GlobalRdrElt] -> TcS ()
+addUsedGREs gres = wrapTcS  $ TcM.addUsedGREs gres
 
 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2547,7 +2738,7 @@ checkWellStagedDFun pred dfun_id 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
@@ -2560,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
@@ -2572,8 +2762,14 @@ 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)
@@ -2600,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.
@@ -2645,45 +2841,34 @@ which will result in two Deriveds to end up in the insoluble set:
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 newFlattenSkolem :: CtFlavour -> CtLoc
                  -> TcType         -- F xis
-                 -> TcS (CtEvidence, TcTyVar)    -- [W] x:: F xis ~ fsk
+                 -> TcS (CtEvidence, Coercion, TcTyVar)    -- [W] x:: F xis ~ fsk
 newFlattenSkolem Given loc fam_ty
   = do { fsk <- newFsk fam_ty
-       ; ev  <- newGivenEvVar loc (mkTcEqPred fam_ty (mkTyVarTy fsk),
-                                   EvCoercion (mkTcNomReflCo fam_ty))
-       ; return (ev, fsk) }
+       ; 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 <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fmv))
-       ; return (ev, fmv) }
+       ; (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 (mkTcEqPred fam_ty (mkTyVarTy fmv))
-       ; return (ev, fmv) }
+       ; 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 $ do { uniq <- TcM.newUnique
-                 ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk")
-                 ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
-
-newFmv fam_ty
-  = wrapTcS $ do { uniq <- TcM.newUnique
-                 ; ref  <- TcM.newMutVar Flexi
-                 ; cur_lvl <- TcM.getTcLevel
-                 ; let details = MetaTv { mtv_info  = FlatMetaTv
-                                        , mtv_ref   = ref
-                                        , mtv_tclvl = fmvTcLevel cur_lvl }
-                       name = TcM.mkTcTyVarName uniq (fsLit "s")
-                 ; return (mkTcTyVar name (typeKind fam_ty) details) }
+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 stuff } }
+            is { inert_flat_cache = insertExactFunEq fc tc xi_args stuff } }
 
 -- Instantiations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2707,12 +2892,12 @@ 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
@@ -2722,26 +2907,57 @@ instFlexiTcSHelper tvname kind
        ; 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 Freshness = Fresh | Cached
+data MaybeNew = Fresh CtEvidence | Cached EvTerm
 
-isFresh :: Freshness -> Bool
-isFresh Fresh  = True
-isFresh Cached = False
+isFresh :: MaybeNew -> Bool
+isFresh (Fresh {})  = True
+isFresh (Cached {}) = False
 
-freshGoals :: [(CtEvidence, Freshness)] -> [CtEvidence]
-freshGoals mns = [ ctev | (ctev, Fresh) <- mns ]
+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 { tc_evbinds <- getTcEvBinds
-       ; wrapTcS $ TcM.addTcEvBind tc_evbinds 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)
@@ -2749,8 +2965,9 @@ setWantedEvBind ev_id tm = setEvBind (mkWantedEvBind ev_id tm)
 setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
 setEvBindIfWanted ev tm
   = case ev of
-      CtWanted { ctev_evar = ev_id } -> setWantedEvBind ev_id tm
-      _                              -> return ()
+      CtWanted { ctev_dest = dest }
+        -> setWantedEvTerm dest tm
+      _ -> return ()
 
 newTcEvBinds :: TcS EvBindsVar
 newTcEvBinds = wrapTcS TcM.newTcEvBinds
@@ -2763,61 +2980,33 @@ newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
 -- immediately bind it to the given term
 -- and return its CtEvidence
 -- See Note [Bind new Givens immediately] in TcRnTypes
--- Precondition: this is not a kind equality
---               See Note [Do not create Given kind equalities]
 newGivenEvVar loc (pred, rhs)
-  = ASSERT2( not (isKindEquality pred), ppr pred $$ pprCtOrigin (ctLocOrigin loc) )
-    do { -- checkReductionDepth loc pred
-       ; new_ev <- newEvVar pred
-       ; setEvBind (mkGivenEvBind new_ev 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 (mkGivenEvBind new_ev rhs)
+       ; return new_ev }
+
 newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
--- Like newGivenEvVar, but automatically discard kind equalities
--- See Note [Do not create Given kind equalities]
-newGivenEvVars loc pts = mapM (newGivenEvVar loc) (filterOut (isKindEquality . fst) pts)
-
-isKindEquality :: TcPredType -> Bool
--- See Note [Do not create Given kind equalities]
-isKindEquality pred = case classifyPredType pred of
-                        EqPred _ t1 _ -> isKind t1
-                        _             -> False
-
-{- 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.
--}
+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
@@ -2825,18 +3014,29 @@ newWantedEvVarNC loc pty
        ; new_ev <- newEvVar pty
        ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$
                                          pprCtLoc loc)
-       ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
+       ; return (CtWanted { ctev_pred = pty, ctev_dest = EvVarDest new_ev
+                          , ctev_loc = loc })}
 
-newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
+newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
 -- For anything except ClassPred, this is the same as newWantedEvVarNC
 newWantedEvVar 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
-                    ; return (ctev, Fresh) } }
+                    ; 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
+  = newWantedEvVar loc pty
 
 emitNewDerived :: CtLoc -> TcPredType -> TcS ()
 emitNewDerived loc pred
@@ -2853,11 +3053,11 @@ emitNewDeriveds loc preds
        ; traceTcS "Emitting new deriveds" (ppr evs)
        ; updWorkListTcS (extendWorkListDeriveds loc evs) }
 
-emitNewDerivedEq :: CtLoc -> TcPredType -> TcS ()
+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 pred
-  = do { ev <- newDerivedNC loc pred
+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) }
 
@@ -2877,15 +3077,24 @@ checkReductionDepth loc ty
          wrapErrTcS $
          solverDepthErrorTcS loc ty }
 
-matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
+matchFam :: TyCon -> [Type] -> TcS (Maybe (Coercion, TcType))
 matchFam tycon args = wrapTcS $ matchFamTcM tycon args
 
-matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (TcCoercion, TcType))
+matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (Coercion, TcType))
 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
 matchFamTcM tycon args
   = do { fam_envs <- FamInst.tcGetFamInstEnvs
-       ; return $ fmap (first TcCoercion) $
-         reduceTyFamApp_maybe fam_envs Nominal tycon args }
+       ; 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]
@@ -2904,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 <- 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_simple = 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_status   = IC_Unsolved
-                                            , 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