Subtype: skip slow-path in local_∀_∃_subtype if inputs contain no ∃…

… typevar. (JuliaLang#53429)

This should be safe as ∀ vars' bounds are frozen in env.
If there's no ∃ var, then the current env won't change after
`local_∀_∃_subtype`.
Thus, the slow path should be equivalent to the fast path if the latter
returns 1.
Close JuliaLang#53371.

src/jltypes.c

@@ -217,7 +217,7 @@ JL_DLLEXPORT jl_array_t *jl_find_free_typevars(jl_value_t *v)
 }
 
 // test whether a type has vars bound by the given environment
-static int jl_has_bound_typevars(jl_value_t *v, jl_typeenv_t *env) JL_NOTSAFEPOINT
+int jl_has_bound_typevars(jl_value_t *v, jl_typeenv_t *env) JL_NOTSAFEPOINT
 {
  while (1) {
  if (jl_is_typevar(v)) {

src/julia_internal.h

@@ -750,6 +750,7 @@ void jl_method_table_activate(jl_methtable_t *mt, jl_typemap_entry_t *newentry);
 jl_typemap_entry_t *jl_method_table_add(jl_methtable_t *mt, jl_method_t *method, jl_tupletype_t *simpletype);
 jl_datatype_t *jl_mk_builtin_func(jl_datatype_t *dt, const char *name, jl_fptr_args_t fptr) JL_GC_DISABLED;
 int jl_obviously_unequal(jl_value_t *a, jl_value_t *b);
+int jl_has_bound_typevars(jl_value_t *v, jl_typeenv_t *env) JL_NOTSAFEPOINT;
 JL_DLLEXPORT jl_array_t *jl_find_free_typevars(jl_value_t *v);
 int jl_has_fixed_layout(jl_datatype_t *t);
 JL_DLLEXPORT int jl_struct_try_layout(jl_datatype_t *dt);

src/subtype.c

@@ -1512,6 +1512,23 @@ static int may_contain_union_decision(jl_value_t *x, jl_stenv_t *e, jl_typeenv_t
  may_contain_union_decision(xb ? xb->ub : ((jl_tvar_t *)x)->ub, e, &newlog);
 }
 
+static int has_exists_typevar(jl_value_t *x, jl_stenv_t *e) JL_NOTSAFEPOINT
+{
+ jl_typeenv_t *env = NULL;
+ jl_varbinding_t *v = e->vars;
+ while (v != NULL) {
+ if (v->right) {
+ jl_typeenv_t *newenv = (jl_typeenv_t*)alloca(sizeof(jl_typeenv_t));
+ newenv->var = v->var;
+ newenv->val = NULL;
+ newenv->prev = env;
+ env = newenv;
+ }
+ v = v->prev;
+ }
+ return env != NULL && jl_has_bound_typevars(x, env);
+}
+
 static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int param, int limit_slow)
 {
  int16_t oldRmore = e->Runions.more;
@@ -1531,13 +1548,19 @@ static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t
  int count = 0, noRmore = 0;
  sub = _forall_exists_subtype(x, y, e, param, &count, &noRmore);
  pop_unionstate(&e->Runions, &oldRunions);
- // we should not try the slow path if `forall_exists_subtype` has tested all cases;
- // Once limit_slow == 1, also skip it if
- // 1) `forall_exists_subtype` return false
+ // We could skip the slow path safely if
+ // 1) `_∀_∃_subtype` has tested all cases
+ // 2) `_∀_∃_subtype` returns 1 && `x` and `y` contain no ∃ typevar
+ // Once `limit_slow == 1`, also skip it if
+ // 1) `_∀_∃_subtype` returns 0
  // 2) the left `Union` looks big
+ // TODO: `limit_slow` ignores complexity from inner `local_∀_exists_subtype`.
  if (limit_slow == -1)
  limit_slow = kindx || kindy;
- if (noRmore || (limit_slow && (count > 3 || !sub)))
+ int skip = noRmore || (limit_slow && (count > 3 || !sub)) ||
+ (sub && (kindx || !has_exists_typevar(x, e)) &&
+ (kindy || !has_exists_typevar(y, e)));
+ if (skip)
  e->Runions.more = oldRmore;
  }
  else {

test/subtype.jl

@@ -2571,3 +2571,12 @@ let a = Tuple{Union{Nothing, Type{Pair{T1}} where T1}}
  b = Tuple{Type{X2} where X2<:(Pair{T2, Y2} where {Src, Z2<:Src, Y2<:Union{Val{Z2}, Z2}})} where T2
  @test !Base.has_free_typevars(typeintersect(a, b))
 end
+
+#issue 53371
+struct T53371{A,B,C,D,E} end
+S53371{A} = Union{Int, <:A}
+R53371{A} = Val{V} where V<:(T53371{B,C,D,E,F} where {B<:Val{A}, C<:S53371{B}, D<:S53371{B}, E<:S53371{B}, F<:S53371{B}})
+let S = Type{T53371{A, B, C, D, E}} where {A, B<:R53371{A}, C<:R53371{A}, D<:R53371{A}, E<:R53371{A}},
+ T = Type{T53371{A, B, C, D, E} where {A, B<:R53371{A}, C<:R53371{A}, D<:R53371{A}, E<:R53371{A}}}
+ @test !(S <: T)
+end