More type soundness progress.

But the system is still not quite right for non-global cenvs.