[Agda] irrelevancy annotation

[mechvel at scico.botik.ru]

Please,
how to fix the following example with irrelevancy denotation?

module _ {A : Set α}
   where
   data Null : List A → Set α  where  isNull : Null []

   head : (xs : List A) .(nn : ¬ Null xs) → A
   head (x ∷ _) _  = x
   head []      nn = contradiction isNull _    -- ?

   test : ∀ {xs} (nn nn' : ¬Null xs) → head xs nn ≡ head xs nn'
   test _ _ = refl

The second pattern in `head` cannot be skipped,
but I do not find how to fix it.

Thanks,

------
Sergei