This came up elsewhere recently, so I guess I should say something.
Equality does not have anything necessarily to do with some ability to 'compare' things decidably. For instance, one can implement the computable real numbers as functions from a precision to a rational approximation at that precision. Given this representation, it is impossible to algorithmically decide that two real numbers are equal; one can only decide that two distinct numbers are not equal. However, that does not mean that a notion of equality does not exist, or that we cannot demonstrate the equality of two real numbers, even if we cannot decide whether two arbitrary numbers are equal or not.
undefined is unequal to (undefined, undefined) because certain programs will behave differently when given the two as input. This is true even though (==) isn't one of those programs.
However, I do think there is a lot to be said toward axioms holding for bottom being a low priority. Roughly, I care about a function's behavior on undefined with regard to how it governs its behavior on well-defined Haskell programs. That is, examining 'f undefined' will tell you how things like 'fix f' will work, but I only care about the latter, not the former, in itself. But the situation under discussion here is exactly one where we are talking about making more programs well-defined, which I tend to think trumps, "this fails a required equation with respect to ill-defined values."
The one thing (that I can see) that the laziness breaks is reducing things like 'm `mappend`
mempty' to just m, and it can only break when the context in which the expression appears requires just the tuple structure to avoid vicious circularity. I'm not sure that's important enough for instant veto.