[Agda] Unification assumes injective postulates?

[Andrés Sicard-Ramírez]

On Tue, Nov 13, 2012 at 6:46 PM, Jan Malakhovski <oxij at oxij.org> wrote:

> 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.
>
>
This doesn't answer your question, but you can fix the above code by

{-# OPTIONS --injective-type-constructors #-}

bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)
bar ()

Note that

$ agda --help

says

--injective-type-constructors                   enable injective type
constructors (makes Agda anti-classical and possibly inconsistent)

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121114/88d041b6/attachment.html