[Agda] using irrelevant field

[Sergei Meshveliani]

People,
consider the program  

---------------------------------------
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
open import Data.Nat using (ℕ; suc)

record Nonzero : Set where  constructor subEl
                            field  elem   : ℕ
                                   .proof : elem ≢ 0
f : (x : ℕ) → x ≢ 0 → ℕ
f x _ =  suc x

g : Nonzero → ℕ
g (subEl x x≢0) =  f x x≢0
---------------------------------------

It is not type-checked
(in Development Agda of February 16, 2014).

1. Is this all right?

2. This can be fixed by making irrelevant the second argument in  f.
Is this the only way to fix?

Thanks,

------
Sergei