Why are unbound implicits invalid when in function position?

44 Views Asked by At

In Type-Driven Development with Idris ch 3, Brady says

Idris will not treat every undefined name as an unbound implicit - only names that begin with a lowercase letter and that appear either on their own or in a function argument. Given the following,

test: f m a -> b -> a

... f isn't treated as an unbound implicit, meaning that it must be defined elsewhere for this type to be valid.

Why can't Idris infer f just as it infers the types of the other variables?

0

There are 0 best solutions below