fix some cases of diagonal subtyping when a var also appears invariantly

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,9 +333,7 @@ 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
+# TODO: These are similar to the methods we currently use but cnvt_all might work better:
 #convert(_::Type{Tuple{Vararg{S}}},
 #        x::Tuple{Any, Vararg{Any}}) where
 #       {S} = cnvt_all(S, x...)

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 can behave differently depending on which other types
+they are compared to, making subtyping not transitive. 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: