Some work on type soundness.

This will require more plumbing than I initially thought, since the cenv
and menv can now change from step to step.