From 6633e39ea6b916b39381f7625dbb839f7d394a64 Mon Sep 17 00:00:00 2001
From: N5N3 <2642243996@qq.com>
Date: Tue, 31 Jan 2023 16:33:09 +0800
Subject: [PATCH] Some subtype hack.

This makes the result soundness at the cost of more subtype cost. We should try to fix this on `subtype_leftvar` side.

close #45874.
---
 src/subtype.c   | 27 ++++++++++++++++++++++++++-
 test/subtype.jl |  8 +++-----
 2 files changed, 29 insertions(+), 6 deletions(-)

diff --git a/src/subtype.c b/src/subtype.c
index 7f52d5cb518b59..7a999f10205fc7 100644
--- a/src/subtype.c
+++ b/src/subtype.c
@@ -1308,6 +1308,21 @@ static int subtype_tuple(jl_datatype_t *xd, jl_datatype_t *yd, jl_stenv_t *e, in
     return ans;
 }
 
+static int rightvar_in_union(jl_value_t *x, jl_stenv_t *e, jl_tvar_t *y)
+{
+    if (x == y)
+        return 1;
+    if (jl_is_unionall(x))
+        return rightvar_in_union(((jl_unionall_t *)x)->body, e, y);
+    if (jl_is_uniontype(x))
+        return rightvar_in_union(((jl_uniontype_t *)x)->a, e, y) ||
+               rightvar_in_union(((jl_uniontype_t *)x)->b, e, y);
+    if (!jl_is_typevar(x))
+        return 0;
+    jl_varbinding_t *xb = lookup(e, (jl_tvar_t *)x);
+    return xb && xb->right;
+}
+
 // `param` means we are currently looking at a parameter of a type constructor
 // (as opposed to being outside any type constructor, or comparing variable bounds).
 // this is used to record the positions where type variables occur for the
@@ -1321,7 +1336,7 @@ static int subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param)
     if (jl_is_uniontype(y)) {
         if (x == ((jl_uniontype_t*)y)->a || x == ((jl_uniontype_t*)y)->b)
             return 1;
-        if (jl_is_unionall(x))
+        if (jl_is_unionall(x) && (!rightvar_in_union(y, e, NULL) || pick_union_decision(e, 1) == 1))
             return subtype_unionall(y, (jl_unionall_t*)x, e, 0, param);
         int ui = 1;
         if (jl_is_typevar(x)) {
@@ -1369,6 +1384,16 @@ static int subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param)
             // to other left-side variables, so using || here is safe.
             return subtype(xub, y, e, param) || subtype(x, ylb, e, param);
         }
+        jl_varbinding_t *xb = lookup(e, (jl_tvar_t*)x);
+        if ((xb == NULL || !xb->right) &&
+             jl_is_unionall(y) && rightvar_in_union(y, e, (jl_tvar_t*)x) &&
+             pick_union_decision(e, 1) == 0) {
+            // Special case for:
+            //   1) `∀T <: Union{∃S, SomeType{P}} where {P}`: `S == Any` ==> `S >: T`
+            //   2) `∀T <: Union{∀T, SomeType{P}} where {P}`:
+            // TODO: fix this on `subtype_leftvar` side and remove this hack.
+            return subtype_unionall(x, (jl_unionall_t*)y, e, 1, param);
+        }
         return var_lt((jl_tvar_t*)x, y, e, param);
     }
     if (jl_is_typevar(y))
diff --git a/test/subtype.jl b/test/subtype.jl
index a84f4aa5683895..1db7401047a9d5 100644
--- a/test/subtype.jl
+++ b/test/subtype.jl
@@ -2277,8 +2277,7 @@ struct Z38497{T>:Int} <: Y38497{T} end
 #issue #46970
 @test only(intersection_env(Union{S, Matrix{Int}} where S<:Matrix, Matrix)[2]) isa TypeVar
 T46784{B<:Val, M<:AbstractMatrix} = Tuple{<:Union{B, <:Val{<:B}}, M, Union{AbstractMatrix{B}, AbstractMatrix{<:Vector{<:B}}}}
-@testintersect(T46784{T,S} where {T,S}, T46784, !Union{})
-@test_broken T46784 <: T46784{T,S} where {T,S}
+@test T46784 <: T46784{T,S} where {T,S}
 
 #issue 36185
 let S = Tuple{Type{T},Array{Union{T,Missing},N}} where {T,N},
@@ -2361,6 +2360,7 @@ end
                Union{})
 
 @test only(intersection_env(Val{Union{Val{Val{T}} where {T},Int}}, Val{Union{T,Int}} where T)[2]) === Val{Val{T}} where {T}
+@test only(intersection_env(Val{Union{Val{Val{T}} where {T},Ref}}, Val{Union{T,Ref}} where T)[2]) === Val{Val{T}} where {T}
 
 # issue 47654
 Vec47654{T} = Union{AbstractVector{T}, AbstractVector{Union{T,Nothing}}}
@@ -2386,9 +2386,7 @@ end
     # Causes a hang due to jl_critical_error calling back into malloc...
     let S = Pair{Val{P}, AbstractVector{<:Union{P,<:AbstractMatrix{P}}}} where P,
         T = Pair{Val{R}, AbstractVector{<:Union{P,<:AbstractMatrix{P}}}} where {P,R}
-        @test_broken S <: T
-        @test typeintersect(S, T) !== Union{}
-        # @test_broken typeintersect(T, S) <: Any
+        @test S <: T
     end
 
     #issue 40865