Weird Undecidable Instances Bug

[Ashley Yakeley]

On Monday, Sep 8, 2003, at 03:53 US/Pacific, Simon Peyton-Jones wrote:

> 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