In (an idealized version of) Haskell, is there a concrete type a such that we can implement Eq a lawfully, but it is impossible to implement Ord a? The order doesn’t need to be meaningful, and any total order suffices, as long as it is implemented by a function that terminates and obeys the axioms.