Fix a number of subtle solver bugs

As a result of some other unrelated changes I found that
IndTypesPerf was failing, and opened Trac #11408.  There's
a test in indexed-types/should-compile/T11408.

The bug was that a type like
 forall t. (MT (UL t) (UR t) ~ t) => UL t -> UR t -> Int
is in fact unambiguous, but it's a bit subtle to prove
that it is unambiguous.

In investigating, Dimitrios and I found several subtle
bugs in the constraint solver, fixed by this patch

* canRewrite was missing a Derived/Derived case.  This was
  lost by accident in Richard's big kind-equality patch.

* Interact.interactTyVarEq would discard [D] a ~ ty if there
  was a [W] a ~ ty in the inert set.  But that is wrong because
  the former can rewrite things that the latter cannot.
  Fix: a new function eqCanDischarge

* In TcSMonad.addInertEq, the process was outright wrong for
  a Given/Wanted in the (GWModel) case.  We were adding a new
  Derived without kicking out things that it could rewrite.
  Now the code is simpler (no special GWModel case), and works
  correctly.

* The special case in kickOutRewritable for [W] fsk ~ ty,
  turns out not to be needed.  (We emit a [D] fsk ~ ty which
  will do the job.

I improved comments and documentation, esp in TcSMonad.

8 files changed, 304 insertions, 191 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index fa2b8c8cb5..031c5dbb3f 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1453,9 +1453,9 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2
       -- the floating step looks for meta tyvars on the left
       | isMetaTyVar tv2 = True
 
-      -- So neither is a meta tyvar
+      -- So neither is a meta tyvar (including FlatMetaTv)
 
-      -- If only one is a flatten tyvar, put it on the left
+      -- If only one is a flatten skolem, put it on the left
       -- See Note [Eliminate flat-skols]
       | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
 
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 20f77a7650..06ef6930cf 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -242,7 +242,7 @@ BUT this works badly for Trac #10340:
 For 'foo' we instantiate 'get' at types mm ss
        [W] MonadState ss mm, [W] mm ss ~ State Any Any
 Flatten, and decompose
-       [W] MnadState ss mm, [W] Any ~ fmv, [W] mm ~ State fmv, [W] fmv ~ ss
+       [W] MonadState ss mm, [W] Any ~ fmv, [W] mm ~ State fmv, [W] fmv ~ ss
 Unify mm := State fmv:
        [W] MonadState ss (State fmv), [W] Any ~ fmv, [W] fmv ~ ss
 If we orient with (untouchable) fmv on the left we are now stuck:
@@ -1147,7 +1147,7 @@ flatten_exact_fam_app_fully tc tys
        ; fr <- getFlavourRole
        ; case mb_ct of
            Just (co, rhs_ty, flav)  -- co :: F xis ~ fsk
-             | (flav, NomEq) `canDischargeFR` fr
+             | (flav, NomEq) `funEqCanDischargeFR` fr
              ->  -- Usable hit in the flat-cache
                  -- We certainly *can* use a Wanted for a Wanted
                 do { traceFlat "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty)
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 6d8567157a..37b86149c6 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -506,7 +506,7 @@ solveOneFromTheOther :: CtEvidence  -- Inert
                      -> TcS (InteractResult, StopNowFlag)
 -- Preconditions:
 -- 1) inert and work item represent evidence for the /same/ predicate
--- 2) ip/class/irred evidence (no coercions) only
+-- 2) ip/class/irred constraints only; not used for equalities
 solveOneFromTheOther ev_i ev_w
   | isDerived ev_w         -- Work item is Derived; just discard it
   = return (IRKeep, True)
@@ -843,7 +843,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
                                          , cc_tyargs = args, cc_fsk = fsk })
   | Just (CFunEqCan { cc_ev = ev_i
                     , cc_fsk = fsk_i }) <- matching_inerts
