Type intersection sometimes takes several seconds

[topolarity]

Seems to happen when intersecting extremely large tuples.

50+s example from BlochSim.jl:

julia> using BlochSim, ForwardDiff
julia> T = Tuple{Type{MESEBlochSimWorkspace}, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T11, T12, T11, T12, T13, T12, T13, T12, T13, T12, T13, T12, T14, T15, T16, T17, T18, T19, T20, T21} where {T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19, T20, T21}
julia> U = Tuple{Type{MESEBlochSimWorkspace}, ExcitationMatrix, Nothing, ExcitationMatrix, Nothing, Nothing, Nothing, Nothing, Nothing, BlochSim.IdealSpoilingMatrix, Nothing, Any, Any, Any, Any, Any, Any, Any, Any, Any, Any, Any, Any, Any, Any, Matrix, Any, BlochMcConnellWorkspace{T} where T<:(Union{Float64, var"#s41"} where var"#s41"<:(ForwardDiff.Dual)), Vararg{Nothing, 5}};
julia> @time @ccall jl_intersect_types(T::Any, U::Any)::Any;
 52.193790 seconds (77.70 M allocations: 36.309 GiB, 6.26% gc time)

20+s example from StochasticDiffEq.jl:

julia> using StochasticDiffEq, OrdinaryDiffEq, DataStructures
julia> T = Tuple{Type{StochasticDiffEq.SDEOptions{tTypeNoUnits, tType, Controller, F2, F3, F4, F5, F6, F7, tstopsType, discType, ECType, SType, MI, A, R, D, tcache, savecache, disccache} where disccache where savecache where tcache where D where R where A where MI where SType where ECType where discType where tstopsType where F7 where F6 where F5 where F4 where F3 where F2 where Controller where tType where tTypeNoUnits}, Int64, Bool, Bool, Any, Any, Any, Any, Any, Any, Any, Any, Any, Any, Any, OrdinaryDiffEq.PIController{_A} where _A, typeof(DiffEqBase.ODE_DEFAULT_NORM), Nothing, DataStructures.BinaryHeap{_A, DataStructures.FasterForward} where _A, DataStructures.BinaryHeap{_A, DataStructures.FasterForward} where _A, DataStructures.BinaryHeap{_A, DataStructures.FasterForward} where _A, Tuple{}, Tuple{}, Tuple{}, Nothing, Bool, Int64, String, typeof(DiffEqBase.ODE_DEFAULT_PROG_MESSAGE), Bool, Bool, Any, Bool, Bool, Bool, Bool, Nothing, Bool, SciMLBase.CallbackSet{Tuple{}, Tuple{}}, typeof(DiffEqBase.ODE_DEFAULT_ISOUTOFDOMAIN), typeof(DiffEqBase.ODE_DEFAULT_UNSTABLE_CHECK), Vararg{Bool, 5}};
julia> U = Tuple{Type{StochasticDiffEq.SDEOptions{tTypeNoUnits, tType, Controller, F2, F3, F4, F5, F6, F7, tstopsType, discType, ECType, SType, MI, A, R, D, tcache, savecache, disccache} where disccache where savecache where tcache where D where R where A where MI where SType where ECType where discType where tstopsType where F7 where F6 where F5 where F4 where F3 where F2 where Controller where tType where tTypeNoUnits}, MI, Bool, Bool, A, R, tTypeNoUnits, tTypeNoUnits, tTypeNoUnits, tTypeNoUnits, tTypeNoUnits, tTypeNoUnits, tTypeNoUnits, tType, tType, Controller, F2, SType, tstopsType, tstopsType, discType, tcache, savecache, disccache, ECType, Bool, Int64, String, F6, Bool, Bool, D, Bool, Bool, Bool, Bool, F3, Bool, F4, F5, F7, Vararg{Bool, 5}} where disccache where savecache where tcache where D where R where A where MI where SType where ECType where discType where tstopsType where F7 where F6 where F5 where F4 where F3 where F2 where Controller where tType where tTypeNoUnits;
julia> @time @ccall jl_intersect_types(T::Any, U::Any)::Any;
 23.539494 seconds (34.66 M allocations: 14.881 GiB, 6.51% gc time)

