[Agda] Unification assumes injective postulates?

[Jan Malakhovski]

Hello everyone,

Without further ado, the following code:

~~~~
module UnificationWithPostulates where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

postulate foo : ℕ → ℕ

bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)
bar refl = {!!}
~~~~

fails with:
~~~~
zero != succ zero of type ℕ
when checking that the pattern refl has type
foo zero ≡ foo (succ zero)
~~~~

Basically, it sounds like "I have to be inconsistent to allow this match".

I bumped upon this behavior while "manually rewriting" an expression with "with" construct in a proof of a considerable size and was quite surprised to see an unification error which mentioned equality failure for the variables that I didn't bind (generated by a proof term deep inside).
Running Agda with --verbose=10 helped.

It's easy to fix the code above, but I think it's not that easy in the general case.
It might not always be possible not to pattern match or to expand a failing postulate.

By the way, I'm still using 2.3.0.1, but there is no mentions about any unification changes in release notes for 2.3.2, so I assume it still works this way.
Why does it work this way?

Best regards,
  Jan