code: cite the bidirectional inference paper
core: comments and cleanups to checker
core: kind checker refactor, and detect universe malfunctions with tyvars