Version:

julia> versioninfo()
Julia Version 1.9.0-beta4
Commit b75ddb787ff (2023-02-07 21:53 UTC)
Platform Info:
  OS: Linux (x86_64-linux-gnu)
  CPU: 64 × AMD EPYC 7513 32-Core Processor
  WORD_SIZE: 64
  LIBM: libopenlibm
  LLVM: libLLVM-14.0.6 (ORCJIT, znver3)
  Threads: 1 on 64 virtual cores
Environment:
  JULIA_PKG_SERVER = https://internal.juliahub.com
  JULIA_PKG_USE_CLI_GIT = true

I expect that we're going down a combinatorial path among all the tuple components, despite the fact that they don't actually share any typevars.

Fix is in the works 🙂

[topolarity]

Turns out it's not the tuple combinatorics in this case:

This comes from the double-intersection we evaluate in intersect_unionall:

julia/src/subtype.c

Lines 2913 to 2932 in a23b29c

	res = intersect_unionall_(t, u, e, R, param, &vb);
	if (vb.limited) {
	// if the environment got too big, avoid tree recursion and propagate the flag
	if (e->vars)
	e->vars->limited = 1;
	}
	else if (res != jl_bottom_type) {
	if (vb.concrete || vb.occurs_inv>1 || vb.intvalued > 1 || u->var->lb != jl_bottom_type || (vb.occurs_inv && vb.occurs_cov)) {
	restore_env(e, NULL, &se);
	vb.occurs = vb.occurs_cov = vb.occurs_inv = 0;
	vb.constraintkind = vb.concrete ? 1 : 2;
	res = intersect_unionall_(t, u, e, R, param, &vb);
	}
	else if (vb.occurs_cov && !var_occurs_invariant(u->body, u->var, 0)) {
	restore_env(e, save, &se);
	vb.occurs = vb.occurs_cov = vb.occurs_inv = 0;
	vb.constraintkind = 1;
	res = intersect_unionall_(t, u, e, R, param, &vb);
	}
	}

This becomes O(2^N) for nested UnionAll types.

[topolarity]

My first stab at this was to statically adjust our types to reduce type-var nesting, while preserving type-equality.

Unfortunately, our current intersection algorithm will widen when you do this:

julia> T1 = Tuple{Pair{B, C}, C} where {B, C}
julia> T2 = Tuple{Pair{B, C} where B, C} where C
julia> U = Tuple{Pair{B, C}, Union{Real, B}} where {B, C}

julia> (@ccall jl_intersect_types(T1::Any, U::Any)::Any) == Tuple{Pair{B, C}, C} where {B, C<:Union{Real, B}}
true
julia> (@ccall jl_intersect_types(T2::Any, U::Any)::Any) == Tuple{Pair{B, C}, C} where {B, C}
true

Subtyping even becomes incorrect under this transformation (which should preserve type-equality):

julia> T = Tuple{Pair{A, B}, Union{A, Ref{T}}} where {A, B, T}
julia> S1 = Tuple{Pair{A, B}, Union{A, Ref{T}} where T} where {A, B}
julia> S2 = Tuple{Pair{A, B}, Union{A, Ref{T} where T}} where {A, B}

julia> T == S1
false
julia> T == S2
true

[N5N3]

The widening is expected.
IIRC we had some attempt to pull these covariant UnionAlls out and make result more accurate.
Edit: see #23700 and the added broken test there.

[topolarity]

Thanks for the info! That's helpful historical information.

It's a shame that in this case it ends up opting into an exponential algorithm even when it's often not necessary, but I suppose the whole problem here is that the intersection algorithm is not good at dynamically expanding/shrinking UnionAll dependencies (based on the chains of type-vars considered)

I'm going to take a stab at solving this dynamically (by narrowing dependencies during intersection computation), rather than statically (with a type transformation)