idris-lang/Idris-dev — pull request #1346 by bmsherman (2014-06-30 05:27:18+00:00)
Title: Correctly count applications of variables in :search

I found an interesting, somewhat subtle bug in the :search code. I had only found one example of a false match resulting from it: if you search
```Idris
(m, n : Nat) -> n + m = m + n
```
(the type of `plusCommutative`), you'd get this as one of your results:
```Idris
plusAssociative : (left : Nat) ->
(centre : Nat) ->
(right : Nat) -> left + (centre + right) = left + centre + right
```
Why is that? Well, the unifier tells me that
```
m = center + right
n = left = center = right
```
, and so the two types end up becoming (after some simplification)
```
(n : Nat) -> n + (n + n) = (n + n) + n
```
. This type can be constructed by using *either* commutativity or associativity! So it's a ``lower bound" for the two types. But neither type can be constructed from the other, so with my current rules, the result shouldn't be displayed.

The error that I had was that, while my code recognized that with `m = center + right` that `m` had to be instantiated to a specific value, it forgot to count the fact that `center` and `right` also had to be potentially instantiated to specific values. So now I take that into account.