Worthwhile debate on HN over what type checkers can/should verify, and the limits of Hindley-Milner designs: https://news.ycombinator.com/item?id=10271612
miniblog.
Related Posts
Bidirectional type checking versus Hindley-Milner type checking, with some worked examples of subtyping:
So, Rust has a Hindley-Milner type system (Ocaml), hygenic macros (Scheme) and a condition system (Common Lisp). Astoundingly powerful!