Fix/erasure 2

Not a complete fix for erasure yet. But we can now do -Ycheck:frontend and ensure
that typechecked trees typecheck. 

Before attacking erasure, we should merge this pull request and then check all other phases one by one with -Ycheck to make sure their output is type-correct.

Question: Should we enable -Ycheck:all in the checkin tests? The only downside is that it could slow down tests too much. Maybe enable it only for some tests?