[Agda] question on irrelevant argument

[Sergei Meshveliani]

Please,
how to fix  foo2, foo3  shown below?

----------------------------------------------------------------
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Data.Empty using (⊥-elim)
open import Data.Nat   using (ℕ; module ℕ)

open ℕ

foo : (m n : ℕ) → n ≢ zero → ℕ             -- this works
foo _ (suc n) _  =  n
foo _ zero    nz =  ⊥-elim (nz PE.refl)


foo2 : (m n : ℕ) → .(n ≢ zero) → ℕ
foo2 _ (suc n) _ =  n
foo2 _ zero    _ =  ⊥-elim (u PE.refl)     -- is not type-checked
                    where
                    u : zero ≢ zero
                    u = _
{-                                                                              
foo3 : (m n : ℕ) → .{nz : n ≢ zero} → ℕ   
foo3 _ (suc n) {_} =  n                         
foo3 _ zero    {_} =  ⊥-elim (u PE.refl)      -- is not type-checked    
                      where                        
                      u : zero ≢ zero                                
                      u = {!!}                             
-}
---------------------------------------------------------------------

The checker   (of  development Agda of January 8, 2014)

does not allow to skip the `zero' branch, nor to set () there,
nor to apply  ⊥-elim  
(nz  is rejected for  u,  as well as '_').

Thanks,

------
Sergei