idris-lang/Idris-dev — pull request #1392 by ziman (2014-07-15 13:43:36+00:00)
Title: Fix erasure from data constructors

The comparison `compare arity (length args)` is backwards. Strangely enough, I can't construct a failing testcase because other features of the language seem to always exactly saturate data constructors — and that's probably also the reason that the bug has not manifested so far.

This also means that all that elaborate code that handles underapplied data constructors is 1) unused 2) untested. Maybe we should delete it.

[On the other hand, I'm now experimenting with erasure from functions (arguments are actually *removed*, not `NULL`ed) so if that turns out to be a worthwhile optimisation, that code will actually be put to use.]