idris-lang/Idris-dev — pull request #1106 by ziman (2014-04-24 17:28:39+00:00)
Title: Fix erasure from data constructors

This patch includes two changes:
* more careful erasure from underapplied data constructors (+ a test that explains the bug)
* a workaround for non-trivial case-inspection of trivial values

The latter means that, for some reason, we are getting case-inspections like
```Haskell
case {e0} of
refl x => ...
_ => ...
```
The `DefaultCase` is clearly superfluent if the constructor is detaggable (= the only constructor of the family), which is sub-optimal.

What's worse, the extra branch prevents the newtype optimiser from spotting the optimising opportunity, thus generating incorrect code.

This patch adds two ways of dealing with this:
* a workaround for the most common `case x of refl => ...; _ => ...`
* a check that detaggable constructors don't occur in non-trivial case-expressions

However, the correct solution is to make the case-tree elaborator *not* generate unnecessary `DefaultCase` branches.