As understand it, you've proposed changes in context reduction to restore confluence:
yes.
What is your plan to deal with non-termination (e.g. examples 6 and 16 of the FD-CHR paper)?
I haven't read all the suggestions that Martin, you, and others have made in that area yet (still busy with overlaps), including those in the revised FD-CHR paper, so I can't make concrete suggestions yet, beyond those I've already posted here: 1 we all want terminating instance inference, but trying to assure that via restrictions is bound to be limiting (does GHC still have to build part of the hierarchical libs with -fallow-undecidable-instances?). I'm not opposed to it, but I'd like Haskell' to document current practice, in that we have the option to switch of termination checks whenever they are not able to see that our programs are terminating (available in Hugs and GHC, and all too often necessary). 2 that said, termination checks can do a lot, and it is certainly useful know various methods of checking terminations, as well as terminating examples beyond current termination checks. the old FD-CHR draft already discussed relaxed FD conditions, but was somewhat hampered because confluence checks seemed entangled with termination. with confluence problems out of the way, the restrictions can focus on termination. was there any other reason not to go for the relaxed FD conditions as a start? 3 in http://www.haskell.org//pipermail/haskell-prime/2006-February/000825.html I gave two examples that are terminating, but for which the current conditions are too restrictive. the first could be cured by taking "smaller" predicates into account, in addition to smaller types and smaller variable sets, and the second turned out to be a special case of the relaxed coverage condition, I think. I run into both problems all the time (the first is especially annoying as it prevents calling out to simpler "helper" predicates..). 4 example 6, FD-CHR, is vector multiplication Mul. I argued that it is wrong to call the declarations faulty and invalid just because there are some invalid calls. I also suggested one way in which the declarations can be permitted, while ruling out the faulty call: http://www.haskell.org//pipermail/haskell-prime/2006-March/000847.html basically, the idea is that FDs specify type-level functions, so unless we can demonstrate that those functions are non-strict, we need to rule out cyclic type-level programs that feed the range of an FD into one of its domain parameters, by a generalized occurs check. simply looking at the intersection of variables is easy to implement; that method is still too conservative (eg, if the range is simly a copy of the domain), but adding it to our repertoire of termination checks definitely improves the situation, and is sufficient to permit the declarations in example 6, while ruling out the offending call. 5 example 16, CHR, defines an instance that hides an increasing type behind an FD. my intuition on that one tells me that we are again ignoring the functional character of FDs (as we did in 4). instead of ruling out types determined entirely by FDs via the bound variable restriction, as the paper suggests, we could extend the termination check to collect information about FDs. just think of type constructors as simple FDs and try to treat real FDs similarly: adding a constructor around a type variable in the context means we cannot guarantee termination by reasoning about shrinking types. determining a type variable in the context by putting it in the range of an FD means we cannot guarantee termination by reasoning about shrinking types, unless we have some conservative approximation of the relation between domain and range of the FD to tell us so. the example case: class F a b | a-> b instance F [a] [[a]] clearly shows the range to be more complex than the domain, so we can account for that increase in complexity when we see F t x in an instance context. if instead, we only had: class F a b | a->b instance F [[a]] [a] the range would be less complex than the domain, so we could permit use of this, even though the bound variable condition would treat it the same way - forbid it. there are whole yearly workshops dedicated to termination. we shouldn't assume that we can reach any satisfactory solution by a mere handful of restrictions. which means that we need to add to our repertoire of termination checks, and to keep open the option of switching of those checks. cheers, claus