I really don't see how. There's a ton of useful stuff with HKTs, type families, GADTs, etc that you can't hope to achieve with ocaml's type system. Recently,

I really don't see how. There's a ton of useful stuff with HKTs, type families, GADTs, etc that you can't hope to achieve with ocaml's type system. Recently, I've found myself using extensive type-level arithmetic for automatic hardware generation and verification. This requires a number of powerful type system features (type level literals, kind promotion, type functions and equality constraints a la type families, type normalization plugins) that wouldn't work at all in ocaml.