[Agda] Irrelevance and resurrection in type signatures

[Matus Tejiscak]

Dear all,

I have the following program.

> open import Data.Nat
> 
> data Vec (A : Set) : ℕ → Set where
>   Nil : Vec A zero
>   Cons : (n : ℕ) → (x : A) → (xs : Vec A n) → Vec A (suc n)
> 
> vlen : ∀ {A} → .(n : ℕ) → Vec A n → ℕ
> vlen .(zero)   Nil = zero
> vlen .(suc n) (Cons n x xs) = suc (vlen n xs)

Agda complains in the type signature of `vlen` that `n` is declared irrelevant
so it cannot be used in the expression `Vec A n`.

PDF page 12 of http://www2.tcs.ifi.lmu.de/~abel/talkFoSSaCS11.pdf mentions
that "Could not reconcile this with typed equality and large eliminations."

Could anyone shed some light on what the problem is there (and why does ICC*
not suffer from it)? Why cannot we resurrect the context in type signatures?

Thanks!
Matus