Order of implicit arguments in idris

Question

How does the order of implicit arguments affect idris?

I just read this post and I got curious about MkPair's type signature. I tried MkPair 10 on REPL and I got

(input):Can't infer argument B to Builtins.MkPair

And this is exactly what I expected. From its type signature Builtins.MkPair : {A : Type} -> {B : Type} -> (a : A) -> (b : B) -> (A, B), I have to pass B(whether it's implicit or explicit) before apply a value for a. At the same time, I expected q 10 to work, cause its type is q : {A : Type} -> (a : A) -> {B : Type} -> (b : B) -> (A, B) which tells me that I don't need any value for B before I apply a value for A and a.

But it also failed with the same message!

(input):Can't infer argument B to Main.q

What happens to q?

And I have one more question . Before I found that q worked neither, I was gonna ask the reason that Idris compiler prefers MkPair's signature to q's one. MkPair looks unnecessarily eager to me. Why does it demand B too early?

Julian Kniephoff Julian Kniephoff · Accepted Answer · 2020-01-14T15:55:09

Without any context to guide the compiler, I guess Idris stays true to its eager by default attitude and tries to infer all the implicit arguments that appear before the last "explicit" one specified, before doing automatic partial application.

Note that you can suppress this behavior by placing the expression in an appropriately typed hole:

the ({b : Type} -> b -> (Nat, b)) (q 10)

-- or

r : {b : Type} -> b -> (Nat, b)
r = q 10

Order of implicit arguments in idris

1 Answers