idris-lang/Idris-dev — pull request #1026 by ziman (2014-04-04 15:37:41+00:00)
Title: Erasure by usage analysis (initial version)

Usage warnings are off by default for now, until we improve general usability:

* case-tree building should avoid dotted fields in constructors
* usage error reporting should give more, clearer information
* (ir)relevance annotations should be implemented to trigger warnings ASAP (without `main`), which is necessary for library writers

You can use `--warnreach` to get them anyway and possibly `--dumpcases` to get a better idea why they pop up.

Some programs that use this new erasure to improve their *asymptotic* complexity can be seen in https://github.com/ziman/idris-benchmarks.