Hi there!
Exercises in the chapter 10.1.6 (page 328 ) are based on the TakeN datatype:

data TakeN : List a -> Type where
  Fewer : TakeN xs
  Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)

Although I've managed to solve both exercises I'm a bit confused about how the matching works given that `rest` is an implicit argument.
Say I have a branch:

groupN n (n_xs ++ rest) | (Exact n_xs) = ?rhs

How is the value bound to the rest variable at runtime?

Things seem less confusing if I add `rest` as an explicit argument to the Exact constructor.

'rest' is an implicit argument to Fewer, so it is a field of Fewer at run time. That way, it can be bound by pattern matching on Fewer, and then the type checker infers that it must be the same as the second argument of ++.

This is true of all implicit arguments - at least conceptually, you can think of them as being fields of data types. I say "conceptually" because if we actually did this, it would be disastrous for performance. Fortunately, Idris does some analysis of which fields get used and erases those which are either not used or which can be inferred from elsewhere, so in practice you don't need to worry about it.

Thanks, that makes sense!
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.
Thanks for your patience.

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.

Thanks, Ilya. I guess I kind of get it now after reading your answer several times.
One thing I had to wrap my head around was the fact you can unify arguments to (++) which is arbitrary function, not data constructor.

You're welcome!
Yes, surely type checker can (and should) unify function arguments. In fact, after we allow arbitrary expressions in type arguments, type checker has to be able to unify arbitrary expressions.

Hi, I now think my previous comment was really confusing, sorry. Now I understand your concern about unifying function arguments, you are right, in general you wouldn't want to allow this, as it would allow you to prove injectivity for arbitrary function as thus Void. I just hit this bug in my own toy language .

But I still believe that in your example the type checker figured rest1 = rest by the means of unification. I still have to figure out the exact rules but intuitively the use of unification is two-fold: 1.) find valid instantiation for implicits and 2.) learn constraints from dependent data type constructors. And while we definitely don't want to unify function arguments while we are doing 2.), it's safe (and usually does the right thing) while doing 1.).

Don't know if I made it any clearer