How does the order of implicit arguments affect idris?

Question

This fails:

> the ({A : Type} -> A -> {B : Type} -> B -> (A, B)) MkPair
(input):1:5:When checking argument value to function Prelude.Basics.the:
        Type mismatch between
                A -> B1 -> (A, B1) (Type of MkPair)
        and
                A1 -> B -> (A1, B) (Expected type)

        Specifically:
                Type mismatch between
                        Pair A
                and
                        \uv => uv -> uv

This works:

> ({A : Type} -> {B : Type} -> A -> B -> (A, B)) MkPair
\A1, B1 => MkPair : A -> B -> (A, B)

Oddly:

q : {A : Type} -> A -> {B : Type} -> B -> (A, B)
q a b = MkPair a b

> :t q
q : A -> B -> (A, B)

> :t MkPair
MkPair : A -> B -> (A, B)

Why do q and MkPair appear to have the same type? Do they really have the same type? Why does the order of implicit arguments matter?

Anton Trunov Anton Trunov · Accepted Answer · 2017-10-21T06:58:22

In some sense implicit arguments are no different from non-implicit ones. The compiler infers them for you most of the time, but they are still arguments and must be present because at the level of the core language there are no implicit arguments. You can ask REPL to show implicits for you:

λΠ> :set showimplicits
λΠ> :t MkPair
Builtins.MkPair : {A : Type} -> {B : Type} -> (a : A) -> (b : B) -> (A, B)
λΠ> :t q
Main.q : {A : Type} -> A -> {B : Type} -> B -> (A, B)

If you substitute ordinary parentheses for curly braces in the above types, you'll see that the types of MkPair and q are different because of the different order of their parameters.

How does the order of implicit arguments affect idris?

1 Answers