Dear all, Thanks for your replies. Just to clarify: I am fully aware that inside Haskell there is no guarantee that certain (intended) requirements on type class instances are satisfied. I was asking whether the intention for Eq is that (==) is commutative, because if it was, I would require that as an axiom for the equivalent of Eq in our formal setting (I'm using the proof assistant Isabelle/HOLCF [1]). Afterwards only types for which one could prove commutativity could be instances of Eq. But if there where already "standard" instances which violated this requirement, adding it in the formal setting would prevent it from being applicable to "standard" Haskell programs. Btw: Isabelle/HOLCF unifies all error values and nontermination in a single bottom element _|_. Currently we are using the following axioms for our formal Eq class (where I'm using Haskell syntax although the real sources [2] use Isabelle/HOLCF syntax which is slightly different; (=) is meta-equality). (x == y) = True ==> x = y (x == y) = False ==> not (x = y) (x == _|_) = _|_ (_|_ == y) = _|_ Those axioms state that (==) is sound w.r.t. to meta-equality and strict in both it's arguments. The question is whether we should also add. (x == y) = _|_ ==> (y == x) = _|_ Which would directly imply (x == y) = (y == x) cheers chris [1] http://isabelle.in.tum.de (and http://isabelle.in.tum.de/dist/library/HOL/HOLCF/) [2] http://sourceforge.net/p/holcf-prelude