subtype: Tweak the diagonal rule to make it more clear

[Keno]

Pop quiz: Which of these make T diagonal:

Tuple{S, T} where S<:T where T
Tuple{S, T} where S<:Tuple{T} where T
Tuple{S, T} where S<:Tuple{T,T} where T

The answer right now is 2 and 3, but I would argue that 2 is a bit of an accident of implementation, because Tuple turns back on the variable occurrence counting that the typevar consitency check tried to turn off (but we depend on 3 and it clearly "looks" diagonal).

This PR changes the semantics so that 2 is no longer considered diagonal. Instead, the diagonal rule conceptually applies to Tuples: The diagonal rule applies whenever any Tuple sees 2+ active typevars in covariant position (and the typevar was not statically found in invariant position by the outer UnionAll - same as before).

For a more extensive set of examples of cases that change behaviors, see the test suite, but of note none of our existing tests depended on this (other than a test_broken that now passes).

A particular motivation for this change is intersection, since intersection needs to extensively reason about whether or not it is possible for a variable to become diagonal (no intersection changes are made in this PR, because intersection is not currently correct with respect to various diagonal cases - however fixing that requires defining what correctness means).

Idea by me. Tests by GPT-5.5 Pro. Implemented by Claude Opus 4.7.

[topolarity]

I think I would have expected all three of these to be diagonal, from the perspective that:

Tuple{S ∩ T, T} where S where T
Tuple{S ∩ Tuple{T}, T} where S where T
Tuple{S ∩ Tuple{T,T}, T} where S where T

are all "clearly" diagonal (i.e. the bounds "carry" T to the other covariant position)

I'm not totally clear on what the proposed rule for "covariant position" is in bounds. For example:

Tuple{Ref{T},S,S} where S>:T where T      # is S diagonal?

It's a bit strange that bounds would confer invariant status but not covariant status.

[adienes]

my expectation would be that the bounds do indeed make it covariant, since we can observe

julia> X{T} = Tuple{S, T} where S<:T where T;

julia> X{Real} <: X{Number}
true

which would imply T diagonal in all three examples.

[topolarity]

Ah the lower bound is contravariant, so it disables the diagonal rule:

julia> Tuple{Float64,Int,String} <: Tuple{S,S,T} where {T,S>:T}
true

The behavior actually depends on bounds order:

julia> Tuple{Float64,Int,String} <: Tuple{S,S,T} where {S,T<:S}
false

[vtjnash]

Tuple{S, T} where S<:Tuple{T} where T

What is Tuple{Tuple{T}, T} were T? I'd expect those two are type equal (lemma by covariance), which seems to pre-suppose that T is diagonal in both cases or neither case

[Keno]

I think I would have expected all three of these to be diagonal, from the perspective that:

That is a consistent position, but goes against the original design intent, as well as the explicit use in intersection of the S<:T pattern to make a variable non-diagonal. We cannot change the diagonality of either case 1 or 3 - they are heavily relied on in existing code.

I'm not totally clear on what the proposed rule for "covariant position" is in bounds. For example:

The diagonal rule has an additional (oft ignored) constraint that it is disabled unless the (declared) lower bound of the typevar is "obviously concrete" (including Union{}). This change was made in response to a suggestion by the Northeastern folks for substantially this case.

my expectation would be that the bounds do indeed make it covariant, since we can observe

julia> X{T} = Tuple{S, T} where S<:T where T;

julia> X{Real} <: X{Number}
true

type application does not in general preserve the diagonal rule or imply subtyping. In particular fact, type application is allowed with non-concrete elements for diagonal vars:

julia> Y = Tuple{T, T} where T
Tuple{T, T} where T

julia> Y{Any}
Tuple{Any, Any}

julia> Y{Any} <: Y
false

What is Tuple{Tuple{T}, T} were T? I'd expect those two are type equal (lemma by covariance), which seems to pre-suppose that T is diagonal in both cases or neither case

It's diagonal. The covariance transform does not hold with respect to the diagonal rule. As I said above, I think it would be consistent to impose this (which would require diagonality for case 1), but that's not the design choice we've made.

[Keno]

@nanosoldier runtests()

[vtjnash]

What is Tuple{Tuple{T}, T} were T? I'd expect those two are type equal (lemma by covariance), which seems to pre-suppose that T is diagonal in both cases or neither case`

It's diagonal. The covariance transform does not hold with respect to the diagonal rule. As I said above, I think it would be consistent to impose this (which would require diagonality for case 1), but that's not the design choice we've made.

I'm not yet sure what position to take on case 1, just finding that subtyping appears to become incorrect for case 2 on this branch currently:

 _/ |\__'_|_|_|\__'_|  |  kf/diagruletweak/dc778b8d37 (fork: 1 commits, 1 day)

julia> (Tuple{Tuple{T},T} where T) == Tuple{S,T} where S<:Tuple{T} where T
true

julia> (Tuple{T,Tuple{T}} where T) == Tuple{T,S} where S<:Tuple{T} where T
true

vs case 1 that is correct (or at least internally consistent)

julia> (Tuple{S,T} where S<:T where T) <: Tuple{T,T} where T
false

julia> (Tuple{S,T} where S<:T where T) >: Tuple{T,T} where T
true

[Keno]

I'm not yet sure what position to take on case 1, just finding that subtyping appears to become incorrect for case 2 on this branch currently:

Yes, that's a bug. Will fix.

[nanosoldier]

The package evaluation job you requested has completed - possible new issues were detected.
The full report is available.

Report summary

❗ Packages that crashed

249 packages crashed on the previous version too.

✖ Packages that failed

19 packages failed only on the current version.

• Package has test failures: 1 packages
• Package tests unexpectedly errored: 1 packages
• Test duration exceeded the time limit: 16 packages
• Test log exceeded the size limit: 1 packages

1057 packages failed on the previous version too.

✔ Packages that passed tests

11 packages passed tests only on the current version.

• Other: 11 packages

5905 packages passed tests on the previous version too.

~ Packages that at least loaded

1 packages successfully loaded only on the current version.

• Other: 1 packages

3689 packages successfully loaded on the previous version too.

➖ Packages that were skipped altogether

897 packages were skipped on the previous version too.

[Keno]

Looks like noise, but let's rerun to be sure:

@nanosoldier runtests(["SimpleLooper", "ConvolutionInterpolations", "Gabs", "ASCertain", "Oxygen", "DMRGenie", "DynamicalSystemsBase", "ApproxManifoldProducts", "OnlinePCA", "BloodFlowTrixi", "ControlSystemsMTK", "MultiAgentPathFinding", "QuantumAnnealingAnalytics", "SurfaceWaterIntegratedModeling", "CO2BatchFill", "PlantModules", "UnfoldMakie", "FundamentalsNumericalComputation"])

[nanosoldier]

The package evaluation job you requested has completed - possible new issues were detected.
The full report is available.

Report summary

✖ Packages that failed

1 packages failed only on the current version.

• Test duration exceeded the time limit: 1 packages

6 packages failed on the previous version too.

✔ Packages that passed tests

1 packages passed tests only on the current version.

• Other: 1 packages

8 packages passed tests on the previous version too.

~ Packages that at least loaded

2 packages successfully loaded on the previous version too.

[Keno]

Caught up with @JeffBezanson offline - his opinion was that case 2 being diagonal is a bug and was not intended.