<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"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></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 -> (_A -> _B) -> _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> 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 <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a><br>
<mailto:<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>>> 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 (ℕ; _≮_; _≤_; _≥_; _<_)<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 <→≤ : ∀ {m n} → m < 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< m<n _ _ ) → ⊥-elim (m≮n m<n)<br>
; (tri≈ _ m=n _ ) → ≤refl m=n<br>
; (tri> _ _ m>n) → let n<m : n < m<br>
n<m = m>n<br>
<br>
n≤m : n ≤ m<br>
n≤m = <→≤ {n} {m} n<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< m<n _ _ = ⊥-elim (m≮n m<n)<br>
≮→≥ m≮n | tri≈ _ m=n _ = ≤refl m=n<br>
≮→≥ {m} {n} m≮n | tri> _ _ m>n =<br>
let n<m : n < m<br>
n<m = m>n<br>
<br>
n≤m : n ≤ m<br>
n≤m = <→≤ {n} {m} n<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 <>< 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>