alternative translation of type classes toCHR(was:relaxedinstance rules spec)

[Claus Reinke]

another interesting improvement in confluence, not related to FDs:

the old CHR translation generated proof obligations for superclass
contexts via propagation rules, which (similar to the propagation
rules for instance improvement) might be in conflict with the
instance simplification rules, jeopardizing confluence unless existence
of superclass instances is checked separately (as currently required
in Haskell).

by putting superclass constraints as proof obligations on par with
instance inference and FD-based improvement in the new CHR 
translation, we have ensured that the CHR will be confluent even 
if the superclass check is omitted. take example 28 from "theory 
of overloading":

    class E t
    instance E t => E [t]
    instance E Int
    class E t => O t
    instance O [t]

which generates these CHR (I switched the implementation from
TH to HSX as a frontend, to avoid GHC's built-in checks):

    /* one constraint, two roles + superclasses */
    e(T) <=> infer_e(T), memo_e(T), true.

    /* instance inference: */
    infer_e(list(T)) <=> e(T).

    /* instance inference: */
    infer_e(int) <=> true.

    /* one constraint, two roles + superclasses */
    o(T) <=> infer_o(T), memo_o(T), e(T).

    /* instance inference: */
    infer_o(list(T)) <=> true.

consider the problematic constraint, and we see that there is not
even room for initial divergence, as the proof obligation for the
superclass constraint is established before inference for o can
even begin:

        o(list(U))
<=> infer_o(list(U)), memo_u(list(U)), e(list(U))
<=> memo_u(list(U)), e(list(U))
<=> memo_u(list(U)), infer_e(list(U)), memo_e(list(U))

(note the outstanding proof obligation infer_e(list(U)) ).

this means that we could remove the early superclass constraint
check from Haskell, and the resulting uglinesses:

- superclass instances have to be visible at subclass instance 
    declaration time, not at subclass constraint usage time (this
    is really weird)
- lack of superclass instances causes compilation to fail, instead
    of just causing unusability of subclass instances
- superclass contexts cannot be used to abstract out common
    contexts from methods/instances/goals, because superclass
    contexts behave differently from other contexts

what do you think about this suggestion?

cheers,
claus

ps that example 28 is interesting for another reason, too:
    the missing instance is "instance E t", but GHC will _not_
    accept the program if you add that instance, unless we
    specify allow-incoherent-instances! Hugs will accept it,
    but its behaviour is that of GHC's "bad" flag (always
    select the most general instance)..

    the error message given by GHC, without that flag, is
    the interesting bit: even though we have instances of E
    for any type, GHC can't determine that (it would require
    a differentiation by cases)!