* GADTs: generalized algebraic data types. As the name suggests, GADTs broaden the set of type-level constraints that one can encode using ADTs. A canonical example involves using GADTs to strongly type an AST and evaluator function s.t. attempting to construct or operate on an invalid AST, e.g., one that represents addition between a boolean and an integer, is a compile-time error [1]. Another great tutorial on GADTs is [2].
* Row polymorphism: statically type-checked duck types, for lack of a better description. In dynamic languages like python or javascript, it's common to pass dict or dict-like objects to functions and have them extract the key/value pairs that they need. Row polymorphism lets you have your cake and eat it too by enforcing enough structure to ensure that functions only receive records containing all relevant keys — without requiring that functions take a specific concrete type.
* First-class modules: another tool for type-level programming and modularity. I won't say much since it's hard to understand why you want and at times need them until you've organically come across a use-case for them. Once you do, you'll wish that other languages had them. Here's a resource, though: [4].
* Let binding operators: these let you define your semantics for binding values to variables. A common use-case is defining let* as the monadic bind operator for some type: let (let*) x f = bind x f, after which writing monadic functions is way more pleasant syntax-wise. In contrast to the other items on this list, this is pure syntactic sugar but incredibly impactful [5].
* Algebraic effects: the conceptual root of concepts such as generators (yield), async/await, and checked assumptions. Informally, they're (among other things) a way to encapsulate computation and jump around code like a goto statement, but in a more structured and type/memory-safe way [6].
* Modular implicits: these allow (among other things) ad-hoc polymorphism, meaning that the same operator, e.g. (+), can operate on both integers and floats. That's the oft-cited use-case, and it sounds pedestrian, seeing as most mainstream languages with weaker type systems have it. There's more to it than that [7]. Haskell and Scala have type classes and implicits as mechanisms for ad-hoc polymorphism, but modular implicits (if implemented) seem to strike a nice balance between readability, flexibility, and transparency.
* GADTs
* Row polymorphism with inference
* First-class modules
* Let binding operators, e.g., let* for monadic binding
On the coming soon to OCaml (hopefully) and way ahead front:
* Algebraic effects
* Modular implicits