Reorganise parsing of base types, and prove it sound.

Two cheats in completeness proof, but this should only be temporary.
Merged