Incorrect subtyping result for `Ref{Vector{Tuple{K}} where K} <: Ref{<:Vector{K}} where K`

[topolarity]

I might be reasoning about this incorrectly, but Julia declares:

julia> Ref{Vector{Tuple{K}} where K} <: Ref{<:Vector{K}} where K
true

I think this is incorrect because it requires proving that ∃K'. (Vector{Tuple{K}} where K) <: Vector{K'} which is false.

For comparison:

julia> Ref{Vector{K} where K} <: Ref{<:Vector{K}} where K
false

[N5N3]

Another comparison:

julia> Ref{Vector{Tuple{K}} where K} <: Ref{<:Vector{K}} where K
true

julia> Ref{Vector{Val{K}} where K} <: Ref{<:Vector{K}} where K
false

Fixing should be simple, just replace var_occurs_invariant(t, v) with var_occurs_inside(t, v, 0, 0)

julia/src/subtype.c

Lines 937 to 950 in 9f9e989

	jl_varbinding_t *btemp = e->vars;
	if (vb.lb != vb.ub) {
	while (btemp != NULL) {
	jl_value_t *vu = btemp->ub;
	jl_value_t *vl = btemp->lb;
	// TODO: this takes a significant amount of time
	if (btemp->depth0 != vb.depth0 &&
	((vu != (jl_value_t*)vb.var && btemp->var->ub != vu && var_occurs_invariant(vu, vb.var)) ||
	(vl != (jl_value_t*)vb.var && btemp->var->lb != vl && var_occurs_invariant(vl, vb.var)))) {
	ans = 0; break;
	}
	btemp = btemp->prev;
	}
	}

Perhaps a typo in #24104?

[vtjnash]

Seems to have been intentional, but simply was wrong. Perhaps at the time it was avoiding some other bug. Did you want to make a PR and we can try PkgEval on it?

[topolarity]

Thanks @N5N3 !