Bidirectional type checking versus Hindley-Milner type checking, with some worked examples of subtyping: https://www.haskellforall.com/2022/06/the-appeal-of-bidirectional-type.html