A while back, after some discussion, we updated the antisymetry law of Ord from:

-- | - Antisymmetry: if `a <= b` and `b <= a` then `a = b`

to

-- | - Antisymmetry: if `a <= b` and `b <= a` then `a == b`

so as to connect Eq and Ord. See issue #174 and PR #298.

Ever since, the reflexivity law has been bugging me and I think we need to update that too. Currently, it reads

-- | - Reflexivity: `a <= a`

and I think it should read

-- | - Reflexivity: if `a == b` then `a <= b`

To explain why, I return to my old example of unreduced rational numbers. Take a rational number represented as a record with two fields (n and d) where d is not zero but without the requirement that n and d are coprime. We can define equality as

eq (Rat x) (Rat y) = x.n * y.d == y.n * x.d

But what if we then define Ord using dictionary order

compare (Rat x) (Rat y) = case compare x.n y.n of
  EQ -> compare x.d y.d
  neq -> neq

These two definitions satisfy the current laws, specifically Ord is reflexive, but:

> x = Rat {n: 2, d: 4}
> y = Rat {n: 1, d: 2}
> x == y
true

> x <= y
false

which is surely not what we want.