idris-lang/Idris-dev — pull request #1341 by bmsherman (2014-06-28 14:57:20+00:00)
Title: Improve :search results by checking injectivity and allowing typeclass introduction

I've made a couple more changes to :search which should improve the results that are found:

- I'm more careful about considering which variables are "matched" due to a given unification result. For example, suppose we are matching
```Idris
Ord t => t -> t -> Bool
```
with
```Idris
(Ord a, Ord b) => (a, b) -> (a, b) -> Bool
```
. Unification will tell us that we need `t ~ (a, b)`. This uniquely tells me that `t` is, but because the pair type constructor (i.e., `(,) : Type -> Type -> Type`, although this isn't actually valid Idris) is injective, it also uniquely tells me that `a` and `b` are. Therefore, I can claim to have matched all three variables.

I had handled this in two different ways in the past, both wrong. In one case, I would only claim to match more than one variable from a unification result if it looked like `t ~ a`; that is, one variable exactly matches another. Then, I realized I was missing results, and I overcompensated: I took all variables that were mentioned. So suppose I got a result `t ~ snd (a, b)` (this is made up, since this would have been simplified, I'm pretty sure). I would incorrectly consider `a` to be matched here, even though it isn't determined at all by the expression.

Now, I use the `isInjective` function in `Idris.Core.TT` to make a conservative approximation as to what variables have been matched; if I consider a variable to have been matched, then it *definitely* was uniquely determined.

Here's an example of where this pares down results. If I search
```Idris
(z : t) -> z = z
```
, I no longer get results such as these
```
Prelude.Pairs.Exists.getProof : (x : Exists P) ->
P (getWitness x)

Prelude.Pairs.Sigma.getProof : (x : Sigma a P) ->
P (getWitness x)

Prelude.Pairs.Subset.getProof : (x : Subset a P) ->
P (getWitness x)
```
, which were being matched in this logically invalid way.

- I now allow search results where types differ by introduction or elimination of typeclass constraints. If I search
```Idris
a -> a -> a
```
, I'll now get results such as these
```
> Prelude.Classes.(*) : Num a => a -> a -> a
> Prelude.Classes.(+) : Num a => a -> a -> a
> Prelude.Classes.(-) : Num a => a -> a -> a
> Prelude.Algebra.(<*>) : Ring a => a -> a -> a
> Prelude.Algebra.(<+>) : Semigroup a => a -> a -> a
> Prelude.Algebra.(<->) : Group a => a -> a -> a
> Prelude.Classes.div : Integral a => a -> a -> a
> Prelude.Algebra.join : JoinSemilattice a => a -> a -> a
> Prelude.Classes.max : Ord a => a -> a -> a
> Prelude.Algebra.meet : MeetSemilattice a => a -> a -> a
> Prelude.Classes.min : Ord a => a -> a -> a
> Prelude.Classes.mod : Integral a => a -> a -> a
```
And of course, the symbols to the left (`>`) properly indicate that the searched type is more general than any of these types, which restrict `a` to a given typeclass.

And the 5 top results for searching
```
(Num a, Ord a) => a -> a -> a
```
are all new due to this change:
```
< Prelude.Classes.(*) : Num a => a -> a -> a
< Prelude.Classes.(+) : Num a => a -> a -> a
< Prelude.Classes.(-) : Num a => a -> a -> a
< Prelude.Classes.max : Ord a => a -> a -> a
< Prelude.Classes.min : Ord a => a -> a -> a
```

The downside of this change is that the time to compute the similarity between two types may increase exponentially (compared to before) with the total number of typeclass constraints. So a search like
```
(Num a, Ord a, Eq a, Show a) => a -> a -> a
```
is taking roughly 15 seconds on my computer...