Gleb Alexeyev wrote:
The only missing piece of the puzzle here is how exactly is `rest` inferred by the compiler when Exact constructor is applied.
takeN (S n) (x :: xs) should return TakeN (x :: xs).
To implement it, we make a recursive call takeN n xs returning Exact {rest} n_xs such that xs = n_xs ++ rest.
Then we construct Exact (x :: n_xs), which has type of the form TakeN (x :: n_xs ++ rest1) for some rest1 and which should unify with TakeN (x :: xs). Somehow Idris is smart enough to understand that rest1 and rest are equal, but how it does this is beyond me.
But you already have all the needed pieces in the above quote. Because we are working on the Exact clause, the type checker learned that xs should be n_xs ++ rest. And the return type should be TakenN (x :: xs) or (by substitution of xs) TakeN (x :: n_xs ++ rest). And Exact (x :: n_xs) has the type TakeN (x :: n_xs ++ rest1) for some rest1. Unifying it with the return type we get rest1 = rest.
If you are really attentive you might object me and say, look, but the return type is TakeN (x :: (n_xs ++ rest)) and the type of Exact (x :: n_xs) is TakeN ((x :: n_xs) ++ rest1), so how would we unify these two?
The answer is (x :: xs) ++ ys reduces to x :: (xs ++ ys) by the definition of List.++ and Idris can see that.
Going back to your initial question, I think Edwin has answered it already, I just want to mention that explicit/implicit arguments distinction has nothing to do with computationally relevant/irrelevant distinction. Implicit arguments are just a convenience: it actually up to you to decide if you'll make an argument implicit or explicit. For example, you could make everything implicit and use { pattern } everywhere. On the other hand use could make everything explicit and just use a lot of underscores. Usually you choose something in between. The rule of thumb is if an argument can be inferred at most call sites, use implicit, otherwise, use explicit.
|