Performance/compiler temporary hack: %erase

This is a (temporary!) annotation for erasing implicit constructor
arguments which are not forceable, and would otherwise remain in
compiled code. e.g.:

  data Binary : (width : Nat) -> (value : Nat) -> Type where
         zero : Binary Z Z
         num  : %erase bit, v
                Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)

This would erase 'bit' and 'v' from the num constructor (w is already
forceable). If bit or v is required for any reason, compilation will
fail.

This is a TEMPORARY HACK (no, honestly, it is) until we have more
general erasure of implicit arguments (which is coming) but this is a
placeholder which is required for some existing examples. Use at your
own risk!

Note that any code which abuses this will fail to compile, so it is at
least sound...