An executable checker for type annotated expressions.

check_e checks that an annotated expression does indeed type check.
I've proved that if check_e says it type checks, then the core type
system (type_e) does too.  I've not proved the other direction because
that seems less important.  I hope that the translator can now also
easily prove that it is generating well-typed programs using check_e.

There are 3 cheats where the expression and patterns need more
annotation: for raise expressions and the two cases of constructor
application, but I didn't want to add those while we're in a good state
on the master branch.

I haven't written a check_ds counterpart for type_ds.

I've used an exception monad throughout, so check_e might also be an
interesting test case for the translator for generating real exception
raising code (I never handle any exceptions).