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.

This comes from the consideration that, to use certain efficient data structures such as Data.Set, we must have a decidable total order. However sets can technically be implemented with Eq alone, just that it becomes very inefficient. So is it possible to always implement Ord? All the counterexamples I know of — Integer -> Bool for example — can’t implement Eq either. There is a likely candidate, though. The type (Integer -> Bool) -> Bool, surprisingly, has computable Eq, I’m still not sure whether Ord is possible though.

I’m also interested in this question in other (non-contrived) type theories. There is indeed a type theory in which we have counterexamples: with nominal types, the atoms can be compared for equality but not order since everything is invariant under permutation of names by construction. What about MLTT? Or system F?