Reify PTS & implement subtyping

Don't merge before #112; the only extra commit is 4b75f42.