[commit: ghc] wip/ext-solver: A comment showing a problem with `solverSimplify` and an idea on how to solve it. (cb9b93b)

[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/cb9b93bd12937d83b5e6b7e9628b66d798b5edd2/ghc

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

commit cb9b93bd12937d83b5e6b7e9628b66d798b5edd2
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sun May 11 08:53:14 2014 -0700

    A comment showing a problem with `solverSimplify` and an idea on how to solve it.


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

cb9b93bd12937d83b5e6b7e9628b66d798b5edd2
 compiler/typecheck/TcTypeNats.hs | 60 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)

diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index a206236..5c52fa5 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -1085,6 +1085,66 @@ solverFindConstraidction proc viRef others ours =
 {- Try to solve as much as possible from the given list of constraints.
 Returns the solved constraints (with evidence), and all other constraints.
 -}
+{-
+Consider this example:
+
+ex4 :: p a -> p b -> p ((a + a) + b) -> p (2 * a + b)
+ex4 _ = id
+
+A: a + a = u
+B: x + b = v
+C: 2 * a = w
+D: w + b = v
+
+If we solve `B` or `D` first, then we are essnetially done,
+as all the others can be substituted within each other.
+
+However, what if we happen to consider `C` first?
+
+(A,B,D) => C
+
+This goal is essentially:
+
+((a + a) + b ~ (2 * a) + b) => (a + a) ~ 2 * a
+
+which can be proved by cancelling `b` on both sides.
+
+Now, we are left with just `A,B,D`, which amounts to having
+to prove:
+
+(a + a) + b   ~   w + b
+
+We can't do this because we've lost the information about `w`.
+
+
+Perhaps the answer is to solve all goals at the same time
+(this also has the benefit of being more efficeint!).
+
+If we need to solve a collection of goals:
+
+A /\ B /\ C /\ D
+
+we look for a counter example, which amounts to finding a model for:
+
+not (A /\ B /\ C /\ D)
+
+If such a model does not exist, than we can solve all the goals.
+If it does exits, then we can't solve all the golas, at which point
+we could give up.
+
+Instead of giving up, it is nicer to try to identify a small
+subset of all goals that can't be solved, to report a more
+reasonable error.  For example, if the goals were:
+
+(x = 2,  a + 0 ~ a)
+
+We can't solve these togethere (there is no reason why `x` should be 2),
+but we could solve the `a + 0 ~ a` part.
+-}
+
+
+
+
 solverSimplify :: SolverProcess -> IORef VarInfo ->
                   [Ct] -> IO ([(EvTerm,Ct)], [Ct])
 solverSimplify proc viRef cts =