<br><br><div class="gmail_quote">On Tue, Nov 13, 2012 at 6:46 PM, Jan Malakhovski <span dir="ltr">&lt;<a href="mailto:oxij@oxij.org" target="_blank">oxij@oxij.org</a>&gt;</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 &quot;I have to be inconsistent to allow this match&quot;.<br>
<br>
I bumped upon this behavior while &quot;manually rewriting&quot; an expression with &quot;with&quot; 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&#39;t bind (generated by a proof term deep inside).<br>


Running Agda with --verbose=10 helped.<br>
<br>
It&#39;s easy to fix the code above, but I think it&#39;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&#39;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>