[Agda] `with' question

[Sergei Meshveliani]

Please, what is wrong in the below program?

-----------------------------------------------------------
module Useful where
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Data.Nat   using (ℕ)
open import Data.List  using (List; []; _∷_)

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

    null? :  (xs : List A) → Dec (Null xs)
    null? []      = yes isNull
    null? (_ ∷ _) = no λ()

--------------------------------------------------------                   
f : List ℕ  → ℕ
f []      =  1
f (_ ∷ _) =  0

postulate  ps : List ℕ

g : Dec (f ps ≡ 1)
g with null? ps
... | yes null-ps =  yes (h null-ps)
... | no _        =  no neq
                     where
                     postulate neq : f ps ≢ 1

g' : Dec (f ps ≡ 1)
g'
   with ps | null? ps
... | _ | yes null-ps =  yes (h null-ps)
... | _ | no _        =  no neq
                         where
                         postulate neq : f ps ≢ 1
--------------------------------------------------------------------

g  is type-checked,
and for  g'  it reports that  null-ps  has not the needed type.

(The Agda language is difficult in its proof composition part. 
I do not understand basics of Agda after 3 year practicing with it). 

In this example, the part  "ps |"  is dummy.
But in the real example I need to use both  ps  and  null? ps,
like this:

  ... | []           | null-ps =  foo null-ps
  ... | (_ , 0) :: _ | _       =  \bot-elim ... 0>0
  ...

g'  is a simplification for this real example.

Thank you in advance for explanation,

------
Sergei