[Agda] --exact-split

[Martin Escardo]

I have a development that uses --exact-split in all modules.

But I have a function I can't make to satisfy --exact-split.

I developed this function using case-split.

One question is: shouldn't be the case that if all pattern matching is
developed not manually but mechanically using case-split, then
--exact-split should be automatically satisfied?

At first I thought this could have something to do with the simultaneous
use of --without-K. But then I removed all pattern matching on
identifications, using helper functions that pass the --exact-split test.

The main question is: what promises does --exact-split (not) make, and
what promises should I, as its user, fulfill?

Martin