I urge you to read our paper "Understanding functional dependencies via Constraint Handling Rules", which you can find here http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/.
Simon, I had already read that paper briefly, but had moved on to scan some of the other publications in that area (ats, ..), because I was unhappy with its limitations, omissions, and what I perceived as overly quick conclusions. I have now returned to it, and although I still haven't read it in full, I see that my misgivings were mostly the result of impatience - it may not be the final word, but, together with: P. J. Stuckey and M. Sulzmann. A theory of overloading. ACM Transactions on Programming Languages and Systems (TOPLAS), 27(6):1-54, 2005. it does provide a good, and necessary start, and a useful basis for discussions. [may I suggest a reference section on the main Haskell' page, listing these and other important inputs to difficult Haskell' issues?]
It will tell you more than you want to know about why relaxing apparently-conservative rules is entirely non-trivial. It's one of those areas in which it is easy to suggest a plausible-sounding alternative, but much harder to either prove or disprove whether the alternative a sound one.
what I've read so far tells me less than I want to know, exactly because I think more relaxations are necessary, but are left for future work. also, while it is true that plausible-sounding variations may lead to surprising results, it is unfortunately also true that the first explanation of such surprises isn't always the best one. case in point: you replied to my suggestion to relax the coverage condition to a recursive coverage condition, and the paper you refer to contains an example which seems to demonstrate that this wouldn't be safe (example 6): class Mul a b c | a b -> c where.. instance Mul Int Int Int where .. instance Mul a b c => Mul a (Vec b) (Vec c) where .. this looks terminating, because it recurses down a finite type in its second parameter, but it violates the coverage condition in the second instance, where c is not in {a,b}. as I've argued in my message, I'd like to think of recursive coverage here, because c is covered via the FD in the recursive call. now, the paper presents an example expression that leads to the following constraint, with a non-terminating inference: Mul a (Vec b) b --{b=Vec c}--> Mul a (Vec c) c and the paper claims that this is a direct consequence of the violation of the coverage condition! so, one of us is wrong, either my "plausibility" argument for recursive coverage, or the paper's claim that recursive coverage (or, for that matter, any relaxation of coverage that would permit that instance declaration) leads to non-termination. but note that the paper says "direct consequence", not "necessary consequence", and whether or not my informal argument can be proven, if you just read it side by side with the non-terminating inference in question, you'll see immediately that the paper is jumping to conclusions here (or at least leading the reader to such jumps..): - Mul recurses down a type in its second parameter - types in Haskell are finite - there is a non-terminating Mul inference the problem is that we have somehow conjured up an infinite type for Mul to recurse on without end! Normally, such infinite types are ruled out by occurs-checks (unless you are working with Prolog III;-), so someone forgot to do that here. why? where? how? well, there is that functional dependency that says that parameters a and b are inputs and parameter c is an output of Mul, and there is that initial constraint that says that b contains c! we have managed to write a (non-productive) cyclic program at the type-level, and while each recursive step strips one layer of its second input, it also refines it to include an extra layer, via the output and cycle! imho, the instance is okay, but the constraint should be rejected because if we write the FD as a function call with result (c=FD-Mul a b), then the constraint asks for: b=FD-Mul a (Vec b)) which should trigger a (generalised, conservative) occurs-check error (pending more refined tests). for the purposes of termination in this kind of example, the non-recursive coverage condition appears to be an (overly conservative) approximation. in fact, even the generalised occurs- check may be overly conservative (a functional dependency is not a type constructor, so the result of FD-C a b may not even include both a and b). the paper does discuss this as the (refined) weak coverage condition, with stronger constraints for confluence (fulfilled here), and under assumption of other termination proofs (theorem 2). unfortunately, it still assumes that example 6 is non-terminating, whereas I think that generalising the standard occurs-check to account for FDs gives a simple way to dispell that myth. so, I'll stick to my suggestion, on the grounds that -barring cyclic type-level programs- there are no expressions of infinite types in Haskell. but I'm open to arguments!-) cheers, claus | 2. the coverage condition only refers to the instance head. this | excludes programs such as good old record selection (which | should terminate because it recurses over finite types, and is | confluent -in fact deterministic- because of best-fit overlap | resolution): | | -- | field selection | infixl #? | | class Select label val rec | label rec -> val where | (#?) :: rec -> label -> val | | instance Select label val ((label,val),r) where | ((_,val),_) #? label = val | | instance Select label val r => Select label val (l,r) where | (_,r) #? label = r #? label | | now, it is true that in the second instance declaration, "val" is | not covered in {label,(l,r)}. however, it is covered in the recursive | call, subject to the very same FD, if that recursive call complies | with the (recursive) coverage criterion. in fact, for this particular | task, that is the only place where it could be covered. | | would it be terribly difficult to take such indirect coverage (via | the instance constraints) into account? there'd be no search | involved (the usual argument against looking at the constraints), | and it seems strange to exclude such straightforward "consume | a type" recursions, doesn't it? | | cheers, | claus