idris-lang/Idris-dev — pull request #718 by ziman (2013-12-10 17:43:53+00:00)
Title: Recursive constructor disjointness + cleanup in DataOpts.hs

These changes are mostly a by-product of my attempt to add recursive forcing (which we already know is not a good idea). I removed the recursive forcing, leaving the recursive disjointness and the general cleanup in.

The changes:
* Collapsibility reformulated in terms of conditional/unconditional forceability and disjointness, hopefully in a more readable and straightforward way.
* Constructor target disjointness check made recursive — now it can distinguish between `[]`, `[x]`, and `x :: y :: xs`.
* `[Int]` replaced by `IntMap`, which is both more convenient and readable.
* Some overly verbose `do`-blocks replaced by simpler `Applicative` expressions.
* Some expressions that were unnecessarily monadic simplified to the pure form.

There's also a `Binary` instance for `Forceability` in `IBC.hs` but I expect it to be overwritten when `IBC.hs` is generated next time.