If I understand correctly, right now the rule for Tuple{T,T} where T>:t is: T is considered diagonal unless it is obvious that t is abstract. Therefore, in the examples below the types on the right are not diagonal:

julia> (Tuple{A,A} where A>:Integer) <: Tuple{T,T} where T>:Number
true

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

In the following modification of the previous example, however, T is considered diagonal despite the fact that its lower bound S can be abstract.

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

I totally see that it is a hard task to determine concreteness of types involving variables. What I would suggest is to change the strategy for Tuple{T,T} where T>:t and consider T non-diagonal unless it is obvious that t is concrete. I think that if programmers write lower bounds, it is likely that they really want to switch off the diagonal rule.