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.