Hello,
On 4/13/06, Ross Paterson
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