Bidirectional typing for dependent types: Why are Sigma, Pi synthesized?
IMHO, it's not like constructors are checked, but introduction rules (including tuples, lambdas, data constructors, etc.) are checked (while elimination rules are synthesized). The kind constructors you mentioned are called formation rules, which are not introduction rules. You can also think this way: if a constructor is checked, then it has a corresponding eliminator which is synthesized. If type constructors should be checked, there should be a corresponding thing synthesized. But there's no such thing (you can't pattern match on $\cal U$).