[Agda] coverage in Agda-2.1.3

[Thorsten Altenkirch]

Hi,

I have just installed 2.1.3 on my desktop, while my laptop still runs  
2.1.2. It seems that the coverage checker has become more fascist. The  
following definition was accepted on 2.1.2

   fpair : forall {m n} -> Fin m -> Fin n -> Fin (m × n)
   fpair {succ m} {n} fz     i = finl {n} {m × n} i
   fpair {succ m} {n} (fs j) i = finr {n} {m × n} (fpair j i)

but is rejected on 2.1.3:

Incomplete pattern matching for fpair. Missing cases:
   fpair {zero} {_} _ _
when checking the definition of fpair

I don't agree since fz, fs already constitute a cover. In any case,  
how would I fill in this case? I tried

   fpair : forall {m n} -> Fin m -> Fin n -> Fin (m × n)
   fpair {zero}   {n} i      ()
   fpair {succ m} {n} fz     i = finl {n} {m × n} i
   fpair {succ m} {n} (fs j) i = finr {n} {m × n} (fpair j i)

but Agda says (in the ghci buffer !?)

Fin n should be empty, but it isn't (as far as I can see)
when checking that the clause fpair {zero} {n} i () has type ...

It seems that I have the choice to revert to 2.1.2 or:

   impossible : {A : Set} -> Fin zero -> A
   impossible ()

   fpair : forall {m n} -> Fin m -> Fin n -> Fin (m × n)
   fpair {zero}   {n} j      _ = impossible j
   fpair {succ m} {n} fz     i = finl {n} {m × n} i
   fpair {succ m} {n} (fs j) i = finr {n} {m × n} (fpair j i)

Cheers,
Thorsten
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.