Do you have a revised set of restrictions on the form of instances?
sure, but you won't like them any better now than the last time I mentioned them:-) - as for confluence, none of the restrictions seem necessary without FDs, type class inference proceeds by _matching_ of instance heads to constraints, and without overlapping instances, there cannot be more than one matching head. so the only divergence comes from reductions on separate parts of the constraint store, which are independent, so the divergence is temporary. with FDs, type class inference adds _unification_, but only for FD range parameters. instance heads that only differ in FD range positions are now overlapping, but only as far as improvement is concerned. note also that the resulting overlap in the left hand side of rules is over variables, so no variable instantiation can disable such rules. to be initially diverging, such overlapping improvement rules must have different unifications as their right hand sides. memoisation ensures that any improvement that was possible at any point in the reduction process remains possible throughout. so following either of two conflicting improvements will leave the other enabled, ensuring failure of the constraint store instead of non-determistic results. consistency condition: neither necessary nor sufficient coverage/bound variable condition: as far as confluence is concerned, these were possibly motivated by the wish to have variable-restricted CHR, without which arbitrary rule systems might introduce non-confluence by following different instantiations for the fresh variables, through unification with different left hand sides. but due to the peculiarities of Haskell's type classes, such instantiations do not appear to be a problem, as sketched above. (as far as termination is concerned, I remain unconvinced that these two rules are the right way to exclude problematic cases, as they exclude many valid programs just because these might be invoked with problematic queries. in such cases, I'd prefer to exclude the problematic queries.) early checking for superclass instances: also does not seem to be needed any more; as the superclass constraints will be introduced as proof obligations in the same step that introduces infer_Class and memo_Class constraints, they cannot be "forgotten", and inference cannot terminate successfully if those instances are missing (they may, however, be provided later than now, accepting more valid programs). (sigh, I'm sure I've written this before, as so many other things here.. I may well be wrong in what I'm saying - if that is the case, please tell me so, but _please_ don't keep asking me to repeat myself..) - as for termination, the checks not related to the conditions above are a useful start, but they are incomplete, and overly restrictive. in fact, we know that we are dealing with an undecidable problem here, so that no finite system of restrictions will be able to do the job statically. we've already discussed various improvements to the current set of checks here, as have others here and elsewhere. my preference here is unchanged: the variant without static termination checks needs to be the basis, and it needs to be defined clearly, so that all implementations of Haskell' accept the same programs and give the same results. the reason for this preference is my opinion that Haskell has become too complex a language already. heaping special cases on top of restrictions that are necessarily incomplete adds complexity to the language, while restricting its expressiveness. on top of that basis, we should have termination conditions, and we should keep trying to push the envelope by making them encompass more valid programs, but that also means that these termination conditions need to keep evolving! so we should have warnings if the current set of termination checks cannot statically determine whether or not some type class program will terminate, and by all means, have a flag to decide whether or not those warnings should become error messages (for teaching contexts, or for any other software development processes based on strict coding standard conformance, the former might be the right default option). but in the near future, I do not expect to see either of the following two: a set of termination conditions that will cover and permit all practically relevant programs, or a correct and terminating, practically motivated type class program that will run much longer than it takes me to read and understand the warnings produced by the current set of termination checks. oh, two more things: if type class inference fails to terminate, I never get to run my program, so that is perfectly type safe; and if, as will eventually happen, part of my terminating type class programs are beyond the abilities of the current set of termination checks, I do not want to have to resort to a module- or project-wide license to get my code through. I'm no expert in this, but I believe that those folks who are concerned with termination proofs accept it as a matter of routine that tailoring a termination-ordering for each particular problem is an important part of their business; but if Haskell' does not support this, and still insists on doing mandatory termination checks by default, it should at least allow me to indicate which of the type classes/instances I want to take responsibility for (via a pragma, most likely), using its checks on all others. cheers, claus