From here on out, I can start playing with concrete code that attempts to actually typecheck limited syntactic constructs, and see what I end up with.