relaxed instance rules spec (was: the MPTC Dilemma (pleasesolve))

[Claus Reinke]

> The main focus of the FD paper is how to restore confluence which is
> important for complete inference. 

That is indeed my second major problem with the paper!-)

There are examples in the paper that show how some conditions 
are sufficient to ensure confluence, but they hardly ever seem to be 
necessary for the original program, only for the current mapping.

The way I interpret FDs implies that they introduce a systematic space
leak into the inference process: if any stage in the inference uses *any*
constraint with a class which is subject to an FD, that results in an 
additional bit of information about that class' FD. and we *cannot*
throw that bit of information away unless we know that we will
never need to refer to it in the remainder of the inference chain.

As I mentioned before, capturing this is the one point where I can
imagine an advantage of using CHRs, by putting the "memo-table"
for the type function implied by an FD into the global constraint
store. So I was rather surprised to see the way FDs are currently
mapped into CHRs. And indeed, as far as I noticed, *nearly all* 
the confluence problems are due to that mapping, not due to FDs.

In a way, it is nice that loosing confluence shows up cases where
information about an FD may be thrown away while there are still
opportunities to use it, but since confluence is hard to check without
termination, that doesn't really help in practice unless we take it as
an additional reason to want guaranteed termination..

So, why not get rid of that problem and clearly model the memo
effect of FDs as an aspect separable from the instance constraint?

    class C a b | a -> b
    instance Ctxt => C t1 t2

in the current mapping, the class FD CHR needs two constraints
for C to generate an equation for the two b parameters, but the
instance simplification rules may take constraints away before that
class FD CHR was applied, resulting in the danger of non-confluence.

the instance FD CHRs, instead, need only a single constraint to
generate an equation, because they compare that constraint to one
of the instances. still, the constraint might be simplified away before
its instance FD CHR was applied. this is slightly less risky, because
any new constraint that might profit from the information we threw
away is itself subject to the instance FD CHR. but it still results in
the danger of non-confluence, corresponding to ignoring some 
information about the class' FD contributed by independent
constraints "communicating" via the same instance FD CHR!

the paper suggests not generating the class FD CHR in the first
place, or restricting the order in which rules may be applied.

but why not encode the memo aspect of FDs directly in the
constraint store? we'd have to represent _separately_ the 
constraints that need to be proven, and the memo aspect of 
those constraints we _have used_ at any point in the deduction.
for the class C above, something roughly like this (tweak as
needed;):

    (instance FD) 
    rule C t1 t2 <==> Ctxt, MEMO-C t1 t2  

    (class FD)
    rule C t1 t2, MEMO-C t1 t3 ==> t2==t3

note that the (instance FD) CHR could also be called the
(constraint FD) CHR, because it triggers whenever any constraint
is simplified using a specific instance declaration in the inference.
unlike the current instance improvement CHR, which hard-codes 
the part of the information gathered from the instance declaration,
this mapping separates the generation and use of FD information,
but ties the generation to simplification.

unlike ordinary constraints, MEMO constraints no longer
imply proof obligations in terms of instance inference, they 
just record a type dependency that has been used in a 
simplification step. if my understanding of propagation rules
in CHR is correct, applications of the class FD CHR will
preserve that recorded information, so there will always
be a second constraint to compare with when we want to
use FDs to generate equations.

I'm not entirely sure how consistency of constraints is checked
in CHR - we may need to add a rule that exposes inconsistent
MEMO constraints:

    (inconsistent FD)
    rule MEMO-C t1 t2, MEMO t1 t3 ==> t2/=t3 | YELL!-)

am I on the right track here?

cheers,
claus