Fix solveOneFromTheOther for RecursiveSuperclasses

This patch fixes the redundant superclass expansion
in Trac #14774.

The main change is to fix TcInterac.solveOneFromTheOther, so
that it does not prefer a work-item with a binding if that binding
transitively depends on the inert item we are comparing it with.

Explained in Note [Replacement vs keeping] in TcInert, esp
item (c) of the "Constraints coming from the same level" part.

To make this work I refactored out a new function
TcEvidence.findNeededEvVars, which was previously buried
inside TcSimplify.neededEvVars.

I added quite a few more comments and signposts about superclass
expansion.

8 files changed, 119 insertions, 43 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 1e1fa397fd..868d785b18 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -241,19 +241,19 @@ So here's the plan:
 
 1. Eagerly generate superclasses for given (but not wanted)
    constraints; see Note [Eagerly expand given superclasses].
-   This is done in canClassNC, when we take a non-canonical constraint
-   and cannonicalise it.
+   This is done using mkStrictSuperClasses in canClassNC, when
+   we take a non-canonical Given constraint and cannonicalise it.
 
    However stop if you encounter the same class twice.  That is,
-   expand eagerly, but have a conservative termination condition: see
-   Note [Expanding superclasses] in TcType.
+   mkStrictSuperClasses expands eagerly, but has a conservative
+   termination condition: see Note [Expanding superclasses] in TcType.
 
 2. Solve the wanteds as usual, but do no further expansion of
    superclasses for canonical CDictCans in solveSimpleGivens or
    solveSimpleWanteds; Note [Danger of adding superclasses during solving]
 
-   However, /do/ continue to eagerly expand superlasses for /given/
-   non-canonical constraints (canClassNC does this).  As Trac #12175
+   However, /do/ continue to eagerly expand superlasses for new /given/
+   /non-canonical/ constraints (canClassNC does this).  As Trac #12175
    showed, a type-family application can expand to a class constraint,
    and we want to see its superclasses for just the same reason as
    Note [Eagerly expand given superclasses].
@@ -261,9 +261,11 @@ So here's the plan:
 3. If we have any remaining unsolved wanteds
         (see Note [When superclasses help] in TcRnTypes)
    try harder: take both the Givens and Wanteds, and expand
-   superclasses again.  This may succeed in generating (a finite
-   number of) extra Givens, and extra Deriveds. Both may help the
-   proof.  This is done in TcSimplify.expandSuperClasses.
+   superclasses again.  See the calls to expandSuperClasses in
+   TcSimplify.simpl_loop and solveWanteds.
+
+   This may succeed in generating (a finite number of) extra Givens,
+   and extra Deriveds. Both may help the proof.
 
 4. Go round to (2) again.  This loop (2,3,4) is implemented
    in TcSimplify.simpl_loop.
@@ -285,10 +287,31 @@ Why do we do this?  Two reasons:
 When we take a CNonCanonical or CIrredCan, but end up classifying it
 as a CDictCan, we set the cc_pend_sc flag to False.
 
+Note [Superclass loops]
+~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+  class C a => D a
+  class D a => C a
+
+Then, when we expand superclasses, we'll get back to the self-same
+predicate, so we have reached a fixpoint in expansion and there is no
+point in fruitlessly expanding further.  This case just falls out from
+our strategy.  Consider
+  f :: C a => a -> Bool
+  f x = x==x
+Then canClassNC gets the [G] d1: C a constraint, and eager emits superclasses
+G] d2: D a, [G] d3: C a (psc).  (The "psc" means it has its sc_pend flag set.)
+When processing d3 we find a match with d1 in the inert set, and we always
+keep the inert item (d1) if possible: see Note [Replacement vs keeping] in
+TcInteract.  So d3 dies a quick, happy death.
+
 Note [Eagerly expand given superclasses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In step (1) of Note [The superclass story], why do we eagerly expand
-Given superclasses by one layer?  Mainly because of some very obscure
+Given superclasses by one layer?  (By "one layer" we mean expand transitively
+until you meet the same class again -- the conservative criterion embodied
+in expandSuperClasses.  So a "layer" might be a whole stack of superclasses.)
+We do this eagerly for Givens mainly because of some very obscure
 cases like this:
 
    instance Bad a => Eq (T a)
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index bee70451e0..0930d7afd8 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -21,7 +21,7 @@ module TcEvidence (
   -- EvTerm (already a CoreExpr)
   EvTerm(..), EvExpr,
   evId, evCoercion, evCast, evDFunApp,  evSelector,
-  mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable,
+  mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
 
   evTermCoercion,
   EvCallStack(..),
@@ -765,6 +765,33 @@ evTermCoercion (EvExpr (Coercion co)) = co
 evTermCoercion (EvExpr (Cast tm co))  = mkCoCast (evTermCoercion (EvExpr tm)) co
 evTermCoercion tm                     = pprPanic "evTermCoercion" (ppr tm)
 
+
+{-
+************************************************************************
+*                                                                      *
+                  Free variables
+*                                                                      *
+************************************************************************
+-}
+
+findNeededEvVars :: EvBindMap -> VarSet -> VarSet
+findNeededEvVars ev_binds seeds
+  = transCloVarSet also_needs seeds
+  where
+   also_needs :: VarSet -> VarSet
+   also_needs needs = nonDetFoldUniqSet add emptyVarSet needs
+     -- It's OK to use nonDetFoldUFM here because we immediately
+     -- forget about the ordering by creating a set
+
+   add :: Var -> VarSet -> VarSet
+   add v needs
+     | Just ev_bind <- lookupEvBind ev_binds v
+     , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
+     , is_given
+     = evVarsOfTerm rhs `unionVarSet` needs
+     | otherwise
+     = needs
+
 evVarsOfTerm :: EvTerm -> VarSet
 evVarsOfTerm (EvExpr e)         = exprSomeFreeVars isEvVar e
 evVarsOfTerm (EvTypeable _ ev)  = evVarsOfTypeable ev
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 59eea70048..9a2f64d672 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -568,6 +568,8 @@ solveOneFromTheOther ev_i ev_w
      loc_w = ctEvLoc ev_w
      lvl_i = ctLocLevel loc_i
      lvl_w = ctLocLevel loc_w
+     ev_id_i = ctEvEvId ev_i
+     ev_id_w = ctEvEvId ev_w
 
      different_level_strategy
        | isIPPred pred, lvl_w > lvl_i = KeepWork
@@ -584,14 +586,15 @@ solveOneFromTheOther ev_i ev_w
        | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
        = KeepInert
 
-       | has_binding binds ev_w
-       , not (has_binding binds ev_i)
+       | has_binding binds ev_id_w
+       , not (has_binding binds ev_id_i)
+       , not (ev_id_i `elemVarSet` findNeededEvVars binds (unitVarSet ev_id_w))
        = KeepWork
 
        | otherwise
        = KeepInert
 
-     has_binding binds ev = isJust (lookupEvBind binds (ctEvEvId ev))
+     has_binding binds ev_id = isJust (lookupEvBind binds ev_id)
 
 {-
 Note [Replacement vs keeping]
@@ -616,22 +619,34 @@ we keep?  More subtle than you might think!
 
   * Constraints coming from the same level (i.e. same implication)
 
-       - Always get rid of InstSC ones if possible, since they are less
-         useful for solving.  If both are InstSC, choose the one with
-         the smallest TypeSize
-         See Note [Solving superclass constraints] in TcInstDcls
+       (a) Always get rid of InstSC ones if possible, since they are less
+           useful for solving.  If both are InstSC, choose the one with
+           the smallest TypeSize
+           See Note [Solving superclass constraints] in TcInstDcls
 
-       - Keep the one that has a non-trivial evidence binding.
-            Example:  f :: (Eq a, Ord a) => blah
-            then we may find [G] d3 :: Eq a
-                             [G] d2 :: Eq a
-              with bindings  d3 = sc_sel (d1::Ord a)
+       (b) Keep the one that has a non-trivial evidence binding.
+              Example:  f :: (Eq a, Ord a) => blah
+              then we may find [G] d3 :: Eq a
+                               [G] d2 :: Eq a
+                with bindings  d3 = sc_sel (d1::Ord a)
             We want to discard d2 in favour of the superclass selection from
             the Ord dictionary.
-         Why? See Note [Tracking redundant constraints] in TcSimplify again.
-
-  * Finally, when there is still a choice, use IRKeep rather than
-    IRReplace, to avoid unnecessary munging of the inert set.
+            Why? See Note [Tracking redundant constraints] in TcSimplify again.
+
+       (c) But don't do (b) if the evidence binding depends transitively on the
+           one without a binding.  Example (with RecursiveSuperClasses)
+              class C a => D a
+              class D a => C a
+           Inert:     d1 :: C a, d2 :: D a
+           Binds:     d3 = sc_sel d2, d2 = sc_sel d1
+           Work item: d3 :: C a
+           Then it'd be ridiculous to replace d1 with d3 in the inert set!
+           Hence the findNeedEvVars test.  See Trac #14774.
+
+  * Finally, when there is still a choice, use KeepInert rather than
+    KeepWork, for two reasons:
+      - to avoid unnecessary munging of the inert set.
+      - to cut off superclass loops; see Note [Superclass loops] in TcCanonical
 
 Doing the depth-check for implicit parameters, rather than making the work item
 always override, is important.  Consider
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index b92ebfd862..53be7926ef 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -1463,7 +1463,7 @@ expandSuperClasses unsolved
   | not (anyBag superClassesMightHelp unsolved)
   = return (True, unsolved)
   | otherwise
-  = do { traceTcS "expandSuperClasses {" empty
+  = do { traceTcS "expandSuperClasses {" (ppr unsolved)
        ; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
              get acc ct | Just ct' <- isPendingScDict ct
                         = (ct':acc, ct')
@@ -1474,7 +1474,10 @@ expandSuperClasses unsolved
          then do { traceTcS "End expandSuperClasses no-op }" empty
                  ; return (True, unsolved) }
          else
-    do { new_given  <- makeSuperClasses pending_given
+    do { traceTcS "expandSuperClasses mid"
+             (vcat [ text "pending_given:" <+> ppr pending_given
+                   , text "pending_wanted:" <+> ppr pending_wanted ])
+       ; new_given  <- makeSuperClasses pending_given
        ; solveSimpleGivens new_given
        ; new_wanted <- makeSuperClasses pending_wanted
        ; traceTcS "End expandSuperClasses }"
@@ -1696,7 +1699,7 @@ neededEvVars implic@(Implic { ic_info = info
       ; let seeds1        = foldrBag add_implic_seeds old_needs implics
             seeds2        = foldEvBindMap add_wanted seeds1 ev_binds
             seeds3        = seeds2 `unionVarSet` tcvs
-            need_inner    = transCloVarSet (also_needs ev_binds) seeds3
+            need_inner    = findNeededEvVars ev_binds seeds3
             live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds
             need_outer    = foldEvBindMap del_ev_bndr need_inner live_ev_binds
                             `delVarSetList` givens
@@ -1729,19 +1732,6 @@ neededEvVars implic@(Implic { ic_info = info
      | is_given  = needs  -- Add the rhs vars of the Wanted bindings only
      | otherwise = evVarsOfTerm rhs `unionVarSet` needs
 
-   also_needs :: EvBindMap -> VarSet -> VarSet
-   also_needs ev_binds needs
-     = nonDetFoldUniqSet add emptyVarSet needs
-     -- It's OK to use nonDetFoldUFM here because we immediately
-     -- forget about the ordering by creating a set
-     where
-       add v needs
-        | Just ev_bind <- lookupEvBind ev_binds v
-        , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
-        , is_given
-        = evVarsOfTerm rhs `unionVarSet` needs
-        | otherwise
-        = needs
 
 {- Note [Delete dead Given evidence bindings]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/typecheck/should_compile/Makefile b/testsuite/tests/typecheck/should_compile/Makefile
index a7780efb0f..c3065f3cd2 100644
--- a/testsuite/tests/typecheck/should_compile/Makefile
+++ b/testsuite/tests/typecheck/should_compile/Makefile
@@ -6,6 +6,10 @@ T14434:
 	'$(TEST_HC)' $(TEST_HC_OPTS) -c T14434.hs -ddump-simpl | grep toStringX
          # Expecting toStringX = toString, not discarding argument
 
+T14774:
+	'$(TEST_HC)' $(TEST_HC_OPTS) -c T14774.hs -ddump-simpl | grep p1D
+         # Expecting no superclass selections to actually happen
+
 tc170:
 	$(RM) Tc170_Aux.hi Tc170_Aux.o tc170.hi tc170.o
 	'$(TEST_HC)' $(TEST_HC_OPTS) -c Tc170_Aux.hs
diff --git a/testsuite/tests/typecheck/should_compile/T14774.hs b/testsuite/tests/typecheck/should_compile/T14774.hs
new file mode 100644
index 0000000000..ed45e07d47
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14774.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module T14774 where
+
+class C a => D a where
+  cop :: a -> Bool
+
+class D a => C a where
+  dop :: a -> a
+
+f :: C a => Int -> a -> Bool
+f 0 x = cop x
+f n x = f (n-1) x
diff --git a/testsuite/tests/typecheck/should_compile/T14774.stdout b/testsuite/tests/typecheck/should_compile/T14774.stdout
new file mode 100644
index 0000000000..e98489e760
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14774.stdout
@@ -0,0 +1,3 @@
+T14774.$p1D :: forall a. D a => C a
+ RULES: Built in rule for T14774.$p1D: "Class op $p1D"]
+T14774.$p1D
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 49683b7db4..a3aae5ee2b 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -592,3 +592,4 @@ test('T14590', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutio
 test('T13032', normal, compile, [''])
 test('T14273', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
 test('T14732', normal, compile, [''])
+test('T14774', [], run_command, ['$MAKE -s --no-print-directory T14774'])