Previously, I posted about 7-liner Hindley–Milner type inference written in Prolog.

Today I’ve managed to extend it to support higher-kinded polymorphism (a.k.a. type constructor polymorphsim) and kind polymorphism (of couse, both rank 1).

It is only 25 lines, but I left out pattern matching expressoins because there could be several differnt design choices (e.g. nested pattern support). As long as we are dealing with regular datatypes only, type inference for pattern matching shouldn’t be fundamentally complicated.

One trick I had to come up with is delaying the kind sanity check for function type introduction. If you just call on kind/3 inside type(..., A->B, ...), either one or both of A and B may contain variables that would later be further speciallized and we don’t have enough information for kind checking.