FDs and confluence

[Iavor Diatchki]

Hello,

On 4/13/06, Ross Paterson <ross at soi.city.ac.uk> wrote:
> They are equivalent, but C [a] b d, Num c and C [a] c d, Num c are not.

I agree that this is the case if you are thinking of
"forall a b c d. (C [a] b d, Num c) <=> (C [a] c d, Num c)"
Here is a counter example (assume we also add an instance B Char Int
to the example)
a = Char, b = Char, c = Int, d = Bool
LHS: (C [Char] Char Bool, Num Int) => B Char Char => False
RHS: (C [Char] Int Bool, Num Int) => B Char Int => True

However, I don't think this is the case if you are thinking of:
"forall a c d. exists b. (C [a] b d, Num c) <=> (C [a] c d, Num c)"
becuase I can pick 'b' to be 'c'.

In any case I think this thread is drifting in the wrong direction.  I
was just looking for a concrete example of where we have a problem
with the non-conflence that people have found, e.g. somehitng like
'here is an expression for which we can infer these two schemas, and
they have different sets of monomorphic instances'.  I think such an
example would be very useful for me (and perhaps others) to clarify
exactly what is the problem, so that we can try to correct it.

-Iavor