But I fail to see how having Maybe on the inside remedies this situation. Furthermore, on Eq types these sets are not so interesting, for the following reason.
With Maybe on the outside, you can't jump straight to defining the function; you must first determine whether the intersection is empty. To my mind, a more natural definition for (possibly empty) sets is
data Set a = Set {find :: (a -> Maybe b) -> Maybe b}
which really explains how this is a set.
One can write a function
Eq a => ((a -> Bool) -> a) -> [a]
that enumerates the elements of the set. Because we have universal quantification, this list can not be infinite. Which makes sense, topologically: These so-called searchable sets are topologically compact, and the Eq constraint means the space is discrete. Compact subsets of a discrete space are finite.
I don't understand how that's finite and not just countable.