Oh if you use those features to express what "sum type as subtyping" can, it sure gets confusing. But it's not those things that I want to express that are hard to reason about, the confusing part is the additions to the HM type system.

A meta point: it seems to me that a lot of commenters in my thread don't know that vanilla HM cannot express subtypes. This allows the type system to "run backwards" and you have full type inference without any type annotations. One can call it a good tradeoff but it IS a tradeoff.

Yes and my point was, when you want what you present in the first comment, quoting my post, you have tools for that, available in OCaml. But there is cases, when you do not want to treat each branch of your constructors "as a type", when the encoding of visitors is just rough. This is why I think it is nice to have sum type, to complete product type. So i am not sure why we are arguing :)