Is there an implementation of higher kinded types in typed lambda calculus?
I doubt you find mainstream languages with HKTs simpler than Scala and
Haskell. And even those don't implement HKTs fully.
Tim Sheard's &Omega;mega   and
some interactive proof assistants have HKTs too.

Chapters 29 and 30 of   Types and Programming Languages 
show exactly how HKTs are added to a typing-system and how to do type-checking with HKTs. Why not do it yourself, it's instructive!