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?