As C++ features go, HKTs in the form of template arguments and templated associated types are fairly straightforward to use and understand. In fact we had usable type level lambdas before we got actual lambdas in the language.

Of course, as the rest of templates there is no actual definition time type checking.