Support A-normalization & cleanups

* Support A-normalization, written in CPS. In fact, Tillmann convinced me we probably want to use a writer monad instead of CPS, because it's more flexible for variations of A-normalization (such as producing one let with many variables instead of many lets, and relatedly CSE).
* Support let in untyped syntax & type inference.
* Cleanups in type inference.