| I'm wondering if the general method of avoiding non-termination can be | made to work in these more complex cases. | | Incidentally, the constraint solver stack overflow problem can be | turned to our advantage. The typechecker's exhausting the stack should | be considered a failure to match the instance -- and so the | typechecker should mark the current instance inappropriate and try | another one, if any. Ultimately, this boils down to solving the halting problem, I believe. Stack-overflow isn't a proof that the thing isn't soluble. I can believe that it woks nicely in practice, but it's a bit of a hack! Simon