Reify PTS & implement language subtyping, v2

Updated version of #113. If this is fine, I should probably squash to a single commit.