[Agda] Wrong reporting error ? (Was question on `compare')

[Andreas Abel]

Ah, I think it is because type information is not propagated optimally 
into an extended lambda (in this case at least).

It infers the wrong result type (m \leq n) from the clause rhs (\leqrefl 
m=n) and then fails when checking the subsequent clauses.

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.

This explains the puzzle.

Andreas


On 11.02.2015 16:43, Andreas Abel wrote:
> Yes, the error location is wrong when clause tri> comes before
> tri\approx (otherwise it is correct).  Weird.
>
> On 11.02.2015 14:18, Andrés Sicard-Ramírez wrote:
>>
>> On 11 February 2015 at 05:37, Sergei Meshveliani <mechvel at botik.ru
>> <mailto:mechvel at botik.ru>> wrote:
>>
>>     Please, what is wrong here?
>>
>>     --------------------------------------------------------------------
>>     open import Function        using (case_of_)
>>     open import Relation.Binary using (module DecTotalOrder;
>>                                         module StrictTotalOrder;
>> module Tri)
>>     open import Data.Empty using (⊥-elim)
>>     open import Data.Nat as Nat using (ℕ; _≮_; _≤_; _≥_; _<_)
>>     open import Data.Nat.Properties as NatProp using ()
>>
>>     open StrictTotalOrder NatProp.strictTotalOrder using (compare)
>>     open DecTotalOrder    Nat.decTotalOrder using ()
>>                                              renaming (reflexive to
>> ≤refl)
>>     open Tri
>>
>>
>>     postulate  <→≤ : ∀ {m n} → m < n → m ≤ n
>>
>>     ≮→≥ : ∀ {m n} → m ≮ n → n ≤ m
>>     ≮→≥ {m} {n} m≮n =
>>          case compare m n
>>          of \
>>          { (tri< m<n _   _   ) → ⊥-elim (m≮n m<n)
>>          ; (tri≈ _   m=n _   ) → ≤refl m=n
>>          ; (tri> _   _    m>n) → let n<m : n < m
>>                                      n<m = m>n
>>
>>                                      n≤m : n ≤ m
>>                                      n≤m = <→≤ {n} {m} n<m
>>                                  in
>>                                  n≤m
>>          }
>>
>>
>> ​Rewriting the function by
>>
>> ≮→≥ : ∀ {m n} → m ≮ n → n ≤ m
>> ≮→≥ {m} {n} m≮n with compare m n
>> ≮→≥         m≮n | tri< m<n _   _   = ⊥-elim (m≮n m<n)
>> ≮→≥         m≮n | tri≈ _   m=n _   = ≤refl m=n
>> ≮→≥ {m} {n} m≮n | tri> _   _   m>n =
>>    let n<m : n < m
>>        n<m = m>n
>>
>>        n≤m : n ≤ m
>>        n≤m = <→≤ {n} {m} n<m
>>    in n≤m
>>
>> Why does ​Agda (correctly) report the error ​in `≤refl m=n`, but using
>> the original function Agda reports the error `n≤m`?
>>
>> --
>> Andrés
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/