-  = if ev_i `canDischarge` ev
+  = if ev_i `funEqCanDischarge` ev
     then  -- Rewrite work-item using inert
       do { traceTcS "reactFunEq (discharge work item):" $
            vcat [ text "workItem =" <+> ppr workItem
@@ -851,7 +851,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
          ; reactFunEq ev_i fsk_i ev fsk
          ; stopWith ev "Inert rewrites work item" }
     else  -- Rewrite inert using work-item
-      ASSERT2( ev `canDischarge` ev_i, ppr ev $$ ppr ev_i )
+      ASSERT2( ev `funEqCanDischarge` ev_i, ppr ev $$ ppr ev_i )
       do { traceTcS "reactFunEq (rewrite inert item):" $
            vcat [ text "workItem =" <+> ppr workItem
                 , text "inertItem=" <+> ppr ev_i ]
@@ -881,15 +881,15 @@ improveLocalFunEqs loc inerts fam_tc args fsk
   = do { traceTcS "interactFunEq improvements: " $
          vcat [ ptext (sLit "Eqns:") <+> ppr improvement_eqns
               , ptext (sLit "Candidates:") <+> ppr funeqs_for_tc
-              , ptext (sLit "TvEqs:") <+> ppr tv_eqs ]
+              , ptext (sLit "Model:") <+> ppr model ]
        ; mapM_ (unifyDerived loc Nominal) improvement_eqns }
   | otherwise
   = return ()
   where
-    tv_eqs        = inert_model inerts
+    model         = inert_model inerts
     funeqs        = inert_funeqs inerts
     funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
-    rhs           = lookupFlattenTyVar tv_eqs fsk
+    rhs           = lookupFlattenTyVar model fsk
 
     --------------------
     improvement_eqns
@@ -906,14 +906,14 @@ improveLocalFunEqs loc inerts fam_tc args fsk
 
     --------------------
     do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
-      = sfInteractInert ops args rhs iargs (lookupFlattenTyVar tv_eqs ifsk)
+      = sfInteractInert ops args rhs iargs (lookupFlattenTyVar model ifsk)
     do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
 
     --------------------
     -- See Note [Type inference for type families with injectivity]
     do_one_injective injective_args
                     (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
-      | rhs `tcEqType` lookupFlattenTyVar tv_eqs ifsk
+      | rhs `tcEqType` lookupFlattenTyVar model ifsk
       = [Pair arg iarg | (arg, iarg, True)
                            <- zip3 args iargs injective_args ]
       | otherwise
@@ -922,8 +922,7 @@ improveLocalFunEqs loc inerts fam_tc args fsk
 
 -------------
 lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType
--- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
--- this is used only when dealing with a CFunEqCan
+-- See Note [lookupFlattenTyVar]
 lookupFlattenTyVar model ftv
   = case lookupVarEnv model ftv of
       Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs
@@ -950,7 +949,18 @@ reactFunEq from_this fsk1 solve_this fsk2
        ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
                                      ppr solve_this $$ ppr fsk2) }
 
-{-
+{- Note [lookupFlattenTyVar]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Supppose we have an injective function F and
+  inert_funeqs:   F t1 ~ fsk1
+                  F t2 ~ fsk2
+  model           fsk1 ~ fsk2
+
+We never rewrite the RHS (cc_fsk) of a CFunEqCan.  But we /do/ want to
+get the [D] t1 ~ t2 from the injectiveness of F.  So we look up the
+cc_fsk of CFunEqCans in the model when trying to find derived
+equalities arising from injectivity.
+
 Note [Type inference for type families with injectivity]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have a type family with an injectivity annotation:
@@ -1086,10 +1096,10 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
                                           , cc_eq_rel = eq_rel })
   | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
                              <- findTyEqs inerts tv
-                         , ev_i `canDischarge` ev
+                         , ev_i `eqCanDischarge` ev
                          , rhs_i `tcEqType` rhs ]
-  =  -- Inert:     a ~ b
-     -- Work item: a ~ b
+  =  -- Inert:     a ~ ty
+     -- Work item: a ~ ty
     do { setEvBindIfWanted ev $
           EvCoercion (tcDowngradeRole (eqRelRole eq_rel)
                                       (ctEvRole ev_i)
@@ -1100,7 +1110,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
   | Just tv_rhs <- getTyVar_maybe rhs
   , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
                              <- findTyEqs inerts tv_rhs
-                         , ev_i `canDischarge` ev
+                         , ev_i `eqCanDischarge` ev
                          , rhs_i `tcEqType` mkTyVarTy tv ]
   =  -- Inert:     a ~ b
      -- Work item: b ~ a
@@ -1530,7 +1540,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
                                         `mkTcTransCo` ctEvCoercion old_ev) )
 
        ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
-       ; emitWorkCt new_ct
+       ; updWorkListTcS (extendWorkListFunEq new_ct)
        ; stopWith old_ev "Fun/Top (given, shortcut)" }
 
   | otherwise
