idris-lang/Idris-dev — pull request #1324 by bmsherman (2014-06-21 20:55:52+00:00)
Title: Improvements to :search, primarily in handling typeclasses

I've made some changes to the :search function, primarily in order to handle typeclasses more appropriately. Before, :search was handling typeclasses in a very ad-hoc manner; it was able to do either an exact match of typeclasses, or it was able to find an exact instance (e.g., `Show Int`). Otherwise, typeclasses (or rather, their dictionaries) were handled as mundane arguments, and so :search would find
```
t -> a -> a -> a
```
quite similar to
```
Ord a => a -> a -> a
```
, because the latter is simply the former with `Ord a` plugged in for `t`.

I've now rewritten the search code to handle typeclasses in the special manner they deserve! The possibilities are endless! (Right now, that is unfortunately not a joke. I've instilled a cutoff to ensure it doesn't hang). Here are some new matches that you'll find that were not possible before:
```
Idris> :s Monad m => m a -> (a -> b) -> m b
< Prelude.Applicative.liftA : Applicative f => (a -> b) ->
f a -> f b
Lift a function to an applicative

< Prelude.Functor.map : Functor f => (a -> b) -> f a -> f b
The action of the functor on morphisms
```
Similarly,
```
Idris> :s (a -> b) -> Vect n a -> Vect n b
< Prelude.Applicative.liftA : Applicative f => (a -> b) ->
f a -> f b
Lift a function to an applicative

< Prelude.Functor.map : Functor f => (a -> b) -> f a -> f b
The action of the functor on morphisms
```
```
Idris> :s Functor f => f a -> (a -> f b) -> f b
> io_bind : IO a -> (a -> IO b) -> IO b

> Prelude.Maybe.maybe_bind : Maybe a ->
(a -> Maybe b) -> Maybe b

> prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b

> Prelude.Monad.>>= : Monad m => m a -> (a -> m b) -> m b
```
And if you have the patience to wait a few seconds,
```
Idris> :s (Ord a, Ord b) => (a, b) -> (a, b) -> Bool
< Prelude.Classes.< : Ord a => a -> a -> Bool
< Prelude.Classes.<= : Ord a => a -> a -> Bool
< Prelude.Classes.> : Ord a => a -> a -> Bool
< Prelude.Classes.>= : Ord a => a -> a -> Bool
< Prelude.Classes./= : Eq a => a -> a -> Bool
< Prelude.Classes.== : Eq a => a -> a -> Bool
```
[Take that, Hoogle!](http://www.haskell.org/hoogle/?hoogle=%28Ord+a%2C+Ord+b%29+%3D%3E+%28a%2C+b%29+-%3E+%28a%2C+b%29+-%3E+Bool)

There is still a lot to be done, but I think this is a step in the right direction!