Unable to find `replace` using REPL `:search`

[msmorgan]

It doesn't appear to be possible to find replace using :search.

Steps to Reproduce

     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 1.1.0
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Idris> :consolewidth infinite
Idris> :set showimplicits
Idris> :type replace
replace : {a : Type} -> {x : a} -> {y : a} -> {P : a -> Type} -> ((=) {A = a} {B = a} x y) -> P x -> P y
Idris> {a : Type} -> {x, y : a} -> {P : a -> Type} -> x = y -> P x -> P y
{a : Type} -> {x : a} -> {y : a} -> {P : a -> Type} -> ((=) {A = a} {B = a} x y) -> P x -> P y : Type
Idris> :search {a : Type} -> {x, y : a} -> {P : a -> Type} -> x = y -> P x -> P y
No results found
Idris>

Expected Behavior

replace should be found with that search.

Observed Behavior

replace was not found.

[ahmadsalim]

Thanks for reporting the issue.

[mpickering]

I looked at this and it wasn't obvious what the problem was. The code path is TypeSearch.matchTypesBulk which then calls unifyQueue which calls match_unify. Then at some point the a fails to unify with a1 but which a and a1 this was isn't clear to me. I think this is more difficult than a "low hanging fruit" beginner task.

[LeifW]

I've found I can get replace by searching with P filled in to something specific, e.g. (x = y) -> Maybe x -> Maybe y. Also, if I search for (a = b) -> (b = c) -> a = c, I additionally get replace. Maybe = c is a concrete enough P for it to search for replace? You are able to search for things where the type constructor is free, e.g. (f : Type -> Type) -> (a -> b) -> f a -> f, but that type constructor only takes type, rather than anything like the constructor P : a -> Type or Category's cat : k -> k -> Type.