[commit: ghc] wip/ext-solver: A comment describing a problem with the current approach. (1815f26)

[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/1815f26946d625606ea49f49c5300124f6d6fd70/ghc

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

commit 1815f26946d625606ea49f49c5300124f6d6fd70
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sun May 4 19:54:52 2014 -0700

    A comment describing a problem with the current approach.


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

1815f26946d625606ea49f49c5300124f6d6fd70
 compiler/typecheck/TcInteract.lhs | 35 ++++++++++++++++++++++++++++++++++-
 1 file changed, 34 insertions(+), 1 deletion(-)

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 9575038..6740d47 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -723,7 +723,40 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs , cc_ev
        ; return (Nothing, True) }
 
   | otherwise
-  = do { _ <- extSolAssume workItem -- XXX: Check result?
+  = do { _ <- extSolAssume workItem
+          {- XXX: This is not correct in two ways:
+              1. The kicked-out constraints are not purged from the external
+                 solver!  Thus, when they go around the solver loop, they will
+                 be "solved" in terms of themselves.  Clearly wrong.
+
+              2. Even if we could remove them from the external solver,
+                 we are not "kicking-out" enough constraints.  Consider,
+                 the following example:
+
+                 A: [W]  1 <=? x   ~   True
+                 B: [W]  1 + n     ~   x
+
+                 If we process them in this order (A first, then B), then we
+                 can't solve either constraint.
+                 If we reverse their order (i.e., B first, then A), then
+                 we can solve `A` because we have more information about `x`.
+
+                 In other words, in this case `B` should have kicked-out `A`.
+
+              I think that both of these problems will be avoided, if
+              we moved the external solver outside of the pipeline, like this:
+                - Let GHC process constraints until they are "inert".
+                - Extract inert constraints relevant to the external solver,
+                  and compute "improvements" (i.e., extra equalities).
+                - If there were additional equalities, add them to the work
+                  queue and let GHC process things again until they are inert.
+                - This can be repeated a few times, but it will eventually
+                  stop, as the external solver will run out of equalities to
+                  find (this is bound by the number of variables in scope)
+                - Finally, the external solver can be run to solve
+                  any inert wanted constraintsthat it knows about.
+           -}
+
        ; mb_solved <- trySpontaneousSolve ev tv rhs
        ; case mb_solved of
            SPCantSolve   -- Includes givens