This is precisely what I was describing, perhaps I wasn't clear enough. I should have mentioned Typed Racket as well. Unless you think this is different from what I said? Typed Racket's unions are just like TypeScript and Flow's unions, in fact TypeScript uses a similar occurrence typing algorithm where you need to do a type check in order to compute with a union value, e.g.

    if (isString(x)) {
      // only now can we call string functions on x
    } else if (isNumber(x)) {
      // only now can we call number functions on x
    }

OK, then we're on the same page regarding Elm's name choice: That is, it's a poor choice if they are actually disjoint unions aka sum types.

That said, forgive me pedantry for a moment: I think your use of the word "tag" is unclear. Typically, both sum types and union types must be tagged. If you think about something like the JVM, every object is tagged with a pointer to it's class. Untagged, or "tagless", objects are closely related to "unboxed" objects, but still not quite the same thing. The point is that the tag is something that can be inspected, switched on, etc at runtime. Where as a tagless representation does not require that runtime overhead.

It's possible to have a Union(int, String) or something like that where one type is typically untagged and the other typically tagged. If the compiler could eliminate the tag at runtime from context, then it would just eliminate the union and substitute the type with either int or String directly. So if it can't tell from context, it must actually make it a Union(Box<int>, String) so it can discriminate by tag.

Tangential: There is of course a trade off in tagless representations in terms of type system complexity and runtime cost. If you want to change from a List<int> (specialized list of machine ints) to a List<Integer> (nullable boxed ints), that's an O(N) operation to add the tags (and a more complex type system).

The thing is, "sum types" really only works if you're familiar with the analogy between boolean algebra and arithmetic (why OR becomes +).

Yes, they are disjoint union, but there's really no such thing as non-disjoint union in a statically typed language i.e. that's what makes it typesafe.

You can have "non-disjoint unions" in typesafe languages, you just will be no longer capable of distinguishing between the types of the members.