fix some cases of diagonal subtyping

fix #26108, fix #26716, fix #31824

NEWS.md

@@ -8,6 +8,9 @@ New language features
 Language changes
 ----------------
 
+* Converting arbitrary tuples to `NTuple`, e.g. `convert(NTuple, (1, ""))` now gives an error,
+  where it used to be incorrectly allowed. This is because `NTuple` refers only to homogeneous
+  tuples (this meaning has not changed) ([#34272]).
 
 Multi-threading changes
 -----------------------

base/essentials.jl

@@ -333,20 +333,8 @@ convert(T::Type{Tuple{Vararg{V}}}, x::Tuple) where {V} =
 #convert(_::Type{Tuple{Vararg{S, N}}},
 #        x::Tuple{Vararg{Any, N}}) where
 #       {S, N} = cnvt_all(S, x...)
-# TODO: These currently can't be used since
-#   Type{NTuple} <: (Type{Tuple{Vararg{S}}} where S) is true
-#   even though the value S doesn't exist
-#convert(_::Type{Tuple{Vararg{S}}},
-#        x::Tuple{Any, Vararg{Any}}) where
-#       {S} = cnvt_all(S, x...)
-#convert(_::Type{Tuple{Vararg{S}}},
-#        x::Tuple{Vararg{Any}}) where
-#       {S} = cnvt_all(S, x...)
 #cnvt_all(T) = ()
 #cnvt_all(T, x, rest...) = (convert(T, x), cnvt_all(T, rest...)...)
-# TODO: These may be necessary if the above are enabled
-#convert(::Type{Tuple{}}, ::Tuple{}) = ()
-#convert(::Type{Tuple{Vararg{S}}} where S, ::Tuple{}) = ()
 
 """
     oftype(x, y)

doc/src/devdocs/types.md

@@ -403,17 +403,38 @@ f(nothing, 2.0)
 These examples are telling us something: when `x` is `nothing::Nothing`, there are no
 extra constraints on `y`.
 It is as if the method signature had `y::Any`.
-This means that whether a variable is diagonal is not a static property based on
-where it appears in a type.
-Rather, it depends on where a variable appears when the subtyping algorithm *uses* it.
-When `x` has type `Nothing`, we don't need to use the `T` in `Union{Nothing,T}`, so `T`
-does not "occur".
 Indeed, we have the following type equivalence:
 
 ```julia
 (Tuple{Union{Nothing,T},T} where T) == Union{Tuple{Nothing,Any}, Tuple{T,T} where T}
 ```
 
+The general rule is: a concrete variable in covariant position acts like it's
+not concrete if the subtyping algorithm only *uses* it once.
+When `x` has type `Nothing`, we don't need to use the `T` in `Union{Nothing,T}`;
+we only use it in the second slot.
+This arises naturally from the observation that in `Tuple{T} where T` restricting
+`T` to concrete types makes no difference; the type is equal to `Tuple{Any}` either way.
+
+However, appearing in *invariant* position disqualifies a variable from being concrete
+whether that appearance of the variable is used or not.
+Otherwise types become incoherent, behaving differently depending on which other types
+they are compared to. For example, consider
+
+Tuple{Int,Int8,Vector{Integer}} <: Tuple{T,T,Vector{Union{Integer,T}}} where T
+
+If the `T` inside the Union is ignored, then `T` is concrete and the answer is "false"
+since the first two types aren't the same.
+But consider instead
+
+Tuple{Int,Int8,Vector{Any}} <: Tuple{T,T,Vector{Union{Integer,T}}} where T
+
+Now we cannot ignore the `T` in the Union (we must have T == Any), so `T` is not
+concrete and the answer is "true".
+That would make the concreteness of `T` depend on the other type, which is not
+acceptable since a type must have a clear meaning on its own.
+Therefore the appearance of `T` inside `Vector` is considered in both cases.
+
 ## Subtyping diagonal variables
 
 The subtyping algorithm for diagonal variables has two components: