[commit: ghc] wip/ext-solver: Bugfix: avoid non-termination. (a1b3e4d)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/ext-solver
Link       : http://ghc.haskell.org/trac/ghc/changeset/a1b3e4d0ded3f434dbfca9fe92ed7fbc42f2bf0c/ghc

>---------------------------------------------------------------

commit a1b3e4d0ded3f434dbfca9fe92ed7fbc42f2bf0c
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sun Jun 8 18:37:35 2014 -0700

    Bugfix: avoid non-termination.
    
    When we compute new derived work, we need to check that the result
    is not already in the inert set.   If we don't do this, we keep finding
    the same constraints over and over again, if they don't do anything to the
    inert set.


>---------------------------------------------------------------

a1b3e4d0ded3f434dbfca9fe92ed7fbc42f2bf0c
 compiler/typecheck/TcInteract.lhs | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index babaeb6..3d057ae 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -156,6 +156,8 @@ interactExternSolver inGivenStage =
          relList    = bagToList relFeqs
          othersList = funEqsToList otherFeqs
 
+         eqs = inert_eqs iCans
+
          {- `survived` should be a sub-set of the inert funeqs.
          This function rebuilds the inert set, after we've remove a constraint
          (e.g., because they were solved, or caused a contradiciton. -}
@@ -189,8 +191,11 @@ interactExternSolver inGivenStage =
             ExtSolOk newWork
 
                -- We found some new work to do.
-               | not (null newWork) ->
-                 do updWorkListTcS (extendWorkListEqs newWork)
+               | let reallyNew
+                       | inGivenStage = newWork
+                       | otherwise    = filter (notKnownEq eqs) newWork
+               , not (null reallyNew) ->
+                 do updWorkListTcS (extendWorkListEqs reallyNew)
                     return True
 
               -- Nothing else to do.
@@ -208,7 +213,17 @@ interactExternSolver inGivenStage =
                                 mapM_ setEv solved
                                 return False
 
+
   where
+  notKnownEq eqs ct =
+    case getEqPredTys_maybe (ctPred ct) of
+      Just (_,tvt,ty)
+        | Just tv <- getTyVar_maybe tvt ->
+           all (not . tcEqType ty)
+                    [ t | CTyEqCan { cc_rhs = t } <- findTyEqs eqs tv ]
+      _ -> True
+
+
   addCt ct mp =
     case ct of
       CFunEqCan { cc_fun = tc, cc_tyargs = tys } -> addFunEq mp tc tys ct