Implicit arguments in Idris

Question

I need some help interpreting an error message regarding implicit arguments in Idris and why a small change fixes it. This is the code:

import Data.Vect

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse {n} (x :: xs)
  = let result = myReverse xs ++ [x] in
                 ?rhs

It results in this error:

When checking left hand side of myReverse:
When checking an application of Main.myReverse:
        Type mismatch between
                Vect (S len) elem (Type of x :: xs)
        and
                Vect n elem (Expected type)

        Specifically:
                Type mismatch between
                        S len
                and
                        n

However, replacing {n} with {n = S len}, the code type-checks.

I thought that using {n} was simply meant to bring the implicit n argument of the function into scope. Why would this result in an error?
What does the error message mean? The only interpretation I can think of is that the implicit argument n in the type is rewritten due to pattern-matching x::xs into S len, and Idris loses information that these are the same.
How does replacing it with {n = S len} work?

Markus Markus · Accepted Answer · 2018-07-12T14:57:20

Your best bet in these cases is to use idris to do the programming for you. If you start with

myReverse : Vect n elem -> Vect n elem
myReverse {n} xs = ?myReverse_rhs

and now case split on xs you get

myReverse : Vect n elem -> Vect n elem
myReverse {n = Z} [] = ?myReverse_rhs_1
myReverse {n = (S len)} (x :: xs) = ?myReverse_rhs_2

So not only did idris do a case split on xs, but also on n, since for an empty vector the length must be Z, and for a nonempty vector it must be at least S len. Which also implies that xs is now of length len.

Since n is also on the right hand side of your function, it is obvious that you need to provide something for myReverse_rhs_2 which is of length S len which equals n when you did the pattern matching right.

In the error message idris doesn't know what n is, hence the message.

Implicit arguments in Idris

1 Answers