idris - 为什么在函数位置时未绑定的隐式无效？

Question

在Idris ch 3的类型驱动开发中，Brady 说

Idris 不会将每个未定义的名称视为未绑定的隐式名称 - 仅以小写字母开头并且单独出现或出现在函数参数中的名称。鉴于以下情况，

test: f m a -> b -> a

...f不被视为未绑定的隐式，这意味着必须在其他地方定义它才能使此类型有效。

为什么 Idris 不能f像推断其他变量的类型一样推断？