Consider an instance decl like:
instance (Lte a b l,If l b a c) => Max a b c
(This is a real example.) Notice that "l" is used on the LHS of the => but not the RHS. The idea is that "l" will get unified by a functional dependency. But if such a unification re-starts the solving process from scratch, we just get into an infinite loop (apply instance decl, apply fds, unify, start again, apply instance decl again, etc).
Could you give me an example of a goal you had in mind, where this method fails? I tried
(Lte a b l,If l b a c) |- (Max a b c)
but the method works on this.
This reminds me of Prolog, somewhat. I wonder if it would be worth prototyping confluent solvers in Prolog? I might try this actually, as a way of getting a handle on the problem. I'd be especially interested in any "tricky examples" you may have.
On the other hand, does the solver have to be confluent? What if it spawned off different "threads", and gave up after doing a certain amount of "work", which the user could set (like -fcontext-stack)? Provided the "solver thread" scheduling is deterministic, I imagine that every correct program would be solvable in a finite amount of work.
I guess one possibility might be to make such an instance decl illegal.
Nooo!!! My workaround was simply to put the instance declaration in a later module. Then "g" type-checks fine.
-- Ashley Yakeley, Seattle WA
_______________________________________________ Glasgow-haskell-bugs mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
