<br><br><div class="gmail_quote">On Tue, Nov 13, 2012 at 6:46 PM, Jan Malakhovski <span dir="ltr"><<a href="mailto:oxij@oxij.org" target="_blank">oxij@oxij.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello everyone,<br>
<br>
Without further ado, the following code:<br>
<br>
~~~~<br>
module UnificationWithPostulates where<br>
<br>
data _≡_ {A : Set} (x : A) : A → Set where<br>
refl : x ≡ x<br>
<br>
data ℕ : Set where<br>
zero : ℕ<br>
succ : ℕ → ℕ<br>
<br>
postulate foo : ℕ → ℕ<br>
<br>
bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)<br>
bar refl = {!!}<br>
~~~~<br>
<br>
fails with:<br>
~~~~<br>
zero != succ zero of type ℕ<br>
when checking that the pattern refl has type<br>
foo zero ≡ foo (succ zero)<br>
~~~~<br>
<br>
Basically, it sounds like "I have to be inconsistent to allow this match".<br>
<br>
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).<br>
Running Agda with --verbose=10 helped.<br>
<br>
It's easy to fix the code above, but I think it's not that easy in the general case.<br>
It might not always be possible not to pattern match or to expand a failing postulate.<br>
<br></blockquote><div><br>This doesn't answer your question, but you can fix the above code by<br><br>{-# OPTIONS --injective-type-constructors #-}<br><br>bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)<br>
bar () <br><br>Note that <br><br>$ agda --help<br><br>says<br><br>--injective-type-constructors
enable injective type constructors (makes Agda anti-classical and
possibly inconsistent)<br></div></div><br>-- <br>Andrés<br><br>