normalize unions made in subtyping

[vtjnash]

We observed a case where simple_tmeet made a Union of egal things, which is undesirable. There also was no sorting of the result, as it normally done, and theoretically, simplification with an omit_bad_union to remove S could similar result in a Union that should be further simplified to remove redundancies.

Union{Union{Val{T}, S} where T<:AbstractString, Union{Val{T}, Int64} where T<:AbstractString} where S

(In principle, that simplification might also be possible to do during the original jl_type_union call when flattening it.)

This prevents the bad inference path that occurs in #48228 from happening, without fixing the type system issue there (which can be reproduced on master by starting inference at one of the later stack frames where the complex unions are already present)

[gbaraldi]

What does that union simplify to then?

[vtjnash]

Without simplification, there may be 2 copies of Val{T} where T<:AbstractString in the result

[gbaraldi]

Oh, so the normalization here moves the where out because it's the same for both parts of the union, got it.

[vtjnash]

The normalization here replaces S with Union{}, but that other simplification I am working on now.

[N5N3]

Perhaps we should follow the rule below (see subtype path in simple_join)?
Although this path has been turned off

// issue #24521: don't merge Type{T} where typeof(T) varies
        !(jl_is_type_type(a) && jl_is_type_type(b) && jl_typeof(jl_tparam0(a)) != jl_typeof(jl_tparam0(b)))) {

[vtjnash]

Good observation. I moved that here. I wanted to be careful not to make too big of a change at once, in case something in a package was depending on it significantly doing one thing. Maybe we should try to move more of that simple_tmeet function into simple_union, but I think a couple things are heuristic based there, so maybe not all of it should be combined.

[N5N3]

but I think a couple things are heuristic based there, so maybe not all of it should be combined.

I think a basic rule is keeping the pointer identity if possible?
#49277 seems to be a good template and if we do that, I think we can move all type-specific branch into simple_union and let simple_join handle non-type bits along.

BTW, I didn't measure the performance influence.
But if we decided to turn this path on, then a good optimization to have is skipping all check if temp[i] and temp[j] come from the same part.

[vtjnash]

I was thinking of this check mostly, since I don't know if this is accurate for a Union in general:

    if (jl_is_typevar(a) && obviously_egal(b, ((jl_tvar_t*)a)->lb))
         return a;

That may be a good thing to check for during jl_type_union too to save repeated work in the case of repeatedly appending one element (e.g. Union{Union{Union{A, B}, C}, Union{D, E}}, since we only need to check the new elements against the old ones). A starting point for that might be to alloca a second buffer that holds the index of which where union starts from to fill the buffer. I think the trickiest ones to detect are cases like this, since "obviously" it can return the first object, but since we only do a subtype check (not equality), we may conclude the result should be that of prepending A to the second Union, and fail to realize that will give back the first Union:

Union{ Union{A,B,C}, Union{B,C} }

That suggests perhaps we should also do the same exhaustive sort of check afterwards too, as templated in #49277, to see if all the elements remaining are equivalent to an existing one. Once we merge this and #49277, I can try prototyping that additional check.

[N5N3]

I was thinking of this check mostly, since I don't know if this is accurate for a Union in general:

I think it's accurate for Union, at least for those without free vars?
But since Union doesn't normalize it for now, I think we can leave these 2 branches in simple_join.

[N5N3]

That suggests perhaps we should also do the same exhaustive sort of check afterwards too, as templated in #49277

Hoist some egal check here seems good?
Then we just need to count how many remaining temp comes from a or b.