Comments only, mainly on superclasses

This tidies up all the comments about recursive superclasses
and when to add superclasses.  Lots of duplicate and contradictory
comments removed!

4 files changed, 264 insertions, 521 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 493e742058..ee8b201bcc 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -242,67 +242,95 @@ emitSuperclasses _ = panic "emit_superclasses of non-class!"
 {-
 Note [Adding superclasses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
-Since dictionaries are canonicalized only once in their lifetime, the
-place to add their superclasses is canonicalisation (The alternative
-would be to do it during constraint solving, but we'd have to be
-extremely careful to not repeatedly introduced the same superclass in
-our worklist). Here is what we do:
-
-For Givens:
-       We add all their superclasses as Givens.
-
-For Wanteds:
-       Generally speaking we want to be able to add superclasses of
-       wanteds for two reasons:
-
-       (1) Oportunities for improvement. Example:
-                  class (a ~ b) => C a b
-           Wanted constraint is: C alpha beta
-           We'd like to simply have C alpha alpha. Similar
-           situations arise in relation to functional dependencies.
-
-       (2) To have minimal constraints to quantify over:
-           For instance, if our wanted constraint is (Eq a, Ord a)
-           we'd only like to quantify over Ord a.
-
-       To deal with (1) above we only add the superclasses of wanteds
-       which may lead to improvement, that is: equality superclasses or
-       superclasses with functional dependencies.
-
-       We deal with (2) completely independently in TcSimplify. See
-       Note [Minimize by SuperClasses] in TcSimplify.
-
 
-       Moreover, in all cases the extra improvement constraints are
-       Derived. Derived constraints have an identity (for now), but
-       we don't do anything with their evidence. For instance they
-       are never used to rewrite other constraints.
-
-       See also [New Wanted Superclass Work] in TcInteract.
-
-
-For Deriveds:
-       We do nothing.
+Since dictionaries are canonicalized only once in their lifetime, the
+place to add their superclasses is canonicalisation.  See Note [Add
+superclasses only during canonicalisation].  Here is what we do:
+
+  Deriveds: Do nothing.
+
+  Givens:   Add all their superclasses as Givens.
+
+  Wanteds:  Add all their superclasses as Derived.
+            Not as Wanted: we don't need a proof.
+            Nor as Given: that leads to superclass loops.
+
+We also want to ensure minimal constraints to quantify over.  For
+instance, if our wanted constraint is (Eq a, Ord a) we'd only like to
+quantify over Ord a.  But we deal with that completely independently
+in TcSimplify. See Note [Minimize by SuperClasses] in TcSimplify.
+
+Examples of how adding superclasses as Derived is useful
+
+    --- Example 1
+        class C a b | a -> b
+    Suppose we want to solve
+         [G] C a b
+         [W] C a beta
+    Then adding [D] beta~b will let us solve it.
+
+    -- Example 2 (similar but using a type-equality superclass)
+        class (F a ~ b) => C a b
+    And try to sllve:
+         [G] C a b
+         [W] C a beta
+    Follow the superclass rules to add
+         [G] F a ~ b
+         [D] F a ~ beta
+    Now we we get [D] beta ~ b, and can solve that.
+
+Example of why adding superclass of a Wanted as a Given would
+be terrible, see Note [Do not add superclasses of solved dictionaries]
+in TcSMonad, which has this example:
+        class Ord a => C a where
+        instance Ord [a] => C [a] where ...
+Suppose we are trying to solve
+  [G] d1 : Ord a
+  [W] d2 : C [a]
+If we (bogusly) added the superclass of d2 as Gievn we'd have
+  [G] d1 : Ord a
+  [W] d2 : C [a]
+  [G] d3 : Ord [a]   -- Superclass of d2, bogus
+
+Then we'll use the instance decl to give
+  [G] d1 : Ord a     Solved: d2 : C [a] = $dfCList d4
+  [G] d3 : Ord [a]   -- Superclass of d2, bogus
+  [W] d4: Ord [a]
+
+ANd now we could bogusly solve d4 from d3.
+
+
+Note [Add superclasses only during canonicalisation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We add superclasses only during canonicalisation, on the passage
+from CNonCanonical to CDictCan.  A class constraint can be repeatedly
+rewritten, and there's no point in repeatedly adding its superclasses.
 
-Here's an example that demonstrates why we chose to NOT add
-superclasses during simplification: [Comes from ticket #4497]
+Here's a serious, but now out-dated example, from Trac #4497:
 
    class Num (RealOf t) => Normed t
    type family RealOf x
 
 Assume the generated wanted constraint is:
-   RealOf e ~ e, Normed e
+   [W] RealOf e ~ e
+   [W] Normed e
+
 If we were to be adding the superclasses during simplification we'd get:
-   Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf
+   [W] RealOf e ~ e
+   [W] Normed e
+   [D] RealOf e ~ fuv
+   [D] Num fuv
 ==>
-   e ~ uf, Num uf, Normed e, RealOf e ~ e
-==> [Spontaneous solve]
-   Num uf, Normed uf, RealOf uf ~ uf
+   e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv
 
-While looks exactly like our original constraint. If we add the superclass again we'd loop.
-By adding superclasses definitely only once, during canonicalisation, this situation can't
+While looks exactly like our original constraint. If we add the
+superclass of (Normed fuv) again we'd loop.  By adding superclasses
+definitely only once, during canonicalisation, this situation can't
 happen.
--}
+
+Mind you, now that Wanteds cannot rewrite Derived, I think this particular
+situation can't happen.
+  -}
 
 newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS ()
 -- Returns superclasses, see Note [Adding superclasses]
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 1955c1f218..c8746ff00e 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -1105,6 +1105,9 @@ See Trac #3731, #4809, #5751, #5913, #6117, #6161, which all
 describe somewhat more complicated situations, but ones
 encountered in practice.
 
+See also tests tcrun020, tcrun021, tcrun033
+
+
 ----- THE PROBLEM --------
 The problem is that it is all too easy to create a class whose
 superclass is bottom when it should not be.
@@ -1190,8 +1193,6 @@ that is *not* smaller than the target so we can't take *its*
 superclasses.  As a result the program is rightly rejected, unless you
 add (Super (Fam a)) to the context of (i3).
 
-
-
 Note [Silent superclass arguments] (historical interest)
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 NB1: this note describes our *old* solution to the
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 41f508daef..8b85a712e9 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -901,8 +901,6 @@ solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
 -- Precondition: kind(xi) is a sub-kind of kind(tv)
 -- Precondition: CtEvidence is Wanted or Derived
 -- Precondition: CtEvidence is nominal
--- See [New Wanted Superclass Work] to see why solveByUnification
---     must work for Derived as well as Wanted
 -- Returns: workItem where
 --        workItem = the new Given constraint
 --
@@ -1100,342 +1098,6 @@ double unifications is the main reason we disallow touchable
 unification variables as RHS of type family equations: F xis ~ alpha.
 
 
-
-Note [Superclasses and recursive dictionaries]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-    Overlaps with Note [SUPERCLASS-LOOP 1]
-                  Note [SUPERCLASS-LOOP 2]
-                  Note [Recursive instances and superclases]
-    ToDo: check overlap and delete redundant stuff
-
-Right before adding a given into the inert set, we must
-produce some more work, that will bring the superclasses
-of the given into scope. The superclass constraints go into
-our worklist.
-
-When we simplify a wanted constraint, if we first see a matching
-instance, we may produce new wanted work. To (1) avoid doing this work
-twice in the future and (2) to handle recursive dictionaries we may ``cache''
-this item as given into our inert set WITHOUT adding its superclass constraints,
-otherwise we'd be in danger of creating a loop [In fact this was the exact reason
-for doing the isGoodRecEv check in an older version of the type checker].
-
-But now we have added partially solved constraints to the worklist which may
-interact with other wanteds. Consider the example:
-
-Example 1:
-
-    class Eq b => Foo a b        --- 0-th selector
-    instance Eq a => Foo [a] a   --- fooDFun
-
-and wanted (Foo [t] t). We are first going to see that the instance matches
-and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
-       d1 :_g Foo [t] t                 d1 := EvDFunApp fooDFun d3
-Our work list is going to contain a new *wanted* goal
-       d3 :_w Eq t
-
-Ok, so how do we get recursive dictionaries, at all:
-
-Example 2:
-
-    data D r = ZeroD | SuccD (r (D r));
-
-    instance (Eq (r (D r))) => Eq (D r) where
-        ZeroD     == ZeroD     = True
-        (SuccD a) == (SuccD b) = a == b
-        _         == _         = False;
-
-    equalDC :: D [] -> D [] -> Bool;
-    equalDC = (==);
-
-We need to prove (Eq (D [])). Here's how we go:
-
-        d1 :_w Eq (D [])
-
-by instance decl, holds if
-        d2 :_w Eq [D []]
-        where   d1 = dfEqD d2
-
-*BUT* we have an inert set which gives us (no superclasses):
-        d1 :_g Eq (D [])
-By the instance declaration of Eq we can show the 'd2' goal if
-        d3 :_w Eq (D [])
-        where   d2 = dfEqList d3
-                d1 = dfEqD d2
-Now, however this wanted can interact with our inert d1 to set:
-        d3 := d1
-and solve the goal. Why was this interaction OK? Because, if we chase the
-evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
-are really setting
-        d3 := dfEqD2 (dfEqList d3)
-which is FINE because the use of d3 is protected by the instance function
-applications.
-
-So, our strategy is to try to put solved wanted dictionaries into the
-inert set along with their superclasses (when this is meaningful,
-i.e. when new wanted goals are generated) but solve a wanted dictionary
-from a given only in the case where the evidence variable of the
-wanted is mentioned in the evidence of the given (recursively through
-the evidence binds) in a protected way: more instance function applications
-than superclass selectors.
-
-Here are some more examples from GHC's previous type checker
-
-
-Example 3:
-This code arises in the context of "Scrap Your Boilerplate with Class"
-
-    class Sat a
-    class Data ctx a
-    instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
-    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2
-
-    class Data Maybe a => Foo a
-
-    instance Foo t => Sat (Maybe t)                             -- dfunSat
-
-    instance Data Maybe a => Foo a                              -- dfunFoo1
-    instance Foo a        => Foo [a]                            -- dfunFoo2
-    instance                 Foo [Char]                         -- dfunFoo3
-
-Consider generating the superclasses of the instance declaration
-         instance Foo a => Foo [a]
-
-So our problem is this
-    [G] d0 : Foo t
-    [W] d1 : Data Maybe [t]   -- Desired superclass
-
-We may add the given in the inert set, along with its superclasses
-[assuming we don't fail because there is a matching instance, see
- topReactionsStage, given case ]
-  Inert:
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  WorkList
-    [W] d1 : Data Maybe [t]
-
-Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
-  Inert:
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-  WorkList
-    [W] d2 : Sat (Maybe [t])
-    [W] d3 : Data Maybe t
-
-Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
-  Inert:
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-        d2 : Sat (Maybe [t])
-  WorkList:
-    [W] d3 : Data Maybe t
-    [W] d4 : Foo [t]
-
-Now, we can just solve d3 from d01; d3 := d01
-  Inert
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-        d2 : Sat (Maybe [t])
-  WorkList
-    [W] d4 : Foo [t]
-
-Now, solve d4 using dfunFoo2;  d4 := dfunFoo2 d5
-  Inert
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-        d2 : Sat (Maybe [t])
-        d4 : Foo [t]
-  WorkList:
-    [W] d5 : Foo t
-
-Now, d5 can be solved! d5 := d0
-
-Result
-   d1 := dfunData2 d2 d3
-   d2 := dfunSat d4
-   d3 := d01
-   d4 := dfunFoo2 d5
-   d5 := d0
-
-      d0 :_g Foo t
-      d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
-      d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
-      d4 :_g Foo [t]                  d4 := dfunFoo2 d5
-      d5 :_g Foo t                    d5 := dfunFoo1 d7
-  WorkList:
-      d7 :_w Data Maybe t
-      d6 :_g Data Maybe [t]
-      d8 :_g Data Maybe t            d8 := EvDictSuperClass d5 0
-      d01 :_g Data Maybe t
-
-Now, two problems:
-   [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
-       we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
-       that must not be used (look at case interactInert where both inert and workitem
-       are givens). So we have several options:
-       - Drop the workitem always (this will drop d8)
-              This feels very unsafe -- what if the work item was the "good" one
-              that should be used later to solve another wanted?
-       - Don't drop anyone: the inert set may contain multiple givens!
-              [This is currently implemented]
-
-The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
-  [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
-      d7. Now the [isRecDictEv] function in the ineration solver
-      [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
-      precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
-
-      So, no interaction happens there. Then we meet d01 and there is no recursion
-      problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
-
-Note [SUPERCLASS-LOOP 1]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We have to be very, very careful when generating superclasses, lest we
-accidentally build a loop. Here's an example:
-
-  class S a
-
-  class S a => C a where { opc :: a -> a }
-  class S b => D b where { opd :: b -> b }
-
-  instance C Int where
-     opc = opd
-
-  instance D Int where
-     opd = opc
-
-From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
-Simplifying, we may well get:
-        $dfCInt = :C ds1 (opd dd)
-        dd  = $dfDInt
-        ds1 = $p1 dd
-Notice that we spot that we can extract ds1 from dd.
-
-Alas!  Alack! We can do the same for (instance D Int):
-
-        $dfDInt = :D ds2 (opc dc)
-        dc  = $dfCInt
-        ds2 = $p1 dc
-
-And now we've defined the superclass in terms of itself.
-Two more nasty cases are in
-        tcrun021
-        tcrun033
-
-Solution:
-  - Satisfy the superclass context *all by itself*
-    (tcSimplifySuperClasses)
-  - And do so completely; i.e. no left-over constraints
-    to mix with the constraints arising from method declarations
-
-
-Note [SUPERCLASS-LOOP 2]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We need to be careful when adding "the constaint we are trying to prove".
-Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
-
-        class Ord a => C a where
-        instance Ord [a] => C [a] where ...
-
-Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
-superclasses of C [a] to avails.  But we must not overwrite the binding
-for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
-build a loop!
-
-Here's another variant, immortalised in tcrun020
-        class Monad m => C1 m
-        class C1 m => C2 m x
-        instance C2 Maybe Bool
-For the instance decl we need to build (C1 Maybe), and it's no good if
-we run around and add (C2 Maybe Bool) and its superclasses to the avails
-before we search for C1 Maybe.
-
-Here's another example
-        class Eq b => Foo a b
-        instance Eq a => Foo [a] a
-If we are reducing
-        (Foo [t] t)
-
-we'll first deduce that it holds (via the instance decl).  We must not
-then overwrite the Eq t constraint with a superclass selection!
-
-At first I had a gross hack, whereby I simply did not add superclass constraints
-in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
-because it lost legitimate superclass sharing, and it still didn't do the job:
-I found a very obscure program (now tcrun021) in which improvement meant the
-simplifier got two bites a the cherry... so something seemed to be an Stop
-first time, but reducible next time.
-
-Now we implement the Right Solution, which is to check for loops directly
-when adding superclasses.  It's a bit like the occurs check in unification.
-
-Note [Recursive instances and superclases]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this code, which arises in the context of "Scrap Your
-Boilerplate with Class".
-
-    class Sat a
-    class Data ctx a
-    instance  Sat (ctx Char)             => Data ctx Char
-    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
-
-    class Data Maybe a => Foo a
-
-    instance Foo t => Sat (Maybe t)
-
-    instance Data Maybe a => Foo a
-    instance Foo a        => Foo [a]
-    instance                 Foo [Char]
-
-In the instance for Foo [a], when generating evidence for the superclasses
-(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
-Using the instance for Data, we therefore need
-        (Sat (Maybe [a], Data Maybe a)
-But we are given (Foo a), and hence its superclass (Data Maybe a).
-So that leaves (Sat (Maybe [a])).  Using the instance for Sat means
-we need (Foo [a]).  And that is the very dictionary we are bulding
-an instance for!  So we must put that in the "givens".  So in this
-case we have
-        Given:  Foo a, Foo [a]
-        Wanted: Data Maybe [a]
-
-BUT we must *not not not* put the *superclasses* of (Foo [a]) in
-the givens, which is what 'addGiven' would normally do. Why? Because
-(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
-by selecting a superclass from Foo [a], which simply makes a loop.
-
-On the other hand we *must* put the superclasses of (Foo a) in
-the givens, as you can see from the derivation described above.
-
-Conclusion: in the very special case of tcSimplifySuperClasses
-we have one 'given' (namely the "this" dictionary) whose superclasses
-must not be added to 'givens' by addGiven.
-
-There is a complication though.  Suppose there are equalities
-      instance (Eq a, a~b) => Num (a,b)
-Then we normalise the 'givens' wrt the equalities, so the original
-given "this" dictionary is cast to one of a different type.  So it's a
-bit trickier than before to identify the "special" dictionary whose
-superclasses must not be added. See test
-   indexed-types/should_run/EqInInstance
-
-We need a persistent property of the dictionary to record this
-special-ness.  Current I'm using the InstLocOrigin (a bit of a hack,
-but cool), which is maintained by dictionary normalisation.
-Specifically, the InstLocOrigin is
-             NoScOrigin
-then the no-superclass thing kicks in.  WATCH OUT if you fiddle
-with InstLocOrigin!
-
-
 ************************************************************************
 *                                                                      *
 *          Functional dependencies, instantiation of equations
@@ -1498,9 +1160,6 @@ doTopReact :: InertSet -> WorkItem -> TcS (StopOrContinue Ct)
 --   (a) The place to add superclasses in not here in doTopReact stage.
 --       Instead superclasses are added in the worklist as part of the
 --       canonicalization process. See Note [Adding superclasses].
---
---   (b) See Note [Given constraint that matches an instance declaration]
---       for some design decisions for given dictionaries.
 
 doTopReact inerts work_item
   = do { traceTcS "doTopReact" (ppr work_item)
@@ -1834,113 +1493,6 @@ This should probably be well typed, with
 
 So the inner binding for ?x::Bool *overrides* the outer one.
 Hence a work-item Given overrides an inert-item Given.
-
-Note [Given constraint that matches an instance declaration]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What should we do when we discover that one (or more) top-level
-instances match a given (or solved) class constraint? We have
-two possibilities:
-
-  1. Reject the program. The reason is that there may not be a unique
-     best strategy for the solver. Example, from the OutsideIn(X) paper:
-       instance P x => Q [x]
-       instance (x ~ y) => R [x] y
-
-       wob :: forall a b. (Q [b], R b a) => a -> Int
-
-       g :: forall a. Q [a] => [a] -> Int
-       g x = wob x
-
-       will generate the impliation constraint:
-            Q [a] => (Q [beta], R beta [a])
-       If we react (Q [beta]) with its top-level axiom, we end up with a
-       (P beta), which we have no way of discharging. On the other hand,
-       if we react R beta [a] with the top-level we get  (beta ~ a), which
-       is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
-       now solvable by the given Q [a].
-
-     However, this option is restrictive, for instance [Example 3] from
-     Note [Recursive instances and superclases] will fail to work.
-
-  2. Ignore the problem, hoping that the situations where there exist indeed
-     such multiple strategies are rare: Indeed the cause of the previous
-     problem is that (R [x] y) yields the new work (x ~ y) which can be
-     *spontaneously* solved, not using the givens.
-
-We are choosing option 2 below but we might consider having a flag as well.
-
-
-Note [New Wanted Superclass Work]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Even in the case of wanted constraints, we may add some superclasses
-as new given work. The reason is:
-
-        To allow FD-like improvement for type families. Assume that
-        we have a class
-             class C a b | a -> b
-        and we have to solve the implication constraint:
-             C a b => C a beta
-        Then, FD improvement can help us to produce a new wanted (beta ~ b)
-
-        We want to have the same effect with the type family encoding of
-        functional dependencies. Namely, consider:
-             class (F a ~ b) => C a b
-        Now suppose that we have:
-               given: C a b
-               wanted: C a beta
-        By interacting the given we will get given (F a ~ b) which is not
-        enough by itself to make us discharge (C a beta). However, we
-        may create a new derived equality from the super-class of the
-        wanted constraint (C a beta), namely derived (F a ~ beta).
-        Now we may interact this with given (F a ~ b) to get:
-                  derived :  beta ~ b
-        But 'beta' is a touchable unification variable, and hence OK to
-        unify it with 'b', replacing the derived evidence with the identity.
-
-        This requires trySpontaneousSolve to solve *derived*
-        equalities that have a touchable in their RHS, *in addition*
-        to solving wanted equalities.
-
-We also need to somehow use the superclasses to quantify over a minimal,
-constraint see note [Minimize by Superclasses] in TcSimplify.
-
-
-Finally, here is another example where this is useful.
-
-Example 1:
-----------
-   class (F a ~ b) => C a b
-And we are given the wanteds:
-      w1 : C a b
-      w2 : C a c
-      w3 : b ~ c
-We surely do *not* want to quantify over (b ~ c), since if someone provides
-dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
-of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
-
-     Step 1: We will get new *given* superclass work,
-             provisionally to our solving of w1 and w2
-
-               g1: F a ~ b, g2 : F a ~ c,
-               w1 : C a b, w2 : C a c, w3 : b ~ c
-
-             The evidence for g1 and g2 is a superclass evidence term:
-
-               g1 := sc w1, g2 := sc w2
-
-     Step 2: The givens will solve the wanted w3, so that
-               w3 := sym (sc w1) ; sc w2
-
-     Step 3: Now, one may naively assume that then w2 can be solve from w1
-             after rewriting with the (now solved equality) (b ~ c).
-
-             But this rewriting is ruled out by the isGoodRectDict!
-
-Conclusion, we will (correctly) end up with the unsolved goals
-    (C a b, C a c)
-
-NB: The desugarer needs be more clever to deal with equalities
-    that participate in recursive dictionary bindings.
 -}
 
 data LookupInstResult
@@ -2068,22 +1620,27 @@ matchClassInst inerts clas tys loc
 {-
 Note [Instance and Given overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Assume that we have an inert set that looks as follows:
-       [Given] D [Int]
-And an instance declaration:
-       instance C a => D [a]
-A new wanted comes along of the form:
-       [Wanted] D [alpha]
-
-One possibility is to apply the instance declaration which will leave us
-with an unsolvable goal (C alpha). However, later on a new constraint may
-arise (for instance due to a functional dependency between two later dictionaries),
-that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
-will be transformed to [Wanted] D [Int], which could have been discharged by the given.
-
-The solution is that in matchClassInst and eventually in topReact, we get back with
-a matching instance, only when there is no Given in the inerts which is unifiable to
-this particular dictionary.
+Example, from the OutsideIn(X) paper:
+       instance P x => Q [x]
+       instance (x ~ y) => R y [x]
+
+       wob :: forall a b. (Q [b], R b a) => a -> Int
+
+       g :: forall a. Q [a] => [a] -> Int
+       g x = wob x
+
+This will generate the impliation constraint:
+            Q [a] => (Q [beta], R beta [a])
+If we react (Q [beta]) with its top-level axiom, we end up with a
+(P beta), which we have no way of discharging. On the other hand,
+if we react R beta [a] with the top-level we get  (beta ~ a), which
+is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
+now solvable by the given Q [a].
+
+The solution is that:
+  In matchClassInst (and thus in topReact), we return a matching
+  instance only when there is no Given in the inerts which is
+  unifiable to this particular dictionary.
 
 The end effect is that, much as we do for overlapping instances, we delay choosing a
 class instance if there is a possibility of another instance OR a given to match our
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index a04bf9f43c..56c8a9ab2f 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -378,6 +378,165 @@ Type-family equations, of form (ev : F tys ~ ty), live in three places
     using w3 itself!
 
   * The inert_funeqs are un-solved but fully processed and in the InertCans.
+
+Note [Solved dictionaries]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we apply a top-level instance declararation, we add the "solved"
+dictionary to the inert_solved_dicts.  In general, we use it to avoid
+creating a new EvVar when we have a new goal that we have solved in
+the past.
+
+But in particular, we can use it to create *recursive* dicationaries.
+The simplest, degnerate case is
+    instance C [a] => C [a] where ...
+If we have
+    [W] d1 :: C [x]
+then we can apply the instance to get
+    d1 = $dfCList d
+    [W] d2 :: C [x]
+Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
+    d1 = $dfCList d
+    d2 = d1
+
+See Note [Example of recursive dictionaries]
+Other notes about solved dictionaries
+
+* See also Note [Do not add superclasses of solved dictionaries]
+
+* The inert_solved_dicts field is not rewritten by equalities, so it may
+  get out of date.
+
+Note [Do not add superclasses of solved dictionaries]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Every member of inert_solved_dicts is the result of applying a dictionary
+function, NOT of applying superclass selection to anything.
+Consider
+
+        class Ord a => C a where
+        instance Ord [a] => C [a] where ...
+
+Suppose we are trying to solve
+  [G] d1 : Ord a
+  [W] d2 : C [a]
+
+Then we'll use the instance decl to give
+
+  [G] d1 : Ord a     Solved: d2 : C [a] = $dfCList d3
+  [W] d3 : Ord [a]
+
+We must not add d4 : Ord [a] to the 'solved' set (by taking the
+superclass of d2), otherwise we'll use it to solve d3, without ever
+using d1, which would be a catastrophe.
+
+Solution: when extending the solved dictionaries, do not add superclasses.
+That's why each element of the inert_solved_dicts is the result of applying
+a dictionary function.
+
+Note [Example of recursive dictionaries]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--- Example 1
+
+    data D r = ZeroD | SuccD (r (D r));
+
+    instance (Eq (r (D r))) => Eq (D r) where
+        ZeroD     == ZeroD     = True
+        (SuccD a) == (SuccD b) = a == b
+        _         == _         = False;
+
+    equalDC :: D [] -> D [] -> Bool;
+    equalDC = (==);
+
+We need to prove (Eq (D [])). Here's how we go:
+
+   [W] d1 : Eq (D [])
+By instance decl of Eq (D r):
+   [W] d2 : Eq [D []]      where   d1 = dfEqD d2
+By instance decl of Eq [a]:
+   [W] d3 : Eq (D [])      where   d2 = dfEqList d3
+                                   d1 = dfEqD d2
+Now this wanted can interact with our "solved" d1 to get:
+    d3 = d1
+
+-- Example 2:
+This code arises in the context of "Scrap Your Boilerplate with Class"
+
+    class Sat a
+    class Data ctx a
+    instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
+    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2
+
+    class Data Maybe a => Foo a
+
+    instance Foo t => Sat (Maybe t)                             -- dfunSat
+
+    instance Data Maybe a => Foo a                              -- dfunFoo1
+    instance Foo a        => Foo [a]                            -- dfunFoo2
+    instance                 Foo [Char]                         -- dfunFoo3
+
+Consider generating the superclasses of the instance declaration
+         instance Foo a => Foo [a]
+
+So our problem is this
+    [G] d0 : Foo t
+    [W] d1 : Data Maybe [t]   -- Desired superclass
+
+We may add the given in the inert set, along with its superclasses
+  Inert:
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  WorkList
+    [W] d1 : Data Maybe [t]
+
+Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
+  Inert:
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+  WorkList:
+    [W] d2 : Sat (Maybe [t])
+    [W] d3 : Data Maybe t
+
+Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
+  Inert:
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+        d2 : Sat (Maybe [t])
+  WorkList:
+    [W] d3 : Data Maybe t
+    [W] d4 : Foo [t]
+
+Now, we can just solve d3 from d01; d3 := d01
+  Inert
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+        d2 : Sat (Maybe [t])
+  WorkList
+    [W] d4 : Foo [t]
+
+Now, solve d4 using dfunFoo2;  d4 := dfunFoo2 d5
+  Inert
+    [G] d0  : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+        d2 : Sat (Maybe [t])
+        d4 : Foo [t]
+  WorkList:
+    [W] d5 : Foo t
+
+Now, d5 can be solved! d5 := d0
+
+Result
+   d1 := dfunData2 d2 d3
+   d2 := dfunSat d4
+   d3 := d01
+   d4 := dfunFoo2 d5
+   d5 := d0
 -}
 
 -- All Given (fully known) or Wanted or Derived
@@ -435,11 +594,8 @@ data InertSet
 
        , inert_solved_dicts   :: DictMap CtEvidence
               -- Of form ev :: C t1 .. tn
-              -- Always the result of using a top-level instance declaration
-              -- - Used to avoid creating a new EvVar when we have a new goal
-              --   that we have solved in the past
-              -- - Stored not necessarily as fully rewritten
-              --   (ToDo: rewrite lazily when we lookup)
+              -- See Note [Solved dictionaries]
+              -- and Note [Do not add superclasses of solved dictionaries]
        }
 
 instance Outputable InertCans where
@@ -514,6 +670,7 @@ insertInertItemTcS item
 
 addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
 -- Add a new item in the solved set of the monad
+-- See Note [Solved dictionaries]
 addSolvedDict item cls tys
   | isIPPred (ctEvPred item)    -- Never cache "solved" implicit parameters (not sure why!)
   = return ()