[wyager]

Not all type systems allow for subtyping. In particular, Hindley-Milner does not. Nor, as far as I'm aware, do any of the consistently-typed proof languages (like Agda, Coq, etc.)