[Agda] Argument order, universes and erasability

[Mathijs Kwik]

Hi all,

I have a bunch of questions, but I think they are somehow related.

A little while ago, the idris standard library chose to swap the
arguments for Vec from `Vec A n` to `Vec n A`. I did not really pay
attention at the time, but a while later I found the paper "Hasochism:
The Pleasure and Pain of Dependently Typed Haskell", which explores
how far haskell can go already towards dependent types. This paper
used `Vec n A` as well, which proved convenient when defining
Traversable/Foldable/Functor instances for it. Are there any other
advantages or disadvantages either way?

I tried to declare `Vec n A` with agda as well, but because agda makes
this clear distinction between parameters and indexes, this meant I
had to make the Set parameter into an index, which forces `Vec n A` to
become Set1.
Now, I have some understanding of Russell's paradox, and Set-in-Set
problems, so I understand why a List of Sets becomes Set1 itself. But
I don't see why this would apply to Vec if it's indexed with one
instead of parameterized. It's still just _a Set_, not Set itself.
What's the logic behind this?

One reason I could think of myself is that it has to do with
static/dynamic stuff. If for some reason all indexes are kept around
dynamically, and initiated on construction (when creating a Vec at
runtime), I can see how "something that keeps track of a Set" cannot
be a Set by itself, but that sounds more like a technical issue, and
I'm not at all sure if this is true.

But speaking of dynamic stuff: how far is Agda able to erase type
information when compiling? I understand this might be very tricky. If
I only use indexes to guard myself from making mistakes (tracking
meta-info), I would like all that to be erased from runtime. For
example:

test1 : forall {n} -> Vec Nat n -> Nat
test1 v = head (v ++ (0 :: []))

In this case I really don't care about n at runtime, but vectors still
guard me from applying head to something empty at compile-time.
While in this example:

length1 : forall {n A} -> Vec A n -> Nat
length1 [] = zero
length1 (x :: xs) = succ (length1 xs)

length2 : forall {n A} -> Vec A n -> Nat
length2 {n} v = n

I would expect length1 to have an erasable n (at the cost of
traversing the vector to get its length), while length2 would have a
runtime Nat associated with it.
Am I correct in this assumption? Or is reality far more complicated? :)

Thanks,
Mathijs