Vector eltype depends on code executed before - only 1.9rc

[aplavin]

# run in a fresh session
@show typeof([1, missing, 2])

prints typeof([1, missing, 2]) = Vector{Union{Missing, Int64}} as expected.
But add a totally irrelevant line, and eltype changes:

# run in a fresh session
[1, missing, nothing, 2]
@show typeof([1, missing, 2])

prints typeof([1, missing, 2]) = Vector{Any}.

Only happens on 1.9rc, not 1.8 nor 1.9 betas.

[christiangnrd]

25bad181eb184bce7d3a32a18699fe9f9f9a9325 is the first bad commit
commit 25bad181eb184bce7d3a32a18699fe9f9f9a9325
Author: Jeff Bezanson <jeff.bezanson@gmail.com>
Date:   Tue Jan 24 09:05:18 2023 -0500

    fix #47658, state stack overflow on unions containing typevars (#48221)
    
    (cherry picked from commit 596ce6542624e9b8c3782b19936e2226f307e118)

 src/subtype.c   | 34 ++++++++++++++++++++++++++++++++++
 test/subtype.jl | 24 +++++++++++++++++++++++-
 2 files changed, 57 insertions(+), 1 deletion(-)

[giordano]

CC @JeffBezanson

[N5N3]

Looks like a dispatch failure

julia> @which promote_rule(Union{Missing, Int}, Int)
promote_rule(T::Type{>:Missing}, S::Type)
     @ Base missing.jl:59

julia> [1, missing, nothing, 2]
4-element Vector{Union{Missing, Nothing, Int64}}:
 1
  missing
  nothing
 2

julia> @which promote_rule(Union{Missing, Int}, Int)
promote_rule(T::Type{>:Union{Missing, Nothing}}, S::Type)
     @ Base missing.jl:49

But the subtyping is correct

julia> S = ans.sig
Tuple{typeof(promote_rule), Type{>:Union{Missing, Nothing}}, Type}
julia> T = Tuple{typeof(promote_rule), Type{Union{Missing, Int}}, Type{Int}}
Tuple{typeof(promote_rule), Type{Union{Missing, Int64}}, Type{Int64}}

julia> T <: S
false

[maleadt]

Also reproduces on 596ce65, but not on latest master. Bisected the fix:

96acd4d4e90647caab17af0f689723f5a2594cfd is the first good commit
commit 96acd4d4e90647caab17af0f689723f5a2594cfd
Author: N5N3 <2642243996@qq.com>
Date:   Thu Feb 2 11:41:26 2023 +0800

    Subtype: avoid false alarm caused by eager `forall_exists_subtype`. (#48441)

    * Avoid earsing `Runion` within nested `forall_exists_subtype`

    If `Runion.more != 0` we‘d better not erase the local `Runion` as we need it if the subtyping fails after.

    This commit replaces `forall_exists_subtype` with a local version.
    It first tries `forall_exists_subtype` and estimates the "problem scale".
    If subtyping fails and the scale looks small then it switches to the slow path.

    TODO: At present, the "problem scale" only counts the number of checked `Lunion`s.
    But perhaps we need a more accurate result (e.g. sum of `Runion.depth`)

    * Change the reversed subtyping into a local check.

    Make sure we don't forget the bound in `env`.
    (And we can fuse `local_forall_exists_subtype`)

    * Optimization for non-union invariant parameter.

 src/subtype.c   | 119 ++++++++++++++++++++++++++++++++++++++------------------
 test/subtype.jl |  13 +++++--
 2 files changed, 91 insertions(+), 41 deletions(-)
bisect run success

[KristofferC]

Should add a test for this (and backport it).

[N5N3]

Ok, get the subtyping bug.

S = Type{Union{Missing, Int}}
T = Type{Union{Missing, Nothing, Int}}
S<:T # 1.9rc: true; 1.8.5/master: false; 

I guess the localized reversed subtyping in forall_exists_equal fix the problem. But I haven't verified that.

[KristofferC]

@N5N3, can you help with the backport here? From what I understand, #48441 and #48603 have to be backported but when I try to do so I get down a rabbit hole of conflicts with earlier changes by you to subtyping.

[N5N3]

I’ll take a look tomorrow.

[vtjnash]

We should perhaps revert Jeff's commit instead so we can get the release out without adding more uncertainty

[KristofferC]

Yeah, maybe that is a better idea.

[KristofferC]

I pushed the revert.

[N5N3]

OK, the example above was caused by a mess on Lunion.
Before #48441, we let the root forall loop handle the >: check in forall_exists_equal.
Even if eq_union failed for the 1st Lunion, it might pass in the 2nd round as the global Lunion has been changed and thus some checks might be skipped.
(The fastpath should not use the same Lunion as the norm path.)

#48441 fixes such risk as forall_exists_equal no more changes global Lunion.
I think we can add the MWE to test and close this issue.

[JeffBezanson]

I would rather backport the new fix #48441 as well; some people (Catlab) are depending on this being fixed and they will be sad.

[KristofferC]

Well, then I need help with the backport(s).