<div dir="ltr"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">Thanks for the explanation!<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 11 February 2015 at 10:50, Andreas Abel <span dir="ltr">&lt;<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Ah, I think it is because type information is not propagated optimally into an extended lambda (in this case at least).<br>
<br>
It infers the wrong result type (m \leq n) from the clause rhs (\leqrefl m=n) and then fails when checking the subsequent clauses.<br>
<br>
In particular as case_of_ has type _A -&gt; (_A -&gt; _B) -&gt; _B  and the arguments are checked before unifying _B with the expected return type (n \leq m), result type _B is actually inferred from the clause rhss.<br>
<br>
This explains the puzzle.<span class="HOEnZb"><font color="#888888"><br>
<br>
Andreas</font></span><div class="HOEnZb"><div class="h5"><br>
<br>
<br>
On 11.02.2015 16:43, Andreas Abel wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Yes, the error location is wrong when clause tri&gt; comes before<br>
tri\approx (otherwise it is correct).  Weird.<br>
<br>
On 11.02.2015 14:18, Andrés Sicard-Ramírez wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
On 11 February 2015 at 05:37, Sergei Meshveliani &lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a><br>
&lt;mailto:<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;&gt; wrote:<br>
<br>
    Please, what is wrong here?<br>
<br>
    ------------------------------<u></u>------------------------------<u></u>--------<br>
    open import Function        using (case_of_)<br>
    open import Relation.Binary using (module DecTotalOrder;<br>
                                        module StrictTotalOrder;<br>
module Tri)<br>
    open import Data.Empty using (⊥-elim)<br>
    open import Data.Nat as Nat using (ℕ; _≮_; _≤_; _≥_; _&lt;_)<br>
    open import Data.Nat.Properties as NatProp using ()<br>
<br>
    open StrictTotalOrder NatProp.strictTotalOrder using (compare)<br>
    open DecTotalOrder    Nat.decTotalOrder using ()<br>
                                             renaming (reflexive to<br>
≤refl)<br>
    open Tri<br>
<br>
<br>
    postulate  &lt;→≤ : ∀ {m n} → m &lt; n → m ≤ n<br>
<br>
    ≮→≥ : ∀ {m n} → m ≮ n → n ≤ m<br>
    ≮→≥ {m} {n} m≮n =<br>
         case compare m n<br>
         of \<br>
         { (tri&lt; m&lt;n _   _   ) → ⊥-elim (m≮n m&lt;n)<br>
         ; (tri≈ _   m=n _   ) → ≤refl m=n<br>
         ; (tri&gt; _   _    m&gt;n) → let n&lt;m : n &lt; m<br>
                                     n&lt;m = m&gt;n<br>
<br>
                                     n≤m : n ≤ m<br>
                                     n≤m = &lt;→≤ {n} {m} n&lt;m<br>
                                 in<br>
                                 n≤m<br>
         }<br>
<br>
<br>
​Rewriting the function by<br>
<br>
≮→≥ : ∀ {m n} → m ≮ n → n ≤ m<br>
≮→≥ {m} {n} m≮n with compare m n<br>
≮→≥         m≮n | tri&lt; m&lt;n _   _   = ⊥-elim (m≮n m&lt;n)<br>
≮→≥         m≮n | tri≈ _   m=n _   = ≤refl m=n<br>
≮→≥ {m} {n} m≮n | tri&gt; _   _   m&gt;n =<br>
   let n&lt;m : n &lt; m<br>
       n&lt;m = m&gt;n<br>
<br>
       n≤m : n ≤ m<br>
       n≤m = &lt;→≤ {n} {m} n&lt;m<br>
   in n≤m<br>
<br>
Why does ​Agda (correctly) report the error ​in `≤refl m=n`, but using<br>
the original function Agda reports the error `n≤m`?<br>
<br>
--<br>
Andrés<br>
<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br>
</blockquote>
<br>
<br>
</blockquote>
<br>
<br>
-- <br>
Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</div></div></blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr">Andrés</div></div></div></div>
</div>