@@ -1549,8 +1559,9 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
                      (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
                             `mkTcTransCo` new_co)
 
-       ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
-       ; emitWorkCt new_ct
+       ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
+                                , cc_tyargs = xis, cc_fsk = fsk }
+       ; updWorkListTcS (extendWorkListFunEq new_ct)
        ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
   where
     loc = ctEvLoc old_ev
@@ -1631,7 +1642,7 @@ Note [Cached solved FunEqs]
 When trying to solve, say (FunExpensive big-type ~ ty), it's important
 to see if we have reduced (FunExpensive big-type) before, lest we
 simply repeat it.  Hence the lookup in inert_solved_funeqs.  Moreover
-we must use `canDischarge` because both uses might (say) be Wanteds,
+we must use `funEqCanDischarge` because both uses might (say) be Wanteds,
 and we *still* want to save the re-computation.
 
 Note [MATCHING-SYNONYMS]
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index cdda69666e..6f2f2e3bdd 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -112,7 +112,8 @@ module TcRnTypes(
 
         CtFlavour(..), ctEvFlavour,
         CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
-        eqCanRewrite, eqCanRewriteFR, canDischarge, canDischargeFR,
+        eqCanRewrite, eqCanRewriteFR,  eqCanDischarge,
+        funEqCanDischarge, funEqCanDischargeFR,
 
         -- Pretty printing
         pprEvVarTheta,
@@ -2273,54 +2274,74 @@ we can; straight from the Wanteds during improvment. And from a Derived
 ReprEq we could conceivably get a Derived NomEq improvment (by decomposing
 a type constructor with Nomninal role), and hence unify.
 
-Note [canDischarge]
-~~~~~~~~~~~~~~~~~~~
-(x1:c1 `canDischarge` x2:c2) returns True if we can use c1 to
-/discharge/ c2; that is, if we can simply drop (x2:c2) altogether,
-perhaps adding a binding for x2 in terms of x1.  We only ask this
-question in two cases:
-
-* Identical equality constraints:
-      (x1:s~t) `canDischarge` (xs:s~t)
-  In this case we can just drop x2 in favour of x1.
-
-* Function calls with the same LHS:
-    (x1:F ts ~ f1) `canDischarge` (x2:F ts ~ f2)
-  Here we can drop x2 in favour of x1, either unifying
-  f2 (if it's a flatten meta-var) or adding a new Given
-  (f1 ~ f2), if x2 is a Given.
-
-This is different from eqCanRewrite; for exammple, a Wanted
-can certainly discharge an identical Wanted.  So canDicharge
-does /not/ define a can-rewrite relation in the sense of
-Definition [Can-rewrite relation] in TcSMonad.
+Note [funEqCanDischarge]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have two CFunEqCans with the same LHS:
+    (x1:F ts ~ f1) `funEqCanDischarge` (x2:F ts ~ f2)
+Can we drop x2 in favour of x1, either unifying
+f2 (if it's a flatten meta-var) or adding a new Given
+(f1 ~ f2), if x2 is a Given?
+
+Answer: yes if funEqCanDischarge is true.
+
+Note [eqCanDischarge]
+~~~~~~~~~~~~~~~~~~~~~
+Suppose we have two identicla equality constraints
+(i.e. both LHS and RHS are the same)
+      (x1:s~t) `eqCanDischarge` (xs:s~t)
+Can we just drop x2 in favour of x1?
+
+Answer: yes if eqCanDischarge is true.
+
+Note that we do /not/ allow Wanted to discharge Derived.
+We must keep both.  Why?  Because the Derived may rewrite
+other Deriveds in the model whereas the Wanted cannot.
+
+However a Wanted can certainly discharge an identical Wanted.  So
+eqCanDischarge does /not/ define a can-rewrite relation in the
+sense of Definition [Can-rewrite relation] in TcSMonad.
 -}
 
+-----------------
 eqCanRewrite :: CtEvidence -> CtEvidence -> Bool
-eqCanRewrite ev1 ev2 = eqCanRewriteFR (ctEvFlavourRole ev1)
-                                      (ctEvFlavourRole ev2)
-
-eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
 -- Very important function!
 -- See Note [eqCanRewrite]
 -- See Note [Wanteds do not rewrite Wanteds]
 -- See Note [Deriveds do rewrite Deriveds]
-eqCanRewriteFR (Given, NomEq)  (_, _)      = True
-eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True
-eqCanRewriteFR _               _           = False
+eqCanRewrite ev1 ev2 = eqCanRewriteFR (ctEvFlavourRole ev1)
+                                      (ctEvFlavourRole ev2)
 
-canDischarge :: CtEvidence -> CtEvidence -> Bool
--- See Note [canDischarge]
-canDischarge ev1 ev2 = canDischargeFR (ctEvFlavourRole ev1)
+eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
+eqCanRewriteFR (Given, NomEq)   (_, _)           = True
+eqCanRewriteFR (Given, ReprEq)  (_, ReprEq)      = True
+eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True
+eqCanRewriteFR _                _                = False
+
+-----------------
+funEqCanDischarge :: CtEvidence -> CtEvidence -> Bool
+-- See Note [funEqCanDischarge]
+funEqCanDischarge ev1 ev2 = funEqCanDischargeFR (ctEvFlavourRole ev1)
                                       (ctEvFlavourRole ev2)
 
-canDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
-canDischargeFR (_, ReprEq)  (_, NomEq)   = False
-canDischargeFR (Given,   _) _            = True
-canDischargeFR (Wanted,  _) (Wanted,  _) = True
-canDischargeFR (Wanted,  _) (Derived, _) = True
-canDischargeFR (Derived, _) (Derived, _) = True
-canDischargeFR _            _            = False
+funEqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
+funEqCanDischargeFR (_, ReprEq)  (_, NomEq)   = False
+funEqCanDischargeFR (Given,   _) _            = True
+funEqCanDischargeFR (Wanted,  _) (Wanted,  _) = True
+funEqCanDischargeFR (Wanted,  _) (Derived, _) = True
+funEqCanDischargeFR (Derived, _) (Derived, _) = True
+funEqCanDischargeFR _            _            = False
+
+-----------------
+eqCanDischarge :: CtEvidence -> CtEvidence -> Bool
+-- See Note [eqCanDischarge]
+eqCanDischarge ev1 ev2 = eqCanDischargeFR (ctEvFlavourRole ev1)
+                                          (ctEvFlavourRole ev2)
+eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
+eqCanDischargeFR (_, ReprEq)  (_, NomEq)   = False
+eqCanDischargeFR (Given,   _) (Given,_)    = True
+eqCanDischargeFR (Wanted,  _) (Wanted,  _) = True
+eqCanDischargeFR (Derived, _) (Derived, _) = True
+eqCanDischargeFR _            _            = False
 
 {-
 ************************************************************************
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 697f3f9032..099be19d94 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -6,7 +6,8 @@ module TcSMonad (
     -- The work list
     WorkList(..), isEmptyWorkList, emptyWorkList,
     extendWorkListNonEq, extendWorkListCt, extendWorkListDerived,
-    extendWorkListCts, extendWorkListEq, appendWorkList,
+    extendWorkListCts, extendWorkListEq, extendWorkListFunEq,
+    appendWorkList,
     selectNextWorkItem,
     workListSize, workListWantedCount,
     updWorkListTcS,
@@ -53,7 +54,7 @@ module TcSMonad (
     getUnsolvedInerts,
     removeInertCts, getPendingScDicts, isPendingScDict,
     addInertCan, addInertEq, insertFunEq,
-    emitInsoluble, emitWorkNC, emitWorkCt,
+    emitInsoluble, emitWorkNC,
 
     -- The Model
     InertModel, kickOutAfterUnification,
@@ -243,7 +244,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 }
@@ -553,12 +554,16 @@ data InertCans   -- See Note [Detailed InertCans Invariants] for more
        , inert_funeqs :: FunEqMap Ct
               -- All CFunEqCans; index is the whole family head type.
               -- All Nominal (that's an invarint of all CFunEqCans)
+              -- LHS is fully rewritten (modulo eqCanRewrite constraints)
+              --     wrt inert_eqs/inert_model
               -- We can get Derived ones from e.g.
               --   (a) flattening derived equalities
               --   (b) emitDerivedShadows
 
        , inert_dicts :: DictMap Ct
               -- Dictionaries only
+              -- All fully rewritten (modulo flavour constraints)
+              --     wrt inert_eqs/inert_model
 
        , inert_safehask :: DictMap Ct
               -- Failed dictionary resolution due to Safe Haskell overlapping
@@ -634,34 +639,38 @@ 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 Given or Wanted (a ~N ty) in
+       inert_eqs.
 
-   * If (a -> ty) is in the model, then it is
-     as if we had an inert constraint [D] a ~N ty.
+   * 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
+   * Domain of the model = skolems + untouchables.
+     A touchable unification variable wouuld 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 costraints.
 
 Note [inert_eqs: the inert equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -783,7 +792,7 @@ The idea is that
 
 * 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.  Intuitivel, since 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.
 
@@ -1085,18 +1094,9 @@ 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)
+    * Always (G/W/D) kick out constraints that can be rewritten
+      (respecting flavours) by the new constraint. This is done
+      by kickOutRewritable.
 
   Then, when adding:
 
@@ -1104,7 +1104,7 @@ Note [Adding an inert canonical constraint the InertCans]
         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):
+        2. (DShadow) Do emitDerivedShadows
              For every inert G/W constraint c, st
               (a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]),
                   and
@@ -1114,18 +1114,18 @@ Note [Adding an inert canonical constraint the InertCans]
              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)
+          1. Add it to inert_eqs
+          2. Emit [D] a~ty
+       As a result of (2), the current model will rewrite teh new [D] a~ty
+       during canonicalisation, and then it'll be added to the model using
+       the steps of [Derived] above.
 
-     * [Given/Wanted] a ~R ty: just add it to inert_eqs
+     * [Representational equalities] 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:
+* 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]
@@ -1196,33 +1196,32 @@ add_inert_eq ics@(IC { inert_count = n
                      , inert_eqs = old_eqs
                      , inert_model = old_model })
              ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv
-                          , cc_rhs = rhs })
+                          , cc_rhs = _rhs })
+  | ReprEq <- eq_rel
+  = return new_ics
+
+--   | isGiven ev
+--   = return (new_ics { inert_model = extendVarEnv old_model tv ct }) }
+-- No no!   E.g.
+--   work-item [G] a ~ [b], model has [D] b ~ a.
+--   We must not add the given to the model as-is.  Instead,
+--   we put a shadow [D] a ~ [b] in the work-list
+--   When we process it, we'll rewrite to a ~ [a] and get an occurs check
+
   | isDerived ev
   = do { emitDerivedShadows ics tv
        ; return (ics { inert_model = extendVarEnv old_model tv ct }) }
 
