subtype triangular rule mistake with UnionAll in Union

[vtjnash]

julia> f(::Type{Union{T,Nothing}}, ::T) where {T} = T

julia> f(Nothing, nothing) # good
Nothing

julia> f(Union{Nothing, Integer}, nothing) # okay
Union{Nothing, Integer}

julia> f(Union{Nothing, Int}, nothing) # okay
Union{Nothing, Int64}

julia> f(Union{Nothing, Vector}, nothing) # bad
ERROR: MethodError: no method matching f(::Core.TypeEgal{Union{Nothing, Vector}}, ::Nothing)
The function `f` exists, but no method is defined for this combination of argument types.

Closest candidates are:
  f(::Type{Union{Nothing, T}}, ::T) where T
   @ Main REPL[1]:1

Stacktrace:
 [1] top-level scope
   @ REPL[4]:1

The witness check is the clincher: with T explicitly bound to Union{Nothing,Vector}, x <: Tuple{Type{Union{T,Nothing}}, T} is true — so a valid witness exists, but forall_exists_subtype fails to find it in the where T form. That's a clean incompleteness in <:, and it's pre-existing (all versions).

Verdict: you found a real bug:
The bug x <: Y and typeintersect(x, Y) disagree, which they never should (x ∩ Y = x ⟹ x ⊆ Y ⟹ x <: Y):
x = Tuple{Type{Union{Nothing,Vector}}, Nothing}
Y = Tuple{Type{Union{T,Nothing}}, T} where T
x <: Y == false # WRONG
typeintersect(x,Y) == x == true # x ⊆ Y
x <: Y[T := Union{Nothing,Vector}] == true # witness exists Tight characterization — the failure needs both:

1. the covariant ::T slot forces the absorbed solution (T must contain Nothing, so the exposed T=Vector is rejected by T >: Nothing); and 2. the other union member is a UnionAll (Vector). Make it concrete (Vector{Int}) and it works; use only the exposed solution (2nd slot Vector{Int}) and it works; use an abstract DataType (Integer, Real) and it works.

[Keno]

x = Tuple{Type{Union{Nothing,Vector}}, Nothing}
Y = Tuple{Type{Union{T,Nothing}}, T} where T
x <: Y == false # WRONG

You're saying this should instantiate to T == Union{Nothing, Vector}? If so, this is a bit of an instance of a general problem that our current algorithm is unable to form these types because of where the union selection bits sit. I have a branch to fix it somewhere, but the algorithm is super-exponential. Possibly this particular case could be fixed with a cheaper hack.

[Keno]

See if this commit catches it: 41b1779

[vtjnash]

That does not appear to rescue this case (I'm also not claiming we need to fix this, just continuing to collect examples of failures)