§ We can't define choice for finite sets in Haskell!
If all you have is a decidable equality relation on the elements, then there seems to be no function which can implement choice. That is, you can’t write a function choose :: Set a -> Maybe (a, Set a)
Concretely, suppose we represent sets as lists of nonrepeated elements. Then, we can write an operation choose :: Set a -> Maybe (a, Set a), which just returns a pair of the head and the tail if the list is nonempty, and returns Nothing if it is empty.
However, this operation does not respect equality on sets. Note that any permutation of a list representing a given set also represents that same set, but the choose operation returns different answers for different permutations. As a result, this operation is not a function, since it does not behave extensionally on finite sets!
I feel there should be an argument involving parametricity which makes this work for arbitrary datatype representations, since all we rely on is the fact that equality can’t distinguish permutations. But I haven’t found it yet.