-  | 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 ct isn't inert; emit it
-  = do { emitNewDerivedEq loc (eqRelRole eq_rel) (mkTyVarTy tv) rhs
+  | otherwise -- modelCanRewrite old_model rw_tvs   -- Shadow of new ct isn't inert; emit it
+  = do { emitNewDerived loc pred
        ; return new_ics }
-
-  | otherwise   -- Shadow of new constraint is inert wrt model
-                -- so extend model, and create shadows it can now rewrite
-  = do { emitDerivedShadows ics tv
-       ; return (new_ics { inert_model = new_model }) }
-
   where
     loc     = ctEvLoc ev
     pred    = ctEvPred ev
-    rw_tvs  = tyCoVarsOfType 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)
 
@@ -1233,14 +1232,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 [ ptext (sLit "tyvar =") <+> ppr new_tv
+              , ptext (sLit "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   $
@@ -1248,18 +1247,56 @@ 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!
       && (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 = 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 [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,
+becuase we've already added its superclasses.  So we won't re-add
+them.  If we forget the pend_sc flag, our cunning scheme for avoiding
+generating superclasses repeatedly will fail.
+
+See Trac #11379 for a case of this.
+-}
+
 modelCanRewrite :: InertModel -> TcTyCoVarSet -> Bool
 -- See Note [Emitting shadow constraints]
 -- True if there is any intersection between dom(model) and tvs
@@ -1285,12 +1322,9 @@ addInertCan ct
 
        -- Emit shadow derived if necessary
        -- See Note [Emitting shadow constraints]
-       ; let ev     = ctEvidence ct
-             pred   = ctEvPred ev
-             rw_tvs = rewritableTyCoVars ct
-
-       ; when (not (isDerived ev) && modelCanRewrite (inert_model ics) rw_tvs)
-              (emitNewDerived (ctEvLoc ev) pred)
+       ; let rw_tvs = rewritableTyCoVars ct
+       ; when (not (isDerivedCt ct) && modelCanRewrite (inert_model ics) rw_tvs)
+              (emitWork [mkShadowCt ct])
 
        ; traceTcS "addInertCan }" $ empty }
 
@@ -1328,39 +1362,23 @@ kickOutRewritable :: CtFlavourRole  -- Flavour/role of the equality that
                   -> 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)
-    -- Lemma (L2) in Note [Extending the inert equalities]
-  = 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
@@ -1388,20 +1406,24 @@ kickOutRewritable new_fr new_tv (IC { inert_eqs      = tv_eqs
       -- Kick out even insolubles; see Note [Kick out insolubles]
 
     fr_can_rewrite :: CtEvidence -> Bool
-    fr_can_rewrite = (new_fr `eqCanRewriteFR`) . ctEvFlavourRole
+    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 =  fr_can_rewrite ev
-                     && new_tv `elemVarSet` tyCoVarsOfType (ctEvPred ev)
-         -- See Note [Kicking out inert constraints]
+    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], TyVarEnv EqualCtList)
                  -> ([Ct], TyVarEnv EqualCtList)
@@ -1477,20 +1499,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!
+
+{- 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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2550,11 +2591,6 @@ emitWork cts
   = do { traceTcS "Emitting fresh work" (vcat (map ppr cts))
        ; updWorkListTcS (extendWorkListCts cts) }
 
-emitWorkCt :: Ct -> TcS ()
-emitWorkCt ct
-  = do { traceTcS "Emitting fresh (canonical) work" (ppr ct)
-       ; updWorkListTcS (extendWorkListCt ct) }
-
 emitInsoluble :: Ct -> TcS ()
 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
 emitInsoluble ct
diff --git a/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs b/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs
index f011bcf465..7cfd19f751 100644
--- a/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs
+++ b/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs
@@ -51,6 +51,50 @@ merge ::
 -}
 merge x y = mkMerge (merger x y) x y
 
+
+{- ------------- NASTY TYPE FOR merge -----------------
+   -- See Trac #11408
+
+   x:tx, y:ty
+   mkMerge @ gamma
+   merger @ alpha beta
+   merge :: tx -> ty -> tr
+
+Constraints generated:
+   gamma ~ MergerType alpha beta
+   UnmergedLeft gamma ~ tx
+   UnmergedRight gamma ~ ty
+   alpha ~ tx
+   beta ~ ty
+   tr ~ Merged gamma
+   Mergeable tx ty
+   Merger gamma
+
+One solve path:
+  gamma := t
+  tx := alpha := UnmergedLeft t
+  ty := beta  := UnmergedRight t
+
+  Mergeable (UnmergedLeft t) (UnmergedRight t)
+  Merger t
+  t ~ MergerType (UnmergedLeft t) (UnmergedRight t)
+
+  LEADS TO AMBIGUOUS TYPE
+
+Another solve path:
+  tx := alpha
+  ty := beta
+  gamma := MergerType alpha beta
+
+  UnmergedLeft (MergerType alpah beta) ~ alpha
+  UnmergedRight (MergerType alpah beta) ~ beta
+  Merger (MergerType alpha beta)
+  Mergeable alpha beta
+
+  LEADS TO NON-AMBIGUOUS TYPE
+---------------  -}
+
+
 data TakeRight a
 data TakeLeft a
 data DiscardRightHead a b c d
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 15c5b3e027..fe2688e109 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -270,3 +270,4 @@ test('T11067', normal, compile, [''])
 test('T10318', normal, compile, [''])
 test('UnusedTyVarWarnings', normal, compile, ['-W'])
 test('UnusedTyVarWarningsNamedWCs', normal, compile, ['-W'])
+test('T11408', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
index 9aef660dbd..b142cb18bd 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
@@ -1,6 +1,6 @@
 
 tcfail201.hs:17:56: error:
-    • Couldn't match type ‘a’ with ‘HsDoc id0’
+    • Couldn't match type ‘a’ with ‘HsDoc t0’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           gfoldl' :: forall (c :: * -> *) a.
@@ -8,7 +8,7 @@ tcfail201.hs:17:56: error:
                      -> (forall g. g -> c g) -> a -> c a
         at tcfail201.hs:15:12
       Expected type: c a
-        Actual type: c (HsDoc id0)
+        Actual type: c (HsDoc t0)
     • In the expression: z DocEmpty
       In a case alternative: DocEmpty -> z DocEmpty
       In the expression: case hsDoc of { DocEmpty -> z DocEmpty }