[Agda] Trouble with the 'with' clause

[Balaji Rao]

Hi,

I ran into a problem with the ‘with’ clause and here’s a silly demonstration. 

--
open import Data.Nat
open import Relation.Binary.PropositionalEquality

module Test where
  postulate
    f : ℕ → ℕ
    h : ∀ {a} (b : ℕ) → f a ≡ b → a ≡ a
    
  g : ∀ {a} → a ≡ a
  g {a} with f a 
  ... | b = h b {!!} 
—

I end up with a goal to prove f a = b, and refl doesn’t work. Is it a bug ?

-- 
Balaji