Idris - Use implicit variable inside function

Question

How can we use an implicit variable inside a function? Reducing to the simplest possible case, is it possible to have:

dim : Vect n a -> Nat
dim vec = n

without getting the error:

When elaborating right hand side of rep:
No such variable n

Is there a way to access there values from inside? Or is it the same as asking for n inside sin n?

In this case, is it possible to prove that Vect is a "bijection" and recover the variables from there?

Answer 1

There is really no such variable n because it is not bounded by pattern matching.

You need to explicitly bring implicit variables in scope:

dim : Vect n a -> Nat
dim {n} vec = n

It is possible to view them in idris REPL:

*> :set showimplicits
*> :t dim 
Main.dim : {n : Prelude.Nat.Nat} -> {a : Type} ->
     (__pi_arg : Prelude.Vect.Vect n a) -> Prelude.Nat.Nat