counterexample for subtyping transitivity involving types of types

[nsajko]

julia> a = Type{Tuple{UnitRange{Int64}, Symbol, X} where {X}}
Type{Tuple{UnitRange{Int64}, Symbol, X} where X}

julia> b = Type{Tuple{UnitRange{Int64}, Symbol, Any}}
Type{Tuple{UnitRange{Int64}, Symbol, Any}}

julia> c = DataType
DataType

julia> a <: b
true

julia> a <: c
false

julia> b <: a
true

julia> b <: c
true

julia> c <: a
false

julia> c <: b
false

So we have (a <: b) && (b <: c), but !(a <: c).

See also comments by @topolarity here: #57631 (comment)

[topolarity]

To be explicit, this is the cause of unsoundness in inference:

foo(x::Type{Tuple{Integer}}, y::DataType) = (@noinline rand(Bool)) ? x : y
function bar()
    A = Core.compilerbarrier(:type, Tuple{X} where X<:Integer)
    B = Core.compilerbarrier(:type, Int)
    T = @noinline foo(A, B)
    @show T
    @show T isa DataType
    return T
end

julia> @show bar() isa DataType;
T = Tuple{X} where X<:Integer
T isa DataType = true
bar() isa DataType = false

Sometimes transitivity issues are benign, but not in this case.