[Agda] coverage in Agda-2.1.3

[Conor McBride]

Hi Thorsten

On 7 May 2008, at 10:54, Thorsten Altenkirch wrote:
> 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

That's a matter of fact.

> more fascist.

That's a matter of opinion.


> 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.

My guess would be that the coverage checker isn't trying
all possible splitting strategies. The error suggests
that your explicit {succ m} patterns have provoked into
splitting the first number, so now it has a {zero} case
which you haven't covered. Ana's suggested fix is a good
one; there's a slightly trickier fix with

   fpair .{succ m} {n} (fz {m}) i
   fpair .{succ m} {n} (fs {m} j) i

which forces the split you want.

So this email is just by way of an old Epigram troll
saying that it is sometimes useful to choose explicitly
what to do case on. I have another example, which I'll
send along later...

This does raise the question of what Agda's strategy
actually is, when choosing the way to construct the
tree. It's not just about whether or not to complain
about coverage failure. It can sometimes affect the
definitional equations which hold on open terms, and
sometimes we care quite a lot about that issue.

My suspicion is that Agda splits on the leftmost
argument for which a constructor pattern occurs in
some line of the program: is that so?

Examples such as Thorsten's above show that it might
be preferable to split on more-indexed arguments
before less-indexed arguments, and on arguments
where all constructors are present before arguments
where some are missing. Crucially though, it would
be good to split on arguments which have a
constructor in all lines before those which have,
say, variables in some lines and constructors in
others: otherwise we lose definitional equations.

There may also be a case to instate the missing bit
of the Brady notation, which would allow

   fpair {.succ m} {n} fz i
   fpair {.succ m} {n} (fs j) i

This can only split on the Fin, but then *projects*
m out from under the succ which is already known to
be present without further matching.

But I guess the key priority is to ensure that the
equational theory is as predictable (controllable?)
as possible, so humans should probably follow the
heuristic "if you can think of an impossible case,
write it down".

It may be disturbing, but managing the intensional
behaviour of terms is important. We need enough
language to allow us that level of control.

All the best

Conor