[Agda] Unification assumes injective postulates?

[Nils Anders Danielsson]

On 2012-11-14 00:46, Jan Malakhovski wrote:
> 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)
> ~~~~

The only way Agda can succeed here is if zero and succ zero are
definitionally equal.

For some discussion about whether postulates should be injective or not,
see the following bug report:

   http://code.google.com/p/agda/issues/detail?id=170

-- 
/NAD