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

[Andreas Abel]

https://code.google.com/p/agda/issues/detail?id=1431

On 11.02.2015 16:50, Andreas Abel wrote:
> 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/