Why not universally quantify over a?

[ChristopherKing42]

One thing I notice is that all of the Search a b terms in the module are of the form forall a. Ord a => Search a b, for some b (except return). Therefore, I propose we just throw that into the definition.

There are two equivalent ways to do this. Either

data Scorer a b where
    eval :: Ord a => !(b -> a) -> Scorer a b

newtype Search b = Search {optimum :: Scorer a b -> b}

if you prefer GADTs or

newtype Search b = Search {optimum :: forall a. Ord a => (b -> a) -> b}

if you prefer foralls. I'll use the second one for the remainder of the post, but like I said, they're isomorphic.

You might be wondering is if the monad instance will still type check. I checked, and the answer is yes, with the only change being to change Search a b to Search b. I'm pretty sure most of the other terms and instances type check.

There would be some things we lose. We would no longer have Profunctor since Search now has only one type argument instead of two. We could still implement a variation on lmap with type (forall a. Ord a => Scorer a' a) -> Search b -> Search b. In practice, it would be simpler just to implement it with specific types as needed. For example, pessimum :: Ord a => Search b -> (b -> a) -> b would be pessimum s p = optimum s (Down . p). To tell the truth, the Profunctor instance probably isn't great anyways, since it allows you to make an invalid instance of Search without directly using Search on an invalid argument.

We also no longer could create a search that provides us with (() -> a) -> () for nonOrd a. Same thing for U1 and Proxy a and similar things for return and cont. I do not think these are major loses though. In particular, we can still define Search () and the other things, it's just that Ord a is now implied.

One thing we gain is isomorphism with the traditional search type (a -> Bool) -> a (assuming valid instances only). In the easy direction we get something like:

convert :: Search b -> (b -> Bool ) -> b
convert = coerce (optimum :: forall b. Search b -> (b -> B) -> b)

the nontrivial direction is also less efficient, but still interesting

unconvert s = Search $ \p -> s $ \b -> p b >= p (s $ \b' -> p b' > p b)

Another thing we get is element given by element s = optimum s $ const (), which just returns some element of a searchable type. There is also highest and lowest, which is given by highest s = optimum s id and lowest s = pessimum s id (although it only works if you can compare elements of b in finite time).