[Agda] Odd Type Checking Problem

[karim kanso]

Hello Agda users, recently I have encountered a strange problem.

See code below.

While defining equality between elements of Fin n, the two definitions
fineq and fineq' below behave differently when type checking. The fist
definition defined by using equality on ℕ where the second is defined
directly.

At the end of the program, where giving an element of Result, the final
proof that Fineq (suc zero) (negate zero) fails with fineq but succeeds with
fineq'. Agda allows for the trivial proof to be refined but then when type
checked fails with the error:

zero != (suc 0) of type ℕ
when checking that the expression tt has type
Fineq 2 (suc zero) (negate _56)

>From the error message it looks like that there are holes in the term, this
should not be the case as all terms are grounded.

Could someone explain why these two definitions provide different behavior?
To me they appear that they should be the same. I have tried using refl and
it worked with no problems, but am interested why this occurs.

I have tested using the latest development version of both Agda and the
standard
library.

Karim Kanso
Swansea University

module oddprob where

open import Data.Nat
open import Data.Fin
open import Data.Bool
open import Data.Unit

_==_ : ℕ → ℕ → Bool
zero == zero = true
(suc n) == (suc m) = n == m
_ == _ = false

fineq : (n : ℕ) → Fin n → Fin n → Bool
fineq k n m = toℕ n == toℕ m

fineq' : (n : ℕ) → Fin n → Fin n → Bool
fineq' .(suc n) (zero {n}) zero = true
fineq' .(suc n) (zero {n}) (suc i) = false
fineq' .(suc n) (suc {n} i) zero = false
fineq' .(suc n) (suc {n} i) (suc i') = fineq' n i i'

Fineq : (n : ℕ) → Fin n → Fin n → Set
Fineq k n m = T (fineq k n m)

negate : (s : Fin 2) → Fin 2
negate zero = suc zero
negate (suc zero) = zero
negate (suc (suc ()))

data Result (a : Fin 2) : Fin 2 → Set where
  res : (b : Fin 2) → Fineq 2 b (negate a) → Result a b

r : Result zero (suc zero)
r = res (suc zero) tt
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091212/a70e373e/attachment.html