Comment by Nelkins

There are libraries that simulate a lot of these things (e.g. https://github.com/G-Research/TypeEquality for GADTs). You're absolutely right that it's not as first class as in OCaml, but the tools are there if you want them.