[Agda] Agda patterns

[Martin Escardo]

Consider the following, which works:

data _≡_ {ℓ} {X : Set ℓ} : X → X → Set ℓ where
   refl : {x : X} → x ≡ x

pattern reflp x = refl {x}
pattern reflv x = refl {_} {_} {x}

J : ∀ {i j} (X : Set i) (A : (x y : X) → x ≡ y → Set j)
   → ((x : X) → A x x (reflv x))
   → (x y : X) (p : x ≡ y) → A x y p
J X A f x x (reflp x) = f x

The idea is to make the argument of refl explicit if we wish, via the 
pattern definition.

However, the patterns behave differently "as patterns" and "as values". 
For instance, the following doesn't work:

J : ∀ {i j} (X : Set i) (A : (x y : X) → x ≡ y → Set j)
   → ((x : X) → A x x (reflp x))  -- error here
   → (x y : X) (p : x ≡ y) → A x y p
J X A f x x (reflp x) = f x

This doesn't work either:

J : ∀ {i j} (X : Set i) (A : (x y : X) → x ≡ y → Set j)
   → ((x : X) → A x x (reflv x))
   → (x y : X) (p : x ≡ y) → A x y p
J X A f x x (reflv x) = f x -- error here

It would be desirable to have a definition that works both as a pattern 
and as a value. Is that possible?

Thanks,
Martin