Search for `auto`-params is inconsistent when searched type is function

[buzden]

Consider some definitions

data X : Type

someX : X

data Y : Type

fun : X -> (X -> Y) => Nat

It is important what Y is abstract (no definition), or defined somwhere being exported non-publicly, or defined with [noHints] option.

Consider also that we have some function, that takes a function X -> Y as an auto-implicit argument:

f1 : (X -> Y) => Nat
f1 = fun someX + 5

It typechecks, as expected.

One can add additional parameters, say, in front of the auto-implicit argument and all still typechecks:

f1' : Integer -> (X -> Y) => Nat
f1' _ = fun someX + 5

Steps to Reproduce

Now, add an (irrelevant) parameter of type X, i.e. a type that is also an argument type of a function, which is a type of the auto-implicit parameter:

f2 : X -> (X -> Y) => Nat
f2 _ = fun someX + 5

One can add it also after the auto-implicit parameter:

f2' : (X -> Y) => X -> Nat
f2' _ = fun someX + 5

One can also have value of type X in the scope, not exactly as a parameter:

f2'' : (X -> Y) => Nat
f2'' = let xx = someX in fun someX + 5

Expected Behavior

I'd expect all the changes to typecheck.

Observed Behavior

All additions fail similarly:

Error: While processing right hand side of f2. Can't find an implementation for Y.

WrongSearchedAuto:16:8--16:17
 15 | f2 : X -> (X -> Y) => Nat
 16 | f2 _ = fun someX + 5
             ^^^^^^^^^

and

Error: While processing right hand side of f2'. Can't find an implementation for Y.

WrongSearchedAuto:19:9--19:18
 18 | f2' : (X -> Y) => X -> Nat
 19 | f2' _ = fun someX + 5
              ^^^^^^^^^

and

Error: While processing right hand side of f2''. Can't find an implementation for Y.

WrongSearchedAuto:24:26--24:35
 23 | f2'' : (X -> Y) => Nat
 24 | f2'' = let xx = someX in fun someX + 5
                               ^^^^^^^^^

Discussion

It seems that having an X value in the scope makes the auto-parameter's search facility to look for Y once X -> Y is required. This is validated by the fact that this typechecks:

f3 : X -> Y => Nat
f3 _ = fun someX + 5

[buzden]

BTW, making someX to be %hint, or X being implemented without [noHint] does not change anything. I.e., only local scope affects to this issue.