That’s what I thought as well, but higher-kinded types are not necessary, as long as you limit the number of unique variables in an expression. Then it’s fairly straightforward to build a state machine to capture the variables and perform partial application. Only downside is the code size, which can be reduced somewhat but is roughly O(2ⁿ) w.r.t. the number of unique variables.
Re: Kotlin. It can also be implemented in Java or any language with subtyping and generics (I believe). It’s just a proof of concept, but also a demonstration that less powerful type systems like Kotlin and Java are also capable of encoding some interesting properties.
In terms of usability, it would be easier to implement arity-checking and currying at runtime but if implemented at the type-level would allow for code completion and inference. The
#arrow folks are using a similar approach for their curry implementation, which is order-sensitive:
https://github.com/arrow-kt/arrow/blob/master/modules/core/arrow-syntax/src/main/kotlin/arrow/syntax/function/currying.kt