[snip]
No, it doesn't, because that wasn't my argument. Consider:
f :: C a => a->a g :: C a => a->a
Now if we can define just one instance of C, eg T1 where f (x::T1) \= g (x::T1), then we can tell f and g apart for all instances of C, even when there is another instance of C, eg T2, for which f (x::T2) == g (x::T2). Thus we can't just interchange the uses of f and g in the program because we can always use values of T1 to distinguish between uses of f :: T2 -> T2 and g :: T2 -> T2.
If f (x::T1) == g (x::T1) then nothing has been demonstrated, as you rightly point out, because there could be another instance of of C eg T3 for which f (x::T3) \= g(x::T3).
I agree to this point.
It is the inequality that is the key to breaking referential transparency, because the discovery of an inequality implies different code.
Here is where you make the jump that I don't follow. You appear to be claiming that the AbsNum module coerces a Haskell compiler into breaking referential integrity by allowing you to discover a difference between the following two functions: f :: (Num a) => a -> a f x = x + 2 and g :: (Num a) => a -> a g x = x + 1 + 1 From an earlier post:
Now since f and g compute the same results for the same inputs, anywhere in a program that you can use f you could just replace f by g and the observable behaviour of the program would be completely unaffected. This is what referential transparency means.
My essential claim is that the above statement is in error (but in a fairly subtle way). It is only true when f and g are instantiated at appropriate types. This is what I meant by saying that overloading was muddying the waters. The original post did not have a type signature, so one _could_ assume that MR forced defaulting to Integer (the MR is evil, _evil_ I say), which would then make the statement true _in that context_. However the post with the AbsNum code instantiates f and g at a different type with different properties, and the equality does not hold.
Interesting! Referential transparency (as I understand it) has indeed been violated. Perhaps the interaction of GADTs and type classes was not sufficiently studied before being introduced to the language.
I believe your reasoning is correct, but you are using a false supposition. Rob Dockins