They seem to both agree that union types are about being possibly non-disjoint, and ADT being always disjoint, with values tagged as of a single type. I can acc

They seem to both agree that union types are about being possibly non-disjoint, and ADT being always disjoint, with values tagged as of a single type. I can accept that since it defines union as the same concept as in set theory. There’s nothing there regarding types being ad hoc, though that is arguably a consequence of the syntax since using a symbol between different types to “union” them cannot be expected to result in a disjointed type union. So, I think that’s a useful and defensible position, but I don’t think many people will use these definitions consistently given there’s already a lot of confusion in the use of these terms.