Andreas Abel

The positivity checker does not have knowledge of the _later_ modality, so it rejects this negative definition. Is it safe to ignore negative occurrences under _later_? Is there some literature...

Positivity checking is not integrated with termination checking, see: - https://github.com/agda/agda/issues/4563 (Your issue might be a duplicate of this one.) So you cannot write things like ```agda data Ty :...

The testsuite does not build, but the library seems to build, does it?

From your report it seems that 2 golden values are wrong for a 32 bit system. One could insert some `#if` conditionals so that if built on a 32 bit...

FYI: benchmark run: ``` time ./words.bin +RTS -s < /usr/share/dict/words 235976 1,749,384,800 bytes allocated in the heap 10,807,296 bytes copied during GC 62,848 bytes maximum residency (2 sample(s)) 35,456 bytes...

Thanks, @PiotrJustyna for the contribution!

@ocharles PR ready.

Ping @ocharles

@plt-amy: please also correct the milestone for this issue.

I tried current `master` of cabal and that one works fine.