Lambda the Ultimate

Ωmega by Tim Sheard

...Ocaml counts, though I wouldn't exactly call it pleasant just yet. At ICFP, Jacque Garrigue reported that there was work underway to increase the amount of type inference done on programs with first-class modules, which will surely help a lot.

Also, Agda supports higher kinded programming, as does Coq.

OCaml and other MLs do not provide higher kinds directly, but they can be emulated through the use of functors.

C++ has "template template arguments", which give you a form of higher-order type constructors. Since they are basically untyped, there arguably are no kinds, though.

Any language with type universes, like Coq or Agda, subsumes higher kinds. In these language, kinds are just types one level up, with the full expressive power of "ordinary" types, and there usually is an infinite tower of them.

There are also languages that collapse this tower, i.e. "type" (aka the kind "*") is just a type itself. These are even more expressive -- to the point that they are no longer logically consistent.

Ur by Adam Chlipala.