// This file is a part of Julia. License is MIT: https://julialang.org/license

/*
  subtyping predicate

  Uses the algorithm described in section 4.2.2 of https://github.com/JeffBezanson/phdthesis/
  This code adds the following features to the core algorithm:

  - Type variables can be restricted to range over only concrete types.
    This is done by returning false if such a variable's lower bound is not concrete.
  - Diagonal rule: a type variable is concrete if it occurs more than once in
    covariant position, and never in invariant position. This sounds like a syntactic
    property, but actually isn't since it depends on which occurrences of a type
    variable the algorithm actually uses.
  - Unconstrained type vars (Bottom<:T<:Any) can match non-type values.
  - Vararg types have an int-valued length parameter N (in `Vararg{T,N}`).
  - Type{T}<:S if isa(T,S). Existing code assumes this, but it's not strictly
    correct since a type can equal `T` without having the same representation.
  - Free type variables are tolerated. This can hopefully be removed after a
    deprecation period.
*/
#include <stdlib.h>
#include <string.h>
#ifdef _OS_WINDOWS_
#include <malloc.h>
#endif
#include "julia.h"
#include "julia_internal.h"
#include "julia_assert.h"

#ifdef __cplusplus
extern "C" {
#endif

// stack of bits to keep track of which combination of Union components we are
// looking at (0 for Union.a, 1 for Union.b). forall_exists_subtype and
// exists_subtype loop over all combinations by updating a binary count in
// this structure.
// Union type decision points are discovered while the algorithm works.
// If a new Union decision is encountered, the `more` flag is set to tell
// the forall/exists loop to grow the stack.

typedef struct jl_bits_stack_t {
    uint32_t data[16];
    struct jl_bits_stack_t *next;
} jl_bits_stack_t;

typedef struct {
    int16_t depth;
    int16_t more;
    int16_t used;
    jl_bits_stack_t stack;
} jl_unionstate_t;

typedef struct {
    int16_t depth;
    int16_t more;
    int16_t used;
    uint8_t *stack;
} jl_saved_unionstate_t;

// Linked list storing the type variable environment. A new jl_varbinding_t
// is pushed for each UnionAll type we encounter. `lb` and `ub` are updated
// during the computation.
// Most of the complexity is due to the "diagonal rule", requiring us to
// identify which type vars range over only concrete types.
typedef struct jl_varbinding_t {
    jl_tvar_t *var; // store NULL to "delete" this from env (temporarily)
    jl_value_t *JL_NONNULL lb;
    jl_value_t *JL_NONNULL ub;
    int8_t existential; // whether this variable should be treated as existential
    int8_t occurs_inv;  // occurs in invariant position
    int8_t occurs_cov;  // # of occurrences in covariant position within the
                        // current consistency-check scope (reset on entry to
                        // `subtype_ccheck` / `intersect_aside`, restored on
                        // exit). Saturates at 2. Covariant occurrences inside
                        // nested Tuple{} accumulate into this counter as long
                        // as no consistency check is entered.
    int8_t cov_diag;    // max value `occurs_cov` reached in any (already-closed)
                        // consistency-check scope. The diagonal-rule test is
                        // `max(occurs_cov, cov_diag) > 1`, so a variable is
                        // diagonal iff it occurred >= 2 times in some single
                        // scope (the outer scope or any consistency check),
                        // rather than summed across consistency checks.
    int8_t concrete;    // 1 if another variable has a constraint forcing this one to be concrete
    int8_t max_offset;  // record the maximum positive offset of the variable (up to 32)
                        // max_offset < 0 if this variable occurs outside VarargNum.
    // constraintkind: in covariant position, we try three different ways to compute var ∩ type:
    // let ub = var.ub ∩ type
    // 0 - var.ub <: type ? var : ub
    // 1 - var.ub = ub; return var
    // 2 - var.lb = lb; return ub
    int8_t constraintkind;
    int8_t intvalued; // intvalued: must be integer-valued; i.e. occurs as N in Vararg{_,N}
    int8_t limited;
    int8_t intersected; // whether this variable has been intersected
    int8_t widened_to_kind;   // Type{X} was widened to a union of kinds
    int8_t tainted_inner; // 1 if this var's bounds reference a TypeVar from a vb that
                          // was pushed at depth0 *strictly greater* than this var's
                          // depth0 and has since been popped. Such "inner" tvars
                          // would not be substituted by going to a more concrete LHS
                          // (they live inside Type{...}/etc value positions), so the
                          // binding is leaky regardless of what `constrained` says.
    int8_t body_occurs_inv; // cached `var_occurs_invariant(u->body, u->var)` — the
                            // static "occurs invariantly" check used by the diagonal
                            // rule (since #34272). Unlike the dynamic `occurs_inv`
                            // counter, this is a pure structural property of the
                            // UnionAll body and does not change during traversal.
    int16_t depth0;         // # of invariant constructors nested around the UnionAll type for this var
    // array of typevars that our bounds depend on, whose UnionAlls need to be
    // moved outside ours.
    jl_array_t *innervars;
    struct jl_varbinding_t *prev;
} jl_varbinding_t;

typedef struct jl_ivarbinding_t {
    jl_tvar_t **var;
    jl_value_t **lb;
    jl_value_t **ub;
    jl_varbinding_t *root;
    struct jl_ivarbinding_t *next;
} jl_ivarbinding_t;

// subtype algorithm state
typedef struct jl_stenv_t {
    // N.B.: varbindings are created on the stack and rooted there
    jl_varbinding_t *vars;    // type variable environment
    jl_unionstate_t Lunions;  // union state for unions on the left of A <: B
    jl_unionstate_t Runions;  // union state for unions on the right
    // N.B.: envout is gc-rooted
    jl_value_t **envout;      // for passing caller the computed bounds of right-side variables
    int envsz;                // length of envout
    int envidx;               // current index in envout
    int invdepth;             // current number of invariant constructors we're nested in
    int intersection;         // true iff subtype is being called from intersection
    int emptiness_only;       // true iff intersection only needs to test for emptiness
    int triangular;           // when intersecting Ref{X} with Ref{<:Y}
    // Used to represent the length difference between 2 vararg.
    // intersect(X, Y) ==> X = Y + Loffset
    int Loffset;
} jl_stenv_t;

// state manipulation utilities

// look up a type variable in an environment
static int binding_has_innervar(jl_varbinding_t *b, jl_tvar_t *v) JL_NOTSAFEPOINT
{
    if (b->innervars == NULL)
        return 0;
    for (size_t i = 0; i < jl_array_len(b->innervars); i++) {
        if ((jl_tvar_t*)jl_array_ptr_ref(b->innervars, i) == v)
            return 1;
    }
    return 0;
}

static void push_innervar(jl_varbinding_t *b, jl_value_t *v)
{
    assert(jl_is_typevar(v));
    if (binding_has_innervar(b, (jl_tvar_t*)v))
        return;
    if (b->innervars == NULL)
        b->innervars = jl_alloc_array_1d(jl_array_any_type, 0);
    jl_array_ptr_1d_push(b->innervars, v);
}

#ifdef __clang_gcanalyzer__
static jl_varbinding_t *lookup_binding(jl_stenv_t *e, jl_tvar_t *v, int *innervar) JL_GLOBALLY_ROOTED JL_NOTSAFEPOINT;
#else
static jl_varbinding_t *lookup_binding(jl_stenv_t *e, jl_tvar_t *v, int *innervar) JL_GLOBALLY_ROOTED JL_NOTSAFEPOINT
{
    jl_varbinding_t *b = e->vars;
    while (b != NULL) {
        if (b->var == v) {
            if (innervar)
                *innervar = 0;
            return b;
        }
        b = b->prev;
    }
    if (innervar) {
        b = e->vars;
        while (b != NULL) {
            if (binding_has_innervar(b, v)) {
                *innervar = 1;
                return NULL;
            }
            b = b->prev;
        }
        *innervar = 0;
    }
    return NULL;
}
#endif

static jl_varbinding_t *lookup(jl_stenv_t *e, jl_tvar_t *v) JL_GLOBALLY_ROOTED JL_NOTSAFEPOINT
{
    return lookup_binding(e, v, NULL);
}

// union-stack tools

static int statestack_get(jl_unionstate_t *st, int i) JL_NOTSAFEPOINT
{
    assert(i >= 0 && i < 32767); // limited by the depth bit.
    // get the `i`th bit in an array of 32-bit words
    jl_bits_stack_t *stack = &st->stack;
    while (i >= sizeof(stack->data) * 8) {
        // We should have set this bit.
        assert(stack->next);
        stack = stack->next;
        i -= sizeof(stack->data) * 8;
    }
    return (stack->data[i>>5] & (1u<<(i&31))) != 0;
}

static void statestack_set(jl_unionstate_t *st, int i, int val) JL_NOTSAFEPOINT
{
    assert(i >= 0 && i < 32767); // limited by the depth bit.
    jl_bits_stack_t *stack = &st->stack;
    while (i >= sizeof(stack->data) * 8) {
        if (__unlikely(stack->next == NULL)) {
            stack->next = (jl_bits_stack_t *)malloc(sizeof(jl_bits_stack_t));
            stack->next->next = NULL;
        }
        stack = stack->next;
        i -= sizeof(stack->data) * 8;
    }
    if (val)
        stack->data[i>>5] |= (1u<<(i&31));
    else
        stack->data[i>>5] &= ~(1u<<(i&31));
}

#define has_next_union_state(e, R) ((((R) ? &(e)->Runions : &(e)->Lunions)->more) != 0)

static int next_union_state(jl_stenv_t *e, int8_t R) JL_NOTSAFEPOINT
{
    jl_unionstate_t *state = R ? &e->Runions : &e->Lunions;
    if (state->more == 0)
        return 0;
    // reset `used` and let `pick_union_decision` clean the stack.
    state->used = state->more;
    statestack_set(state, state->used - 1, 1);
    return 1;
}

static int pick_union_decision(jl_stenv_t *e, int8_t R) JL_NOTSAFEPOINT
{
    jl_unionstate_t *state = R ? &e->Runions : &e->Lunions;
    if (state->depth >= state->used) {
        statestack_set(state, state->used, 0);
        state->used++;
    }
    int ui = statestack_get(state, state->depth);
    state->depth++;
    if (ui == 0)
        state->more = state->depth; // memorize that this was the deepest available choice
    return ui;
}

static jl_value_t *pick_union_element(jl_value_t *u JL_PROPAGATES_ROOT, jl_stenv_t *e, int8_t R) JL_NOTSAFEPOINT
{
    do {
        if (pick_union_decision(e, R))
            u = ((jl_uniontype_t*)u)->b;
        else
            u = ((jl_uniontype_t*)u)->a;
    } while (jl_is_uniontype(u));
    return u;
}

#define push_unionstate(saved, src)                                  \
    do {                                                             \
        (saved)->depth = (src)->depth;                               \
        (saved)->more = (src)->more;                                 \
        (saved)->used = (src)->used;                                 \
        jl_bits_stack_t *srcstack = &(src)->stack;                   \
        int pushbits = ((saved)->used+7)/8;                          \
        (saved)->stack = (uint8_t *)alloca(pushbits);                \
        for (int n = 0; n < pushbits; n += sizeof(srcstack->data)) { \
            assert(srcstack != NULL);                                \
            int rest = pushbits - n;                                 \
            if (rest > sizeof(srcstack->data))                       \
                rest = sizeof(srcstack->data);                       \
            memcpy(&(saved)->stack[n], &srcstack->data, rest);       \
            srcstack = srcstack->next;                               \
        }                                                            \
    } while (0);

#define pop_unionstate(dst, saved)                                  \
    do {                                                            \
        (dst)->depth = (saved)->depth;                              \
        (dst)->more = (saved)->more;                                \
        (dst)->used = (saved)->used;                                \
        jl_bits_stack_t *dststack = &(dst)->stack;                  \
        int popbits = ((saved)->used+7)/8;                          \
        for (int n = 0; n < popbits; n += sizeof(dststack->data)) { \
            assert(dststack != NULL);                               \
            int rest = popbits - n;                                 \
            if (rest > sizeof(dststack->data))                      \
                rest = sizeof(dststack->data);                      \
            memcpy(&dststack->data, &(saved)->stack[n], rest);      \
            dststack = dststack->next;                              \
        }                                                           \
    } while (0);

static int current_env_length(jl_stenv_t *e)
{
    jl_varbinding_t *v = e->vars;
    int len = 0;
    while (v) {
        len++;
        v = v->prev;
    }
    return len;
}

// Per-var saved env layout: [occurs_inv, occurs_cov, cov_diag, max_offset].
#define JL_SAVEDENV_BYTES_PER_VAR 4

// Combined covariance count used for diagonal-rule decisions: the max of the
// counter for the current consistency-check scope and the largest count
// observed in any already-closed scope. A variable is diagonal iff
// `cov_count(vb) > 1`.
static inline int8_t cov_count(const jl_varbinding_t *vb) JL_NOTSAFEPOINT
{
    return vb->occurs_cov > vb->cov_diag ? vb->occurs_cov : vb->cov_diag;
}

typedef struct {
    int8_t *buf;
    int rdepth;
    int8_t _space[32]; // == 8 * JL_SAVEDENV_BYTES_PER_VAR
    jl_gcframe_t gcframe;
    jl_value_t *roots[24]; // == 8 * 3 (lb, ub, innervars)
} jl_savedenv_t;

// Position of a subtype/intersect call within a type's structure. Determines
// whether (and how) a typevar occurrence at this position counts toward the
// diagonal rule (see record_var_occurrence).
typedef enum {
    PARAM_NONE      = 0,  // not inside a covariant/invariant context (top-level
                          // entry, UnionAll body before any constructor, or
                          // bound consistency recheck) — no occurrence recorded
    PARAM_COVARIANT = 1,  // inside a covariant parameter (Tuple/Vararg element)
    PARAM_INVARIANT = 2,  // inside an invariant parameter (most DataType
                          // parameters, Vararg length)
} jl_param_pos_t;

static void re_save_env(jl_stenv_t *e, jl_savedenv_t *se, int root)
{
    jl_value_t **roots = NULL;
    int nroots = 0;
    if (root) {
        if (se->gcframe.nroots == JL_GC_ENCODE_PUSHARGS(1)) {
            jl_svec_t *sv = (jl_svec_t*)se->roots[0];
            assert(jl_is_svec(sv));
            roots = jl_svec_data(sv);
            nroots = jl_svec_len(sv);
        }
        else {
            roots = se->roots;
            nroots = JL_GC_DECODE_NROOTS(se->gcframe.nroots);
        }
    }
    jl_varbinding_t *v = e->vars;
    int i = 0, j = 0;
    while (v != NULL) {
        if (root) {
            roots[i++] = v->lb;
            roots[i++] = v->ub;
            roots[i++] = (jl_value_t*)v->innervars;
        }
        se->buf[j++] = v->occurs_inv;
        se->buf[j++] = v->occurs_cov;
        se->buf[j++] = v->cov_diag;
        se->buf[j++] = v->max_offset;
        v = v->prev;
    }
    assert(i == nroots); (void)nroots;
    se->rdepth = e->Runions.depth;
}

static void alloc_env(jl_stenv_t *e, jl_savedenv_t *se, int root)
{
    jl_task_t *ct = jl_current_task;
    int len = current_env_length(e);
    se->gcframe.nroots = 0;
    se->gcframe.prev = NULL;
    se->roots[0] = NULL;
    if (len > 8) {
        if (root) {
            se->gcframe.nroots = JL_GC_ENCODE_PUSHARGS(1);
            se->gcframe.prev = ct->gcstack;
            ct->gcstack = &se->gcframe;
            jl_svec_t *sv = jl_alloc_svec(len * 3);
            se->roots[0] = (jl_value_t*)sv;
        }
    }
    else {
        if (root && len) {
            for (int i = 0; i < len * 3; i++)
                se->roots[i] = NULL;
            se->gcframe.nroots = JL_GC_ENCODE_PUSHARGS(len * 3);
            se->gcframe.prev = ct->gcstack;
            ct->gcstack = &se->gcframe;
        }
    }
    se->buf = (len > 8 ? (int8_t*)malloc_s(len * JL_SAVEDENV_BYTES_PER_VAR) : se->_space);
#ifdef __clang_gcanalyzer__
    memset(se->buf, 0, len * JL_SAVEDENV_BYTES_PER_VAR);
#endif
}

static void save_env(jl_stenv_t *e, jl_savedenv_t *se, int root)
{
    alloc_env(e, se, root);
    re_save_env(e, se, root);
}

static void free_env(jl_savedenv_t *se) JL_NOTSAFEPOINT
{
    if (se->gcframe.nroots) {
        assert(jl_current_task->gcstack == &se->gcframe);
        JL_GC_POP();
    }
    if (se->buf != se->_space)
        free(se->buf);
    se->buf = NULL;
}

static void free_stenv(jl_stenv_t *e) JL_NOTSAFEPOINT
{
    for (int R = 0; R < 2; R++) {
        jl_bits_stack_t *temp = R ? e->Runions.stack.next : e->Lunions.stack.next;
        while (temp != NULL) {
            jl_bits_stack_t *next = temp->next;
            free(temp);
            temp = next;
        }
    }
}

static void restore_env(jl_stenv_t *e, jl_savedenv_t *se, int root) JL_NOTSAFEPOINT
{
    jl_value_t *JL_NONNULL *roots = NULL;
    int nroots = 0;
    if (root) {
        if (se->gcframe.nroots == JL_GC_ENCODE_PUSHARGS(1)) {
            jl_svec_t *sv = (jl_svec_t*)se->roots[0];
            assert(jl_is_svec(sv));
            roots = jl_svec_data(sv);
            nroots = jl_svec_len(sv);
        }
        else {
            roots = se->roots;
            nroots = JL_GC_DECODE_NROOTS(se->gcframe.nroots);
        }
    }
    jl_varbinding_t *v = e->vars;
    int i = 0, j = 0;
    while (v != NULL) {
        if (root) {
            v->lb = roots[i++];
            v->ub = roots[i++];
            v->innervars = (jl_array_t*)roots[i++];
        }
        v->occurs_inv = se->buf[j++];
        v->occurs_cov = se->buf[j++];
        v->cov_diag = se->buf[j++];
        v->max_offset = se->buf[j++];
        v = v->prev;
    }
    assert(i == nroots); (void)nroots;
    e->Runions.depth = se->rdepth;
    if (e->envout && e->envidx < e->envsz)
        memset(&e->envout[e->envidx], 0, (e->envsz - e->envidx)*sizeof(void*));
}

#define flip_offset(e) ((e)->Loffset *= -1)

// type utilities

static int is_typeofbottom_typealias(jl_value_t *t) JL_NOTSAFEPOINT
{
    if (t == NULL)
        return 0;
    if (jl_typeofbottom_type == NULL)
        return 0;
    return t == (jl_value_t*)jl_typeofbottom_type ||
           (jl_is_typeeq(t) && jl_typeeq_T(t) == jl_bottom_type);
}

static jl_value_t *normalize_typeofbottom_typealias(jl_value_t *t) JL_NOTSAFEPOINT
{
    return is_typeofbottom_typealias(t) ? (jl_value_t*)jl_typeofbottom_type : t;
}

// quickly test that two types are identical
static int obviously_egal(jl_value_t *a, jl_value_t *b) JL_NOTSAFEPOINT
{
    if (a == b) return 1;
    a = normalize_typeofbottom_typealias(a);
    b = normalize_typeofbottom_typealias(b);
    if (a == b) return 1;
    if (jl_typeof(a) != jl_typeof(b)) return 0;
    if (jl_is_datatype(a)) {
        jl_datatype_t *ad = (jl_datatype_t*)a;
        jl_datatype_t *bd = (jl_datatype_t*)b;
        if (ad->name != bd->name) return 0;
        if (ad->isconcretetype || bd->isconcretetype) return 0;
        size_t i, np = jl_nparams(ad);
        if (np != jl_nparams(bd)) return 0;
        for (i = 0; i < np; i++) {
            if (!obviously_egal(jl_tparam(ad,i), jl_tparam(bd,i)))
                return 0;
        }
        return 1;
    }
    if (jl_is_uniontype(a) || jl_is_intersecttype(a)) {
        return obviously_egal(((jl_uniontype_t*)a)->a, ((jl_uniontype_t*)b)->a) &&
            obviously_egal(((jl_uniontype_t*)a)->b, ((jl_uniontype_t*)b)->b);
    }
    if (jl_is_unionall(a)) {
        return ((jl_unionall_t*)a)->var == ((jl_unionall_t*)b)->var &&
            obviously_egal(((jl_unionall_t*)a)->body, ((jl_unionall_t*)b)->body);
    }
    if (jl_is_vararg(a)) {
        jl_vararg_t *vma = (jl_vararg_t *)a;
        jl_vararg_t *vmb = (jl_vararg_t *)b;
        return obviously_egal(jl_unwrap_vararg(vma), jl_unwrap_vararg(vmb)) &&
            ((!vma->N && !vmb->N) || (vma->N && vmb->N && obviously_egal(vma->N, vmb->N)));
    }
    if (jl_is_typeeq(a))
        return obviously_egal(jl_typeeq_T(a), jl_typeeq_T(b));
    if (jl_is_typevar(a)) return 0;
    return !jl_is_type(a) && jl_egal(a,b);
}

static int obviously_unequal(jl_value_t *a, jl_value_t *b) JL_NOTSAFEPOINT
{
    if (a == b)
        return 0;
    a = normalize_typeofbottom_typealias(a);
    b = normalize_typeofbottom_typealias(b);
    if (a == b)
        return 0;
    if (jl_is_unionall(a))
        a = jl_unwrap_unionall(a);
    if (jl_is_unionall(b))
        b = jl_unwrap_unionall(b);
    if (jl_is_datatype(a)) {
        if (b == jl_bottom_type)
            return 1;
        if (jl_is_datatype(b)) {
            jl_datatype_t *ad = (jl_datatype_t*)a;
            jl_datatype_t *bd = (jl_datatype_t*)b;
            if (a == (jl_value_t*)jl_typeofbottom_type && jl_is_typeeq(b))
                return obviously_unequal(jl_bottom_type, jl_tparam(bd, 0));
            if (jl_is_typeeq(a) && b == (jl_value_t*)jl_typeofbottom_type)
                return obviously_unequal(jl_tparam(ad, 0), jl_bottom_type);
            if (ad->name != bd->name)
                return 1;
            int istuple = (ad->name == jl_tuple_typename);
            if (jl_type_equality_is_identity(a, b))
                return 1;
            size_t i, np;
            if (istuple) {
                size_t na = jl_nparams(ad), nb = jl_nparams(bd);
                if (jl_is_va_tuple(ad)) {
                    na -= 1;
                    if (jl_is_va_tuple(bd))
                        nb -= 1;
                }
                else if (jl_is_va_tuple(bd)) {
                    nb -= 1;
                }
                else if (na != nb) {
                    return 1;
                }
                np = na < nb ? na : nb;
            }
            else {
                np = jl_nparams(ad);
                if (np != jl_nparams(bd))
                    return 1;
            }
            for (i = 0; i < np; i++) {
                if (obviously_unequal(jl_tparam(ad, i), jl_tparam(bd, i)))
                    return 1;
            }
        }
    }
    else if (a == jl_bottom_type && jl_is_datatype(b)) {
        return 1;
    }
    if (jl_is_typevar(a) && jl_is_typevar(b) && obviously_unequal(((jl_tvar_t*)a)->ub, ((jl_tvar_t*)b)->ub))
        return 1;
    if (jl_is_long(a)) {
        if (jl_is_long(b) && jl_unbox_long(a) != jl_unbox_long(b))
            return 1;
    }
    else if (jl_is_long(b)) {
        return 1;
    }
    if ((jl_is_symbol(a) || jl_is_symbol(b)) && a != b)
        return 1;
    return 0;
}

int jl_obviously_unequal(jl_value_t *a, jl_value_t *b)
{
    return obviously_unequal(a, b);
}

static int in_union(jl_value_t *u, jl_value_t *x) JL_NOTSAFEPOINT
{
    if (u == x) return 1;
    if (!jl_is_uniontype(u)) return 0;
    return in_union(((jl_uniontype_t*)u)->a, x) || in_union(((jl_uniontype_t*)u)->b, x);
}

static int obviously_in_union(jl_value_t *u, jl_value_t *x)
{
    jl_value_t *a = NULL, *b = NULL;
    if (jl_is_uniontype(x)) {
        a = ((jl_uniontype_t*)x)->a;
        b = ((jl_uniontype_t*)x)->b;
        JL_GC_PUSH2(&a, &b);
        int res = obviously_in_union(u, a) && obviously_in_union(u, b);
        JL_GC_POP();
        return res;
    }
    if (jl_is_uniontype(u)) {
        a = ((jl_uniontype_t*)u)->a;
        b = ((jl_uniontype_t*)u)->b;
        JL_GC_PUSH2(&a, &b);
        int res = obviously_in_union(a, x) || obviously_in_union(b, x);
        JL_GC_POP();
        return res;
    }
    return obviously_egal(u, x);
}

// the types whose instances are all themselves types: the concrete kinds plus the
// abstract kind `AnyType` (`== Type`, though not `===`)
STATIC_INLINE int is_kind_or_anytype(jl_value_t *t) JL_NOTSAFEPOINT
{
    return jl_is_kind(t) || t == (jl_value_t*)jl_anytype_type;
}

int obviously_disjoint(jl_value_t *a, jl_value_t *b, int specificity) JL_NOTSAFEPOINT
{
    if (a == b || a == (jl_value_t*)jl_any_type || b == (jl_value_t*)jl_any_type)
        return 0;
    if (specificity && a == (jl_value_t*)jl_typeofbottom_type)
        return 0;
    if (jl_is_concrete_type(a) && jl_is_concrete_type(b) && jl_type_equality_is_identity(a, b))
        return 1;
    if (jl_is_unionall(a)) a = jl_unwrap_unionall(a);
    if (jl_is_unionall(b)) b = jl_unwrap_unionall(b);
    if (jl_is_uniontype(a))
        return obviously_disjoint(((jl_uniontype_t *)a)->a, b, specificity) &&
               obviously_disjoint(((jl_uniontype_t *)a)->b, b, specificity);
    if (jl_is_uniontype(b))
        return obviously_disjoint(a, ((jl_uniontype_t *)b)->a, specificity) &&
               obviously_disjoint(a, ((jl_uniontype_t *)b)->b, specificity);
    if (jl_is_datatype(a) && jl_is_datatype(b)) {
        jl_datatype_t *ad = (jl_datatype_t*)a, *bd = (jl_datatype_t*)b;
        if (ad->name != bd->name) {
            jl_datatype_t *temp = ad;
            while (temp != jl_any_type && temp->name != bd->name)
                temp = temp->super;
            if (temp == jl_any_type) {
                temp = bd;
                while (temp != jl_any_type && temp->name != ad->name)
                    temp = temp->super;
                if (temp == jl_any_type)
                    return 1;
                bd = temp;
            }
            else {
                ad = temp;
            }
            if (specificity) {
                // account for declared subtypes taking priority (issue #21710)
                return 0;
            }
        }
        int istuple = (ad->name == jl_tuple_typename);
        size_t np;
        if (istuple) {
            size_t na = jl_nparams(ad), nb = jl_nparams(bd);
            if (jl_is_va_tuple(ad)) {
                na -= 1;
                if (jl_is_va_tuple(bd))
                    nb -= 1;
            }
            else if (jl_is_va_tuple(bd)) {
                nb -= 1;
            }
            else if (!specificity && na != nb) {
                // note: some disjoint types (e.g. tuples of different lengths) can be more specific
                return 1;
            }
            np = na < nb ? na : nb;
        }
        else {
            np = jl_nparams(ad);
        }
        size_t i;
        for (i = 0; i < np; i++) {
            jl_value_t *ai = jl_tparam(ad, i);
            jl_value_t *bi = jl_tparam(bd, i);
            if (jl_is_typevar(ai) || jl_is_typevar(bi))
                continue; // it's possible that Union{} is in this intersection
            if (jl_is_type(ai)) {
                if (jl_is_type(bi)) {
                    if (istuple && (ai == jl_bottom_type || bi == jl_bottom_type))
                        ; // TODO: this can return 1 if and when Tuple{Union{}} === Union{}
                    else if (obviously_disjoint(ai, bi, specificity))
                        return 1;
                }
                else if (ai != (jl_value_t*)jl_any_type) {
                    return 1;
                }
            }
            else if (jl_is_type(bi)) {
                if (bi != (jl_value_t*)jl_any_type)
                    return 1;
            }
            else if (!jl_egal(ai, bi)) {
                return 1;
            }
        }
    }
    else if (a == jl_bottom_type || b == jl_bottom_type) {
        return 1;
    }
    return 0;
}

jl_value_t *simple_union(jl_value_t *a, jl_value_t *b);
// compute a least upper bound of `a` and `b`
static jl_value_t *simple_join(jl_value_t *a, jl_value_t *b)
{
    if (a == jl_bottom_type || b == (jl_value_t*)jl_any_type || obviously_egal(a, b))
        return b;
    if (b == jl_bottom_type || a == (jl_value_t*)jl_any_type)
        return a;
    if (!(jl_is_type(a) || jl_is_typevar(a)) || !(jl_is_type(b) || jl_is_typevar(b)))
        return (jl_value_t*)jl_any_type;
    if (jl_is_kind(a) && jl_is_typeeq(b) && jl_typeof(jl_typeeq_T(b)) == a)
        return a;
    if (jl_is_kind(b) && jl_is_typeeq(a) && jl_typeof(jl_typeeq_T(a)) == b)
        return b;
    if (jl_is_typevar(a) && obviously_egal(b, ((jl_tvar_t*)a)->lb))
        return a;
    if (jl_is_typevar(b) && obviously_egal(a, ((jl_tvar_t*)b)->lb))
        return b;
    return simple_union(a, b);
}

jl_value_t *simple_intersect(jl_value_t *a, jl_value_t *b, int overesi);
// Compute a greatest lower bound of `a` and `b`
// For the subtype path, we need to over-estimate this by returning `b` in many cases.
// But for `merge_env`, we'd better under-estimate and return a `Union{}`
static jl_value_t *simple_meet(jl_value_t *a, jl_value_t *b, int overesi)
{
    if (a == (jl_value_t*)jl_any_type || b == jl_bottom_type || obviously_egal(a,b))
        return b;
    if (b == (jl_value_t*)jl_any_type || a == jl_bottom_type)
        return a;
    if (overesi == 1 && (jl_is_intersecttype(a) || jl_is_intersecttype(b)))
        // one operand is already an internal `Intersect` meet node.
        // Represent the combined meet exactly by nesting.
        return jl_new_struct(jl_intersect_type, a, b);
    if (!(jl_is_type(a) || jl_is_typevar(a)) || !(jl_is_type(b) || jl_is_typevar(b)))
        return jl_bottom_type;
    if (jl_is_kind(a) && jl_is_typeeq(b) && jl_typeof(jl_typeeq_T(b)) == a)
        return b;
    if (jl_is_kind(b) && jl_is_typeeq(a) && jl_typeof(jl_typeeq_T(a)) == b)
        return a;
    if (jl_is_typevar(a) && obviously_egal(b, ((jl_tvar_t*)a)->ub))
        return a;
    if (jl_is_typevar(b) && obviously_egal(a, ((jl_tvar_t*)b)->ub))
        return b;
    return simple_intersect(a, b, overesi);
}

// Over-approximate an internal `Intersect` meet node (see #61917) by a real
// type, so it cannot escape subtyping into a result type or static parameter.
// An `Intersect` only ever occurs as the top layer of a varbinding's `ub`
// (possibly as a spine of nested `Intersect`s, but never under another type
// constructor), so it suffices to peel that spine here. `Intersect{a, b}`
// denotes `a ∩ b`, which `simple_meet` with `overesi==2` over-approximates by a
// real supertype. `typeintersect` may over-approximate, so this is sound.
static jl_value_t *widen_intersect(jl_value_t *t)
{
    if (t == NULL || !jl_is_intersecttype(t))
        return t;
    jl_value_t *a = NULL, *b = NULL, *res = NULL;
    JL_GC_PUSH2(&a, &b);
    a = widen_intersect(((jl_intersecttype_t*)t)->a);
    b = widen_intersect(((jl_intersecttype_t*)t)->b);
    res = simple_meet(a, b, 2);
    JL_GC_POP();
    return res;
}

// main subtyping algorithm

static int subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_param_pos_t param);

static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_param_pos_t param, int limit_slow);

static int is_leaf_typevar(jl_tvar_t *v) JL_NOTSAFEPOINT;

// Check whether env (variable bounds & diagonality) changed compared to saved env.
static int env_unchanged(jl_stenv_t *e, jl_savedenv_t *se) JL_NOTSAFEPOINT
{
    jl_value_t **roots = NULL;
    if (se->gcframe.nroots == JL_GC_ENCODE_PUSHARGS(1)) {
        jl_svec_t *sv = (jl_svec_t*)se->roots[0];
        assert(jl_is_svec(sv));
        roots = jl_svec_data(sv);
    }
    else if (se->gcframe.nroots) {
        roots = se->roots;
    }
    jl_varbinding_t *v = e->vars;
    int i = 0, j = 1;
    while (v != NULL) {
        assert(roots != NULL);
        if (v->existential) {
            if (v->lb != roots[i] || v->ub != roots[i + 1])
                return 0; // check if bounds changed
            int8_t saved_cov = se->buf[j];     // saved occurs_cov
            int8_t saved_diag = se->buf[j+1];  // saved cov_diag
            int8_t saved_max = saved_cov > saved_diag ? saved_cov : saved_diag;
            if (is_leaf_typevar(v->var) && v->body_occurs_inv == 0 && cov_count(v) > 1 && saved_max <= 1)
                return 0; // check if a variable became diagonal from non-diagonal
        }
        i += 3; // lb, ub, innervars
        j += JL_SAVEDENV_BYTES_PER_VAR;
        v = v->prev;
    }
    return 1;
}

static int push_consistency_scope(jl_stenv_t *e, int8_t *saved) JL_NOTSAFEPOINT;
static void pop_consistency_scope(jl_stenv_t *e, const int8_t *saved, int nsaved) JL_NOTSAFEPOINT;

// subtype for variable bounds consistency check. needs its own forall/exists environment.
static int subtype_ccheck(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
{
    if (jl_is_long(x) && jl_is_long(y))
        return jl_unbox_long(x) == jl_unbox_long(y) + e->Loffset;
    if (x == y)
        return 1;
    if (x == jl_bottom_type && jl_is_type(y))
        return 1;
    if (y == (jl_value_t*)jl_any_type && jl_is_type(x))
        return 1;
    if (jl_is_uniontype(x) && jl_egal(x, y))
        return 1;
    if (x == (jl_value_t*)jl_any_type && jl_is_datatype(y))
        return 0;
    if (obviously_in_union(y, x))
        return 1;
    jl_saved_unionstate_t oldLunions; push_unionstate(&oldLunions, &e->Lunions);
    // Consistency check for a typevar bound: covariant occurrences inside this
    // call should not accumulate into the surrounding scope's diagonality
    // counter. Save & reset the counters, then fold the local max into
    // cov_diag on exit.
    int8_t *saved_cov = (int8_t*)alloca(current_env_length(e));
    int nsaved_cov = push_consistency_scope(e, saved_cov);
    int sub = local_forall_exists_subtype(x, y, e, PARAM_COVARIANT, 1);
    pop_consistency_scope(e, saved_cov, nsaved_cov);
    pop_unionstate(&e->Lunions, &oldLunions);
    return sub;
}

static int subtype_left_var(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_param_pos_t param)
{
    if (jl_is_long(x) && jl_is_long(y))
        return jl_unbox_long(x) == jl_unbox_long(y) + e->Loffset;
    if (x == y && !(jl_is_unionall(y)))
        return 1;
    if (x == jl_bottom_type && jl_is_type(y))
        return 1;
    if (y == (jl_value_t*)jl_any_type && jl_is_type(x))
        return 1;
    if (jl_is_uniontype(x) && jl_egal(x, y))
        return 1;
    if (x == (jl_value_t*)jl_any_type && jl_is_datatype(y))
        return 0;
    return subtype(x, y, e, param);
}

// use the current context to record where a variable occurred, for the purpose
// of determining whether the variable is concrete.
static void record_var_occurrence(jl_varbinding_t *vb, jl_stenv_t *e, jl_param_pos_t param) JL_NOTSAFEPOINT
{
    if (vb != NULL && param != PARAM_NONE) {
        // saturate counters at 2; we don't need values bigger than that
        if (param == PARAM_INVARIANT && e->invdepth > vb->depth0) {
            if (vb->occurs_inv < 2)
                vb->occurs_inv++;
        }
        else if (vb->occurs_cov < 2) {
            vb->occurs_cov++;
        }
        // Always set `max_offset` to `-1` during the 1st round intersection.
        // Would be recovered in `intersect_varargs`/`subtype_tuple_varargs` if needed.
        if (!vb->intersected)
            vb->max_offset = -1;
    }
}

// Scope the diagonal-rule's covariance counter to the surrounding
// covariant-position context, so that occurrences inside a consistency check
// (`subtype_ccheck` / `intersect_aside`) of a typevar's bound do not
// contaminate the outer covariance count. Covariant positions in covariant
// position tuples within the same scope still accumulate as before.
//
// `push_consistency_scope` saves the current `occurs_cov` of every live var
// into `saved` and resets it to 0; `pop_consistency_scope` folds the in-scope
// value into `cov_diag` (via max) and restores `occurs_cov` from `saved`.
// The diagonal-rule test then becomes `max(occurs_cov, cov_diag) > 1`: a
// variable is diagonal iff it occurred >= 2 times in some single scope (the
// outer scope or any consistency check), rather than summed across all
// consistency checks.
static int push_consistency_scope(jl_stenv_t *e, int8_t *saved) JL_NOTSAFEPOINT
{
    jl_varbinding_t *v = e->vars;
    int i = 0;
    while (v != NULL) {
        saved[i++] = v->occurs_cov;
        v->occurs_cov = 0;
        v = v->prev;
    }
    return i;
}

static void pop_consistency_scope(jl_stenv_t *e, const int8_t *saved, int nsaved) JL_NOTSAFEPOINT
{
    jl_varbinding_t *v = e->vars;
    int i = 0;
    while (v != NULL && i < nsaved) {
        if (v->occurs_cov > v->cov_diag)
            v->cov_diag = v->occurs_cov;
        v->occurs_cov = saved[i++];
        v = v->prev;
    }
}

// When expanding a universal variable's declared upper/lower bound during
// `var_lt` / `var_gt`, occurrences contributed by the expanded bound (which
// can only mention forall-side vars) must not combine with occurrences in the
// enclosing tuple body. We push a separate evidence frame for forall vars
// only: their counts are reset before the recursive subtype call and folded
// into `cov_diag` afterward, while exists-side vars continue accumulating in
// the current scope (their occurrences in the call's right-hand structure are
// still part of the surrounding pattern).
static int push_forall_bound_scope(jl_stenv_t *e, int8_t *saved) JL_NOTSAFEPOINT
{
    jl_varbinding_t *v = e->vars;
    int i = 0;
    while (v != NULL) {
        saved[i++] = v->occurs_cov;
        if (!v->existential)
            v->occurs_cov = 0;
        v = v->prev;
    }
    return i;
}

static void pop_forall_bound_scope(jl_stenv_t *e, const int8_t *saved, int nsaved) JL_NOTSAFEPOINT
{
    jl_varbinding_t *v = e->vars;
    int i = 0;
    while (v != NULL && i < nsaved) {
        if (!v->existential) {
            if (v->occurs_cov > v->cov_diag)
                v->cov_diag = v->occurs_cov;
            v->occurs_cov = saved[i];
        }
        i++;
        v = v->prev;
    }
}

// is var x's quantifier outside y's in nesting order
static int var_outside(jl_stenv_t *e, jl_tvar_t *x, jl_tvar_t *y)
{
    jl_varbinding_t *btemp = e->vars;
    while (btemp != NULL) {
        if (btemp->var == x) return 0;
        if (btemp->var == y) return 1;
        btemp = btemp->prev;
    }
    return 0;
}

static jl_value_t *intersect_aside(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int depth);

static int reachable_var(jl_value_t *x, jl_tvar_t *y, jl_stenv_t *e);

static int singleton_typevar_subtype(jl_tvar_t *v, jl_value_t *a) JL_NOTSAFEPOINT
{
    if (a == (jl_value_t*)v || a == (jl_value_t*)jl_any_type)
        return 1;
    if (jl_is_uniontype(a))
        return singleton_typevar_subtype(v, ((jl_uniontype_t*)a)->a) ||
               singleton_typevar_subtype(v, ((jl_uniontype_t*)a)->b);
    return 0;
}

static int subtype_singleton_typevar(jl_value_t *a, jl_tvar_t *v) JL_NOTSAFEPOINT
{
    if (a == (jl_value_t*)v || a == jl_bottom_type)
        return 1;
    if (jl_is_uniontype(a))
        return subtype_singleton_typevar(((jl_uniontype_t*)a)->a, v) &&
               subtype_singleton_typevar(((jl_uniontype_t*)a)->b, v);
    return 0;
}

// check that type var `b` is <: `a`, and update b's upper bound.
static int var_lt(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, jl_param_pos_t param, jl_varbinding_t *bb, int innervar)
{
    if (bb == NULL) {
        if (innervar && e->intersection)
            return 1;
        if (innervar)
            return subtype_left_var(b->ub, a, e, param);
        return singleton_typevar_subtype(b, a);
    }
    record_var_occurrence(bb, e, param);
    assert(!jl_is_long(a) || e->Loffset == 0);
    if (e->Loffset != 0 && !jl_is_typevar(a) &&
        a != jl_bottom_type && a != (jl_value_t *)jl_any_type)
        return 0;
    if (!bb->existential) {  // check ∀b . b<:a
        // The expanded bound `bb->ub` lives in the forall-side context;
        // its covariant typevar occurrences must not combine with the
        // surrounding tuple body's occurrences.
        int8_t *saved_fb = (int8_t*)alloca(current_env_length(e));
        int nsaved_fb = push_forall_bound_scope(e, saved_fb);
        int sub = subtype_left_var(bb->ub, a, e, param);
        pop_forall_bound_scope(e, saved_fb, nsaved_fb);
        return sub;
    }
    if (bb->ub == a)
        return 1;
    if (!((bb->lb == jl_bottom_type && !jl_is_type(a) && !jl_is_typevar(a)) || subtype_ccheck(bb->lb, a, e)))
        return 0;
    // for this to work we need to compute issub(left,right) before issub(right,left),
    // since otherwise the issub(a, bb.ub) check in var_gt becomes vacuous.
    if (e->intersection) {
        jl_value_t *ub = intersect_aside(a, bb->ub, e, bb->depth0);
        JL_GC_PUSH1(&ub);
        if (ub != (jl_value_t*)b && (!jl_is_typevar(ub) || !reachable_var(ub, b, e)))
            bb->ub = ub;
        JL_GC_POP();
    }
    else {
        // `simple_meet` resolves the greatest-lower-bound of `bb->ub` and `a`
        // precisely when one operand subsumes the other (or they are disjoint);
        // otherwise it now returns an exact `Intersect{bb->ub, a}` meet node
        // rather than over-approximating to one side, which would let `b` escape
        // its declared range (e.g. equating `∃b<:Foo` with an outer `∀a<:Bar`
        // even though `Bar ⊄ Foo`). See #61917.
        bb->ub = simple_meet(bb->ub, a, 1);
    }
    assert(bb->ub != (jl_value_t*)b);
    return 1;
}

// check that type var `b` is >: `a`, and update b's lower bound.
static int var_gt(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, jl_param_pos_t param, jl_varbinding_t *bb, int innervar)
{
    if (bb == NULL) {
        if (innervar && e->intersection)
            return 1;
        if (innervar)
            return subtype_left_var(a, b->lb, e, param);
        return subtype_singleton_typevar(a, b);
    }
    record_var_occurrence(bb, e, param);
    assert(!jl_is_long(a) || e->Loffset == 0);
    if (e->Loffset != 0 && !jl_is_typevar(a) &&
        a != jl_bottom_type && a != (jl_value_t *)jl_any_type)
        return 0;
    if (!bb->existential) {  // check ∀b . b>:a
        // Symmetric to var_lt: scope forall-side occurrences from the expanded
        // lower bound away from the enclosing tuple body.
        int8_t *saved_fb = (int8_t*)alloca(current_env_length(e));
        int nsaved_fb = push_forall_bound_scope(e, saved_fb);
        int sub = subtype_left_var(a, bb->lb, e, param);
        pop_forall_bound_scope(e, saved_fb, nsaved_fb);
        return sub;
    }
    if (bb->lb == a)
        return 1;
    if (!((bb->ub == (jl_value_t*)jl_any_type && !jl_is_type(a) && !jl_is_typevar(a)) || subtype_ccheck(a, bb->ub, e)))
        return 0;
    jl_value_t *lb = simple_join(bb->lb, a);
    JL_GC_PUSH1(&lb);
    if (!e->intersection || !jl_is_typevar(lb) || !reachable_var(lb, b, e))
        bb->lb = lb;
    JL_GC_POP();
    // this bound should not be directly circular
    assert(bb->lb != (jl_value_t*)b);
    return 1;
}

static int subtype_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int R, jl_param_pos_t param, jl_varbinding_t *bb, int innervar)
{
    if (e->intersection) {
        jl_value_t *bub = bb ? bb->ub : innervar ? ((jl_tvar_t*)b)->ub : (jl_value_t*)b;
        jl_value_t *blb = bb ? bb->lb : innervar ? ((jl_tvar_t*)b)->lb : (jl_value_t*)b;
        if (bub == blb && jl_is_typevar(bub) && bub != (jl_value_t*)b) {
            int bubinner = 0;
            jl_varbinding_t *bubb = lookup_binding(e, (jl_tvar_t*)bub, &bubinner);
            int sub = subtype_var((jl_tvar_t *)bub, a, e, R, param, bubb, bubinner);
            return sub;
        }
    }
    if (e->Loffset != 0 && jl_is_long(a)) {
        int old_offset = R ? -e->Loffset : e->Loffset;
        jl_value_t *na = jl_box_long(jl_unbox_long(a) + old_offset);
        JL_GC_PUSH1(&na);
        e->Loffset = 0;
        int sub = R ? var_gt(b, na, e, param, bb, innervar) : var_lt(b, na, e, param, bb, innervar);
        e->Loffset = R ? -old_offset : old_offset;
        JL_GC_POP();
        return sub;
    }
    return R ? var_gt(b, a, e, param, bb, innervar) : var_lt(b, a, e, param, bb, innervar);
}

// check that a type is concrete or quasi-concrete (Type{T}).
// this is used to check concrete typevars:
// issubtype is false if the lower bound of a concrete type var is not concrete.
int is_leaf_bound(jl_value_t *v) JL_NOTSAFEPOINT
{
    if (v == jl_bottom_type)
        return 1;
    if (jl_is_intersecttype(v)) // internal meet node (see #61917), not a concrete leaf
        return 0;
    if (jl_is_typeeq(v))
        return 1;
    if (jl_is_datatype(v)) {
        if (((jl_datatype_t*)v)->name->abstract) {
            return 0;
        }
        return ((jl_datatype_t*)v)->isconcretetype;
    }
    return !jl_is_type(v) && !jl_is_typevar(v);
}

static int is_leaf_typevar(jl_tvar_t *v) JL_NOTSAFEPOINT
{
    return is_leaf_bound(v->lb);
}

static jl_value_t *widen_Type_if_concrete(jl_value_t *t JL_PROPAGATES_ROOT) JL_NOTSAFEPOINT
{
    if (jl_is_typeeq(t) && !jl_is_typevar(jl_typeeq_T(t)))
        return jl_typeof(jl_typeeq_T(t));
    if (jl_is_uniontype(t)) {
        jl_value_t *a = widen_Type_if_concrete(((jl_uniontype_t*)t)->a);
        jl_value_t *b = widen_Type_if_concrete(((jl_uniontype_t*)t)->b);
        if (a == b)
            return a;
    }
    if (jl_is_unionall(t)) {
        jl_unionall_t *u = (jl_unionall_t*)t;
        jl_value_t *body = widen_Type_if_concrete(u->body);
        if (body != u->body && !jl_has_typevar(body, u->var))
            return body;
    }
    return t;
}

static int try_subtype_in_env(jl_value_t *a, jl_value_t *b, jl_stenv_t *e);

// Map Type{X} to kind type (DataType, UnionAll, Union, TypeofBottom) over union
// only if the widened kind satisfies `bound` , otherwise leave unchanged
static jl_value_t *widen_Type_to_union(jl_value_t *t, jl_value_t *bound, jl_stenv_t *e)
{
    if (jl_is_typeeq(t) && !jl_is_typevar(jl_typeeq_T(t))) {
        jl_value_t *T = jl_typeeq_T(t);
        jl_value_t *w = jl_typeof(T);
        if (!try_subtype_in_env(w, bound, e))
            return t;
        return w;
    }
    if (jl_is_uniontype(t)) {
        jl_value_t *wa = NULL, *wb = NULL;
        JL_GC_PUSH2(&wa, &wb);
        wa = widen_Type_to_union(((jl_uniontype_t*)t)->a, bound, e);
        wb = widen_Type_to_union(((jl_uniontype_t*)t)->b, bound, e);
        if (wa != ((jl_uniontype_t*)t)->a || wb != ((jl_uniontype_t*)t)->b)
            wa = simple_join(wa, wb);
        else
            wa = t;
        JL_GC_POP();
        return wa;
    }
    if (jl_is_unionall(t)) {
        jl_unionall_t *u = (jl_unionall_t*)t;
        jl_value_t *body = NULL;
        JL_GC_PUSH1(&body);
        body = widen_Type_to_union(u->body, bound, e);
        if (body != u->body && !jl_has_typevar(body, u->var)) {
            JL_GC_POP();
            return body;
        }
        JL_GC_POP();
    }
    return t;
}

static int var_occurs_inside(jl_value_t *v, jl_tvar_t *var, int inside, int want_inv) JL_NOTSAFEPOINT;

// wrap a TypeVar env entry as svec(tvar, constrained): preserves TypeVar
// identity while carrying the "constrained by any concrete subtype" bit.
// `tvar` is the uncertain value (typically a TypeVar); `constrained` is 1
// iff any concrete subtype of the LHS will pin this var to a definite value.
static jl_value_t *wrap_tvar_env(jl_value_t *tvar, int constrained)
{
    return (jl_value_t*)jl_svec2(tvar, constrained ? jl_true : jl_false);
}

// Static check mirroring Core.Compiler.constrains_param: is `var` guaranteed
// to be pinned by any concrete leaftype subtype of `typ`? Conservative: a
// false return is always safe. Used only on fast paths where we don't have
// dynamic varbinding state to draw from.
static int constrains_param_static(jl_tvar_t *var, jl_value_t *typ, int covariant) JL_NOTSAFEPOINT
{
    if (typ == (jl_value_t*)var)
        return 1;
    while (jl_is_unionall(typ)) {
        jl_unionall_t *ua = (jl_unionall_t*)typ;
        if (covariant && constrains_param_static(var, ua->var->ub, covariant))
            return 1;
        // ua->var->lb doesn't constrain var
        typ = ua->body;
    }
    if (jl_is_uniontype(typ)) {
        // both alternatives must constrain var
        return constrains_param_static(var, ((jl_uniontype_t*)typ)->a, covariant) &&
               constrains_param_static(var, ((jl_uniontype_t*)typ)->b, covariant);
    }
    else if (jl_is_typeeq(typ)) {
        jl_value_t *T = jl_typeeq_T(typ);
        if (T == (jl_value_t*)var && var->ub == (jl_value_t*)jl_any_type) {
            return 0;
        }
        return constrains_param_static(var, T, 0);
    }
    else if (jl_is_datatype(typ)) {
        jl_datatype_t *dt = (jl_datatype_t*)typ;
        size_t fc = jl_nparams(dt);
        if (fc > 0) {
            if (dt->name == jl_tuple_typename) {
                for (size_t i = 0; i < fc - 1; i++) {
                    if (constrains_param_static(var, jl_tparam(dt, i), covariant))
                        return 1;
                }
                jl_value_t *lastp = jl_tparam(dt, fc - 1);
                jl_value_t *vararg = jl_unwrap_unionall(lastp);
                if (jl_is_vararg(vararg)) {
                    jl_value_t *vN = jl_unwrap_vararg_num(vararg);
                    if (vN) {
                        if (constrains_param_static(var, vN, covariant))
                            return 1;
                    }
                    else if (constrains_param_static(var, lastp, covariant)) {
                        return 1;
                    }
                }
                else if (constrains_param_static(var, lastp, covariant)) {
                    return 1;
                }
            }
            else {
                for (size_t i = 0; i < fc; i++) {
                    if (constrains_param_static(var, jl_tparam(dt, i), 0))
                        return 1;
                }
            }
        }
    }
    return 0;
}

typedef int (*tvar_callback)(void*, int8_t, jl_stenv_t *, int);

static int var_occurs_invariant(jl_value_t *v, jl_tvar_t *var) JL_NOTSAFEPOINT
{
    return var_occurs_inside(v, var, 0, 1);
}

static jl_unionall_t *unalias_unionall(jl_unionall_t *u, jl_stenv_t *e)
{
    jl_varbinding_t *btemp = e->vars;
    // if the var for this unionall (based on identity) already appears somewhere
    // in the environment, rename to get a fresh var.
    JL_GC_PUSH1(&u);
    while (btemp != NULL) {
        int aliased = btemp->var == u->var ||
            // outer var can only refer to inner var if bounds changed (mainly for subtyping path)
            (btemp->lb != btemp->var->lb && jl_has_typevar(btemp->lb, u->var)) ||
            (btemp->ub != btemp->var->ub && jl_has_typevar(btemp->ub, u->var));
        if (!aliased && btemp->innervars != NULL) {
            for (size_t i = 0; i < jl_array_len(btemp->innervars); i++) {
                jl_tvar_t *ivar = (jl_tvar_t*)jl_array_ptr_ref(btemp->innervars, i);
                if (ivar == u->var) {
                    aliased = 1;
                    break;
                }
            }
        }
        if (aliased) {
            u = jl_rename_unionall(u);
            break;
        }
        btemp = btemp->prev;
    }
    JL_GC_POP();
    return u;
}

static int has_existential_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->existential) {
            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 has_universal_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->existential) {
            jl_typeenv_t *newenv = (jl_typeenv_t*)alloca(sizeof(jl_typeenv_t));
            newenv->var = v->var;
            newenv->val = NULL;
            newenv->prev = env;
            env = newenv;
        }
        if (v->innervars != NULL) {
            for (size_t i = 0; i < jl_array_len(v->innervars); i++) {
                jl_typeenv_t *newenv = (jl_typeenv_t*)alloca(sizeof(jl_typeenv_t));
                newenv->var = (jl_tvar_t*)jl_array_ptr_ref(v->innervars, i);
                newenv->val = NULL;
                newenv->prev = env;
                env = newenv;
            }
        }
        v = v->prev;
    }
    return env != NULL && jl_has_bound_typevars(x, env);
}

// Helper for the hoisted union-split of a `∀` variable's upper bound in
// `subtype_unionall` below.
// Test whether every occurrence of `var` in `t` is covariant, where covariant
// means reachable purely through Tuple parameters, Union components, and
// Vararg element types. An occurrence under a non-Tuple datatype parameter,
// in a Vararg length, or anywhere inside an inner UnionAll (bounds or body)
// is not covariant. Returns 1 if `var` does not occur at all.
static int var_occurs_covariant_only(jl_value_t *t, jl_tvar_t *var, int covariant) JL_NOTSAFEPOINT
{
    if (t == (jl_value_t*)var)
        return covariant;
    else if (jl_is_uniontype(t)) {
        return var_occurs_covariant_only(((jl_uniontype_t*)t)->a, var, covariant) &&
               var_occurs_covariant_only(((jl_uniontype_t*)t)->b, var, covariant);
    }
    else if (jl_is_unionall(t)) {
        if (((jl_unionall_t*)t)->var == var)
            return 1; // shadowed
        return !jl_has_typevar(t, var);
    }
    else if (jl_is_vararg(t)) {
        jl_vararg_t *vm = (jl_vararg_t*)t;
        if (vm->N && jl_has_typevar(vm->N, var))
            return 0;
        return vm->T == NULL || var_occurs_covariant_only(vm->T, var, covariant);
    }
    else if (jl_is_datatype(t)) {
        int incov = covariant && jl_is_tuple_type(t);
        for (size_t i = 0; i < jl_nparams(t); i++) {
            if (!var_occurs_covariant_only(jl_tparam(t, i), var, incov))
                return 0;
        }
        return 1;
    }
    // conservative for internal nodes (TypeEq, TypeApp, Intersect); plain
    // values contain no typevars
    return !jl_has_typevar(t, var);
}

static jl_value_t *subtype_unionall_envout_value(jl_value_t *t, jl_unionall_t *u, jl_stenv_t *e,
                                                 jl_varbinding_t *vb, jl_value_t *lb,
                                                 jl_value_t **new_tvar JL_REQUIRE_ROOTED_SLOT,
                                                 int constrained)
{
    if (vb->intvalued && lb == (jl_value_t*)jl_any_type)
        return (jl_value_t*)jl_wrap_vararg(NULL, NULL, 0, 0); // special token result that represents N::Int in the envout
    if (!vb->occurs_inv && lb != jl_bottom_type) {
        if (is_leaf_bound(lb))
            return lb;
        if (constrained && !jl_has_free_typevars(t) && !jl_has_free_typevars(lb) &&
            (jl_is_concrete_type(t) ||
             (jl_is_datatype(t) && ((jl_datatype_t*)t)->isdispatchtuple))) {
            // If the LHS is concrete, e.g. Type{Tuple{Ref}} vs Type{Tuple{S}} where {S<:T}, we'd like to still
            // choose the least solution like below, so that our `constrained` logic below is correct.
            // Also accept dispatchtuples, which cover singleton-like LHSes such as
            // `Tuple{typeof(f), Type{X}}` where the Type{} parameter pins to one runtime value.
            // Refuse when `lb` references universally-quantified vars from the
            // current subtype environment: exposing it directly would leak sibling
            // `where`-bound typevars (e.g. `where {S, T>:S}` would expose `S`).
            return lb;
        }
        if (jl_is_typevar(lb)) {
            // The path below would produce `T_new <: T`. This is redundant for bounds purposes,
            // although it could affect diagonality in downstream uses. However, it is problematic
            // to introduce a new tvar for safety here, because intersection can blow up on that
            // pattern.
            return wrap_tvar_env(lb, constrained);
        }
        *new_tvar = (jl_value_t*)jl_new_typevar(u->var->name, jl_bottom_type, lb);
        return wrap_tvar_env(*new_tvar, constrained);
    }
    if (lb == vb->ub || lb != jl_bottom_type) {
        // TODO (lb != jl_bottom_type): for now return the least solution, which is what
        // method parameters expect.
        if (vb->tainted_inner || has_universal_typevar(lb, e))
            return wrap_tvar_env(lb, constrained);
        return lb;
    }
    if (lb == u->var->lb && vb->ub == u->var->ub && !*new_tvar)
        return wrap_tvar_env((jl_value_t*)u->var, constrained);
    if (!*new_tvar) {
        *new_tvar = (jl_value_t*)jl_new_typevar(u->var->name, vb->lb, vb->ub);
        return wrap_tvar_env(*new_tvar, constrained);
    }
    return wrap_tvar_env(*new_tvar, constrained);
}

static int subtype_unionall(jl_value_t *t, jl_unionall_t *u, jl_stenv_t *e, int8_t R, jl_param_pos_t param)
{
    u = unalias_unionall(u, e);
    jl_value_t *new_tvar = NULL;
    jl_varbinding_t vb = { NULL, NULL, NULL, R, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
                           e->invdepth, NULL, e->vars };
    JL_GC_PUSH5(&u, &vb.lb, &vb.ub, &vb.innervars, &new_tvar);
    if (jl_has_typevar(t, u->var))
        u = jl_rename_unionall(u);
    int body_occurs_inv = var_occurs_invariant(u->body, u->var);
    vb.var = u->var;
    vb.lb = u->var->lb;
    vb.ub = u->var->ub;
    vb.body_occurs_inv = body_occurs_inv;
    e->vars = &vb;
    int ans;
    if (R) {
        e->envidx++;
        ans = subtype(t, u->body, e, param);
        e->envidx--;
    }
    else {
        // ∀ path: a variable with a trivial lower bound, a union upper bound,
        // and only covariant occurrences in the body ranges over each arm of
        // its upper bound independently, i.e. the UnionAll distributes over
        // the arms:
        //   (Tuple{T,T} where T<:Union{A,B}) ==
        //       Union{Tuple{T,T} where T<:A, Tuple{T,T} where T<:B}
        // (diagonality, if any, is preserved: each value of the variable is
        // concrete and therefore lies entirely within a single arm).
        // Split the bound here by registering one ordinary left-union decision
        // per Union node, so that the enclosing ∀∃ loop enumerates all arms.
        if (!e->intersection && vb.lb == jl_bottom_type && jl_is_uniontype(vb.ub) &&
            !body_occurs_inv && var_occurs_covariant_only(u->body, u->var, 1))
            vb.ub = pick_union_element(vb.ub, e, 0);
        ans = subtype(u->body, t, e, param);
    }

    // handle the "diagonal dispatch" rule, which says that a type var occurring more
    // than once, and only in covariant position, is constrained to concrete types. E.g.
    //  ( Tuple{Int, Int}    <: Tuple{T, T} where T) but
    // !( Tuple{Int, String} <: Tuple{T, T} where T)
    // Then check concreteness by checking that the lower bound is not an abstract type.
    int diagonal = cov_count(&vb) > 1 && !vb.body_occurs_inv;
    // Widen Type{x} to typeof(x) for ordinary argument-slot occurrences and
    // diagonal constraints, but not invariant matches. This is only a local
    // view for checks and envout; keep `vb.lb` structurally precise.
    int widen_lb = !vb.occurs_inv && (diagonal || (vb.occurs_cov == 1 && vb.cov_diag == 0));
    jl_value_t *widened_lb = widen_lb ? widen_Type_if_concrete(vb.lb) : vb.lb;
    if (ans && (vb.concrete || (diagonal && is_leaf_typevar(u->var)))) {
        jl_value_t *concrete_lb = diagonal ? widened_lb : vb.lb;
        if (vb.concrete && !diagonal && !is_leaf_bound(vb.ub)) {
            // a non-diagonal var can only be a subtype of a diagonal var if its
            // upper bound is concrete.
            ans = 0;
        }
        else if (jl_is_typevar(vb.lb)) {
            jl_tvar_t *v = (jl_tvar_t*)vb.lb;
            jl_varbinding_t *vlb = lookup(e, v);
            if (vlb)
                vlb->concrete = 1;
        }
        else if (!is_leaf_bound(concrete_lb)) {
            ans = 0;
        }
    }
    e->vars = vb.prev;

    if (!ans) {
        JL_GC_POP();
        return 0;
    }

    // An internal `Intersect` meet node (see #61917) is exact for subtyping but
    // must not appear in a result type or static parameter (it is not a real
    // type). It only ever occurs as the top layer of `vb.ub`; over-approximate
    // it now, before `vb.ub` is used to build any result typevar below.
    vb.ub = widen_intersect(vb.ub);

    // If this variable was resolved to something concrete, just use that value for the
    // substitution below.
    if (vb.lb == vb.ub) {
        new_tvar = vb.lb;
    }

    // It is possible for bounds of outer existential vars to refer to universally qualified
    // inner vars. In this case, we should treat this variable as universally qualified over
    // the bounds at this point in future subtype queries. However, we need to do some work
    // to keep track that this situation happened to distinguish it from the case where
    // we have a free typevar in the input.
    jl_varbinding_t *outermost = NULL;
    for (jl_varbinding_t *btemp = vb.prev; btemp; btemp = btemp->prev)
        outermost = btemp;
    for (jl_varbinding_t *btemp = vb.prev; btemp; btemp = btemp->prev) {
        if (!btemp->existential)
            continue;

        // TODO: This takes significant time
        int ub_has_var = jl_has_typevar(btemp->ub, vb.var);
        int lb_has_var = jl_has_typevar(btemp->lb, vb.var);

        jl_tvar_t *old_tvar = vb.var;
        // Rooted by `u` in `vb`'s frame
        JL_GC_PROMISE_ROOTED(old_tvar);
        if (ub_has_var || lb_has_var) {
            if (btemp->depth0 != vb.depth0) {
                // If we've passed through an invariant constructor, the bounds of the outer var can never
                // be satisfied. Consider (ignoring normalization) Ref{T where T} <: Ref{S} where S. This ends
                // up as T<:S<:T. Since `T` is universally qualified over its bounds, this would require `S` to
                // take the full range. However, the `∃` qualifier needs a single value, so unless `T` is similarly
                // constrained, this is unsatisfiable.
                if (vb.lb != vb.ub) {
                    JL_GC_POP();
                    return 0;
                }
            }
            btemp->tainted_inner = 1;

            // We need to rename the typevar to prevent confusion. Ordinarily typevar identity conflicts
            // are taken care of by jl_rename_unionall, but of course if the tvar is not in the environment
            // anymore, that code path does not know that it needs to do any renaming.
            if (!new_tvar) {
                new_tvar = (jl_value_t*)jl_new_typevar(vb.var->name, vb.lb, vb.ub);
                if (outermost != NULL)
                    push_innervar(outermost, new_tvar);
            }
            if (ub_has_var)
                btemp->ub = jl_substitute_var(btemp->ub, old_tvar, (jl_value_t*)new_tvar);
            if (lb_has_var)
                btemp->lb = jl_substitute_var(btemp->lb, old_tvar, (jl_value_t*)new_tvar);
        }

        if (new_tvar && btemp->innervars != NULL) {
            jl_array_t *innervars = btemp->innervars;
            JL_GC_PUSH1(&innervars);
            for (size_t i = 0; i < jl_array_nrows(innervars); i++) {
                jl_tvar_t *ivar = (jl_tvar_t*)jl_array_ptr_ref(innervars, i);
                jl_value_t *lb = NULL;
                jl_value_t *ub = NULL;
                JL_GC_PUSH2(&lb, &ub);
                if (jl_has_typevar(ivar->lb, old_tvar)) {
                    lb = ivar->lb;
                    lb = jl_substitute_var(lb, old_tvar, (jl_value_t*)new_tvar);
                    ivar->lb = lb;
                    jl_gc_wb((jl_value_t*)ivar, lb);
                }
                if (jl_has_typevar(ivar->ub, old_tvar)) {
                    ub = ivar->ub;
                    ub = jl_substitute_var(ub, old_tvar, (jl_value_t*)new_tvar);
                    ivar->ub = ub;
                    jl_gc_wb((jl_value_t*)ivar, ub);
                }
                JL_GC_POP();
            }
            JL_GC_POP();
        }
    }

    // fill variable values into `envout` up to `envsz`
    if (R && ans && e->envidx < e->envsz) {
        jl_value_t *lb = widened_lb;
        int eff_constrained = (vb.occurs_inv || (cov_count(&vb) && u->var->lb == jl_bottom_type));
        jl_value_t *val = subtype_unionall_envout_value(t, u, e, &vb, lb, &new_tvar,
                                                        eff_constrained);
        jl_value_t *oldval = e->envout[e->envidx];
        // if we try to assign different variable values (due to checking
        // multiple union members), consider the value unknown. Use AND
        // semantics on the `constrained` flag across iterations: the var is
        // constrained only if every iteration (i.e., every LHS union branch)
        // pinned it.
        if (oldval && !jl_egal(oldval, val)) {
            int old_iter_constrained;
            if (jl_is_svec(oldval) && jl_svec_len((jl_svec_t*)oldval) == 2)
                old_iter_constrained = jl_svecref(oldval, 1) == jl_true;
            else
                old_iter_constrained = 1; // oldval is a concrete value: iter pinned var
            int new_iter_constrained;
            if (jl_is_svec(val) && jl_svec_len((jl_svec_t*)val) == 2)
                new_iter_constrained = jl_svecref(val, 1) == jl_true;
            else
                new_iter_constrained = 1;
            e->envout[e->envidx] = wrap_tvar_env((jl_value_t*)u->var,
                                                 old_iter_constrained && new_iter_constrained);
        }
        else
            e->envout[e->envidx] = val;
        // TODO: substitute the value (if any) of this variable into previous envout entries
    }

    JL_GC_POP();
    return ans;
}

// check n <: (length of vararg type v)
static int check_vararg_length(jl_value_t *v, ssize_t n, jl_stenv_t *e)
{
    jl_value_t *N = jl_unwrap_vararg_num(v);
    // only do the check if N is free in the tuple type's last parameter
    if (N) {
        jl_value_t *nn = jl_box_long(n);
        JL_GC_PUSH1(&nn);
        e->invdepth++;
        int ans = subtype(nn, N, e, PARAM_INVARIANT) && subtype(N, nn, e, PARAM_NONE);
        e->invdepth--;
        JL_GC_POP();
        if (!ans)
            return 0;
    }
    return 1;
}

static int forall_exists_equal(jl_value_t *x, jl_value_t *y, jl_stenv_t *e);

static int subtype_tuple_varargs(
    jl_vararg_t *vtx, jl_vararg_t *vty,
    jl_value_t *lastx, jl_value_t *lasty,
    size_t vx, size_t vy, size_t x_reps,
    jl_stenv_t *e, jl_param_pos_t param)
{
    jl_value_t *xp0 = jl_unwrap_vararg(vtx); jl_value_t *xp1 = jl_unwrap_vararg_num(vtx);
    jl_value_t *yp0 = jl_unwrap_vararg(vty); jl_value_t *yp1 = jl_unwrap_vararg_num(vty);

    jl_varbinding_t *xlv = NULL, *ylv = NULL;
    if (xp1 && jl_is_typevar(xp1))
        xlv = lookup(e, (jl_tvar_t*)xp1);
    if (yp1 && jl_is_typevar(yp1))
        ylv = lookup(e, (jl_tvar_t*)yp1);

    int8_t max_offsetx = xlv ? xlv->max_offset : 0;
    int8_t max_offsety = ylv ? ylv->max_offset : 0;

    jl_value_t *xl = xlv ? xlv->lb : xp1;
    jl_value_t *yl = ylv ? ylv->lb : yp1;

    if (!xp1) {
        // Unconstrained on the left, constrained on the right
        if (yl && jl_is_long(yl))
            return 0;
    }
    else {
        if (jl_is_long(xl)) {
            if (jl_unbox_long(xl) + 1 == vx) {
                // LHS is exhausted. We're a subtype if the RHS is either
                // exhausted as well or unbounded (in which case we need to
                // set it to 0).
                if (yl) {
                    if (jl_is_long(yl)) {
                        return jl_unbox_long(yl) + 1 == vy;
                    }
                } else {
                    // We can skip the subtype check, but we still
                    // need to make sure to constrain the length of y
                    // to 0.
                    goto constrain_length;
                }
            }
        }
    }
    {
        int x_same = vx > 1 || (lastx && obviously_egal(xp0, lastx));
        int y_same = vy > 1 || (lasty && obviously_egal(yp0, lasty));
        // keep track of number of consecutive identical subtyping
        x_reps = y_same && x_same ? x_reps + 1 : 1;
        if (x_reps > 2) {
            // an identical type on the left doesn't need to be compared to the same
            // element type on the right more than twice.
        }
        else if (x_same && e->Runions.depth == 0 && y_same &&
            !jl_has_free_typevars(xp0) && !jl_has_free_typevars(yp0)) {
            // fast path for repeated elements
        }
        else if ((e->Runions.depth == 0 ? !jl_has_free_typevars(xp0) : jl_is_concrete_type(xp0)) && !jl_has_free_typevars(yp0)) {
            // fast path for separable sub-formulas
            if (!jl_subtype(xp0, yp0))
                return 0;
        }
        else {
            // in Vararg{T1} <: Vararg{T2}, need to check subtype twice to
            // simulate the possibility of multiple arguments, which is needed
            // to implement the diagonal rule correctly.
            if (!subtype(xp0, yp0, e, param)) return 0;
            if (x_reps < 2 && !subtype(xp0, yp0, e, PARAM_COVARIANT)) return 0;
        }
    }
constrain_length:
    if (!yp1) {
        return 1;
    }
    if (!xp1) {
        jl_value_t *yl = yp1;
        jl_varbinding_t *ylv = NULL;
        if (jl_is_typevar(yl)) {
            ylv = lookup(e, (jl_tvar_t*)yl);
            if (ylv)
                yl = ylv->lb;
        }
        if (jl_is_long(yl)) {
            // The length of the x tuple is unconstrained, but the
            // length of the y tuple is now fixed (this could have happened
            // as a result of the subtype call above).
            return 0;
        }

        if (ylv) {
            if (ylv->depth0 != e->invdepth ||
                ylv->lb != jl_bottom_type ||
                ylv->ub != (jl_value_t *)jl_any_type)
                return 0;
            ylv->intvalued = 1;
        }
        // set lb to Any. Since `intvalued` is set, we'll interpret that
        // appropriately.
        e->invdepth++;
        int ans = subtype((jl_value_t*)jl_any_type, yp1, e, PARAM_INVARIANT);
        if (ylv && !ylv->intersected)
            ylv->max_offset = max_offsety;
        e->invdepth--;
        return ans;
    }

    // Vararg{T,N} <: Vararg{T2,N2}; equate N and N2
    e->invdepth++;
    JL_GC_PUSH2(&xp1, &yp1);
    int ans;
    jl_varbinding_t *bxp1 = jl_is_typevar(xp1) ? lookup(e, (jl_tvar_t *)xp1) : NULL;
    jl_varbinding_t *byp1 = jl_is_typevar(yp1) ? lookup(e, (jl_tvar_t *)yp1) : NULL;
    if (bxp1) {
        if (bxp1->intvalued == 0)
            bxp1->intvalued = 1;
        assert(bxp1->lb); // make static analyzer happy
        if (jl_is_long(bxp1->lb))
            xp1 = bxp1->lb;
    }
    if (byp1) {
        if (byp1->intvalued == 0)
            byp1->intvalued = 1;
        assert(byp1->lb); // make static analyzer happy
        if (jl_is_long(byp1->lb))
            yp1 = byp1->lb;
    }
    if (jl_is_long(xp1) && jl_is_long(yp1))
        ans = jl_unbox_long(xp1) - vx == jl_unbox_long(yp1) - vy;
    else {
        if (jl_is_long(xp1) && vx != vy) {
            xp1 = jl_box_long(jl_unbox_long(xp1) + vy - vx);
            vx = vy;
        }
        if (jl_is_long(yp1) && vy != vx) {
            yp1 = jl_box_long(jl_unbox_long(yp1) + vx - vy);
            vy = vx;
        }
        assert(e->Loffset == 0);
        e->Loffset = vx - vy;
        ans = forall_exists_equal(xp1, yp1, e);
        assert(e->Loffset == vx - vy);
        e->Loffset = 0;
    }
    JL_GC_POP();
    if (ylv && !ylv->intersected)
        ylv->max_offset = max_offsety;
    if (xlv && !xlv->intersected)
        xlv->max_offset = max_offsetx;
    e->invdepth--;
    return ans;
}

static int subtype_tuple_tail(jl_datatype_t *xd, jl_datatype_t *yd, int8_t R, jl_stenv_t *e, jl_param_pos_t param)
{
    size_t lx = jl_nparams(xd);
    size_t ly = jl_nparams(yd);
    size_t i = 0, j = 0, vx = 0, vy = 0, x_reps = 1;
    jl_value_t *lastx = NULL, *lasty = NULL;
    jl_value_t *xi = NULL, *yi = NULL;

    for (;;) {
        if (i < lx) {
            xi = jl_tparam(xd, i);
            if (i == lx-1 && (vx || jl_is_vararg(xi))) {
                vx += 1;
            }
        }

        if (j < ly) {
            yi = jl_tparam(yd, j);
            if (j == ly-1 && (vy || jl_is_vararg(yi))) {
                vy += 1;
            }
        }

        if (i >= lx)
            break;

        int all_varargs = vx && vy;
        if (!all_varargs && vy == 1) {
            if (jl_unwrap_vararg(yi) == (jl_value_t*)jl_any_type) {
                // Tuple{...} <: Tuple{..., Vararg{Any, _}}
                // fast path all the type checks away
                xi = jl_tparam(xd, lx-1);
                if (jl_is_vararg(xi)) {
                    all_varargs = 1;
                    // count up to lx-2 rather than lx-1.
                    vy += lx - i - 1;
                    vx = 1;
                } else {
                    break;
                }
            }
        }

        if (all_varargs) {
            // Tuple{..., Vararg{xi, _}} <: Tuple{..., Vararg{yi, _}}
            return subtype_tuple_varargs(
                (jl_vararg_t*)xi,
                (jl_vararg_t*)yi,
                lastx, lasty,
                vx, vy, x_reps, e, param);
        }

        if (j >= ly)
            return !!vx;

        xi = vx ? jl_unwrap_vararg(xi) : xi;
        yi = vy ? jl_unwrap_vararg(yi) : yi;
        int x_same = vx > 1 || (lastx && obviously_egal(xi, lastx));
        int y_same = vy > 1 || (lasty && obviously_egal(yi, lasty));
        // keep track of number of consecutive identical subtyping
        x_reps = y_same && x_same ? x_reps + 1 : 1;
        if (x_reps > 2) {
            // an identical type on the left doesn't need to be compared to the same
            // element type on the right more than twice.
        }
        else if (x_same && e->Runions.depth == 0 &&
            ((y_same && !jl_has_free_typevars(xi) && !jl_has_free_typevars(yi)) ||
             (yi == lastx && !vx && vy && jl_is_concrete_type(xi)))) {
            // fast path for repeated elements
        }
        else if ((e->Runions.depth == 0 ? !jl_has_free_typevars(xi) : jl_is_concrete_type(xi)) && !jl_has_free_typevars(yi)) {
            // fast path for separable sub-formulas
            int sub = jl_subtype(xi, yi);
            if (!sub)
                return 0;
        }
        else {
            int sub = subtype(xi, yi, e, param);
            if (!sub)
                return 0;
        }
        lastx = xi; lasty = yi;
        if (i < lx-1 || !vx)
            i++;
        if (j < ly-1 || !vy)
            j++;
    }

    if (vy && !vx && lx+1 >= ly) {
        // in Tuple{...,tn} <: Tuple{...,Vararg{T,N}}, check (lx+1-ly) <: N
        if (!check_vararg_length(yi, lx+1-ly, e))
            return 0;
    }
    assert((lx + vx == ly + vy) || (vy && (lx >= (vx ? ly : (ly-1)))));
    return 1;
}

static int subtype_tuple(jl_datatype_t *xd, jl_datatype_t *yd, jl_stenv_t *e, jl_param_pos_t param)
{
    // Check tuple compatibility based on tuple length only (fastpath)
    size_t lx = jl_nparams(xd);
    size_t ly = jl_nparams(yd);

    if (lx == 0 && ly == 0)
        return 1;

    jl_vararg_kind_t vvx = JL_VARARG_NONE;
    jl_vararg_kind_t vvy = JL_VARARG_NONE;
    jl_varbinding_t *xbb = NULL;
    jl_value_t *xva = NULL, *yva = NULL;
    if (lx > 0) {
        xva = jl_tparam(xd, lx-1);
        vvx = jl_vararg_kind(xva);
        if (vvx == JL_VARARG_BOUND)
            xbb = lookup(e, (jl_tvar_t *)jl_unwrap_vararg_num(xva));
    }
    if (ly > 0) {
        yva = jl_tparam(yd, ly-1);
        vvy = jl_vararg_kind(yva);
    }
    if (vvx != JL_VARARG_NONE && vvx != JL_VARARG_INT &&
        (!xbb || !jl_is_long(xbb->lb))) {
        if (vvx == JL_VARARG_UNBOUND || (xbb && !xbb->existential)) {
            // Unbounded on the LHS, bounded on the RHS
            if (vvy == JL_VARARG_NONE || vvy == JL_VARARG_INT)
                return 0;
            else if (lx < ly) // Unbounded includes N == 0
                return 0;
        }
        else if (vvy == JL_VARARG_NONE && !check_vararg_length(xva, ly+1-lx, e)) {
            return 0;
        }
    }
    else {
        size_t nx = lx;
        if (vvx == JL_VARARG_INT)
            nx += jl_vararg_length(xva) - 1;
        else if (xbb && jl_is_long(xbb->lb))
            nx += jl_unbox_long(xbb->lb) - 1;
        else
            assert(vvx == JL_VARARG_NONE);
        size_t ny = ly;
        if (vvy == JL_VARARG_INT)
            ny += jl_vararg_length(yva) - 1;
        else if (vvy != JL_VARARG_NONE)
            ny -= 1;
        if (vvy == JL_VARARG_NONE || vvy == JL_VARARG_INT) {
            if (nx != ny)
                return 0;
        }
        else {
            if (ny > nx)
                return 0;
        }
    }

    if (param == PARAM_NONE) param = PARAM_COVARIANT;
    int ans = subtype_tuple_tail(xd, yd, 0, e, param);
    return ans;
}

static int try_subtype_by_bounds(jl_value_t *a, jl_value_t *b, jl_stenv_t *e);

static int subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_param_pos_t param)
{
    if (jl_is_uniontype(x)) {
        if (obviously_egal(x, y))
            return 1;
        if (e->Runions.depth == 0 && jl_is_typevar(y) && !jl_has_free_typevars(x)) {
            // Similar to fast path for repeated elements: if there have been no outer
            // unions on the right, and the right side is a typevar, then we can handle the
            // typevar first before picking a union element, under the theory that it may
            // be easy to match or reject this whole union in comparing and setting the lb
            // and ub of the variable binding, without needing to examine each element.
            // However, if x contains any free typevars, then each element with a free
            // typevar must be handled separately from the union of all elements without
            // free typevars, since the typevars presence might lead to those elements
            // getting eliminated (omit_bad_union) or degenerate (Union{Ptr{T}, Ptr}) or
            // combined (Union{T, S} where {T, S <: T}).
            jl_tvar_t *yvar = (jl_tvar_t *)y;
            int yinner = 0;
            jl_varbinding_t *yb = lookup_binding(e, yvar, &yinner);
            while (e->intersection && yb != NULL && yb->lb == yb->ub && jl_is_typevar(yb->lb)) {
                yvar = (jl_tvar_t *)yb->lb;
                yb = lookup_binding(e, yvar, &yinner);
            }
            // Note: `x <: ∃y` performs a local ∀-∃ check between `x` and `yb->ub`.
            // We need to ensure that there's no ∃ typevar as otherwise that check
            // might cause false alarm due to the accumulated env change.
            if (yb == NULL || !yb->existential || !has_existential_typevar(yb->ub, e))
                return subtype_var(yvar, x, e, 1, param, yb, yinner);
        }
        x = pick_union_element(x, e, 0);
    }
    if (jl_is_uniontype(y)) {
        if (obviously_in_union(y, x))
            return 1;
        if (jl_is_unionall(x))
            return subtype_unionall(y, (jl_unionall_t*)x, e, 0, param);
        int ui = 1;
        if (jl_is_typevar(x)) {
            // The `convert(Type{T},T)` pattern, where T is a Union, required changing priority
            // of unions and vars: if matching `typevar <: union`, first try to match the whole
            // union against the variable before trying to take it apart to see if there are any
            // variables lurking inside.
            // note: for forall var, there's no need to split y if it has no free typevars.
            jl_varbinding_t *xx = lookup(e, (jl_tvar_t *)x);
            ui = ((xx && xx->existential) || jl_has_free_typevars(y)) && pick_union_decision(e, 1);
        }
        if (ui == 1)
            y = pick_union_element(y, e, 1);
    }
    // An internal `Intersect` meet node is only ever produced as an existential
    // upper bound, so it can appear on the right (`x <: a ∩ b`) but never on the
    // left. Handling the left case (`a ∩ b <: y`) precisely needs the
    // intersection machinery, so for now we assert it does not arise.
    assert(!jl_is_intersecttype(x));
    if (jl_is_intersecttype(y)) {
        // `x <: a ∩ b`  iff  `x <: a` and `x <: b` (dual to `Union` on the left).
        jl_intersecttype_t *iy = (jl_intersecttype_t*)y;
        return subtype(x, iy->a, e, param) && subtype(x, iy->b, e, param);
    }
    if (jl_is_typevar(x)) {
        if (jl_is_typevar(y)) {
            if (x == y) return 1;
            int xinner = 0, yinner = 0;
            jl_varbinding_t *xx = lookup_binding(e, (jl_tvar_t*)x, &xinner);
            jl_varbinding_t *yy = lookup_binding(e, (jl_tvar_t*)y, &yinner);
            int xfree_singleton = xx == NULL && !xinner;
            int yfree_singleton = yy == NULL && !yinner;
            if (xfree_singleton && yfree_singleton)
                return 0;
            jl_value_t *xub = xx ? xx->ub : xinner ? ((jl_tvar_t*)x)->ub : x;
            jl_value_t *ylb = yy ? yy->lb : yinner ? ((jl_tvar_t*)y)->lb : y;
            if (e->intersection) {
                jl_value_t *xlb = xx ? xx->lb : xinner ? ((jl_tvar_t*)x)->lb : x;
                jl_value_t *yub = yy ? yy->ub : yinner ? ((jl_tvar_t*)y)->ub : y;
                // find equivalence class for typevars during intersection
                if (xub != x && ((jl_is_typevar(xub) && xub == xlb) ||
                                  !jl_is_type(xub)))
                    return subtype(xub, y, e, param);
                if (yub != y && ((jl_is_typevar(yub) && yub == ylb) ||
                                  !jl_is_type(yub)))
                    return subtype(x, yub, e, param);
            }
            int xr = xx && xx->existential;  // treat free variables as "forall" (left)
            int yr = yy && yy->existential;
            if (xr) {
                if (yr) {
                    // TODO: Why is this sound?
                    if (e->intersection && try_subtype_by_bounds(xx->lb, yy->ub, e))
                        return 1;

                    // Both variables are existential. We need to annotate the constraint
                    // on the inner-most variable, so check which one that is.
                    if (var_outside(e, (jl_tvar_t*)x, (jl_tvar_t*)y)) {
                        record_var_occurrence(xx, e, param);
                        return var_gt((jl_tvar_t*)y, x, e, param, yy, yinner);
                    }
                }
                if (yy) record_var_occurrence(yy, e, param);
                return var_lt((jl_tvar_t*)x, y, e, param, xx, xinner);
            }
            else if (yr) {
                if (xx) {
                    record_var_occurrence(xx, e, param);
                    // This encodes the following:
                    //
                    // When we have `∀A ∃B, A <: B`, then the existence of
                    // `B` depends on every particular choice of `A`
                    // (in particular each choice of `A` may have a different
                    // choice of `B`. We encode this as `B->lb = A`.
                    //
                    // However, `∃B ∀A` is different: This requires a single `B`
                    // that works for all `A`. We encode this as `B->lb = A->ub`
                    // (note that A's ub cannot change during the course of the
                    // algorithm). Semantically, at each invariant depth, we push
                    // all universal quantifiers before all existential qualifiers,
                    // so asking which of these cases we're in is equivalent to
                    // asking whether `B`'s depth is greater than `A`'s depth.
                    if (yy && yy->depth0 < xx->depth0)
                        return var_gt((jl_tvar_t*)y, xx->ub, e, param, yy, yinner);
                }
                return var_gt((jl_tvar_t*)y, x, e, param, yy, yinner);
            }
            // check ∀x,y . x<:y
            // the bounds of left-side variables never change, and can only lead
            // to other left-side variables, so using || here is safe.
            if (xfree_singleton)
                return singleton_typevar_subtype((jl_tvar_t*)x, y);
            if (yfree_singleton)
                return subtype_singleton_typevar(xub, (jl_tvar_t*)y);
            return subtype(xub, y, e, param) || subtype(x, ylb, e, param);
        }
        int xinner = 0;
        jl_varbinding_t *xb = lookup_binding(e, (jl_tvar_t*)x, &xinner);
        if (jl_is_unionall(y)) {
            jl_value_t *xub = xb == NULL ? (xinner ? ((jl_tvar_t *)x)->ub : x) : xb->ub;
            if ((xb == NULL ? !xinner || !e->intersection : !xb->existential) && xub != y) {
                // We'd better unwrap `y::UnionAll` eagerly if `x` isa ∀-var.
                // This makes sure the following cases work correct:
                // 1) `∀T <: Union{∃S, SomeType{P}} where {P}`: `S == Any` ==> `S >: T`
                // 2) `∀T <: Union{∀T, SomeType{P}} where {P}`:
                // note: if xub == y we'd better try `subtype_var` as `subtype_left_var`
                // hit `==` based fast path.
                return subtype_unionall(x, (jl_unionall_t*)y, e, 1, param);
            }
        }
        return subtype_var((jl_tvar_t*)x, y, e, 0, param, xb, xinner);
    }
    if (jl_is_typevar(y)) {
        int yinner = 0;
        jl_varbinding_t *yb = lookup_binding(e, (jl_tvar_t*)y, &yinner);
        return subtype_var((jl_tvar_t*)y, x, e, 1, param, yb, yinner);
    }
    if (y == (jl_value_t*)jl_any_type && !jl_has_free_typevars(x))
        return 1;
    if (x == jl_bottom_type && !jl_has_free_typevars(y))
        return 1;
    jl_value_t *ux = jl_unwrap_unionall(x);
    jl_value_t *uy = jl_unwrap_unionall(y);
    if ((x != ux || y != uy) && y != (jl_value_t*)jl_any_type && jl_is_datatype(ux) && jl_is_datatype(uy) &&
        !jl_is_typeeq(ux)) {
        assert(ux);
        if (uy == (jl_value_t*)jl_any_type)
            return 1;
        jl_datatype_t *xd = (jl_datatype_t*)ux, *yd = (jl_datatype_t*)uy;
        while (xd != NULL && xd != jl_any_type && xd->name != yd->name) {
            xd = xd->super;
        }
        if (xd == jl_any_type)
            return 0;
    }
    // handle forall ("left") vars first
    if (jl_is_unionall(x)) {
        if (x == y && !(e->envidx < e->envsz))
            return 1;
        return subtype_unionall(y, (jl_unionall_t*)x, e, 0, param);
    }
    if (jl_is_unionall(y))
        return subtype_unionall(x, (jl_unionall_t*)y, e, 1, param);
    if (x == (jl_value_t*)jl_typeofbottom_type && jl_is_typeeq(y)) {
        jl_value_t *tp0 = jl_typeeq_T(y);
        e->invdepth++;
        int ans = forall_exists_equal(jl_bottom_type, tp0, e);
        e->invdepth--;
        return ans;
    }
    if (jl_is_typeeq(x) && jl_is_typeeq(y)) {
        e->invdepth++;
        int ans = forall_exists_equal(jl_typeeq_T(x), jl_typeeq_T(y), e);
        e->invdepth--;
        return ans;
    }
    if (jl_is_typeeq(x) && jl_is_datatype(y)) {
        jl_value_t *tp0 = jl_typeeq_T(x);
        if (!jl_is_typevar(tp0)) {
            // TypeEq(T) dispatches as the singleton type of T. For example,
            // TypeEq(Int) is a subtype of DataType, but not of TypeEq.
            return subtype(jl_typeof(tp0), y, e, param);
        }
        // `TypeEq(T)` for a free typevar `T` is the kind of all types matching
        // `T`'s bounds; every such instance is itself a type, i.e. a `Kind`. So
        // `Type{T} <: y` reduces to `Kind <: y` (in particular `Type === Kind`).
        return subtype((jl_value_t*)jl_anytype_type, y, e, param);
    }
    if (jl_is_datatype(x) && jl_is_typeeq(y) && x != (jl_value_t*)jl_typeofbottom_type) {
        jl_value_t *tp0 = jl_typeeq_T(y);
        if (jl_is_typevar(tp0)) {
            // kinds and `AnyType` are subtypes of `Type` but of no narrower `Type{T'}`,
            // and no `TypeEq` appears in their supertype chains to derive this from; so
            // answer as for `Type <: Type{T}`, at the depth where `Type{T}` occurs (the
            // depth of `x` doesn't matter: it doesn't contain the variable)
            if (!is_kind_or_anytype(x))
                return 0;
            return subtype((jl_value_t*)jl_type_type, y, e, param);
        }
        // `Type{Type{T}}` with an unbounded `T` denotes the same set as the bare
        // `TypeEq` (every `Type{X}` value), so a kind contained in `TypeEq` is a subtype
        if (jl_is_typeeq(tp0)) {
            jl_value_t *inner = jl_typeeq_T(tp0);
            if (jl_is_typevar(inner) && ((jl_tvar_t*)inner)->lb == jl_bottom_type &&
                    ((jl_tvar_t*)inner)->ub == (jl_value_t*)jl_any_type)
                return subtype(x, (jl_value_t*)jl_typeeq_type, e, param);
        }
        return 0;
    }
    if (jl_is_datatype(x) && jl_is_datatype(y)) {
        if (x == y) return 1;
        if (y == (jl_value_t*)jl_any_type) return 1;
        jl_datatype_t *xd = (jl_datatype_t*)x, *yd = (jl_datatype_t*)y;
        while (xd != jl_any_type && xd->name != yd->name) {
            if (xd->super == NULL) {
                assert(xd->parameters && jl_is_typename(xd->name));
                jl_errorf("circular type parameter constraint in definition of %s", jl_symbol_name(xd->name->name));
            }
            xd = xd->super;
        }
        if (xd == jl_any_type) return 0;
        if (xd->name == jl_tuple_typename)
            return subtype_tuple(xd, yd, e, param);
        size_t i, np = jl_nparams(xd);
        int ans = 1;
        e->invdepth++;
        for (i=0; i < np; i++) {
            jl_value_t *xi = jl_tparam(xd, i), *yi = jl_tparam(yd, i);
            if (!(xi == yi || forall_exists_equal(xi, yi, e))) {
                ans = 0; break;
            }
        }
        e->invdepth--;
        return ans;
    }
    if (jl_is_type(y))
        return x == jl_bottom_type;
    if (jl_is_long(x) && jl_is_long(y))
        return jl_unbox_long(x) == jl_unbox_long(y) + e->Loffset;
    return jl_egal(x, y);
}

static int is_indefinite_length_tuple_type(jl_value_t *x)
{
    x = jl_unwrap_unionall(x);
    if (!jl_is_tuple_type(x))
        return 0;
    size_t n = jl_nparams(x);
    return n > 0 && jl_vararg_kind(jl_tparam(x, n-1)) == JL_VARARG_UNBOUND;
}

static int is_definite_length_tuple_type(jl_value_t *x)
{
    if (jl_is_typevar(x))
        x = ((jl_tvar_t*)x)->ub;
    x = jl_unwrap_unionall(x);
    if (!jl_is_tuple_type(x))
        return 0;
    size_t n = jl_nparams(x);
    if (n == 0)
        return 1;
    jl_vararg_kind_t k = jl_vararg_kind(jl_tparam(x, n-1));
    return k == JL_VARARG_NONE || k == JL_VARARG_INT;
}

static int is_existential_typevar(jl_value_t *x, jl_stenv_t *e)
{
    if (!jl_is_typevar(x))
        return 0;
    jl_varbinding_t *vb = lookup(e, (jl_tvar_t *)x);
    return vb && vb->existential;
}

static int forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_param_pos_t param);

static int local_forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_param_pos_t param, int limit_slow)
{
    int16_t oldRmore = e->Runions.more;
    int sub;
    // fast-path for #49857
    if (obviously_in_union(y, x))
        return 1;
    int kindx = !jl_has_free_typevars(x);
    int kindy = !jl_has_free_typevars(y);
    if (kindx && kindy)
        return jl_subtype(x, y);
    int has_exists = (!kindx && has_existential_typevar(x, e)) ||
                     (!kindy && has_existential_typevar(y, e));
    if (!has_exists) {
        // We can use ∀_∃_subtype safely for ∃ free inputs.
        // This helps to save some bits in union stack.
        jl_saved_unionstate_t oldRunions; push_unionstate(&oldRunions, &e->Runions);
        e->Lunions.used = e->Runions.used = 0;
        e->Lunions.depth = e->Runions.depth = 0;
        e->Lunions.more = e->Runions.more = 0;
        sub = forall_exists_subtype(x, y, e, param);
        pop_unionstate(&e->Runions, &oldRunions);
        return sub;
    }
    if (is_existential_typevar(x, e) != is_existential_typevar(y, e)) {
        e->Lunions.used = 0;
        while (1) {
            e->Lunions.more = 0;
            e->Lunions.depth = 0;
            sub = subtype(x, y, e, param);
            if (!sub || !next_union_state(e, 0))
                break;
        }
        return sub;
    }
    if (limit_slow == -1)
        limit_slow = kindx || kindy;
    jl_savedenv_t se;
    save_env(e, &se, 1);
    int count, limited = 0, ini_count = 0;
    jl_saved_unionstate_t latestLunions = {0, 0, 0, NULL};
    while (1) {
        count = ini_count;
        if (ini_count == 0)
            e->Lunions.used = 0;
        else
            pop_unionstate(&e->Lunions, &latestLunions);
        while (1) {
            e->Lunions.more = 0;
            e->Lunions.depth = 0;
            if (count < 4) count++;
            sub = subtype(x, y, e, param);
            if (limit_slow && count == 4)
                limited = 1;
            if (!sub || !next_union_state(e, 0))
                break;
            if (limited || e->Runions.more == oldRmore) {
                // re-save env and freeze the ∃decision for previous ∀Union
                ini_count = count;
                push_unionstate(&latestLunions, &e->Lunions);
                re_save_env(e, &se, 1);
                e->Runions.more = oldRmore;
            }
        }
        if (sub || e->Runions.more == oldRmore)
            break;
        assert(e->Runions.more > oldRmore);
        next_union_state(e, 1);
        restore_env(e, &se, 1); // also restore Rdepth here
        e->Runions.more = oldRmore;
    }
    if (!sub)
        assert(e->Runions.more == oldRmore);
    else if (e->Runions.more > oldRmore && (limited || env_unchanged(e, &se)))
        // Ignore the rest ∃Union decisions if env is unchanged/limited.
        // As otherwise it might cause combinatorial explosion without making any difference to the result.
        e->Runions.more = oldRmore;
    free_env(&se);
    return sub;
}

static int equal_var(jl_tvar_t *v, jl_value_t *x, jl_stenv_t *e)
{
    assert(e->Loffset == 0);
    // Theoretically bounds change would be merged for union inputs.
    // But intersection is not happy as splitting helps to avoid circular env.
    assert(!e->intersection || !jl_is_uniontype(x));
    int innervar = 0;
    jl_varbinding_t *vb = lookup_binding(e, v, &innervar);
    if (e->intersection && vb != NULL && vb->lb == vb->ub && jl_is_typevar(vb->lb))
        return equal_var((jl_tvar_t *)vb->lb, x, e);
    record_var_occurrence(vb, e, PARAM_INVARIANT);
    if (vb == NULL) {
        if (innervar && e->intersection)
            return 1;
        if (innervar)
            return local_forall_exists_subtype(x, v->lb, e, PARAM_INVARIANT, !jl_has_free_typevars(x)) &&
                   local_forall_exists_subtype(v->ub, x, e, PARAM_NONE, 0);
        return x == (jl_value_t*)v;
    }
    if (!vb->existential)
        return local_forall_exists_subtype(x, vb->lb, e, PARAM_INVARIANT, !jl_has_free_typevars(x)) &&
               local_forall_exists_subtype(vb->ub, x, e, PARAM_NONE, 0);
    if (vb->lb == x)
        return var_lt(v, x, e, PARAM_NONE, vb, innervar);
    if (!subtype_ccheck(x, vb->ub, e))
        return 0;
    jl_value_t *lb = simple_join(vb->lb, x);
    JL_GC_PUSH1(&lb);
    if (!e->intersection || !jl_is_typevar(lb) || !reachable_var(lb, v, e))
        vb->lb = lb;
    JL_GC_POP();
    if (vb->ub == x)
        return 1;
    if (!subtype_ccheck(vb->lb, x, e))
        return 0;
    // skip `simple_meet` here as we have proven `x <: vb->ub`
    if (!e->intersection || !reachable_var(x, v, e))
        vb->ub = x;
    return 1;
}

static int forall_exists_equal(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
{
    if (obviously_egal(x, y)) return 1;

    if ((is_indefinite_length_tuple_type(x) && is_definite_length_tuple_type(y)) ||
        (is_definite_length_tuple_type(x) && is_indefinite_length_tuple_type(y)))
        return 0;

    if (jl_is_datatype(x) && jl_is_datatype(y)) {
        // Fastpath for nested constructor. Skip the unneeded `>:` check.
        // Note: since there is no changes to the environment or union stack implied by `x` or `y`, this will simply forward to calling
        // `forall_exists_equal(xi, yi, e)` on each parameter `(xi, yi)` of `(x, y)`,
        // which means this subtype call will give the same result for `subtype(x, y)` and `subtype(y, x)`.
        jl_datatype_t *xd = (jl_datatype_t*)x, *yd = (jl_datatype_t*)y;
        if (xd->name != yd->name)
            return 0;
        if (xd->name != jl_tuple_typename)
            return subtype(x, y, e, PARAM_INVARIANT);
    }

    if ((jl_is_uniontype(x) && jl_is_uniontype(y))) {
        // For 2 unions, first try a more efficient greedy algorithm that compares the unions
        // componentwise. If failed, `exists_subtype` would memorize that this branch should be skipped.
        // Note: this is valid because the normal path checks `>:` locally.
        if (pick_union_decision(e, 1) == 0) {
            return forall_exists_equal(((jl_uniontype_t *)x)->a, ((jl_uniontype_t *)y)->a, e) &&
                   forall_exists_equal(((jl_uniontype_t *)x)->b, ((jl_uniontype_t *)y)->b, e);
        }
    }

    if (e->Loffset == 0 && jl_is_typevar(y) && jl_is_type(x) && (!e->intersection || !jl_is_uniontype(x))) {
        // Fastpath for Type == TypeVar.
        // Avoid duplicated `<:` check between adjacent `var_gt` and `var_lt`
        return equal_var((jl_tvar_t *)y, x, e);
    }

    jl_saved_unionstate_t oldLunions; push_unionstate(&oldLunions, &e->Lunions);

    int sub = local_forall_exists_subtype(x, y, e, PARAM_INVARIANT, -1);
    if (sub) {
        flip_offset(e);
        sub = local_forall_exists_subtype(y, x, e, PARAM_NONE, 0);
        flip_offset(e);
    }
    pop_unionstate(&e->Lunions, &oldLunions);
    return sub;
}

static int exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_savedenv_t *se, jl_param_pos_t param)
{
    e->Runions.used = 0;
    while (1) {
        e->Runions.depth = 0;
        e->Runions.more = 0;
        e->Lunions.depth = 0;
        e->Lunions.more = 0;
        if (subtype(x, y, e, param))
            return 1;
        if (next_union_state(e, 1)) {
            // We preserve `envout` here as `subtype_unionall` needs previous assigned env values.
            int oldidx = e->envidx;
            e->envidx = e->envsz;
            restore_env(e, se, 1);
            e->envidx = oldidx;
        }
        else {
            restore_env(e, se, 1);
            return 0;
        }
    }
}

static int forall_exists_subtype(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_param_pos_t param)
{
    // The depth recursion has the following shape, after simplification:
    // ∀₁
    //   ∃₁
    assert(e->Runions.depth == 0);
    assert(e->Lunions.depth == 0);
    jl_savedenv_t se;
    save_env(e, &se, 1);

    e->Lunions.used = 0;
    int sub;
    while (1) {
        sub = exists_subtype(x, y, e, &se, param);
        if (!sub || !next_union_state(e, 0))
            break;
        re_save_env(e, &se, 1);
    }

    free_env(&se);
    return sub;
}

static void init_stenv(jl_stenv_t *e, jl_value_t **env, int envsz)
{
    e->vars = NULL;
    e->envsz = envsz;
    e->envout = env;
    if (envsz) {
        assert(env != NULL);
        memset(env, 0, envsz*sizeof(void*));
    }
    e->envidx = 0;
    e->invdepth = 0;
    e->intersection = 0;
    e->emptiness_only = 0;
    e->triangular = 0;
    e->Loffset = 0;
    e->Lunions.depth = 0;      e->Runions.depth = 0;
    e->Lunions.more = 0;       e->Runions.more = 0;
    e->Lunions.used = 0;       e->Runions.used = 0;
    e->Lunions.stack.next = NULL;
    e->Runions.stack.next = NULL;
}

// subtyping entry points

JL_DLLEXPORT int jl_subtype_env_size(jl_value_t *t)
{
    int sz = 0;
    while (jl_is_unionall(t)) {
        sz++;
        t = ((jl_unionall_t*)t)->body;
    }
    return sz;
}

// compute the minimum bound on the number of concrete types that are subtypes of `t`
// returns 0, 1, or many (2+)
static int concrete_min(jl_value_t *t)
{
    if (jl_is_unionall(t))
        t = jl_unwrap_unionall(t);
    if (t == (jl_value_t*)jl_bottom_type)
        return 1;
    if (jl_is_typeeq(t))
        return 0; // Type{T} may have the concrete supertype `typeof(T)`, so don't try to handle them here
    if (jl_is_datatype(t)) {
        return jl_is_concrete_type(t) ? 1 : 2;
    }
    if (jl_is_vararg(t))
        return 0;
    if (jl_is_typevar(t))
        return 0; // could be 0 or more, since we didn't track if it was unbound
    if (jl_is_uniontype(t)) {
        int count = concrete_min(((jl_uniontype_t*)t)->a);
        if (count > 1)
            return count;
        return count + concrete_min(((jl_uniontype_t*)t)->b);
    }
    assert(!jl_is_kind(t));
    return 1; // a non-Type is also considered concrete
}

static jl_value_t *find_var_body(jl_value_t *t, jl_tvar_t *v) JL_NOTSAFEPOINT
{
    if (jl_is_unionall(t)) {
        if (((jl_unionall_t*)t)->var == v)
            return ((jl_unionall_t*)t)->body;
        jl_value_t *b = find_var_body(((jl_unionall_t*)t)->var->lb, v);
        if (b) return b;
        b = find_var_body(((jl_unionall_t*)t)->var->ub, v);
        if (b) return b;
        return find_var_body(((jl_unionall_t*)t)->body, v);
    }
    else if (jl_is_uniontype(t)) {
        jl_value_t *b = find_var_body(((jl_uniontype_t*)t)->a, v);
        if (b) return b;
        return find_var_body(((jl_uniontype_t*)t)->b, v);
    }
    else if (jl_is_vararg(t)) {
        jl_vararg_t *vm = (jl_vararg_t *)t;
        if (vm->T) {
            jl_value_t *b = find_var_body(vm->T, v);
            if (b) return b;
            if (vm->N) {
                return find_var_body(vm->N, v);
            }
        }
    }
    else if (jl_is_datatype(t)) {
        size_t i;
        for (i=0; i < jl_nparams(t); i++) {
            jl_value_t *b = find_var_body(jl_tparam(t, i), v);
            if (b)
                return b;
        }
    }
    return NULL;
}

// quickly compute if x seems like a possible subtype of y
// especially optimized for x isa concrete type
// returns true if it could be easily determined, with the result in subtype
// the approximation widens typevar bounds under the assumption they are bound
// in the immediate caller--the caller must be conservative in handling the result
static int obvious_subtype(jl_value_t *x, jl_value_t *y, jl_value_t *y0, int *subtype)
{
    if (x == y || y == (jl_value_t*)jl_any_type) {
        *subtype = 1;
        return 1;
    }
    while (jl_is_unionall(x)) {
        if (!jl_is_unionall(y)) {
            if (obvious_subtype(jl_unwrap_unionall(x), y, y0, subtype) && !*subtype)
                return 1;
            return 0;
        }
        x = ((jl_unionall_t*)x)->body;
        y = ((jl_unionall_t*)y)->body;
    }
    if (jl_is_unionall(y))
        y = jl_unwrap_unionall(y);
    if (is_typeofbottom_typealias(x))
        x = (jl_value_t*)jl_typeofbottom_type;
    if (is_typeofbottom_typealias(y))
        y = (jl_value_t*)jl_typeofbottom_type;
    if (x == y || y == (jl_value_t*)jl_any_type) {
        *subtype = 1;
        return 1;
    }
    if (jl_is_typevar(x)) {
        return 0;
    }
    if (jl_is_typevar(y)) {
        return 0;
    }
    if (x == (jl_value_t*)jl_bottom_type) {
        *subtype = 1;
        return 1;
    }
    if (y == (jl_value_t*)jl_bottom_type) {
        *subtype = 0;
        return 1;
    }
    if (jl_is_vararg(x)) {
        if (!jl_is_vararg(y)) {
            *subtype = 0;
            return 1;
        }
        return 0;
    }
    // `Intersect` is an internal meet node, not a real type tag. Handle it
    // before the non-type fallback, which would otherwise treat it as egal-only.
    if (jl_is_intersecttype(y)) {
        jl_intersecttype_t *iy = (jl_intersecttype_t*)y;
        int sub_a, sub_b;
        int known_a = obvious_subtype(x, iy->a, y0, &sub_a);
        if (known_a && !sub_a) {
            *subtype = 0;
            return 1;
        }
        int known_b = obvious_subtype(x, iy->b, y0, &sub_b);
        if (known_b && !sub_b) {
            *subtype = 0;
            return 1;
        }
        if (known_a && sub_a && known_b && sub_b) {
            *subtype = 1;
            return 1;
        }
        return 0;
    }
    if (jl_is_intersecttype(x))
        return 0;
    if (!jl_is_type(x) || !jl_is_type(y)) {
        *subtype = jl_egal(x, y);
        return 1;
    }
    if (jl_is_uniontype(x)) {
        // TODO: consider handling more LHS unions, being wary of covariance
        jl_value_t *xa = ((jl_uniontype_t*)x)->a;
        jl_value_t *xb = ((jl_uniontype_t*)x)->b;
        if (obvious_subtype(xa, y, y0, subtype) && *subtype) {
            if (obvious_subtype(xb, y, y0, subtype) && *subtype)
                return 1;
        }
        //if (obvious_subtype(((jl_uniontype_t*)x)->a, y, y0, subtype)) {
        //    if (!*subtype)
        //        return 1;
        //    if (obvious_subtype(((jl_uniontype_t*)x)->b, y, y0, subtype))
        //        return 1;
        //}
        //else if (obvious_subtype(((jl_uniontype_t*)x)->b, y, y0, subtype)) {
        //    if (!*subtype)
        //        return 1;
        //}
        return 0;
    }
    if (jl_is_uniontype(y)) {
        jl_value_t *ya = ((jl_uniontype_t*)y)->a;
        jl_value_t *yb = ((jl_uniontype_t*)y)->b;
        if (obvious_subtype(x, ya, y0, subtype)) {
            if (*subtype)
                return 1;
            if (obvious_subtype(x, yb, y0, subtype))
                return 1;
        }
        else if (obvious_subtype(x, yb, y0, subtype)) {
            if (*subtype)
                return 1;
        }
        return 0;
    }
    if (x == (jl_value_t*)jl_any_type) {
        *subtype = 0;
        return 1;
    }
    // `Type{T}` is a `TypeEq`, not a `DataType`, so the `jl_is_datatype` cases
    // below miss it; decide the obvious `X <: Type{T}` rejections here.
    if (jl_is_typeeq(y) && !jl_is_typeeq(x) && jl_is_datatype(x) &&
            x != (jl_value_t*)jl_typeofbottom_type) {
        jl_value_t *t0 = jl_typeeq_T(y);
        if (jl_is_typevar(t0)) {
            if (!is_kind_or_anytype(x)) {
                *subtype = 0;    // an ordinary type value is never a subtype of `Type{T}`
                return 1;
            }
            return 0;            // a kind may be: `Type <: Type{T}` is handled by `subtype`
        }
        if (!jl_is_typeeq(t0)) {
            *subtype = 0;        // `X <: Type{ConcreteType}` (X not a `Type{}`) is never true
            return 1;
        }
        // `Type{Type{...}}`: leave to `subtype`
    }
    if (jl_is_datatype(y)) {
        int istuple = (((jl_datatype_t*)y)->name == jl_tuple_typename);
        int iscov = istuple;
        // TODO: this would be a nice fast-path to have, unfortunately,
        //       datatype allocation fails to correctly hash-cons them
        //       and the subtyping tests include tests for this case
        //if (!iscov && ((jl_datatype_t*)y)->isconcretetype && !jl_is_typeeq(x)) {
        //    *subtype = 0;
        //    return 1;
        //}
        if (jl_is_datatype(x)) {
            // Weaker version of above, but runs into the same problem
            //if (((jl_datatype_t*)x)->isconcretetype && ((jl_datatype_t*)y)->isconcretetype && (!istuple || !istuple_x)) {
            //    *subtype = 0;
            //    return 1;
            //}
            int uncertain = 0;
            if (((jl_datatype_t*)x)->name != ((jl_datatype_t*)y)->name) {
                jl_datatype_t *temp = (jl_datatype_t*)x;
                while (temp->name != ((jl_datatype_t*)y)->name) {
                    temp = temp->super;
                    if (temp == NULL) // invalid state during type declaration
                        return 0;
                    if (temp == jl_any_type) {
                        *subtype = 0;
                        return 1;
                    }
                }
                if (obvious_subtype((jl_value_t*)temp, y, y0, subtype) && *subtype)
                    return 1;
                return 0;
            }
            if (!iscov && !((jl_datatype_t*)x)->hasfreetypevars) {
                // by transitivity, if `wrapper <: y`, then `x <: y` if x is a leaf type of its name
                jl_value_t *wrapper = ((jl_datatype_t*)x)->name->wrapper;
                int wrapper_sub = 0;
                JL_GC_PUSH1(&wrapper);
                wrapper_sub = obvious_subtype(wrapper, y, y0, subtype);
                JL_GC_POP();
                if (wrapper_sub && *subtype)
                    return 1;
            }
            int i, npx = jl_nparams(x), npy = jl_nparams(y);
            jl_vararg_kind_t vx = JL_VARARG_NONE;
            jl_vararg_kind_t vy = JL_VARARG_NONE;
            jl_value_t *vxt = NULL;
            int nparams_expanded_x = npx;
            int nparams_expanded_y = npy;
            if (istuple) {
                if (npx > 0) {
                    jl_value_t *xva = jl_tparam(x, npx - 1);
                    vx = jl_vararg_kind(xva);
                    if (vx != JL_VARARG_NONE) {
                        vxt = jl_unwrap_vararg(xva);
                        nparams_expanded_x -= 1;
                        if (vx == JL_VARARG_INT)
                            nparams_expanded_x += jl_vararg_length(xva);
                    }
                }
                if (npy > 0) {
                    jl_value_t *yva = jl_tparam(y, npy - 1);
                    vy = jl_vararg_kind(yva);
                    if (vy != JL_VARARG_NONE) {
                        nparams_expanded_y -= 1;
                        if (vy == JL_VARARG_INT)
                            nparams_expanded_y += jl_vararg_length(yva);
                    }
                }
                // if the nparams aren't equal, or at least one of them is a typevar (uncertain), they may be obviously disjoint
                if (nparams_expanded_x != nparams_expanded_y || (vx != JL_VARARG_NONE && vx != JL_VARARG_INT) || (vy != JL_VARARG_NONE && vy != JL_VARARG_INT)) {
                    // we have a stronger bound on x if:
                    if (vy == JL_VARARG_NONE || vy == JL_VARARG_INT) { // the bound on y is certain
                        if (vx == JL_VARARG_NONE || vx == JL_VARARG_INT || vx == JL_VARARG_UNBOUND || // and the bound on x is also certain
                            nparams_expanded_x > nparams_expanded_y || npx > nparams_expanded_y) { // or x is unknown, but definitely longer than y
                            *subtype = 0;
                            return 1; // number of fixed parameters in x are more than declared in y
                        }
                    }
                    if (nparams_expanded_x < nparams_expanded_y) {
                        *subtype = 0;
                        return 1; // number of fixed parameters in x could be fewer than in y
                    }
                    uncertain = 1;
                }
            }
            else if (npx != npy) {
                *subtype = 0;
                return 1;
            }

            // inspect the fixed parameters in y against x
            for (i = 0; i < npy - (vy == JL_VARARG_NONE ? 0 : 1); i++) {
                jl_value_t *a;
                if (i >= (npx - (vx == JL_VARARG_NONE ? 0 : 1))) {
                    a = vxt;
                    assert(a != NULL);
                }
                else {
                    a = jl_tparam(x, i);
                }
                jl_value_t *b = jl_tparam(y, i);
                if (iscov || jl_is_typevar(b)) {
                    if (obvious_subtype(a, b, y0, subtype)) {
                        if (!*subtype)
                            return 1;
                        if (jl_has_free_typevars(b)) // b is actually more constrained that this
                            uncertain = 1;
                    }
                    else {
                        uncertain = 1;
                    }
                }
                else {
                    if (!obviously_egal(a, b)) {
                        if (obvious_subtype(a, b, y0, subtype)) {
                            if (!*subtype)
                                return 1;
                            if (jl_has_free_typevars(b)) // b is actually more constrained that this
                                uncertain = 1;
                        }
                        else {
                            uncertain = 1;
                        }
                        if (!jl_has_free_typevars(b) && obvious_subtype(b, a, y0, subtype)) {
                            if (!*subtype)
                                return 1;
                            if (jl_has_free_typevars(a)) // a is actually more constrained that this
                                uncertain = 1;
                        }
                        else {
                            uncertain = 1;
                        }
                    }
                }
            }
            if (i < nparams_expanded_x) {
                // there are elements left in x (possibly just a Vararg), check them against the Vararg tail of y too
                assert(vy != JL_VARARG_NONE && istuple && iscov);
                jl_value_t *a1 = (vx != JL_VARARG_NONE && i >= npx - 1) ? vxt : jl_tparam(x, i);
                jl_value_t *b = jl_unwrap_vararg(jl_tparam(y, i));
                if (jl_is_typevar(b)) {
                    jl_value_t *body = find_var_body(y0, (jl_tvar_t*)b);
                    if (body == NULL)
                        body = y0;
                    if (var_occurs_invariant(body, (jl_tvar_t*)b))
                        return 0;
                }
                if (nparams_expanded_x > npy && jl_is_typevar(b) && is_leaf_typevar((jl_tvar_t *)b) && concrete_min(a1) > 1) {
                    // diagonal rule for 2 or more elements: they must all be concrete on the LHS
                    *subtype = 0;
                    return 1;
                }
                jl_value_t *a1u = jl_unwrap_unionall(a1);
                if (jl_is_typeeq(a1u) && jl_is_type(jl_typeeq_T(a1u))) {
                    a1 = jl_typeof(jl_typeeq_T(a1u));
                }
                for (; i < nparams_expanded_x; i++) {
                    jl_value_t *a = (vx != JL_VARARG_NONE && i >= npx - 1) ? vxt : jl_tparam(x, i);
                    if (i > npy && jl_is_typevar(b) && is_leaf_typevar((jl_tvar_t *)b)) { // i == npy implies a == a1
                        // diagonal rule: all the later parameters are also constrained to be type-equal to the first
                        jl_value_t *a2 = a;
                        jl_value_t *au = jl_unwrap_unionall(a);
                        if (jl_is_typeeq(au) && jl_is_type(jl_typeeq_T(au))) {
                            // if a is exactly Type{T}, then use the concrete typeof(T) instead here
                            a2 = jl_typeof(jl_typeeq_T(au));
                        }
                        if (!obviously_egal(a1, a2)) {
                            if (obvious_subtype(a2, a1, y0, subtype)) {
                                if (!*subtype)
                                    return 1;
                                if (jl_has_free_typevars(a1)) // a1 is actually more constrained that this
                                    uncertain = 1;
                            }
                            else {
                                uncertain = 1;
                            }
                            if (obvious_subtype(a1, a2, y0, subtype)) {
                                if (!*subtype)
                                    return 1;
                                if (jl_has_free_typevars(a2)) // a2 is actually more constrained that this
                                    uncertain = 1;
                            }
                            else {
                                uncertain = 1;
                            }
                        }
                    }
                    if (obvious_subtype(a, b, y0, subtype)) {
                        if (!*subtype)
                            return 1;
                        if (jl_has_free_typevars(b)) // b is actually more constrained that this
                            uncertain = 1;
                    }
                    else {
                        uncertain = 1;
                    }
                }
            }
            if (uncertain)
                return 0;
            *subtype = 1;
            return 1;
        }
    }
    return 0;
}

JL_DLLEXPORT int jl_obvious_subtype(jl_value_t *x, jl_value_t *y, int *subtype)
{
    return obvious_subtype(x, y, y, subtype);
}

// `env` is NULL if no typevar information is requested, or otherwise
// points to a rooted array of length `jl_subtype_env_size(y)`.
// This will be populated with the values of variables from unionall
// types at the outer level of `y`.
JL_DLLEXPORT int jl_subtype_env(jl_value_t *x, jl_value_t *y, jl_value_t **env, int envsz)
{
    jl_stenv_t e;
    if (y == (jl_value_t*)jl_any_type || x == jl_bottom_type)
        return 1;
    if (x == y ||
        (jl_typeof(x) == jl_typeof(y) &&
         (jl_is_unionall(y) || jl_is_uniontype(y) || jl_is_typeeq(y)) &&
         jl_types_egal(x, y))) {
        if (envsz != 0) { // quickly copy env from x
            jl_unionall_t *ua = (jl_unionall_t*)x;
            int i;
            for (i = 0; i < envsz; i++) {
                assert(jl_is_unionall(ua));
                int constrained = constrains_param_static(ua->var, ua->body, 1);
                env[i] = wrap_tvar_env((jl_value_t*)ua->var, constrained);
                ua = (jl_unionall_t*)ua->body;
            }
        }
        return 1;
    }
    if (jl_is_typeapp(x) || jl_is_typeapp(y))
        jl_error("internal error: TypeApp in subtyping");
    int obvious_subtype = 2;
    if (jl_obvious_subtype(x, y, &obvious_subtype)) {
#ifdef NDEBUG
        if (obvious_subtype == 0)
            return obvious_subtype;
        else if (envsz == 0)
            return obvious_subtype;
#endif
    }
    else {
        obvious_subtype = 3;
    }
    init_stenv(&e, env, envsz);
    int subtype = forall_exists_subtype(x, y, &e, PARAM_NONE);
    free_stenv(&e);
    assert(obvious_subtype == 3 || obvious_subtype == subtype || jl_has_free_typevars(x) || jl_has_free_typevars(y));
#ifndef NDEBUG
    if (obvious_subtype == 0 || (obvious_subtype == 1 && envsz == 0))
        subtype = obvious_subtype; // this ensures that running in a debugger doesn't change the result
#endif
    return subtype;
}

static int subtype_in_env(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
{
    jl_stenv_t e2;
    init_stenv(&e2, NULL, 0);
    e2.vars = e->vars;
    e2.intersection = e->intersection;
    e2.invdepth = e->invdepth;
    e2.envsz = e->envsz;
    e2.envout = e->envout;
    e2.envidx = e->envidx;
    e2.Loffset = e->Loffset;
    return forall_exists_subtype(x, y, &e2, PARAM_NONE);
}

JL_DLLEXPORT int jl_subtype(jl_value_t *x, jl_value_t *y)
{
    return jl_subtype_env(x, y, NULL, 0);
}

JL_DLLEXPORT int jl_types_equal(jl_value_t *a, jl_value_t *b)
{
    if (a == b)
        return 1;
    if (jl_typeof(a) == jl_typeof(b) && jl_types_egal(a, b))
        return 1;
    if (obviously_unequal(a, b))
        return 0;
    // the following is an interleaved version of:
    //   return jl_subtype(a, b) && jl_subtype(b, a)
    // where we try to do the fast checks before the expensive ones
    if (jl_is_datatype(a) && !jl_is_concrete_type(b)) {
        // if one type looks simpler, check it on the right
        // first in order to reject more quickly.
        jl_value_t *temp = a;
        a = b;
        b = temp;
    }
    // first check if a <: b has an obvious answer
    int subtype_ab = 2;
    if (b == (jl_value_t*)jl_any_type || a == jl_bottom_type) {
        subtype_ab = 1;
    }
    else if (jl_obvious_subtype(a, b, &subtype_ab)) {
#ifdef NDEBUG
        if (subtype_ab == 0)
            return 0;
#endif
    }
    else {
        subtype_ab = 3;
    }
    // next check if b <: a has an obvious answer
    int subtype_ba = 2;
    if (a == (jl_value_t*)jl_any_type || b == jl_bottom_type) {
        subtype_ba = 1;
    }
    else if (jl_obvious_subtype(b, a, &subtype_ba)) {
#ifdef NDEBUG
        if (subtype_ba == 0)
            return 0;
#endif
    }
    else {
        subtype_ba = 3;
    }
    // finally, do full subtyping for any inconclusive test
    jl_stenv_t e;
#ifdef NDEBUG
    if (subtype_ab != 1)
#endif
    {
        init_stenv(&e, NULL, 0);
        int subtype = forall_exists_subtype(a, b, &e, PARAM_NONE);
        free_stenv(&e);
        assert(subtype_ab == 3 || subtype_ab == subtype || jl_has_free_typevars(a) || jl_has_free_typevars(b));
#ifndef NDEBUG
        if (subtype_ab != 0 && subtype_ab != 1) // ensures that running in a debugger doesn't change the result
#endif
        subtype_ab = subtype;
#ifdef NDEBUG
        if (subtype_ab == 0)
            return 0;
#endif
    }
#ifdef NDEBUG
    if (subtype_ba != 1)
#endif
    {
        init_stenv(&e, NULL, 0);
        int subtype = forall_exists_subtype(b, a, &e, PARAM_NONE);
        free_stenv(&e);
        assert(subtype_ba == 3 || subtype_ba == subtype || jl_has_free_typevars(a) || jl_has_free_typevars(b));
#ifndef NDEBUG
        if (subtype_ba != 0 && subtype_ba != 1) // ensures that running in a debugger doesn't change the result
#endif
        subtype_ba = subtype;
    }
    // all tests successful
    return subtype_ab && subtype_ba;
}

JL_DLLEXPORT int jl_is_not_broken_subtype(jl_value_t *a, jl_value_t *b)
{
    // TODO: the final commented out check here isn't correct; it should be closer to the
    // `issingletype` check used by `isnotbrokensubtype` in `base/compiler/typeutils.jl`
    return !jl_is_kind(b) || !jl_is_typeeq(a); // || jl_is_datatype_singleton((jl_datatype_t*)jl_tparam0(a));
}

int jl_tuple1_isa(jl_value_t *child1, jl_value_t **child, size_t cl, jl_datatype_t *pdt)
{
    if (jl_is_tuple_type(pdt) && !jl_is_va_tuple(pdt)) {
        if (cl != jl_nparams(pdt))
            return 0;
        size_t i;
        if (!jl_isa(child1, jl_tparam(pdt, 0)))
            return 0;
        for (i = 1; i < cl; i++) {
            if (!jl_isa(child[i - 1], jl_tparam(pdt, i)))
                return 0;
        }
        return 1;
    }
    jl_value_t *tu = (jl_value_t*)arg_type_tuple(child1, child, cl);
    int ans;
    JL_GC_PUSH1(&tu);
    ans = jl_subtype(tu, (jl_value_t*)pdt);
    JL_GC_POP();
    return ans;
}

int jl_tuple_isa(jl_value_t **child, size_t cl, jl_datatype_t *pdt)
{
    if (cl == 0) {
        if (pdt == jl_emptytuple_type)
            return 1;
        if (jl_is_tuple_type(pdt) && (jl_nparams(pdt) != 1 || !jl_is_va_tuple(pdt)))
            return 0;
        return jl_isa(jl_emptytuple, (jl_value_t*)pdt);
    }
    return jl_tuple1_isa(child[0], &child[1], cl, pdt);
}

// returns true if the intersection of `t` and `Type` is non-empty and not a kind
// this is sufficient to determine if `isa(x, T)` can instead simply check for `typeof(x) <: T`
int jl_has_intersect_type_not_kind(jl_value_t *t)
{
    t = jl_unwrap_unionall(t);
    if (t == (jl_value_t*)jl_any_type)
        return 1;
    assert(!jl_is_vararg(t));
    if (jl_is_uniontype(t))
        return jl_has_intersect_type_not_kind(((jl_uniontype_t*)t)->a) ||
               jl_has_intersect_type_not_kind(((jl_uniontype_t*)t)->b);
    if (jl_is_typeeq(t)) {
        jl_value_t *T = jl_typeeq_T(t);
        return jl_is_typevar(T) || !is_kind_or_anytype(T);
    }
    if (jl_is_typevar(t))
        return jl_has_intersect_type_not_kind(((jl_tvar_t*)t)->ub);
    if (jl_is_datatype(t))
        if (((jl_datatype_t*)t)->name == jl_type_typename)
            return 1;
    return 0;
}

// compute if DataType<:t || Union<:t || UnionAll<:t etc.
int jl_has_intersect_kind_not_type(jl_value_t *t)
{
    t = jl_unwrap_unionall(t);
    if (t == (jl_value_t*)jl_any_type || is_kind_or_anytype(t))
        return 1;
    assert(!jl_is_vararg(t));
    if (jl_is_uniontype(t))
        return jl_has_intersect_kind_not_type(((jl_uniontype_t*)t)->a) ||
               jl_has_intersect_kind_not_type(((jl_uniontype_t*)t)->b);
    if (jl_is_typeeq(t)) {
        jl_value_t *T = jl_typeeq_T(t);
        return jl_is_typevar(T) || is_kind_or_anytype(T);
    }
    if (jl_is_typevar(t))
        return jl_has_intersect_kind_not_type(((jl_tvar_t*)t)->ub);
    return 0;
}


JL_DLLEXPORT int jl_isa(jl_value_t *x, jl_value_t *t)
{
    if (t == (jl_value_t*)jl_any_type || jl_typetagis(x,t))
        return 1;
    if (jl_typetagof(x) < (jl_max_tags << 4) && jl_is_datatype(t) && jl_typetagis(x,((jl_datatype_t*)t)->smalltag << 4))
        return 1;
    if (jl_is_typeapp(t))
        jl_error("internal error: TypeApp in jl_isa");
    if (jl_is_type(x)) {
        if (t == (jl_value_t*)jl_type_type)
            return 1;
        if (!jl_has_free_typevars(x)) {
            if (jl_is_concrete_type(t))
                return 0;
            if (jl_is_typeeq(t))
                return jl_types_equal(x, jl_typeeq_T(t));
            jl_value_t *t2 = jl_unwrap_unionall(t);
            if (jl_is_typeeq(t2)) {
                jl_value_t *tp = jl_typeeq_T(t2);
                if (jl_is_typevar(tp)) {
                    if (((jl_tvar_t*)tp)->lb == jl_bottom_type) {
                        while (jl_is_typevar(tp))
                            tp = ((jl_tvar_t*)tp)->ub;
                        if (!jl_has_free_typevars(tp))
                            return jl_subtype(x, tp);
                    }
                    else if (((jl_tvar_t*)tp)->ub == (jl_value_t*)jl_any_type) {
                        while (jl_is_typevar(tp))
                            tp = ((jl_tvar_t*)tp)->lb;
                        if (!jl_has_free_typevars(tp))
                            return jl_subtype(tp, x);
                    }
                }
            }
            else if (jl_is_datatype(t2)) {
                return jl_subtype(jl_typeof(x), t);
            }
            if (jl_subtype(jl_typeof(x), t))
                return 1;
            if (jl_has_intersect_type_not_kind(t2)) {
                jl_value_t *wrapped = (jl_value_t*)jl_wrap_Type(x);  // TODO jb/subtype avoid jl_wrap_Type
                JL_GC_PUSH1(&wrapped);
                int ans = jl_subtype(wrapped, t);
                JL_GC_POP();
                return ans;
            }
            return 0;
        }
    }
    if (jl_is_concrete_type(t))
        return 0;
    return jl_subtype(jl_typeof(x), t);
}

// type intersection

static jl_value_t *intersect(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_param_pos_t param);

static jl_value_t *intersect_all(jl_value_t *x, jl_value_t *y, jl_stenv_t *e);

// intersect in nested union environment, similar to subtype_ccheck
static jl_value_t *intersect_aside(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int depth)
{
    // band-aid for #30335
    if (x == (jl_value_t*)jl_any_type && !jl_is_typevar(y))
        return y;
    if (y == (jl_value_t*)jl_any_type && !jl_is_typevar(x))
        return x;
    // band-aid for #46736 #56040
    if (obviously_in_union(x, y))
        return y;
    if (obviously_in_union(y, x))
        return x;

    // Consistency check for a typevar bound: covariant occurrences inside this
    // call should not accumulate into the surrounding scope's diagonality
    // counter. Save & reset the counters before any env truncation so all
    // vars are captured, and restore after the env is put back.
    int8_t *saved_cov = (int8_t*)alloca(current_env_length(e));
    int nsaved_cov = push_consistency_scope(e, saved_cov);

    jl_varbinding_t *vars = NULL;
    jl_varbinding_t *bbprev = NULL;
    int xinner = 0, yinner = 0;
    jl_varbinding_t *xb = jl_is_typevar(x) ? lookup_binding(e, (jl_tvar_t *)x, &xinner) : NULL;
    jl_varbinding_t *yb = jl_is_typevar(y) ? lookup_binding(e, (jl_tvar_t *)y, &yinner) : NULL;
    int simple_x = jl_is_typevar(x) ? (xb ? !jl_has_free_typevars(xb->ub) : !xinner) : !jl_has_free_typevars(x);
    int simple_y = jl_is_typevar(y) ? (yb ? !jl_has_free_typevars(yb->ub) : !yinner) : !jl_has_free_typevars(y);
    if (simple_x && simple_y && !(xb && yb)) {
        vars = e->vars;
        e->vars = xb ? xb : yb;
        if (e->vars != NULL) {
            bbprev = e->vars->prev;
            e->vars->prev = NULL;
        }
    }
    jl_saved_unionstate_t oldRunions; push_unionstate(&oldRunions, &e->Runions);
    int savedepth = e->invdepth;
    e->invdepth = depth;
    jl_value_t *res = intersect_all(x, y, e);
    e->invdepth = savedepth;
    pop_unionstate(&e->Runions, &oldRunions);
    if (bbprev) e->vars->prev = bbprev;
    if (vars) e->vars = vars;

    pop_consistency_scope(e, saved_cov, nsaved_cov);
    return res;
}

static jl_value_t *intersect_union(jl_value_t *x, jl_uniontype_t *u, jl_stenv_t *e, int8_t R, jl_param_pos_t param)
{
    int no_free = !jl_has_free_typevars(x) && !jl_has_free_typevars((jl_value_t*)u);
    if (param == PARAM_INVARIANT || no_free) {
        jl_value_t *a=NULL, *b=NULL;
        JL_GC_PUSH2(&a, &b);
        jl_varbinding_t *vars = NULL;
        if (no_free) {
            vars = e->vars;
            e->vars = NULL;
        }
        jl_saved_unionstate_t oldRunions; push_unionstate(&oldRunions, &e->Runions);
        a = R ? intersect_all(x, u->a, e) : intersect_all(u->a, x, e);
        b = R ? intersect_all(x, u->b, e) : intersect_all(u->b, x, e);
        pop_unionstate(&e->Runions, &oldRunions);
        if (vars) e->vars = vars;
        jl_value_t *i = simple_join(a,b);
        JL_GC_POP();
        return i;
    }
    jl_value_t *choice = pick_union_element((jl_value_t*)u, e, 1);
    // try all possible choices in covariant position; union them all together at the top level
    return R ? intersect(x, choice, e, param) : intersect(choice, x, e, param);
}

// set a variable to a non-type constant
static jl_value_t *set_var_to_const(jl_varbinding_t *bb, jl_value_t *v JL_MAYBE_UNROOTED, jl_stenv_t *e, int R)
{
    int offset = R ? -e->Loffset : e->Loffset;
    if (bb->lb == jl_bottom_type && bb->ub == (jl_value_t*)jl_any_type) {
        if (offset == 0)
            bb->lb = bb->ub = v;
        else if (jl_is_long(v)) {
            size_t iv = jl_unbox_long(v);
            v = jl_box_long(iv + offset);
            bb->lb = bb->ub = v;
            // Here we always return the shorter `Vararg`'s length.
            if (offset > 0)
                return jl_box_long(iv);
        }
        else
            return jl_bottom_type;
    }
    else if (jl_is_long(v) && jl_is_long(bb->lb)) {
        if (jl_unbox_long(v) + offset != jl_unbox_long(bb->lb))
            return jl_bottom_type;
        // Here we always return the shorter `Vararg`'s length.
        if (offset < 0) return bb->lb;
    }
    else if (!jl_egal(v, bb->lb)) {
        return jl_bottom_type;
    }
    return v;
}

static jl_value_t *bound_var_below(jl_tvar_t *tv, jl_varbinding_t *bb, jl_stenv_t *e, int R) {
    if (!bb)
        return (jl_value_t*)tv;
    if (bb->depth0 != e->invdepth)
        return jl_bottom_type;
    e->invdepth++;
    record_var_occurrence(bb, e, PARAM_INVARIANT);
    e->invdepth--;
    int offset = R ? -e->Loffset : e->Loffset;
    if (jl_is_long(bb->lb)) {
        ssize_t blb = jl_unbox_long(bb->lb);
        if (blb < offset || blb < 0)
            return jl_bottom_type;
        // Here we always return the shorter `Vararg`'s length.
        if (offset <= 0)
            return bb->lb;
        return jl_box_long(blb - offset);
    }
    if (offset > 0) {
        if (bb->innervars == NULL)
            bb->innervars = jl_alloc_array_1d(jl_array_any_type, 0);
        jl_value_t *ntv = NULL;
        JL_GC_PUSH1(&ntv);
        ntv = (jl_value_t *)jl_new_typevar(tv->name, jl_bottom_type, (jl_value_t *)jl_any_type);
        jl_array_ptr_1d_push(bb->innervars, ntv);
        JL_GC_POP();
        return ntv;
    }
    return (jl_value_t*)tv;
}

static int subtype_by_bounds(jl_value_t *x, jl_value_t *y, jl_stenv_t *e) JL_NOTSAFEPOINT;

// similar to `subtype_by_bounds`, used to avoid stack-overflow caused by circular constraints.
static int try_subtype_by_bounds(jl_value_t *a, jl_value_t *b, jl_stenv_t *e)
{
    if (jl_is_uniontype(a))
        return try_subtype_by_bounds(((jl_uniontype_t *)a)->a, b, e) &&
               try_subtype_by_bounds(((jl_uniontype_t *)a)->b, b, e);
    else if (jl_is_uniontype(b))
        return try_subtype_by_bounds(a, ((jl_uniontype_t *)b)->a, e) ||
               try_subtype_by_bounds(a, ((jl_uniontype_t *)b)->b, e);
    else if (a == jl_bottom_type || b == (jl_value_t *)jl_any_type || obviously_egal(a, b))
        return 1;
    else if (!jl_is_typevar(b))
        return 0;
    else if (jl_is_typevar(a) && subtype_by_bounds(a, b, e))
        return 1;
    // check if `Union{a, ...} <: b`.
    int innervar = 0;
    jl_varbinding_t *vb = lookup_binding(e, (jl_tvar_t *)b, &innervar);
    if (vb == NULL && !innervar)
        return subtype_singleton_typevar(a, (jl_tvar_t*)b);
    jl_value_t *blb = vb ? vb->lb : ((jl_tvar_t *)b)->lb;
    return obviously_in_union(a, blb);
}

static int try_subtype_in_env(jl_value_t *a, jl_value_t *b, jl_stenv_t *e)
{
    if (try_subtype_by_bounds(a, b, e))
        return 1;
    jl_savedenv_t se;
    save_env(e, &se, 1);
    int ret = subtype_in_env(a, b, e);
    restore_env(e, &se, 1);
    free_env(&se);
    return ret;
}

static void set_bound(jl_value_t **bound, jl_value_t *val, jl_tvar_t *v, jl_stenv_t *e) JL_NOTSAFEPOINT
{
    if (in_union(val, (jl_value_t*)v))
        return;
    jl_varbinding_t *btemp = e->vars;
    while (btemp != NULL) {
        if ((btemp->lb == (jl_value_t*)v || btemp->ub == (jl_value_t*)v) &&
            in_union(val, (jl_value_t*)btemp->var))
            return;
        btemp = btemp->prev;
    }
    *bound = val;
}

// subtype, treating all vars as existential
static int subtype_in_env_existential(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
{
    if (x == jl_bottom_type || y == (jl_value_t*)jl_any_type || obviously_in_union(y, x))
        return 1;
    int8_t *rs = (int8_t*)alloca(current_env_length(e));
    jl_varbinding_t *v = e->vars;
    int n = 0;
    while (v != NULL) {
        rs[n++] = v->existential;
        v->existential = 1;
        v = v->prev;
    }
    int issub = subtype_in_env(x, y, e);
    n = 0; v = e->vars;
    while (v != NULL) {
        v->existential = rs[n++];
        v = v->prev;
    }
    return issub;
}

// See if var y is reachable from x via bounds; used to avoid cycles.
static int _reachable_var(jl_value_t *x, jl_tvar_t *y, jl_stenv_t *e, jl_typeenv_t *log)
{
    if (in_union(x, (jl_value_t*)y))
        return 1;
    if (jl_is_uniontype(x) || jl_is_intersecttype(x))
        return _reachable_var(((jl_uniontype_t *)x)->a, y, e, log) ||
               _reachable_var(((jl_uniontype_t *)x)->b, y, e, log);
    if (!jl_is_typevar(x))
        return 0;
    jl_typeenv_t *t = log;
    while (t != NULL) {
        if (x == (jl_value_t *)t->var)
            return 0;
        t = t->prev;
    }
    int innervar = 0;
    jl_varbinding_t *xv = lookup_binding(e, (jl_tvar_t*)x, &innervar);
    if (xv == NULL && !innervar)
        return 0;
    jl_value_t *lb = xv == NULL ? ((jl_tvar_t*)x)->lb : xv->lb;
    jl_value_t *ub = xv == NULL ? ((jl_tvar_t*)x)->ub : xv->ub;
    jl_typeenv_t newlog = { (jl_tvar_t*)x, NULL, log };
    return _reachable_var(ub, y, e, &newlog) || _reachable_var(lb, y, e, &newlog);
}

static int reachable_var(jl_value_t *x, jl_tvar_t *y, jl_stenv_t *e)
{
    return _reachable_var(x, y, e, NULL);
}

// check whether setting v == t implies v == SomeType{v}, which is unsatisfiable.
static int check_unsat_bound(jl_value_t *t, jl_tvar_t *v, jl_stenv_t *e) JL_NOTSAFEPOINT
{
    if (var_occurs_inside(t, v, 0, 0))
        return 1;
    jl_varbinding_t *btemp = e->vars;
    while (btemp != NULL) {
        if (btemp->lb == (jl_value_t*)v && btemp->ub == (jl_value_t*)v &&
            var_occurs_inside(t, btemp->var, 0, 0))
            return 1;
        btemp = btemp->prev;
    }
    return 0;
}


static int intersect_var_ccheck_in_env(jl_value_t *xlb, jl_value_t *xub, jl_value_t *ylb, jl_value_t *yub, jl_stenv_t *e, int flip);

static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int8_t R, jl_param_pos_t param)
{
    int innervar = 0;
    jl_varbinding_t *bb = lookup_binding(e, b, &innervar);
    if (bb == NULL) {
        if (innervar)
            return R ? intersect_aside(a, b->ub, e, 0) : intersect_aside(b->ub, a, e, 0);
        if (singleton_typevar_subtype(b, a))
            return (jl_value_t*)b;
        if (subtype_singleton_typevar(a, b))
            return a;
        return jl_bottom_type;
    }
    if (reachable_var(bb->lb, b, e) || reachable_var(bb->ub, b, e))
        return a;
    if (bb->lb == bb->ub && jl_is_typevar(bb->lb))
        return R ? intersect(a, bb->lb, e, param) : intersect(bb->lb, a, e, param);
    if (!jl_is_type(a) && !jl_is_typevar(a))
        return set_var_to_const(bb, a, e, R);
    if (param == PARAM_INVARIANT) {
        jl_value_t *ub = NULL;
        JL_GC_PUSH1(&ub);
        if (!jl_has_free_typevars(a)) {
            if (R) flip_offset(e);
            int ccheck = intersect_var_ccheck_in_env(bb->lb, bb->ub, a, a, e, !R);
            if (R) flip_offset(e);
            if (!ccheck) {
                JL_GC_POP();
                return jl_bottom_type;
            }
            ub = a;
        }
        else {
            if (jl_subtype(a, bb->ub)) {
                ub = a;
            }
            else {
                e->triangular++;
                ub = R ? intersect_aside(a, bb->ub, e, bb->depth0) : intersect_aside(bb->ub, a, e, bb->depth0);
                e->triangular--;
            }
            jl_savedenv_t se;
            save_env(e, &se, 1);
            int issub = subtype_in_env_existential(bb->lb, ub, e);
            restore_env(e, &se, 1);
            free_env(&se);
            if (!issub) {
                JL_GC_POP();
                return jl_bottom_type;
            }
        }
        if (ub != (jl_value_t*)b) {
            if (jl_has_free_typevars(ub)) {
                if (check_unsat_bound(ub, b, e)) {
                    JL_GC_POP();
                    return jl_bottom_type;
                }
            }
            bb->ub = ub;
            if ((jl_is_uniontype(ub) && !jl_is_uniontype(a)) ||
                (jl_is_unionall(ub) && !jl_is_unionall(a)))
                ub = (jl_value_t*)b;
            else
                bb->lb = ub;
        }
        JL_GC_POP();
        return ub;
    }
    jl_value_t *ub = R ? intersect_aside(a, bb->ub, e, bb->depth0) : intersect_aside(bb->ub, a, e, bb->depth0);
    if (ub == jl_bottom_type)
        return jl_bottom_type;
    if (e->triangular && param == PARAM_COVARIANT) {
        if (check_unsat_bound(ub, b, e))
            return jl_bottom_type;
        set_bound(&bb->ub, ub, b, e);
        return (jl_value_t*)b;
    }
    if (bb->constraintkind == 1) {
        if (!jl_is_typeeq(ub) && !jl_is_uniontype(ub) && !jl_is_unionall(ub)) {
            // this branch is a fast path if there are no `Type`s and not needed for correctness
            set_bound(&bb->ub, ub, b, e);
            return (jl_value_t*)b;
        }
        jl_value_t *ub2 = NULL;
        JL_GC_PUSH2(&ub, &ub2);
        ub2 = widen_Type_to_union(ub, bb->ub, e);
        if (ub2 != ub) {
            set_bound(&bb->ub, ub2, b, e);
            if (jl_is_concrete_type(ub2)) {
                // all members widened to the same concrete kind
                JL_GC_POP();
                return ub;
            }
            bb->widened_to_kind = 1;
            JL_GC_POP();
            return (jl_value_t*)b;
        }
        set_bound(&bb->ub, ub, b, e);
        JL_GC_POP();
        return (jl_value_t*)b;
    }
    else if (bb->constraintkind == 0) {
        JL_GC_PUSH1(&ub);
        if (!jl_is_typevar(a) && try_subtype_in_env(bb->ub, a, e)) {
            JL_GC_POP();
            return (jl_value_t*)b;
        }
        JL_GC_POP();
        return ub;
    }
    assert(bb->constraintkind == 2);
    if (ub == a && bb->lb != jl_bottom_type)
        return ub;
    if (jl_egal(bb->ub, bb->lb))
        return ub;
    if (is_leaf_bound(ub))
        set_bound(&bb->lb, ub, b, e);
    // TODO: can we improve this bound by pushing a new variable into the environment
    // and adding that to the lower bound of our variable?
    //jl_value_t *ntv = NULL;
    //JL_GC_PUSH2(&ntv, &ub);
    //if (bb->innervars == NULL)
    //    bb->innervars = jl_alloc_array_1d(jl_array_any_type, 0);
    //ntv = (jl_value_t*)jl_new_typevar(b->name, bb->lb, ub);
    //jl_array_ptr_1d_push(bb->innervars, ntv);
    //jl_value_t *lb = simple_join(b->lb, ntv);
    //JL_GC_POP();
    //bb->lb = lb;
    return ub;
}

// test whether `var` occurs inside constructors. `want_inv` tests only inside
// invariant constructors. `inside` means we are currently inside a constructor of the
// requested kind.
static int var_occurs_inside(jl_value_t *v, jl_tvar_t *var, int inside, int want_inv) JL_NOTSAFEPOINT
{
    if (v == (jl_value_t*)var) {
        return inside;
    }
    else if (jl_is_uniontype(v) || jl_is_intersecttype(v)) {
        return var_occurs_inside(((jl_uniontype_t*)v)->a, var, inside, want_inv) ||
            var_occurs_inside(((jl_uniontype_t*)v)->b, var, inside, want_inv);
    }
    else if (jl_is_unionall(v)) {
        jl_unionall_t *ua = (jl_unionall_t*)v;
        if (ua->var == var)
            return 0;
        if (var_occurs_inside(ua->var->lb, var, inside, want_inv) || var_occurs_inside(ua->var->ub, var, inside, want_inv))
            return 1;
        return var_occurs_inside(ua->body, var, inside, want_inv);
    }
    else if (jl_is_vararg(v)) {
        jl_vararg_t *vm = (jl_vararg_t*)v;
        if (vm->T) {
            if (var_occurs_inside(vm->T, var, inside || !want_inv, want_inv))
                return 1;
            return vm->N && var_occurs_inside(vm->N, var, 1, want_inv);
        }
    }
    else if (jl_is_typeeq(v)) {
        return var_occurs_inside(jl_typeeq_T(v), var, 1, want_inv);
    }
    else if (jl_is_datatype(v)) {
        size_t i;
        int istuple = jl_is_tuple_type(v);
        for (i=0; i < jl_nparams(v); i++) {
            int ins_i = inside || !want_inv || !istuple;
            if (var_occurs_inside(jl_tparam(v,i), var, ins_i, want_inv))
                return 1;
        }
    }
    return 0;
}

static jl_value_t *omit_bad_union(jl_value_t *u, jl_tvar_t *t)
{
    if (!jl_has_typevar(u, t))
        return u; // return u if possible as many checks use `==`.
    jl_value_t *res = NULL;
    if (jl_is_unionall(u)) {
        jl_tvar_t *var = ((jl_unionall_t *)u)->var;
        jl_value_t *ub = var->ub, *body = ((jl_unionall_t *)u)->body;
        assert(var != t);
        JL_GC_PUSH3(&ub, &body, &var);
        body = omit_bad_union(body, t);
        if (!jl_has_typevar(body, var)) {
            res = body;
        }
        else if (jl_has_typevar(var->lb, t)) {
            res = jl_bottom_type;
        }
        else {
            ub = omit_bad_union(ub, t);
            if (ub == jl_bottom_type && var->lb != ub) {
                res = jl_bottom_type;
            }
            else if (obviously_egal(var->lb, ub)) {
                res = jl_substitute_var_nothrow(body, var, ub, 2);
                if (res == NULL)
                    res = jl_bottom_type;
            }
            else {
                if (ub != var->ub) {
                    var = jl_new_typevar(var->name, var->lb, ub);
                    body = jl_substitute_var(body, ((jl_unionall_t *)u)->var, (jl_value_t *)var);
                }
                res = jl_new_struct(jl_unionall_type, var, body);
            }
        }
        JL_GC_POP();
    }
    else if (jl_is_uniontype(u)) {
        jl_value_t *a = ((jl_uniontype_t *)u)->a;
        jl_value_t *b = ((jl_uniontype_t *)u)->b;
        JL_GC_PUSH2(&a, &b);
        a = omit_bad_union(a, t);
        b = omit_bad_union(b, t);
        res = simple_join(a, b);
        JL_GC_POP();
    }
    else {
        res = jl_bottom_type;
    }
    assert(res != NULL);
    return res;
}

// TODO: fuse with reachable_var?
static int has_typevar_via_flatten_env(jl_value_t *x, jl_tvar_t *t, jl_ivarbinding_t *allvars, int8_t *checked) JL_NOTSAFEPOINT
{
    if (jl_is_unionall(x)) {
        jl_tvar_t *var = ((jl_unionall_t *)x)->var;
        if (has_typevar_via_flatten_env(var->lb, t, allvars, checked) ||
            has_typevar_via_flatten_env(var->ub, t, allvars, checked))
            return 1;
        return has_typevar_via_flatten_env(((jl_unionall_t *)x)->body, t, allvars, checked);
    }
    else if (jl_is_uniontype(x)) {
        return has_typevar_via_flatten_env(((jl_uniontype_t *)x)->a, t, allvars, checked) ||
            has_typevar_via_flatten_env(((jl_uniontype_t *)x)->b, t, allvars, checked);
    }
    else if (jl_is_vararg(x)) {
        jl_vararg_t *v = (jl_vararg_t *)x;
        return (v->T && has_typevar_via_flatten_env(v->T, t, allvars, checked)) ||
            (v->N && has_typevar_via_flatten_env(v->N, t, allvars, checked));
    }
    else if (jl_is_datatype(x)) {
        for (size_t i = 0; i < jl_nparams(x); i++) {
            if (has_typevar_via_flatten_env(jl_tparam(x, i), t, allvars, checked))
                return 1;
        }
        return 0;
    }
    else if (jl_is_typevar(x)) {
        if (t == (jl_tvar_t *)x)
            return 1;
        size_t ind = 0;
        jl_ivarbinding_t *itemp = allvars;
        while (itemp && *itemp->var != (jl_tvar_t *)x)
        {
            ind++;
            itemp = itemp->next;
        }
        if (itemp == NULL || checked[ind])
            return 0;
        checked[ind] = 1;
        return has_typevar_via_flatten_env(*itemp->lb, t, allvars, checked) ||
            has_typevar_via_flatten_env(*itemp->ub, t, allvars, checked);
    }
    return 0;
}

// Caller might not have rooted `res`
static jl_value_t *finish_unionall(jl_value_t *res JL_MAYBE_UNROOTED, jl_varbinding_t *vb, jl_unionall_t *u, jl_stenv_t *e)
{
    jl_value_t *varval = NULL, *ilb = NULL, *iub = NULL, *nivar = NULL;
    jl_tvar_t *newvar = vb->var, *ivar = NULL;
    JL_GC_PUSH6(&res, &newvar, &ivar, &nivar, &ilb, &iub);
    // Note: `Intersect` is subtype accounting only and is widened away before
    // it leaves the subtype path (see `subtype_unionall`), so the intersection
    // result here never contains one.
    assert(!jl_is_intersecttype(vb->ub));
    // try to reduce var to a single value
    if (jl_is_long(vb->ub) && jl_is_typevar(vb->lb)) {
        varval = vb->ub;
    }
    else if (obviously_egal(vb->lb, vb->ub)) {
        // given x<:T<:x, substitute x for T
        varval = vb->ub;
    }
    // TODO: `vb.occurs_cov == 1`, we could also substitute Tuple{<:X} => Tuple{X},
    // but it may change some ambiguity errors so we don't need to do it yet.
    else if (cov_count(vb) && is_leaf_bound(vb->ub) && !jl_has_free_typevars(vb->ub)) {
        // replace T<:x with x in covariant position when possible
        varval = vb->ub;
    }

    if (vb->intvalued) {
        if ((varval && jl_is_long(varval)) ||
            (vb->lb == jl_bottom_type && vb->ub == (jl_value_t*)jl_any_type) ||
            (jl_is_typevar(vb->lb) && vb->ub == vb->lb)) {
            // int-valued typevar must either be an Int, or have Bottom-Any bounds,
            // or be set equal to another typevar.
        }
        else {
            JL_GC_POP();
            return jl_bottom_type;
        }
    }

    // TODO: this can prevent us from matching typevar identities later
    if (!varval && (vb->lb != vb->var->lb || vb->ub != vb->var->ub))
        newvar = jl_new_typevar(vb->var->name, vb->lb, vb->ub);

    // flatten all innervar into a (reversed) list
    size_t icount = 0;
    if (vb->innervars)
        icount += jl_array_nrows(vb->innervars);
    for (jl_varbinding_t *btemp = e->vars; btemp != NULL; btemp = btemp->prev) {
        if (btemp->innervars != NULL)
            icount += jl_array_nrows(btemp->innervars);
    }
    jl_svec_t *p = NULL;
    jl_value_t **iparams;
    jl_value_t **roots;
    JL_GC_PUSHARGS(roots, icount < 22 ? 3*icount : 1);
    if (icount < 22) {
        iparams = roots;
    }
    else {
        p = jl_alloc_svec(3*icount);
        roots[0] = (jl_value_t*)p;
        iparams = jl_svec_data(p);
    }
    jl_ivarbinding_t *allvars = NULL;
    size_t niparams = 0;
    if (vb->innervars) {
        for (size_t i = 0; i < jl_array_nrows(vb->innervars); i++) {
            jl_tvar_t *ivar = (jl_tvar_t *)jl_array_ptr_ref(vb->innervars, i);
            jl_ivarbinding_t *inew = (jl_ivarbinding_t *)alloca(sizeof(jl_ivarbinding_t));
            inew->var = (jl_tvar_t **)&iparams[niparams++]; *inew->var = ivar;
            inew->lb = &iparams[niparams++]; *inew->lb = ivar->lb;
            inew->ub = &iparams[niparams++]; *inew->ub = ivar->ub;
            inew->root = vb;
            inew->next = allvars;
            allvars = inew;
        }
    }
    for (jl_varbinding_t *btemp = e->vars; btemp != NULL; btemp = btemp->prev) {
        jl_ivarbinding_t *inew = (jl_ivarbinding_t *)alloca(sizeof(jl_ivarbinding_t));
        inew->var = &btemp->var;
        inew->lb = &btemp->lb;
        inew->ub = &btemp->ub;
        inew->root = btemp;
        inew->next = allvars;
        allvars = inew;
        if (btemp->innervars) {
            for (size_t i = 0; i < jl_array_nrows(btemp->innervars); i++) {
                jl_tvar_t *ivar = (jl_tvar_t *)jl_array_ptr_ref(btemp->innervars, i);
                jl_ivarbinding_t *inew = (jl_ivarbinding_t *)alloca(sizeof(jl_ivarbinding_t));
                inew->var = (jl_tvar_t **)&iparams[niparams++]; *inew->var = ivar;
                inew->lb = &iparams[niparams++]; *inew->lb = ivar->lb;
                inew->ub = &iparams[niparams++]; *inew->ub = ivar->ub;
                inew->root = btemp;
                inew->next = allvars;
                allvars = inew;
            }
        }
    }

    // remove/replace/rewrap free occurrences of this var in the environment
    int wrapped = 0;
    jl_ivarbinding_t *pwrap = NULL;
    int vcount = icount + current_env_length(e);
    int8_t *checked = (int8_t *)alloca(vcount);
    for (jl_ivarbinding_t *btemp = allvars, *pbtemp = NULL; btemp != NULL; btemp = btemp->next) {
        int bdepth0 = btemp->root->depth0;
        int innerflag = 0;
        ivar = *btemp->var;
        ilb = *btemp->lb;
        iub = *btemp->ub;
        if (jl_has_typevar(ilb, vb->var)) {
            assert(btemp->root->var == ivar || bdepth0 == vb->depth0);
            if (vb->lb == (jl_value_t*)ivar) {
                JL_GC_POP();
                JL_GC_POP();
                return jl_bottom_type;
            }
            if (varval) {
                JL_TRY {
                    *btemp->lb = jl_substitute_var(ilb, vb->var, varval);
                }
                JL_CATCH {
                    res = jl_bottom_type;
                }
            }
            else if (ilb == (jl_value_t*)vb->var) {
                *btemp->lb = vb->lb;
            }
            else {
                innerflag |= 1;
            }
        }
        if (jl_has_typevar(iub, vb->var)) {
            assert(btemp->root->var == ivar || bdepth0 == vb->depth0);
            if (vb->ub == (jl_value_t*)ivar) {
                *btemp->ub = omit_bad_union(iub, vb->var);
                if (*btemp->ub == jl_bottom_type && *btemp->ub != *btemp->lb) {
                    JL_GC_POP();
                    JL_GC_POP();
                    return jl_bottom_type;
                }
            }
            if (varval) {
                iub = jl_substitute_var_nothrow(iub, vb->var, varval, 2);
                if (iub == NULL)
                    res = jl_bottom_type;
                else
                    *btemp->ub = iub;
            }
            else if (iub == (jl_value_t*)vb->var) {
                // TODO: this loses some constraints, such as in this test, where we replace T4<:S3 (e.g. T4==S3 since T4 only appears covariantly once) with T4<:Any
                // a = Tuple{Float64,T3,T4} where T4 where T3
                // b = Tuple{S2,Tuple{S3},S3} where S2 where S3
                // Tuple{Float64, T3, T4} where {S3, T3<:Tuple{S3}, T4<:S3}
                *btemp->ub = vb->ub;
            }
            else {
                innerflag |= 2;
            }
        }
        if (innerflag) {
            memset(checked, 0, vcount);
            if (btemp->root == vb || bdepth0 != vb->depth0 ||
                has_typevar_via_flatten_env(vb->lb, ivar, allvars, checked) ||
                has_typevar_via_flatten_env(vb->ub, ivar, allvars, checked)) {
                if (innerflag & 1)
                    *btemp->lb = jl_new_struct(jl_unionall_type, vb->var, ilb);
                if (innerflag & 2)
                    *btemp->ub = jl_new_struct(jl_unionall_type, vb->var, iub);
            }
            else {
                assert(btemp->root != vb);
                // if our variable is T, and some outer variable has constraint S = Ref{T},
                // move the `where T` outside `where S` instead of putting it here. issue #21243.
                if (newvar != vb->var) {
                    if (innerflag & 1)
                        *btemp->lb = jl_substitute_var(ilb, vb->var, (jl_value_t*)newvar);
                    if (innerflag & 2)
                        *btemp->ub = jl_substitute_var(iub, vb->var, (jl_value_t*)newvar);
                }
                if (!wrapped)
                    pwrap = pbtemp;
                wrapped = 1;
            }
            assert((jl_value_t*)ivar != *btemp->lb);
            assert((jl_value_t*)ivar != *btemp->ub);
        }
        pbtemp = btemp;
    }

    // Insert the newvar into the (reversed) var list if needed.
    if (wrapped) {
        jl_ivarbinding_t *wrap = pwrap == NULL ? allvars : pwrap->next;
        jl_ivarbinding_t *inew = (jl_ivarbinding_t *)alloca(sizeof(jl_ivarbinding_t));
        inew->var = &newvar;
        inew->lb = &newvar->lb;
        inew->ub = &newvar->ub;;
        inew->root = wrap->root;
        inew->next = wrap;
        if (pwrap != NULL)
            pwrap->next = inew;
        else
            allvars = inew;
        vcount++;
    }

    // Re-sort the innervar inside the (reversed) var list.
    // `jl_has_typevar` is used as the partial-ordering predicate.
    // If this is slow, we could possibly switch to a simpler graph sort, such as Tarjan's SCC.
    if (icount > 0) {
        jl_ivarbinding_t *pib1 = NULL;
#ifndef NDEBUG
        size_t sort_count = 0;
#endif
        while (1) {
            jl_ivarbinding_t *ib1 = pib1 == NULL ? allvars : pib1->next;
            if (ib1 == NULL) break;
            assert((++sort_count) <= (vcount * (vcount + 1)) >> 1);
            int lbfree = jl_has_free_typevars(*ib1->lb);
            int ubfree = jl_has_free_typevars(*ib1->ub);
            if (lbfree || ubfree) {
                int changed = 0;
                jl_ivarbinding_t *pib2 = ib1, *ib2 = ib1->next;
                while (ib2 != NULL) {
                    int isinnervar = ib2->root->var != *ib2->var;
                    if (isinnervar && ib1->root->depth0 == ib2->root->depth0 &&
                        ((lbfree && jl_has_typevar(*ib1->lb, *ib2->var)) ||
                         (ubfree && jl_has_typevar(*ib1->ub, *ib2->var)))) {
                        pib2->next = ib2->next;
                        ib2->next = ib1;
                        ib2->root = ib1->root;
                        if (pib1)
                            pib1->next = ib2;
                        else
                            allvars = ib2;
                        changed = 1;
                        break;
                    }
                    pib2 = ib2;
                    ib2 = ib2->next;
                }
                if (changed) continue;
            }
            pib1 = ib1;
        }
    }

    // Freeze the innervars' lb/ub and perform substitution if needed.
    for (jl_ivarbinding_t *btemp1 = allvars; btemp1 != NULL; btemp1 = btemp1->next) {
        ivar = *btemp1->var;
        ilb = *btemp1->lb;
        iub = *btemp1->ub;
        int isinnervar = btemp1->root->var != ivar;
        if (isinnervar && (ivar->lb != ilb || ivar->ub != iub)) {
            nivar = (jl_value_t *)jl_new_typevar(ivar->name, ilb, iub);
            if (jl_has_typevar(res, ivar))
                res = jl_substitute_var(res, ivar, nivar);
            for (jl_ivarbinding_t *btemp2 = btemp1->next; btemp2 != NULL; btemp2 = btemp2->next) {
                ilb = *btemp2->lb;
                iub = *btemp2->ub;
                if (jl_has_typevar(ilb, ivar))
                    *btemp2->lb = jl_substitute_var(ilb, ivar, nivar);
                if (jl_has_typevar(iub, ivar))
                    *btemp2->ub = jl_substitute_var(iub, ivar, nivar);
            }
            if (!wrapped && !varval) {
                // newvar also needs bounds substitution.
                if (jl_has_typevar(vb->lb, ivar))
                    vb->lb = jl_substitute_var(vb->lb, ivar, nivar);
                if (jl_has_typevar(vb->ub, ivar))
                    vb->ub = jl_substitute_var(vb->ub, ivar, nivar);
            }
            *btemp1->var = (jl_tvar_t *)nivar;
        }
    }

    // Switch back the innervars' storage.
    while (1) {
        jl_ivarbinding_t *btemp = allvars;
        jl_varbinding_t *root = btemp ? btemp->root : vb;
        size_t icount = 0;
        while (btemp && btemp->root == root) {
            btemp = btemp->next;
            icount++;
        }
        if (root != vb) icount--;
        if (root->innervars != NULL) {
            jl_array_t *rinnervars = root->innervars;
            JL_GC_PROMISE_ROOTED(rinnervars);
            size_t len = jl_array_nrows(rinnervars);
            if (icount > len)
                jl_array_grow_end(rinnervars, icount - len);
            if (icount < len)
                jl_array_del_end(rinnervars, len - icount);
        }
        else if (icount > 0) {
            root->innervars = jl_alloc_array_1d(jl_array_any_type, icount);
        }
        btemp = allvars;
        for (size_t i = icount; i > 0; i--) {
            jl_array_ptr_set(root->innervars, i - 1, (jl_value_t*)*btemp->var);
            btemp = btemp->next;
        }
        if (root == vb) break;
        assert(*btemp->var == root->var);
        allvars = btemp->next;
        assert(allvars == NULL || allvars->root != root);
    }
    JL_GC_POP();

    // if `v` still occurs, re-wrap body in `UnionAll v` or eliminate the UnionAll
    if (jl_has_typevar(res, vb->var)) {
        if (varval) {
            // you can construct `T{x} where x` even if T's parameter is actually
            // limited. in that case we might get an invalid instantiation here.
            res = jl_substitute_var_nothrow(res, vb->var, varval, 2);
            // simplify chains of UnionAlls where bounds become equal
            while (res != NULL && jl_is_unionall(res) && obviously_egal(((jl_unionall_t*)res)->var->lb,
                                                         ((jl_unionall_t*)res)->var->ub)) {
                jl_unionall_t * ures = (jl_unionall_t *)res;
                res = jl_substitute_var_nothrow(ures->body, ures->var, ures->var->lb, 2);
            }
            if (res == NULL)
                res = jl_bottom_type;
        }
        else {
            // re-fresh newvar if bounds changed.
            if (vb->lb != newvar->lb || vb->ub != newvar->ub)
                newvar = jl_new_typevar(newvar->name, vb->lb, vb->ub);
            if (newvar != vb->var)
                res = jl_substitute_var(res, vb->var, (jl_value_t*)newvar);
            varval = (jl_value_t*)newvar;
            if (!wrapped)
                res = jl_type_unionall((jl_tvar_t*)newvar, res);
        }
    }

    if (vb->innervars != NULL) {
        for (size_t i = 0; i < jl_array_nrows(vb->innervars); i++) {
            jl_tvar_t *var = (jl_tvar_t*)jl_array_ptr_ref(vb->innervars, i);
            res = jl_type_unionall(var, res);
        }
    }

    JL_GC_POP();
    return res;
}

static jl_value_t *intersect_unionall_(jl_value_t *t, jl_unionall_t *u, jl_stenv_t *e, int8_t R, jl_param_pos_t param, jl_varbinding_t *vb)
{
    jl_varbinding_t *btemp = e->vars;
    int envsize = 0;
    while (btemp != NULL) {
        envsize++;
        if (envsize > 120) {
            vb->limited = 1;
            return t;
        }
        btemp = btemp->prev;
    }
    u = unalias_unionall(u, e);
    JL_GC_PUSH1(&u);
    if (jl_has_typevar(t, u->var))
        u = jl_rename_unionall(u);
    vb->var = u->var;
    e->vars = vb;
    jl_value_t *res;
    if (R) {
        e->envidx++;
        res = intersect(t, u->body, e, param);
        e->envidx--;
    }
    else {
        res = intersect(u->body, t, e, param);
    }
    vb->concrete |= (cov_count(vb) > 1 && is_leaf_typevar(u->var) &&
                     !vb->body_occurs_inv);

    // handle the "diagonal dispatch" rule, which says that a type var occurring more
    // than once, and only in covariant position, is constrained to concrete types. E.g.
    //  ( Tuple{Int, Int}    <: Tuple{T, T} where T) but
    // !( Tuple{Int, String} <: Tuple{T, T} where T)
    // Then check concreteness by checking that the lower bound is not an abstract type.
    if (res != jl_bottom_type && vb->concrete) {
        if (jl_is_typevar(vb->lb)) {
        }
        else if (!is_leaf_bound(vb->lb)) {
            res = jl_bottom_type;
        }
    }

    // Propagate "deeper-popped tvar leaks into outer bounds" taint upward.
    // See the matching block in `subtype_unionall`.
    for (jl_varbinding_t *btemp = vb->prev; btemp; btemp = btemp->prev) {
        if ((vb->depth0 > btemp->depth0 || vb->tainted_inner) &&
            (jl_has_typevar(btemp->lb, vb->var) || jl_has_typevar(btemp->ub, vb->var))) {
            btemp->tainted_inner = 1;
        }
    }

    e->vars = vb->prev;

    if (res != jl_bottom_type) {
        if (vb->ub == jl_bottom_type && cov_count(vb)) {
            // T=Bottom in covariant position
            res = jl_bottom_type;
        }
        else if (jl_has_typevar(vb->lb, u->var)) {
            // fail on circular constraints
            res = jl_bottom_type;
        }
        else {
            JL_GC_PUSH1(&res);
            vb->ub = omit_bad_union(vb->ub, u->var);
            JL_GC_POP();
            if (vb->ub == jl_bottom_type && vb->ub != vb->lb)
                res = jl_bottom_type;
        }
    }
    if (res != jl_bottom_type)
        // res is rooted by callee
        res = finish_unionall(res, vb, u, e);
    JL_GC_POP();
    return res;
}

static int always_occurs_cov(jl_value_t *v, jl_tvar_t *var, jl_param_pos_t param) JL_NOTSAFEPOINT
{
    if (param == PARAM_INVARIANT) {
        return 0;
    }
    else if (v == (jl_value_t*)var) {
        return param == PARAM_COVARIANT;
    }
    else if (jl_is_uniontype(v)) {
        return always_occurs_cov(((jl_uniontype_t*)v)->a, var, param) &&
               always_occurs_cov(((jl_uniontype_t*)v)->b, var, param);
    }
    else if (jl_is_unionall(v)) {
        jl_unionall_t *ua = (jl_unionall_t*)v;
        return ua->var != var && (
            always_occurs_cov(ua->var->ub, var, PARAM_NONE) ||
            always_occurs_cov(ua->body, var, param));
    }
    else if (jl_is_vararg(v)) {
        jl_vararg_t *vm = (jl_vararg_t*)v;
        return vm->T && always_occurs_cov(vm->T, var, param);
    }
    else if (jl_is_typeeq(v)) {
        return always_occurs_cov(jl_typeeq_T(v), var, PARAM_INVARIANT);
    }
    else if (jl_is_datatype(v)) {
        jl_param_pos_t nparam = jl_is_tuple_type(v) ? PARAM_COVARIANT : param;
        for (size_t i = 0; i < jl_nparams(v); i++) {
            if (always_occurs_cov(jl_tparam(v, i), var, nparam))
                return 1;
        }
    }
    return 0;
}

static jl_value_t *intersect_unionall(jl_value_t *t, jl_unionall_t *u, jl_stenv_t *e, int8_t R, jl_param_pos_t param)
{
    jl_value_t *res = NULL;
    jl_savedenv_t se;
    int body_occurs_inv = var_occurs_invariant(u->body, u->var);
    jl_varbinding_t vb = { u->var, u->var->lb, u->var->ub, R, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, body_occurs_inv,
                           e->invdepth, NULL, e->vars };
    JL_GC_PUSH4(&res, &vb.lb, &vb.ub, &vb.innervars);
    save_env(e, &se, 1);
    int noinv = !body_occurs_inv;
    if (is_leaf_typevar(u->var) && noinv && always_occurs_cov(u->body, u->var, param))
        vb.constraintkind = 1;
    res = intersect_unionall_(t, u, e, R, param, &vb);
    vb.intersected = 1;
    if (vb.limited) {
        // if the environment got too big, avoid tree recursion and propagate the flag
        if (e->vars)
            e->vars->limited = 1;
    }
    else if (res != jl_bottom_type) {
        int constraint1 = vb.constraintkind;
        if (vb.concrete || vb.occurs_inv>1 || (vb.occurs_inv && cov_count(&vb)))
            vb.constraintkind = vb.concrete ? 1 : 2;
        else if (u->var->lb != jl_bottom_type)
            vb.constraintkind = 2;
        else if (cov_count(&vb) && noinv)
            vb.constraintkind = 1;
        int reintersection = constraint1 != vb.constraintkind || vb.concrete;
        if (reintersection) {
            if (constraint1 == 1) {
                vb.lb = vb.var->lb;
                vb.ub = vb.var->ub;
            }
            restore_env(e, &se, vb.constraintkind == 1 ? 1 : 0);
            vb.occurs_cov = vb.occurs_inv = vb.cov_diag = 0;
            res = intersect_unionall_(t, u, e, R, param, &vb);
        }
    }
    if (res != jl_bottom_type && vb.constraintkind == 1 && vb.widened_to_kind == 1) {
        // a `Type` was widened to a non-concrete kind union during intersection
        if (cov_count(&vb) > 1) {
            // diagonal: reintersect if able to narrow across positions to a leaf bound
            // otherwise use original (possibly non-precise) bound
            if (is_leaf_bound(vb.ub)) {
                restore_env(e, &se, 1);
                vb.lb = vb.var->lb;
                vb.occurs_cov = vb.occurs_inv = vb.cov_diag = 0;
                res = intersect_unionall_(t, u, e, R, param, &vb);
            }
        }
        else {
            // actually non-diagonal: reintersect without widening or constraint
            restore_env(e, &se, 1);
            vb.lb = vb.var->lb;
            vb.ub = vb.var->ub;
            vb.constraintkind = 0;
            vb.widened_to_kind = 0;
            vb.occurs_cov = vb.occurs_inv = vb.cov_diag = 0;
            res = intersect_unionall_(t, u, e, R, param, &vb);
        }
    }
    free_env(&se);
    JL_GC_POP();
    return res;
}

static jl_value_t *intersect_invariant(jl_value_t *x, jl_value_t *y, jl_stenv_t *e);

// check n = (length of vararg type v)
static int intersect_vararg_length(jl_value_t *v, ssize_t n, jl_stenv_t *e, int8_t R)
{
    jl_value_t *N = jl_unwrap_vararg_num(v);
    // only do the check if N is free in the tuple type's last parameter
    if (N && jl_is_typevar(N)) {
        jl_value_t *len = jl_box_long(n);
        JL_GC_PUSH1(&len);
        jl_value_t *il = R ? intersect_invariant(len, N, e) : intersect_invariant(N, len, e);
        JL_GC_POP();
        if (il == NULL || il == jl_bottom_type)
            return 0;
    }
    return 1;
}

static jl_value_t *intersect_varargs(jl_vararg_t *vmx, jl_vararg_t *vmy, ssize_t offset, jl_stenv_t *e, jl_param_pos_t param)
{
    // Vararg: covariant in first parameter, invariant in second
    jl_value_t *xp1=jl_unwrap_vararg(vmx), *xp2=jl_unwrap_vararg_num(vmx),
                *yp1=jl_unwrap_vararg(vmy), *yp2=jl_unwrap_vararg_num(vmy);
    // in Vararg{T1} <: Vararg{T2}, need to check subtype twice to
    // simulate the possibility of multiple arguments, which is needed
    // to implement the diagonal rule correctly.
    if (intersect(xp1, yp1, e, param == PARAM_NONE ? PARAM_COVARIANT : param) == jl_bottom_type)
        return jl_bottom_type;
    jl_value_t *i2=NULL, *ii = intersect(xp1, yp1, e, PARAM_COVARIANT);
    if (ii == jl_bottom_type)
        return jl_bottom_type;
    if (!xp2 && !yp2) {
        if (obviously_egal(xp1, ii))
            ii = (jl_value_t*)vmx;
        else if (obviously_egal(yp1, ii))
            ii = (jl_value_t*)vmy;
        else {
            JL_GC_PUSH1(&ii);
            ii = (jl_value_t*)jl_wrap_vararg(ii, NULL, 1, 0);
            JL_GC_POP();
        }
        return ii;
    }
    JL_GC_PUSH2(&ii, &i2);
    assert(e->Loffset == 0);
    e->Loffset = offset;
    jl_varbinding_t *xb = NULL, *yb = NULL;
    int8_t max_offsetx = 0, max_offsety = 0;
    if (xp2) {
        assert(jl_is_typevar(xp2));
        xb = lookup(e, (jl_tvar_t*)xp2);
        if (xb) xb->intvalued = 1;
        if (xb) max_offsetx = xb->max_offset;
        if (!yp2)
            i2 = bound_var_below((jl_tvar_t*)xp2, xb, e, 0);
    }
    if (yp2) {
        assert(jl_is_typevar(yp2));
        yb = lookup(e, (jl_tvar_t*)yp2);
        if (yb) yb->intvalued = 1;
        if (yb) max_offsety = yb->max_offset;
        if (!xp2)
            i2 = bound_var_below((jl_tvar_t*)yp2, yb, e, 1);
    }
    if (xp2 && yp2) {
        // Vararg{T,N} <: Vararg{T2,N2}; equate N and N2
        i2 = intersect_invariant(xp2, yp2, e);
        if (i2 == NULL || i2 == jl_bottom_type || (jl_is_long(i2) && jl_unbox_long(i2) < 0) ||
            !((jl_is_typevar(i2) && ((jl_tvar_t*)i2)->lb == jl_bottom_type &&
                ((jl_tvar_t*)i2)->ub == (jl_value_t*)jl_any_type) || jl_is_long(i2))) {
            i2 = jl_bottom_type;
        }
    }
    assert(e->Loffset == offset);
    e->Loffset = 0;
    if (i2 == jl_bottom_type) {
        ii = (jl_value_t*)jl_bottom_type;
    }
    else {
        if (xb && !xb->intersected) {
            xb->max_offset = max_offsetx;
            if (offset > xb->max_offset && xb->max_offset >= 0)
                xb->max_offset = offset > 32 ? 32 : offset;
        }
        if (yb && !yb->intersected) {
            yb->max_offset = max_offsety;
            if (-offset > yb->max_offset && yb->max_offset >= 0)
                yb->max_offset = -offset > 32 ? 32 : -offset;
        }
        if (xp2 && obviously_egal(xp1, ii) && obviously_egal(xp2, i2))
            ii = (jl_value_t*)vmx;
        else if (yp2 && obviously_egal(yp1, ii) && obviously_egal(yp2, i2))
            ii = (jl_value_t*)vmy;
        else
            ii = (jl_value_t*)jl_wrap_vararg(ii, i2, 1, 0);
    }
    JL_GC_POP();
    return ii;
}


static jl_value_t *intersect_tuple(jl_datatype_t *xd, jl_datatype_t *yd, jl_stenv_t *e, jl_param_pos_t param)
{
    size_t lx = jl_nparams(xd), ly = jl_nparams(yd);
    size_t llx = lx, lly = ly;
    if (lx == 0 && ly == 0)
        return (jl_value_t*)yd;
    int vx=0, vy=0;
    jl_vararg_kind_t vvx = lx > 0 ? jl_vararg_kind(jl_tparam(xd, lx-1)) : JL_VARARG_NONE;
    jl_vararg_kind_t vvy = ly > 0 ? jl_vararg_kind(jl_tparam(yd, ly-1)) : JL_VARARG_NONE;
    if (vvx == JL_VARARG_INT)
        llx += jl_unbox_long(jl_unwrap_vararg_num((jl_vararg_t *)jl_tparam(xd, lx-1))) - 1;
    if (vvy == JL_VARARG_INT)
        lly += jl_unbox_long(jl_unwrap_vararg_num((jl_vararg_t *)jl_tparam(yd, ly-1))) - 1;
    if (vvx == JL_VARARG_BOUND && (vvy == JL_VARARG_BOUND || vvy == JL_VARARG_UNBOUND)) {
        jl_value_t *xlen = jl_unwrap_vararg_num((jl_vararg_t*)jl_tparam(xd, lx-1));
        assert(xlen && jl_is_typevar(xlen));
        jl_varbinding_t *xb = lookup(e, (jl_tvar_t*)xlen);
        if (xb && xb->intersected && xb->max_offset > 0) {
            assert(xb->max_offset <= 32);
            llx += xb->max_offset;
        }
    }
    if (vvy == JL_VARARG_BOUND && (vvx == JL_VARARG_BOUND || vvx == JL_VARARG_UNBOUND)) {
        jl_value_t *ylen = jl_unwrap_vararg_num((jl_vararg_t*)jl_tparam(yd, ly-1));
        assert(ylen && jl_is_typevar(ylen));
        jl_varbinding_t *yb = lookup(e, (jl_tvar_t*)ylen);
        if (yb && yb->intersected && yb->max_offset > 0) {
            assert(yb->max_offset <= 32);
            lly += yb->max_offset;
        }
    }

    if ((vvx == JL_VARARG_NONE || vvx == JL_VARARG_INT) &&
        (vvy == JL_VARARG_NONE || vvy == JL_VARARG_INT)) {
        if (llx != lly)
            return jl_bottom_type;
    }

    size_t np = llx > lly ? llx : lly;
    jl_value_t *res = NULL;
    jl_svec_t *p = NULL;
    jl_value_t **params;
    jl_value_t **roots;
    JL_GC_PUSHARGS(roots, np < 64 ? np : 1);
    if (np < 64) {
        params = roots;
    }
    else {
        p = jl_alloc_svec(np);
        roots[0] = (jl_value_t*)p;
        params = jl_svec_data(p);
    }
    size_t i=0, j=0;
    jl_value_t *xi, *yi;
    int isx = 1, isy = 1; // try to reuse the object x or y as res whenever we can (e.g. when it is the supertype) instead of allocating a copy
    while (1) {
        vx = vy = 0;
        xi = i < llx ? jl_tparam(xd, i < lx ? i : lx - 1) : NULL;
        yi = j < lly ? jl_tparam(yd, j < ly ? j : ly - 1) : NULL;
        if (xi == NULL && yi == NULL) {
            assert(i == j && i == np);
            break;
        }
        if (xi && jl_is_vararg(xi)) vx = vvx == JL_VARARG_UNBOUND || (vvx == JL_VARARG_BOUND && i == llx - 1);
        if (yi && jl_is_vararg(yi)) vy = vvy == JL_VARARG_UNBOUND || (vvy == JL_VARARG_BOUND && j == lly - 1);
        if (xi == NULL || yi == NULL) {
            if (vx && intersect_vararg_length(xi, lly+1-llx, e, 0)) {
                np = j;
                p = NULL;
            }
            else if (vy && intersect_vararg_length(yi, llx+1-lly, e, 1)) {
                np = i;
                p = NULL;
            }
            else {
                res = jl_bottom_type;
            }
            break;
        }
        jl_value_t *ii = NULL;
        if (vx && vy) {
            ii = intersect_varargs((jl_vararg_t*)xi,
                                   (jl_vararg_t*)yi,
                                   lly - llx, // xi's offset: {A^n...,Vararg{T,N}} ∩ {Vararg{S,M}}
                                            // {(A∩S)^n...,Vararg{T∩S,N}} plus N = M-n
                                   e,
                                   param);
        }
        else {
            ii = intersect(jl_is_vararg(xi) ? jl_unwrap_vararg(xi) : xi,
                           jl_is_vararg(yi) ? jl_unwrap_vararg(yi) : yi,
                           e,
                           param == PARAM_NONE ? PARAM_COVARIANT : param);
        }
        if (ii == jl_bottom_type) {
            if (vx && vy) {
                jl_varbinding_t *xb=NULL, *yb=NULL;
                jl_value_t *xlen = jl_unwrap_vararg_num(xi);
                assert(xlen == NULL || jl_is_typevar(xlen));
                if (xlen) xb = lookup(e, (jl_tvar_t*)xlen);
                jl_value_t *ylen = jl_unwrap_vararg_num(yi);
                assert(ylen == NULL || jl_is_typevar(ylen));
                if (ylen) yb = lookup(e, (jl_tvar_t*)ylen);
                int len = i > j ? i : j;
                if ((xb && jl_is_long(xb->lb) && llx-1+jl_unbox_long(xb->lb) != len) ||
                    (yb && jl_is_long(yb->lb) && lly-1+jl_unbox_long(yb->lb) != len)) {
                    res = jl_bottom_type;
                }
                else {
                    assert(e->Loffset == 0);
                    if (xb) set_var_to_const(xb, jl_box_long(len-llx+1), e, 0);
                    if (yb) set_var_to_const(yb, jl_box_long(len-lly+1), e, 1);
                    np = len;
                    p = NULL;
                }
            }
            else {
                res = jl_bottom_type;
            }
            break;
        }
        isx = isx && ii == xi;
        isy = isy && ii == yi;
        if (p)
            jl_svecset(p, (i > j ? i : j), ii);
        else
            params[i > j ? i : j] = ii;
        if (vx && vy)
            break;
        if (!vx) i++;
        if (!vy) j++;
    }
    // TODO: handle Vararg with explicit integer length parameter
    if (res == NULL) {
        assert(!p || np == jl_svec_len(p));
        isx = isx && lx == np;
        isy = isy && ly == np;
        if (!isx && !isy) {
            // do a more careful check now for equivalence
            if (lx == np) {
                isx = 1;
                for (i = 0; i < np; i++)
                    isx = isx && obviously_egal(params[i], jl_tparam(xd, i));
            }
            if (!isx && ly == np) {
                isy = 1;
                for (i = 0; i < np; i++)
                    isy = isy && obviously_egal(params[i], jl_tparam(yd, i));
            }
        }
        if (isx)
            res = (jl_value_t*)xd;
        else if (isy)
            res = (jl_value_t*)yd;
        else if (p)
            res = jl_apply_tuple_type(p, 1);
        else
            res = jl_apply_tuple_type_v(params, np);
    }
    JL_GC_POP();
    return res;
}

static void flip_vars(jl_stenv_t *e)
{
    jl_varbinding_t *btemp = e->vars;
    while (btemp != NULL) {
        btemp->existential = !btemp->existential;
        btemp = btemp->prev;
    }
}

// intersection where xd nominally inherits from yd
static jl_value_t *intersect_sub_datatype(jl_datatype_t *xd, jl_datatype_t *yd, jl_stenv_t *e, int R, jl_param_pos_t param)
{
    // attempt to populate additional constraints into `e`
    // if that attempt fails, then return bottom
    // otherwise return xd (finish_unionall will later handle propagating those constraints)
    assert(e->Loffset == 0);
    jl_value_t *isuper = R ? intersect((jl_value_t*)yd, (jl_value_t*)xd->super, e, param) :
                             intersect((jl_value_t*)xd->super, (jl_value_t*)yd, e, param);
    if (isuper == jl_bottom_type)
        return jl_bottom_type;
    return (jl_value_t*)xd;
}

static jl_value_t *intersect_invariant(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
{
    if (e->Loffset == 0 && !jl_has_free_typevars(x) && !jl_has_free_typevars(y)) {
        return (jl_subtype(x,y) && jl_subtype(y,x)) ? y : NULL;
    }
    e->invdepth++;
    jl_value_t *ii = intersect(x, y, e, PARAM_INVARIANT);
    e->invdepth--;
    if (jl_is_typevar(x) && jl_is_typevar(y) && jl_is_typevar(ii))
        return ii; // skip the following check due to possible circular constraints.
    if (ii == jl_bottom_type) {
        if (!subtype_in_env(x, jl_bottom_type, e))
            return NULL;
        flip_vars(e); flip_offset(e);
        if (!subtype_in_env(y, jl_bottom_type, e)) {
            flip_vars(e); flip_offset(e);
            return NULL;
        }
        flip_vars(e); flip_offset(e);
        return jl_bottom_type;
    }
    jl_savedenv_t se;
    JL_GC_PUSH1(&ii);
    save_env(e, &se, 1);
    if (!subtype_in_env_existential(x, y, e))
        ii = NULL;
    else {
        restore_env(e, &se, 1);
        flip_offset(e);
        if (!subtype_in_env_existential(y, x, e))
            ii = NULL;
        flip_offset(e);
    }
    restore_env(e, &se, 1);
    free_env(&se);
    JL_GC_POP();
    return ii;
}

// intersection where x == Type{...} and y is not
static jl_value_t *intersect_type_type(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, int8_t R)
{
    assert(e->Loffset == 0);
    jl_value_t *p0 = jl_typeeq_T(x);
    if (!jl_is_typevar(p0))
        return (jl_typeof(p0) == y) ? x : jl_bottom_type;
    if (!is_kind_or_anytype(y)) return jl_bottom_type;
    if (y == (jl_value_t*)jl_typeofbottom_type && ((jl_tvar_t*)p0)->lb == jl_bottom_type)
        return (jl_value_t*)jl_wrap_Type(jl_bottom_type);
    if (((jl_tvar_t*)p0)->ub == (jl_value_t*)jl_any_type)
        return y;
    return x;
    /*
    jl_value_t *ii = R ? intersect_invariant(y, jl_tparam0(x), e) : intersect_invariant(jl_tparam0(x), y, e);
    // NOTE: we cannot express e.g. DataType ∩ (UnionAll T<:Integer Type{T}), so returning `x`
    // here is a conservative over-estimate.
    if (ii == NULL || ii == jl_bottom_type) return x;
    if (ii == y) return ii;
    return (jl_value_t*)jl_wrap_Type(ii);
    */
}

// cmp <= 0: is x already <= y in this environment
// cmp >= 0: is x already >= y in this environment
static int compareto_var(jl_value_t *x, jl_tvar_t *y, jl_stenv_t *e, int cmp) JL_NOTSAFEPOINT
{
    if (x == (jl_value_t*)y)
        return 1;
    if (!jl_is_typevar(x))
        return 0;
    int innervar = 0;
    jl_varbinding_t *xv = lookup_binding(e, (jl_tvar_t*)x, &innervar);
    if (xv == NULL && !innervar)
        return 0;
    int ans = 1;
    if (cmp <= 0)
        ans &= compareto_var(xv ? xv->ub : ((jl_tvar_t*)x)->ub, y, e, cmp);
    if (cmp >= 0)
        ans &= compareto_var(xv ? xv->lb : ((jl_tvar_t*)x)->lb, y, e, cmp);
    return ans;
}

// Check whether the environment already asserts x <: y via recorded bounds.
// This is used to avoid adding redundant constraints that lead to cycles.
// Note this is a semi-predicate: 1 => is a subtype, 0 => unknown
static int subtype_by_bounds(jl_value_t *x, jl_value_t *y, jl_stenv_t *e) JL_NOTSAFEPOINT
{
    if (!jl_is_typevar(x) || !jl_is_typevar(y))
        return 0;
    return compareto_var(x, (jl_tvar_t*)y, e, -1) || compareto_var(y, (jl_tvar_t*)x, e, 1);
}

static int intersect_var_ccheck_in_env(jl_value_t *xlb, jl_value_t *xub, jl_value_t *ylb, jl_value_t *yub, jl_stenv_t *e, int flip)
{
    int easy_check1 = xlb == jl_bottom_type ||
                      yub == (jl_value_t *)jl_any_type ||
                      (e->Loffset == 0 && obviously_in_union(yub, xlb));
    int easy_check2 = ylb == jl_bottom_type ||
                      xub == (jl_value_t *)jl_any_type ||
                      (e->Loffset == 0 && obviously_in_union(xub, ylb));
    int nofree1 = 0, nofree2 = 0;
    if (!easy_check1) {
        nofree1 = !jl_has_free_typevars(xlb) && !jl_has_free_typevars(yub);
        if (nofree1 && e->Loffset == 0) {
            easy_check1 = jl_subtype(xlb, yub);
            if (!easy_check1)
                return 0;
        }
    }
    if (!easy_check2) {
        nofree2 = !jl_has_free_typevars(ylb) && !jl_has_free_typevars(xub);
        if (nofree2 && e->Loffset == 0) {
            easy_check2 = jl_subtype(ylb, xub);
            if (!easy_check2)
                return 0;
        }
    }
    if (easy_check1 && easy_check2)
        return 1;
    int ccheck = 0;
    if ((easy_check1 || nofree1) && (easy_check2 || nofree2)) {
        jl_varbinding_t *vars = e->vars;
        e->vars = NULL;
        ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
        if (ccheck && !easy_check2) {
            flip_offset(e);
            ccheck = subtype_in_env(ylb, xub, e);
            flip_offset(e);
        }
        e->vars = vars;
        return ccheck;
    }
    jl_savedenv_t se;
    save_env(e, &se, 1);
    // first try normal flip.
    if (flip) flip_vars(e);
    ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
    if (ccheck && !easy_check2) {
        flip_offset(e);
        ccheck = subtype_in_env(ylb, xub, e);
        flip_offset(e);
    }
    if (flip) flip_vars(e);
    if (!ccheck) {
        // then try reverse flip.
        restore_env(e, &se, 1);
        if (!flip) flip_vars(e);
        ccheck = easy_check1 || subtype_in_env(xlb, yub, e);
        if (ccheck && !easy_check2) {
            flip_offset(e);
            ccheck = subtype_in_env(ylb, xub, e);
            flip_offset(e);
        }
        if (!flip) flip_vars(e);
    }
    if (!ccheck) {
        // then try existential.
        restore_env(e, &se, 1);
        if (easy_check1)
            ccheck = 1;
        else {
            ccheck = subtype_in_env_existential(xlb, yub, e);
            restore_env(e, &se, 1);
        }
        if (ccheck && !easy_check2) {
            flip_offset(e);
            ccheck = subtype_in_env_existential(ylb, xub, e);
            flip_offset(e);
            restore_env(e, &se, 1);
        }
    }
    free_env(&se);
    return ccheck;
}

static int has_typevar_via_env(jl_value_t *x, jl_tvar_t *t, jl_stenv_t *e)
{
    if (e->Loffset == 0) {
        jl_varbinding_t *temp = e->vars;
        while (temp != NULL) {
            if (temp->var == t)
                break;
            if (temp->lb == temp->ub &&
                temp->lb == (jl_value_t *)t &&
                jl_has_typevar(x, temp->var))
                return 1;
            temp = temp->prev;
        }
    }
    return jl_has_typevar(x, t);
}

static jl_value_t *intersect(jl_value_t *x, jl_value_t *y, jl_stenv_t *e, jl_param_pos_t param)
{
    if (x == y) return y;
    if (jl_is_typevar(x)) {
        if (jl_is_typevar(y)) {
            int xinner = 0, yinner = 0;
            jl_varbinding_t *xx = lookup_binding(e, (jl_tvar_t*)x, &xinner);
            jl_varbinding_t *yy = lookup_binding(e, (jl_tvar_t*)y, &yinner);
            int xfree_singleton = xx == NULL && !xinner;
            int yfree_singleton = yy == NULL && !yinner;
            if (xfree_singleton && yfree_singleton)
                return jl_bottom_type;
            int R = 0;
            if (xx && yy && var_outside(e, (jl_tvar_t*)x, (jl_tvar_t*)y)) {
                // to preserve variable identities correctly, always accumulate bounds
                // on the outer variable, return the outer variable, and set the inner
                // variable equal to the outer variable.
                jl_value_t *temp; jl_varbinding_t *tvb;
                temp = x; x = y; y = temp;
                tvb = xx; xx = yy; yy = tvb;
                R = 1;
            }
            if (param == PARAM_INVARIANT) {
                jl_value_t *xlb = xx ? xx->lb : xinner ? ((jl_tvar_t*)x)->lb : x;
                jl_value_t *xub = xx ? xx->ub : xinner ? ((jl_tvar_t*)x)->ub : x;
                jl_value_t *ylb = yy ? yy->lb : yinner ? ((jl_tvar_t*)y)->lb : y;
                jl_value_t *yub = yy ? yy->ub : yinner ? ((jl_tvar_t*)y)->ub : y;
                if (xx && yy && xx->depth0 != yy->depth0) {
                    record_var_occurrence(xx, e, param);
                    record_var_occurrence(yy, e, param);
                    return subtype_in_env(yy->ub, yy->lb, e) ? y : jl_bottom_type;
                }
                if (xub == xlb && jl_is_typevar(xub) && xub != x) {
                    record_var_occurrence(xx, e, param);
                    if (y == xub) {
                        record_var_occurrence(yy, e, param);
                        return y;
                    }
                    if (R) flip_offset(e);
                    jl_value_t *res = intersect(xub, y, e, param);
                    if (R) flip_offset(e);
                    return res;
                }
                if (yub == ylb && jl_is_typevar(yub) && yub != y) {
                    record_var_occurrence(yy, e, param);
                    if (R) flip_offset(e);
                    jl_value_t *res = intersect(x, yub, e, param);
                    if (R) flip_offset(e);
                    return res;
                }
                record_var_occurrence(xx, e, param);
                record_var_occurrence(yy, e, param);
                int xoffset = R ? -e->Loffset : e->Loffset;
                if (!jl_is_type(ylb) && !jl_is_typevar(ylb)) {
                    if (xx)
                        return set_var_to_const(xx, ylb, e, R);
                    if ((xlb == jl_bottom_type && xub == (jl_value_t*)jl_any_type) || jl_egal(xlb, ylb)) {
                        if (xoffset == 0)
                            return ylb;
                        else if (jl_is_long(ylb)) {
                            if (xoffset > 0)
                                return ylb;
                            else
                                return jl_box_long(jl_unbox_long(ylb) + xoffset);
                        }
                    }
                    return jl_bottom_type;
                }
                if (!jl_is_type(xlb) && !jl_is_typevar(xlb)) {
                    if (yy)
                        return set_var_to_const(yy, xlb, e, !R);
                    if (ylb == jl_bottom_type && yub == (jl_value_t*)jl_any_type) {
                        if (xoffset == 0)
                            return xlb;
                        else if (jl_is_long(xlb)) {
                            if (xoffset < 0)
                                return xlb;
                            else
                                return jl_box_long(jl_unbox_long(ylb) - xoffset);
                        }
                    }
                    return jl_bottom_type;
                }
                int ccheck;
                if (R) flip_offset(e);
                if (xlb == xub && ylb == yub &&
                    jl_has_typevar(xlb, (jl_tvar_t *)y) &&
                    jl_has_typevar(ylb, (jl_tvar_t *)x)) {
                    // special case for e.g.
                    // 1) Val{Y}<:X<:Val{Y} && Val{X}<:Y<:Val{X}
                    // 2) Y<:X<:Y && Val{X}<:Y<:Val{X} => Val{Y}<:Y<:Val{Y}
                    ccheck = 0;
                }
                else if (yub == xub ||
                    (subtype_by_bounds(xlb, yub, e) && subtype_by_bounds(ylb, xub, e))) {
                    ccheck = 1;
                }
                else {
                    // try many subtype check to avoid false `Union{}`
                    ccheck = intersect_var_ccheck_in_env(xlb, xub, ylb, yub, e, R);
                }
                if (R) flip_offset(e);
                if (!ccheck)
                    return jl_bottom_type;
                if ((has_typevar_via_env(xub, (jl_tvar_t*)y, e) || has_typevar_via_env(xub, (jl_tvar_t*)x, e)) &&
                    (has_typevar_via_env(yub, (jl_tvar_t*)x, e) || has_typevar_via_env(yub, (jl_tvar_t*)y, e))) {
                    // TODO: This doesn't make much sense.
                    // circular constraint. the result will be Bottom, but in the meantime
                    // we need to avoid computing intersect(xub, yub) since it won't terminate.
                    return y;
                }
                jl_value_t *ub=NULL, *lb=NULL;
                JL_GC_PUSH2(&lb, &ub);
                int d = xx ? xx->depth0 : yy ? yy->depth0 : 0;
                ub = R ? intersect_aside(yub, xub, e, d) : intersect_aside(xub, yub, e, d);
                if (reachable_var(xlb, (jl_tvar_t*)y, e))
                    lb = ylb;
                else
                    lb = simple_join(xlb, ylb);
                if (yy && xoffset == 0) {
                    yy->lb = lb;
                    if (!reachable_var(ub, (jl_tvar_t*)y, e))
                        yy->ub = ub;
                    assert(yy->ub != y);
                    assert(yy->lb != y);
                }
                if (xx && xoffset == 0 && !reachable_var(y, (jl_tvar_t*)x, e)) {
                    xx->lb = y;
                    xx->ub = y;
                    assert(xx->ub != x);
                }
                JL_GC_POP();
                // Here we always return the shorter `Vararg`'s length.
                return xoffset < 0 ? x : y;
            }
            assert(e->Loffset == 0);
            record_var_occurrence(xx, e, param);
            record_var_occurrence(yy, e, param);
            if (xx && yy && xx->concrete && !yy->concrete) {
                return intersect_var((jl_tvar_t*)x, y, e, R, param);
            }
            return intersect_var((jl_tvar_t*)y, x, e, !R, param);
        }
        record_var_occurrence(lookup(e, (jl_tvar_t*)x), e, param);
        return intersect_var((jl_tvar_t*)x, y, e, 0, param);
    }
    if (jl_is_typevar(y)) {
        record_var_occurrence(lookup(e, (jl_tvar_t*)y), e, param);
        return intersect_var((jl_tvar_t*)y, x, e, 1, param);
    }
    if (e->Loffset == 0 && !jl_has_free_typevars(x) && !jl_has_free_typevars(y)) {
        if (jl_subtype(x, y)) return x;
        if (jl_subtype(y, x)) return y;
    }
    if (jl_is_uniontype(x)) {
        if (obviously_in_union(x, y))
            return y;
        if (jl_is_uniontype(y) && obviously_in_union(y, x))
            return x;
        return intersect_union(y, (jl_uniontype_t*)x, e, 0, param);
    }
    if (jl_is_uniontype(y)) {
        if (obviously_in_union(y, x))
            return x;
        if (jl_is_unionall(x) && (jl_has_free_typevars(x) || jl_has_free_typevars(y)))
            return intersect_unionall(y, (jl_unionall_t*)x, e, 0, param);
        return intersect_union(x, (jl_uniontype_t*)y, e, 1, param);
    }
    if (y == (jl_value_t*)jl_any_type) return x;
    if (x == (jl_value_t*)jl_any_type) return y;
    if (jl_is_unionall(x)) {
        if (jl_is_unionall(y)) {
            jl_value_t *a=NULL, *b=jl_bottom_type, *res=NULL;
            JL_GC_PUSH2(&a, &b);
            jl_savedenv_t se;
            save_env(e, &se, 0);
            a = intersect_unionall(y, (jl_unionall_t*)x, e, 0, param);
            if (jl_is_unionall(a)) {
                jl_unionall_t *ua = (jl_unionall_t*)a;
                if (jl_is_unionall(ua->body)) {
                    jl_unionall_t *ub = (jl_unionall_t*)ua->body;
                    if (jl_has_typevar(ub->var->ub, ua->var) ||
                        jl_has_typevar(ub->var->lb, ua->var)) {
                        restore_env(e, &se, 0); // restore counts
                        b = intersect_unionall(x, (jl_unionall_t*)y, e, 1, param);
                    }
                }
            }
            free_env(&se);
            if (!jl_has_free_typevars(a) && !jl_has_free_typevars(b)) {
                if (jl_subtype(a, b))
                    res = b;
                else if (jl_subtype(b, a))
                    res = a;
            }
            if (!res) res = simple_join(a, b);
            JL_GC_POP();
            return res;
        }
        return intersect_unionall(y, (jl_unionall_t*)x, e, 0, param);
    }
    if (jl_is_unionall(y))
        return intersect_unionall(x, (jl_unionall_t*)y, e, 1, param);
    if (jl_is_typeeq(x) && jl_is_typeeq(y)) {
        jl_value_t *xp = jl_typeeq_T(x);
        jl_value_t *yp = jl_typeeq_T(y);
        jl_value_t *ii = intersect_invariant(xp, yp, e);
        if (ii == NULL)
            return jl_bottom_type;
        JL_GC_PUSH1(&ii);
        jl_value_t *ans = (jl_value_t*)jl_wrap_Type(ii);
        JL_GC_POP();
        return ans;
    }
    if (param != PARAM_INVARIANT) {
        if (jl_is_typeeq(x))
            return intersect_type_type(x, y, e, 0);
        if (jl_is_typeeq(y))
            return intersect_type_type(y, x, e, 1);
    }
    if (jl_is_datatype(x) && jl_is_datatype(y)) {
        jl_datatype_t *xd = (jl_datatype_t*)x, *yd = (jl_datatype_t*)y;
        if (param != PARAM_INVARIANT) {
            if (jl_is_typeeq(x)) {
                if (!jl_is_typeeq(y))
                    return intersect_type_type(x, y, e, 0);
            }
            else if (jl_is_typeeq(y)) {
                return intersect_type_type(y, x, e, 1);
            }
        }
        if (xd->name == yd->name) {
            if (jl_is_tuple_type(xd))
                return intersect_tuple(xd, yd, e, param);
            size_t i, np = jl_nparams(xd);
            jl_value_t **newparams;
            JL_GC_PUSHARGS(newparams, np);
            int isx = 1, isy = 1; // try to reuse the object x or y as res whenever we can (e.g. when it is the supertype) instead of allocating a copy
            for (i = 0; i < np; i++) {
                jl_value_t *xi = jl_tparam(xd, i), *yi = jl_tparam(yd, i);
                jl_value_t *ii = intersect_invariant(xi, yi, e);
                if (ii == NULL)
                    break;
                isx = isx && ii == xi;
                isy = isy && ii == yi;
                newparams[i] = ii;
            }
            jl_value_t *res = jl_bottom_type;
            if (i == np) {
                if (!isx && !isy) {
                    // do a more careful check now for equivalence
                    isx = 1;
                    for (i = 0; i < np; i++)
                        isx = isx && obviously_egal(newparams[i], jl_tparam(xd, i));
                    if (!isx) {
                        isy = 1;
                        for (i = 0; i < np; i++)
                            isy = isy && obviously_egal(newparams[i], jl_tparam(yd, i));
                    }
                }
                if (isx)
                    res = x;
                else if (isy)
                    res = y;
                else {
                    JL_TRY {
                        res = jl_apply_type(xd->name->wrapper, newparams, np);
                    }
                    JL_CATCH {
                        res = jl_bottom_type;
                    }
                }
            }
            JL_GC_POP();
            return res;
        }
        if (param == PARAM_INVARIANT) return jl_bottom_type;
        while (xd != jl_any_type && xd->name != yd->name)
            xd = xd->super;
        if (xd == jl_any_type) {
            xd = (jl_datatype_t*)x;
            while (yd != jl_any_type && yd->name != xd->name)
                yd = yd->super;
            if (yd == jl_any_type)
                return jl_bottom_type;
            return intersect_sub_datatype((jl_datatype_t*)y, xd, e, 1, param);
        }
        return intersect_sub_datatype((jl_datatype_t*)x, yd, e, 0, param);
    }
    if (jl_egal(x, y)) return y;
    return jl_bottom_type;
}

static int merge_env(jl_stenv_t *e, jl_savedenv_t *me, jl_savedenv_t *se, int count)
{
    if (count == 0) {
        save_env(e, me, 1);
        return 1;
    }
    jl_value_t **merged = NULL;
    jl_value_t **saved = NULL;
    int nroots = 0;
    assert(se->gcframe.nroots == me->gcframe.nroots);
    if (se->gcframe.nroots == JL_GC_ENCODE_PUSHARGS(1)) {
        jl_svec_t *sv = (jl_svec_t*)se->roots[0];
        assert(jl_is_svec(sv));
        saved = jl_svec_data(sv);
        nroots = jl_svec_len(sv);
        sv = (jl_svec_t*)me->roots[0];
        assert(jl_is_svec(sv));
        merged = jl_svec_data(sv);
        assert(nroots == jl_svec_len(sv));
    }
    else {
        saved = se->roots;
        merged = me->roots;
        nroots = JL_GC_DECODE_NROOTS(se->gcframe.nroots);
    }
    assert(nroots == current_env_length(e) * 3);
    assert(nroots % 3 == 0);
    int m = 0, n = 0;
    jl_varbinding_t *v = e->vars;
    while (v != NULL) {
        jl_value_t *b0, *b1, *b2;
        // merge `lb`
        b0 = saved[n];
        b1 = merged[n];
        JL_GC_PROMISE_ROOTED(b1); // clang-sagc doesn't know this came from our GC frame
        b2 = v->lb;
        JL_GC_PROMISE_ROOTED(b2); // clang-sagc doesn't know the fields of this are stack GC roots
        merged[n] = (b1 == b0 || b2 == b0) ? b0 : simple_meet(b1, b2, 0);
        // merge `ub`
        b0 = saved[n+1];
        b1 = merged[n+1];
        JL_GC_PROMISE_ROOTED(b1); // clang-sagc doesn't know this came from our GC frame
        b2 = v->ub;
        JL_GC_PROMISE_ROOTED(b2); // clang-sagc doesn't know the fields of this are stack GC roots
        merged[n+1] = (b1 == b0 || b2 == b0) ? b0 : simple_join(b1, b2);
        // merge `innervars`
        b1 = merged[n+2];
        JL_GC_PROMISE_ROOTED(b1); // clang-sagc doesn't know this came from our GC frame
        b2 = (jl_value_t*)v->innervars;
        JL_GC_PROMISE_ROOTED(b2); // clang-sagc doesn't know the fields of this are stack GC roots
        if (b2 && b1 != b2) {
            if (b1)
                jl_array_ptr_1d_append((jl_array_t*)b1, (jl_array_t*)b2);
            else
                merged[n+2] = b2;
        }
        // merge occurs_inv/cov/cov_diag by max (never decrease)
        if (v->occurs_inv > me->buf[m])
            me->buf[m] = v->occurs_inv;
        if (v->occurs_cov > me->buf[m+1])
            me->buf[m+1] = v->occurs_cov;
        if (v->cov_diag > me->buf[m+2])
            me->buf[m+2] = v->cov_diag;
        // merge max_offset by min
        if (!v->intersected && v->max_offset < me->buf[m+3])
            me->buf[m+3] = v->max_offset;
        m = m + JL_SAVEDENV_BYTES_PER_VAR;
        n = n + 3;
        v = v->prev;
    }
    assert(n == nroots); (void)nroots;
    return count + 1;
}

static jl_value_t *intersect_all(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
{
    e->Runions.depth = 0;
    e->Runions.more = 0;
    e->Runions.used = 0;
    jl_value_t **is;
    JL_GC_PUSHARGS(is, 2);
    jl_savedenv_t se, me;
    save_env(e, &se, 1);
    int niter = 0, total_iter = 0;
    is[0] = intersect(x, y, e, PARAM_NONE); // root
    if (is[0] == jl_bottom_type) {
        restore_env(e, &se, 1);
    }
    else if (!e->emptiness_only && has_next_union_state(e, 1)) {
        niter = merge_env(e, &me, &se, niter);
        restore_env(e, &se, 1);
    }
    while (next_union_state(e, 1)) {
        if (e->emptiness_only && is[0] != jl_bottom_type)
            break;
        e->Runions.depth = 0;
        e->Runions.more = 0;

        is[1] = intersect(x, y, e, PARAM_NONE);
        if (is[1] == jl_bottom_type) {
            restore_env(e, &se, 1);
        }
        else if (niter > 0 || (!e->emptiness_only && has_next_union_state(e, 1))) {
            niter = merge_env(e, &me, &se, niter);
            restore_env(e, &se, 1);
        }
        else {
            assert(is[0] == jl_bottom_type);
        }
        if (is[0] == jl_bottom_type)
            is[0] = is[1];
        else if (is[1] != jl_bottom_type) {
            // TODO: the repeated subtype checks in here can get expensive
            is[0] = jl_type_union(is, 2);
        }
        total_iter++;
        if (has_next_union_state(e, 1) && (niter > 4 || total_iter > 400000)) {
            is[0] = y;
            // we give up precise intersection here, just restore the saved env
            restore_env(e, &se, 1);
            if (niter > 0) {
                free_env(&me);
                niter = 0;
            }
            break;
        }
    }
    if (niter) {
        restore_env(e, &me, 1);
        free_env(&me);
    }
    free_env(&se);
    JL_GC_POP();
    return is[0];
}

// type intersection entry points

static jl_value_t *intersect_types(jl_value_t *x, jl_value_t *y, int emptiness_only)
{
    jl_stenv_t e;
    if (obviously_disjoint(x, y, 0))
        return jl_bottom_type;
    if (jl_is_dispatch_tupletype(x) || jl_is_dispatch_tupletype(y)) {
        if (jl_subtype(x, y))
            return x;
        else if (jl_subtype(y, x))
            return y;
        else
            return jl_bottom_type;
    }
    init_stenv(&e, NULL, 0);
    e.intersection = 1;
    e.emptiness_only = emptiness_only;
    jl_value_t *ans = intersect_all(x, y, &e);
    free_stenv(&e);
    return ans;
}

JL_DLLEXPORT jl_value_t *jl_intersect_types(jl_value_t *x, jl_value_t *y)
{
    return intersect_types(x, y, 0);
}

// TODO: this can probably be done more efficiently
JL_DLLEXPORT int jl_has_empty_intersection(jl_value_t *x, jl_value_t *y)
{
    return intersect_types(x, y, 1) == jl_bottom_type;
}

// return a SimpleVector of all vars from UnionAlls wrapping a given type
jl_svec_t *jl_outer_unionall_vars(jl_value_t *u)
{
    int ntvars = jl_subtype_env_size((jl_value_t*)u);
    jl_svec_t *vec = jl_alloc_svec_uninit(ntvars);
    jl_unionall_t *ua = (jl_unionall_t*)u;
    int i;
    for (i = 0; i < ntvars; i++) {
        assert(jl_is_unionall(ua));
        jl_svecset(vec, i, ua->var);
        ua = (jl_unionall_t*)ua->body;
    }
    return vec;
}

// For (possibly unions or unionalls of) tuples `a` and `b`, return the tuple of
// pointwise unions. Note that this may in general be wider than `Union{a,b}`.
// If `a` and `b` are not (non va-)tuples of equal length (or unions or unionalls
// of such), return NULL.
static jl_value_t *switch_union_tuple(jl_value_t *a, jl_value_t *b)
{
    if (jl_is_unionall(a)) {
        jl_unionall_t *ua = (jl_unionall_t*)a;
        if (jl_is_unionall(b)) {
            jl_unionall_t *ub = (jl_unionall_t*)b;
            if (ub->var->lb == ua->var->lb && ub->var->ub == ua->var->ub) {
                jl_value_t *ub2 = jl_instantiate_unionall(ub, (jl_value_t*)ua->var);
                jl_value_t *ans = NULL;
                JL_GC_PUSH2(&ub2, &ans);
                ans = switch_union_tuple(ua->body, ub2);
                if (ans != NULL)
                    ans = jl_type_unionall(ua->var, ans);
                JL_GC_POP();
                return ans;
            }
        }
        jl_value_t *ans = switch_union_tuple(ua->body, b);
        if (ans == NULL)
            return NULL;
        JL_GC_PUSH1(&ans);
        ans = jl_type_unionall(ua->var, ans);
        JL_GC_POP();
        return ans;
    }
    if (jl_is_unionall(b)) {
        jl_value_t *ans = switch_union_tuple(a, ((jl_unionall_t*)b)->body);
        if (ans == NULL)
            return NULL;
        JL_GC_PUSH1(&ans);
        ans = jl_type_unionall(((jl_unionall_t*)b)->var, ans);
        JL_GC_POP();
        return ans;
    }
    if (jl_is_uniontype(a)) {
        a = switch_union_tuple(((jl_uniontype_t*)a)->a, ((jl_uniontype_t*)a)->b);
        if (a == NULL)
            return NULL;
        JL_GC_PUSH1(&a);
        jl_value_t *ans = switch_union_tuple(a, b);
        JL_GC_POP();
        return ans;
    }
    if (jl_is_uniontype(b)) {
        b = switch_union_tuple(((jl_uniontype_t*)b)->a, ((jl_uniontype_t*)b)->b);
        if (b == NULL)
            return NULL;
        JL_GC_PUSH1(&b);
        jl_value_t *ans = switch_union_tuple(a, b);
        JL_GC_POP();
        return ans;
    }
    if (!jl_is_tuple_type(a) || !jl_is_tuple_type(b)) {
        return NULL;
    }
    if (jl_nparams(a) != jl_nparams(b) || jl_is_va_tuple((jl_datatype_t*)a) ||
            jl_is_va_tuple((jl_datatype_t*)b)) {
        return NULL;
    }
    jl_svec_t *vec = jl_alloc_svec(jl_nparams(a));
    JL_GC_PUSH1(&vec);
    for (int i = 0; i < jl_nparams(a); i++) {
        jl_value_t *ts[2];
        ts[0] = jl_tparam(a, i);
        ts[1] = jl_tparam(b, i);
        jl_svecset(vec, i, jl_type_union(ts, 2));
    }
    jl_value_t *ans = jl_apply_tuple_type(vec, 1);
    JL_GC_POP();
    return ans;
}

// `a` might have a non-empty intersection with some concrete type b even if !(a<:b) and !(b<:a)
// For example a=`Tuple{Type{<:Vector}}` and b=`Tuple{DataType}`
// TODO: this query is partly available memoized as jl_type_equality_is_identity
static int might_intersect_concrete(jl_value_t *a) JL_NOTSAFEPOINT
{
    if (jl_is_unionall(a))
        a = jl_unwrap_unionall(a);
    if (jl_is_typevar(a))
        return 1; // (maybe)
    if (jl_is_uniontype(a))
        return might_intersect_concrete(((jl_uniontype_t*)a)->a) ||
               might_intersect_concrete(((jl_uniontype_t*)a)->b);
    if (jl_is_vararg(a))
        return might_intersect_concrete(jl_unwrap_vararg(a));
    if (jl_is_typeeq(a))
        return 1;
    if (jl_is_datatype(a)) {
        int tpl = jl_is_tuple_type(a);
        int i, n = jl_nparams(a);
        for (i = 0; i < n; i++) {
            jl_value_t *p = jl_tparam(a, i);
            if (jl_is_typevar(p))
                return 1;
            if (tpl && p == jl_bottom_type)
                return 1;
            if (tpl && might_intersect_concrete(p))
                return 1;
        }
    }
    return 0;
}

// sets *issubty to 1 iff `a` is a subtype of `b`
jl_value_t *jl_type_intersection_env_s(jl_value_t *a, jl_value_t *b, jl_svec_t **penv, int *issubty)
{
    if (issubty) *issubty = 0;
    if (obviously_disjoint(a, b, 0)) {
        if (issubty && a == jl_bottom_type) *issubty = 1;
        return jl_bottom_type;
    }
    if (jl_is_typeapp(a) || jl_is_typeapp(b))
        jl_error("internal error: TypeApp in type intersection");
    int szb = jl_subtype_env_size(b);
    int sz = 0, i = 0;
    jl_value_t **env, **ans;
    JL_GC_PUSHARGS(env, szb+1);
    ans = &env[szb];
    *ans = jl_bottom_type;
    int lta = jl_is_concrete_type(a);
    int ltb = jl_is_concrete_type(b);
    if (jl_subtype_env(a, b, env, szb)) {
        *ans = a; sz = szb;
        if (issubty) *issubty = 1;
    }
    // else if (lta && ltb) { // !jl_type_equality_is_identity known in this case because obviously_disjoint returned false
    //     goto bot;
    // }
    else if (jl_subtype(b, a)) {
        *ans = b;
    }
    else {
        // TODO: these tests could probably be ordered better with above
        if (lta && !might_intersect_concrete(b))
            goto bot;
        if (ltb && !might_intersect_concrete(a))
            goto bot;
        jl_stenv_t e;
        init_stenv(&e, NULL, 0);
        e.intersection = 1;
        e.envout = env;
        if (szb)
            memset(env, 0, szb*sizeof(void*));
        e.envsz = szb;
        *ans = intersect_all(a, b, &e);
        free_stenv(&e);
        if (*ans == jl_bottom_type) goto bot;
        // TODO: code dealing with method signatures is not able to handle unions, so if
        // `a` and `b` are both tuples, we need to be careful and may not return a union,
        // even if `intersect` produced one
        if (jl_is_tuple_type(jl_unwrap_unionall(a)) && jl_is_tuple_type(jl_unwrap_unionall(b)) &&
            !jl_is_datatype(jl_unwrap_unionall(*ans))) {
            jl_value_t *ans_unwrapped = jl_unwrap_unionall(*ans);
            JL_GC_PUSH1(&ans_unwrapped);
            if (jl_is_uniontype(ans_unwrapped)) {
                ans_unwrapped = switch_union_tuple(((jl_uniontype_t*)ans_unwrapped)->a, ((jl_uniontype_t*)ans_unwrapped)->b);
                if (ans_unwrapped != NULL) {
                    *ans = jl_rewrap_unionall_(ans_unwrapped, *ans);
                }
            }
            JL_GC_POP();
            if (!jl_is_datatype(jl_unwrap_unionall(*ans))) {
                // Bail: caller can't handle a non-datatype here. The env computed
                // by `intersect` is meaningless after this assignment, but the
                // subtype call below recovers a usable env via the `x == y` fast
                // path in `jl_subtype_env` (typevars from `b`).
                *ans = b;
            }
        }
        sz = szb;
        // TODO: compute better `env` directly during intersection.
        // for now, we attempt to compute env by using subtype on the intersection result
        if (szb > 0 && !jl_types_equal(b, (jl_value_t*)jl_type_type)) {
            if (!jl_subtype_env(*ans, b, env, szb)) {
                sz = 0;
            }
        }
    }
    if (sz > 0 && szb > 0) {
        for (i = 0; i < sz; i++) {
            if (!env[i]) {
                sz = 0;
                break;
            }
        }
    }
    if (sz == 0 && szb > 0) {
        jl_unionall_t *ub = (jl_unionall_t*)b;
        while (jl_is_unionall(ub)) {
            int constrained = constrains_param_static(ub->var, ub->body, 1);
            env[i++] = wrap_tvar_env((jl_value_t*)ub->var, constrained);
            ub = (jl_unionall_t*)ub->body;
        }
        sz = szb;
    }
    if (penv) {
        jl_svec_t *e = jl_alloc_svec(sz);
        for (i = 0; i < sz; i++) {
            assert(env[i]);
            jl_svecset(e, i, env[i]);
        }
        *penv = e;
    }
 bot:
    JL_GC_POP();
    return *ans;
}

jl_value_t *jl_type_intersection_env(jl_value_t *a, jl_value_t *b, jl_svec_t **penv)
{
    return jl_type_intersection_env_s(a, b, penv, NULL);
}

JL_DLLEXPORT jl_value_t *jl_type_intersection(jl_value_t *a, jl_value_t *b)
{
    return jl_type_intersection_env(a, b, NULL);
}

JL_DLLEXPORT jl_svec_t *jl_type_intersection_with_env(jl_value_t *a, jl_value_t *b)
{
    jl_svec_t *env = jl_emptysvec;
    jl_value_t *ti = NULL;
    JL_GC_PUSH2(&env, &ti);
    ti = jl_type_intersection_env(a, b, &env);
    jl_svec_t *pair = jl_svec2(ti, env);
    JL_GC_POP();
    return pair;
}

int jl_subtype_matching(jl_value_t *a, jl_value_t *b, jl_svec_t **penv)
{
    int szb = penv ? jl_subtype_env_size(b) : 0;
    if (szb == 0)
        return jl_subtype_env(a, b, NULL, szb);

    jl_value_t **env;
    JL_GC_PUSHARGS(env, szb);
    int sub = jl_subtype_env(a, b, env, szb);
    if (sub) {
        // copy env to svec for return
        int i = 0;
        jl_svec_t *e = jl_alloc_svec(szb);
        for (i = 0; i < szb; i++) {
            assert(env[i]);
            jl_svecset(e, i, env[i]);
        }
        *penv = e;
    }
    JL_GC_POP();
    return sub;
}

// type utils
static void check_diagonal(jl_value_t *t, jl_varbinding_t *troot, jl_param_pos_t param)
{
    if (jl_is_uniontype(t)) {
        int i, len = 0;
        jl_varbinding_t *v;
        for (v = troot; v != NULL; v = v->prev)
            len++;
        // 3 bytes per var: [occurs_inv, occurs_cov, cov_diag].
        int8_t *occurs = (int8_t *)alloca(len * 3);
        for (v = troot, i = 0; v != NULL; v = v->prev, i++) {
            occurs[i*3]   = v->occurs_inv;
            occurs[i*3+1] = v->occurs_cov;
            occurs[i*3+2] = v->cov_diag;
        }
        jl_value_t *a = ((jl_uniontype_t *)t)->a;
        check_diagonal(a, troot, param);
        for (v = troot, i = 0; v != NULL; v = v->prev, i++) {
            int8_t a_inv = v->occurs_inv;
            int8_t a_cov = v->occurs_cov;
            int8_t a_diag = v->cov_diag;
            v->occurs_inv = occurs[i*3];
            v->occurs_cov = occurs[i*3+1];
            v->cov_diag   = occurs[i*3+2];
            occurs[i*3]   = a_inv;
            occurs[i*3+1] = a_cov;
            occurs[i*3+2] = a_diag;
        }
        jl_value_t *b = ((jl_uniontype_t *)t)->b;
        check_diagonal(b, troot, param);
        for (v = troot, i = 0; v != NULL; v = v->prev, i++) {
            if (v->occurs_inv < occurs[i*3])
                v->occurs_inv = occurs[i*3];
            if (v->occurs_cov < occurs[i*3+1])
                v->occurs_cov = occurs[i*3+1];
            if (v->cov_diag  < occurs[i*3+2])
                v->cov_diag  = occurs[i*3+2];
        }
    }
    else if (jl_is_unionall(t)) {
        assert(troot != NULL);
        jl_varbinding_t *v1 = troot, *v2 = troot->prev;
        while (v2 != NULL) {
            if (v2->var == ((jl_unionall_t *)t)->var) {
                v1->prev = v2->prev;
                break;
            }
            v1 = v2;
            v2 = v2->prev;
        }
        jl_value_t *body = ((jl_unionall_t *)t)->body;
        check_diagonal(body, troot, param);
        v1->prev = v2;
    }
    else if (jl_is_typeeq(t)) {
        jl_value_t *T = jl_typeeq_T(t);
        check_diagonal(T, troot, PARAM_INVARIANT);
    }
    else if (jl_is_datatype(t)) {
        jl_param_pos_t nparam = jl_is_tuple_type(t) ? PARAM_COVARIANT : PARAM_INVARIANT;
        if (nparam < param) nparam = param;
        for (size_t i = 0; i < jl_nparams(t); i++) {
            jl_value_t *p = jl_tparam(t, i);
            check_diagonal(p, troot, nparam);
        }
    }
    else if (jl_is_vararg(t)) {
        jl_value_t *T = jl_unwrap_vararg(t);
        jl_value_t *N = jl_unwrap_vararg_num(t);
        int n = (N && jl_is_long(N)) ? jl_unbox_long(N) : 2;
        if (T && n > 0) check_diagonal(T, troot, param);
        if (T && n > 1) check_diagonal(T, troot, param);
        if (N)          check_diagonal(N, troot, PARAM_INVARIANT);
    }
    else if (jl_is_typevar(t)) {
        jl_varbinding_t *v = troot;
        for (; v != NULL; v = v->prev) {
            if (v->var == (jl_tvar_t *)t) {
                if (param == PARAM_COVARIANT && v->occurs_cov < 2) v->occurs_cov++;
                if (param == PARAM_INVARIANT && v->occurs_inv < 2) v->occurs_inv++;
                break;
            }
        }
        if (v == NULL) {
            jl_value_t *ub = ((jl_tvar_t *)t)->ub;
            check_diagonal(ub, troot, PARAM_NONE);
        }
    }
}

static jl_value_t *insert_nondiagonal(jl_value_t *type, jl_varbinding_t *troot, int widen2ub)
{
    if (jl_is_typevar(type)) {
        int concretekind = widen2ub > 1 ? 0 : 1;
        jl_varbinding_t *v = troot;
        for (; v != NULL; v = v->prev) {
            if (v->occurs_inv == 0 &&
                cov_count(v) > concretekind &&
                v->var == (jl_tvar_t *)type)
                break;
        }
        if (v != NULL) {
            if (widen2ub) {
                jl_value_t *ub = ((jl_tvar_t *)type)->ub;
                type = insert_nondiagonal(ub, troot, 2);
            }
            else {
                // we must replace each covariant occurrence of newvar with a different newvar2<:newvar (diagonal rule)
                if (v->innervars == NULL)
                    v->innervars = jl_alloc_array_1d(jl_array_any_type, 0);
                jl_value_t *newvar = NULL, *lb = v->var->lb, *ub = (jl_value_t *)v->var;
                jl_array_t *innervars = v->innervars;
                JL_GC_PUSH4(&newvar, &lb, &ub, &innervars);
                newvar = (jl_value_t *)jl_new_typevar(v->var->name, lb, ub);
                jl_array_ptr_1d_push(innervars, newvar);
                JL_GC_POP();
                type = newvar;
            }
        }
    }
    else if (jl_is_unionall(type)) {
        jl_value_t *body = ((jl_unionall_t*)type)->body;
        jl_tvar_t *var = ((jl_unionall_t*)type)->var;
        jl_varbinding_t *v = troot;
        for (; v != NULL; v = v->prev) {
            if (v->var == var)
                break;
        }
        if (v) v->var = NULL; // Temporarily remove `type->var` from binding list.
        jl_value_t *newbody = insert_nondiagonal(body, troot, widen2ub);
        if (v) v->var = var; // And restore it after inner insertation.
        jl_value_t *newvar = NULL;
        JL_GC_PUSH3(&newbody, &newvar, &type);
        if (body == newbody || jl_has_typevar(newbody, var)) {
            if (body != newbody)
                type = jl_new_struct(jl_unionall_type, var, newbody);
            // n.b. we do not widen lb, since that would be the wrong direction
            jl_value_t *ub = var->ub;
            newvar = insert_nondiagonal(ub, troot, widen2ub);
            if (newvar != ub) {
                jl_value_t *lb = var->lb;
                newvar = (jl_value_t*)jl_new_typevar(var->name, lb, newvar);
                newbody = jl_apply_type1(type, newvar);
                type = jl_type_unionall((jl_tvar_t*)newvar, newbody);
            }
        }
        JL_GC_POP();
    }
    else if (jl_is_uniontype(type)) {
        jl_value_t *a = ((jl_uniontype_t*)type)->a;
        jl_value_t *b = ((jl_uniontype_t*)type)->b;
        jl_value_t *newa = NULL;
        jl_value_t *newb = NULL;
        JL_GC_PUSH2(&newa, &newb);
        newa = insert_nondiagonal(a, troot, widen2ub);
        newb = insert_nondiagonal(b, troot, widen2ub);
        if (newa != a || newb != b)
            type = simple_union(newa, newb);
        JL_GC_POP();
    }
    else if (jl_is_vararg(type)) {
        // As for Vararg we'd better widen its var to ub as otherwise they are still diagonal
        jl_value_t *t = jl_unwrap_vararg(type);
        jl_value_t *n = jl_unwrap_vararg_num(type);
        if (widen2ub == 0)
            widen2ub = !(n && jl_is_long(n)) || jl_unbox_long(n) > 1;
        jl_value_t *newt = insert_nondiagonal(t, troot, widen2ub);
        if (t != newt) {
            JL_GC_PUSH1(&newt);
            type = (jl_value_t *)jl_wrap_vararg(newt, n, 0, 0);
            JL_GC_POP();
        }
    }
    else if (jl_is_typeeq(type)) {
        jl_value_t *T = jl_typeeq_T(type);
        jl_value_t *newT = insert_nondiagonal(T, troot, 1);
        if (T != newT) {
            JL_GC_PUSH1(&newT);
            type = (jl_value_t*)jl_wrap_Type(newT);
            JL_GC_POP();
        }
    }
    else if (jl_is_datatype(type)) {
        if (jl_is_tuple_type(type)) {
            jl_svec_t *newparams = NULL;
            jl_value_t *newelt = NULL;
            JL_GC_PUSH2(&newparams, &newelt);
            for (size_t i = 0; i < jl_nparams(type); i++) {
                jl_value_t *elt = jl_tparam(type, i);
                newelt = insert_nondiagonal(elt, troot, widen2ub);
                if (elt != newelt) {
                    if (!newparams)
                        newparams = jl_svec_copy(((jl_datatype_t*)type)->parameters);
                    jl_svecset(newparams, i, newelt);
                }
            }
            if (newparams)
                type = (jl_value_t*)jl_apply_tuple_type(newparams, 1);
            JL_GC_POP();
        }
    }
    return type;
}

static jl_value_t *_widen_diagonal(jl_value_t *t, jl_varbinding_t *troot) {
    check_diagonal(t, troot, PARAM_NONE);
    int any_concrete = 0;
    for (jl_varbinding_t *v = troot; v != NULL; v = v->prev)
        any_concrete |= cov_count(v) > 1 && v->occurs_inv == 0;
    if (!any_concrete)
        return t; // no diagonal
    return insert_nondiagonal(t, troot, 0);
}

static jl_value_t *widen_diagonal(jl_value_t *t, jl_unionall_t *u, jl_varbinding_t *troot)
{
    jl_varbinding_t vb = { u->var, NULL, NULL, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, NULL, troot };
    jl_value_t *nt = NULL;
    JL_GC_PUSH2(&vb.innervars, &nt);
    if (jl_is_unionall(u->body))
        nt = widen_diagonal(t, (jl_unionall_t *)u->body, &vb);
    else
        nt = _widen_diagonal(t, &vb);
    if (vb.innervars != NULL) {
        for (size_t i = 0; i < jl_array_nrows(vb.innervars); i++) {
            jl_tvar_t *var = (jl_tvar_t*)jl_array_ptr_ref(vb.innervars, i);
            nt = jl_type_unionall(var, nt);
        }
    }
    JL_GC_POP();
    return nt;
}

JL_DLLEXPORT jl_value_t *jl_widen_diagonal(jl_value_t *t, jl_unionall_t *ua)
{
    return widen_diagonal(t, ua, NULL);
}

// specificity comparison
static int count_missing_wrap(jl_value_t *x, jl_typeenv_t *env)
{
    if (!jl_has_free_typevars(x))
        return 0;
    jl_typeenv_t *wrapped = NULL;
    int count = 0;
    for (jl_typeenv_t *env2 = env; env2 != NULL; env2 = env2->prev) {
        int need_wrap = 0;
        for (jl_typeenv_t *env3 = wrapped; env3 != NULL && need_wrap == 0; env3 = env3->prev) {
            if (env3->var == env2->var)
                need_wrap = -1;
            else if (jl_has_typevar(env3->var->lb, env2->var) || jl_has_typevar(env3->var->ub, env2->var))
                need_wrap = 1;
        }
        need_wrap = need_wrap == 0 ? jl_has_typevar(x, env2->var) :
                    need_wrap == -1 ? 0 : 1;
        if (need_wrap) {
            count++;
            jl_typeenv_t *newenv = (jl_typeenv_t*)alloca(sizeof(jl_typeenv_t));
            newenv->var = env2->var;
            newenv->val = NULL;
            newenv->prev = wrapped;
            wrapped = newenv;
        }
    }
    return count;
}

static int obvious_subtype_msp(jl_value_t *x, jl_value_t *y, jl_value_t *y0, int *subtype, int wrapx, int wrapy)
{
    if (wrapx != 0 || wrapy != 0) {
        int wrap_count = wrapx - wrapy;
        while (wrap_count > 0 && jl_is_unionall(y))
        {
            y = ((jl_unionall_t*)y)->body;
            wrap_count--;
        }
        while (wrap_count < 0 && jl_is_unionall(x))
        {
            x = ((jl_unionall_t*)x)->body;
            wrap_count++;
        }
        if (wrap_count > 0) {
            if (obvious_subtype(jl_unwrap_unionall(x), y, y0, subtype) && !*subtype)
                return 1;
            return 0;
        }
    }
    return obvious_subtype(x, y, y0, subtype);
}

static int eq_msp(jl_value_t *a, jl_value_t *b, jl_value_t *a0, jl_value_t *b0, jl_typeenv_t *env)
{
    if (!(jl_is_type(a) || jl_is_typevar(a)) ||
        !(jl_is_type(b) || jl_is_typevar(b)))
        return jl_egal(a, b);
    if (a == b) // assume the TypeVar env is the same??
        return 1;
    if (jl_typeof(a) == jl_typeof(b) && jl_types_egal(a, b))
        return 1;
    if (obviously_unequal(a, b))
        return 0;
    // the following is an interleaved version of:
    //   return jl_type_equal(a, b)
    // where we try to do the fast checks before the expensive ones
    if (jl_is_datatype(a) && !jl_is_concrete_type(b)) {
        // if one type looks simpler, check it on the right
        // first in order to reject more quickly.
        jl_value_t *temp = a;
        a = b;
        b = temp;
    }
    int wrapa = count_missing_wrap(a, env);
    int wrapb = count_missing_wrap(b, env);
    // first check if a <: b has an obvious answer
    int subtype_ab = 2;
    if (b == (jl_value_t*)jl_any_type || a == jl_bottom_type) {
        subtype_ab = 1;
    }
    else if (obvious_subtype_msp(a, b, b0, &subtype_ab, wrapa, wrapb)) {
#ifdef NDEBUG
        if (subtype_ab == 0)
            return 0;
#endif
    }
    else {
        subtype_ab = 3;
    }
    // next check if b <: a has an obvious answer
    int subtype_ba = 2;
    if (a == (jl_value_t*)jl_any_type || b == jl_bottom_type) {
        subtype_ba = 1;
    }
    else if (obvious_subtype_msp(b, a, a0, &subtype_ba, wrapb, wrapa)) {
#ifdef NDEBUG
        if (subtype_ba == 0)
            return 0;
#endif
    }
    else {
        subtype_ba = 3;
    }
    // finally, do full subtyping for any inconclusive test
    JL_GC_PUSH2(&a, &b);
    jl_typeenv_t *env2 = env;
    while (env2 != NULL) {
        a = jl_type_unionall(env2->var, a);
        b = jl_type_unionall(env2->var, b);
        env2 = env2->prev;
    }
    jl_stenv_t e;
#ifdef NDEBUG
    if (subtype_ab != 1)
#endif
    {
        init_stenv(&e, NULL, 0);
        int subtype = forall_exists_subtype(a, b, &e, PARAM_NONE);
        assert(subtype_ab == 3 || subtype_ab == subtype || jl_has_free_typevars(a) || jl_has_free_typevars(b));
#ifndef NDEBUG
        if (subtype_ab != 0 && subtype_ab != 1) // ensures that running in a debugger doesn't change the result
#endif
        subtype_ab = subtype;
#ifdef NDEBUG
        if (subtype_ab == 0) {
            JL_GC_POP();
            return 0;
        }
#endif
    }
#ifdef NDEBUG
    if (subtype_ba != 1)
#endif
    {
        init_stenv(&e, NULL, 0);
        int subtype = forall_exists_subtype(b, a, &e, PARAM_NONE);
        assert(subtype_ba == 3 || subtype_ba == subtype || jl_has_free_typevars(a) || jl_has_free_typevars(b));
#ifndef NDEBUG
        if (subtype_ba != 0 && subtype_ba != 1) // ensures that running in a debugger doesn't change the result
#endif
        subtype_ba = subtype;
    }
    JL_GC_POP();
    // all tests successful
    return subtype_ab && subtype_ba;
}

static int sub_msp(jl_value_t *x, jl_value_t *y, jl_value_t *y0, jl_typeenv_t *env)
{
    jl_stenv_t e;
    if (y == (jl_value_t*)jl_any_type || x == jl_bottom_type)
        return 1;
    if (x == y ||
        (jl_typeof(x) == jl_typeof(y) &&
         (jl_is_unionall(y) || jl_is_uniontype(y)) &&
         jl_types_egal(x, y))) {
        return 1;
    }
    int obvious_sub = 2;
    int wrapx = count_missing_wrap(x, env);
    int wrapy = count_missing_wrap(y, env);
    if (obvious_subtype_msp(x, y, y0, &obvious_sub, wrapx, wrapy)) {
#ifdef NDEBUG
        return obvious_sub;
#endif
    }
    else {
        obvious_sub = 3;
    }
    JL_GC_PUSH2(&x, &y);
    while (env != NULL) {
        if (jl_is_type(x) || jl_is_typevar(x))
            x = jl_type_unionall(env->var, x);
        if (jl_is_type(y) || jl_is_typevar(y))
            y = jl_type_unionall(env->var, y);
        env = env->prev;
    }
    init_stenv(&e, NULL, 0);
    int subtype = forall_exists_subtype(x, y, &e, PARAM_NONE);
    assert(obvious_sub == 3 || obvious_sub == subtype || jl_has_free_typevars(x) || jl_has_free_typevars(y));
#ifndef NDEBUG
    if (obvious_sub == 0 || obvious_sub == 1)
        subtype = obvious_sub; // this ensures that running in a debugger doesn't change the result
#endif
    JL_GC_POP();
    return subtype;
}

static int type_morespecific_(jl_value_t *a, jl_value_t *b, jl_value_t *a0, jl_value_t *b0, int invariant, jl_typeenv_t *env);

static int num_occurs(jl_tvar_t *v, jl_typeenv_t *env);

static jl_value_t *nth_tuple_elt(jl_datatype_t *t JL_PROPAGATES_ROOT, size_t i) JL_NOTSAFEPOINT
{
    size_t len = jl_nparams(t);
    if (len == 0)
        return NULL;
    if (i < len-1)
        return jl_tparam(t, i);
    jl_value_t *last = jl_unwrap_unionall(jl_tparam(t, len-1));
    if (jl_is_vararg(last)) {
        jl_value_t *n = jl_unwrap_vararg_num(last);
        if (n && jl_is_long(n) && i >= len-1+jl_unbox_long(n))
            return NULL;
        return jl_unwrap_vararg(last);
    }
    if (i == len-1)
        return jl_tparam(t, i);
    return NULL;
}

static int tuple_morespecific(jl_datatype_t *cdt, jl_datatype_t *pdt, jl_value_t *c0, jl_value_t *p0, int invariant, jl_typeenv_t *env)
{
    size_t plen = jl_nparams(pdt);
    if (plen == 0) return 0;
    size_t clen = jl_nparams(cdt);
    if (clen == 0) return 1;
    int i = 0;
    jl_value_t *clast = jl_tparam(cdt,clen-1);
    jl_vararg_kind_t ckind = jl_vararg_kind(clast);
    int cva = ckind > JL_VARARG_INT;
    int pva = jl_vararg_kind(jl_tparam(pdt,plen-1)) > JL_VARARG_INT;
    int cdiag = 0, pdiag = 0;
    int some_morespecific = 0;
    while (1) {
        if (cva && pva && i >= clen && i >= plen)
            break;

        jl_value_t *ce = nth_tuple_elt(cdt, i);
        jl_value_t *pe = nth_tuple_elt(pdt, i);

        if (ce == NULL) {
            if (pe == NULL) break;
            return 1;
        }
        if (pe == NULL) {
            if (!cva && !some_morespecific)
                return 0;
            break;
        }

        if (type_morespecific_(pe, ce, p0, c0, invariant, env)) {
            assert(!type_morespecific_(ce, pe, c0, p0, invariant, env));
            return 0;
        }

        if (!cdiag && jl_is_typevar(ce) && num_occurs((jl_tvar_t*)ce,env) > 1)
            cdiag = 1;
        if (!pdiag && jl_is_typevar(pe) && num_occurs((jl_tvar_t*)pe,env) > 1)
            pdiag = 1;

        // in Tuple{a,b...} and Tuple{c,d...} allow b and d to be disjoint
        if (cva && pva && i >= clen-1 && i >= plen-1 && (some_morespecific || (cdiag && !pdiag)))
            return 1;

        int cms = type_morespecific_(ce, pe, c0, p0, invariant, env);

        if (!cms && !sub_msp(ce, pe, p0, env)) {
            /*
              A bound vararg tuple can be more specific despite disjoint elements in order to
              preserve transitivity. For example in
              A = Tuple{Array{T,N}, Vararg{Int,N}} where {T,N}
              B = Tuple{Array, Int}
              C = Tuple{AbstractArray, Int, Array}
              we need A < B < C and A < C.
            */
            return some_morespecific && cva && ckind == JL_VARARG_BOUND && num_occurs((jl_tvar_t*)jl_unwrap_vararg_num(clast), env) > 1;
        }

        // Tuple{..., T} not more specific than Tuple{..., Vararg{S}} if S is diagonal
        if (!cms && i == clen-1 && clen == plen && !cva && pva && eq_msp(ce, pe, c0, p0, env) &&
            jl_is_typevar(ce) && jl_is_typevar(pe) && !cdiag && pdiag)
            return 0;

        if (cms) some_morespecific = 1;
        i++;
    }
    if (cva && pva && clen > plen && (!pdiag || cdiag))
        return 1;
    if (cva && !pva && !some_morespecific)
        return 0;
    return some_morespecific || (cdiag && !pdiag);
}

static size_t tuple_full_length(jl_value_t *t)
{
    size_t n = jl_nparams(t);
    if (n == 0) return 0;
    jl_value_t *last = jl_unwrap_unionall(jl_tparam(t,n-1));
    if (jl_is_vararg(last)) {
        jl_value_t *N = jl_unwrap_vararg_num(last);
        if (jl_is_long(N))
            n += jl_unbox_long(N)-1;
    }
    return n;
}

// Called when a is a bound-vararg and b is not a vararg. Sets the vararg length
// in a to match b, as long as this makes some earlier argument more specific.
static int args_morespecific_fix1(jl_value_t *a, jl_value_t *b, jl_value_t *a0, jl_value_t *b0, int swap, jl_typeenv_t *env)
{
    size_t n = jl_nparams(a);
    int taillen = tuple_full_length(b)-n+1;
    if (taillen <= 0)
        return -1;
    assert(jl_is_va_tuple((jl_datatype_t*)a));
    jl_datatype_t *new_a = NULL;
    jl_value_t *e[2] = { jl_unwrap_vararg_num(jl_unwrap_unionall(jl_tparam(a, n-1))), jl_box_long(taillen) };
    JL_GC_PUSH2(&new_a, &e[1]);
    new_a = (jl_datatype_t*)jl_instantiate_type_with((jl_value_t*)a, e, 1);
    int changed = 0;
    for (size_t i = 0; i < n-1; i++) {
        if (jl_tparam(a, i) != jl_tparam(new_a, i)) {
            changed = 1;
            break;
        }
    }
    int ret = -1;
    if (changed) {
        if (eq_msp(b, (jl_value_t*)new_a, b0, a0, env))
            ret = swap;
        else if (swap)
            ret = type_morespecific_(b, (jl_value_t*)new_a, b0, a0, 0, env);
        else
            ret = type_morespecific_((jl_value_t*)new_a, b, a0, b0, 0, env);
    }
    JL_GC_POP();
    return ret;
}

static int count_occurs(jl_value_t *t, jl_tvar_t *v) JL_NOTSAFEPOINT
{
    if (t == (jl_value_t*)v)
        return 1;
    if (jl_is_uniontype(t)) {
        int a = count_occurs(((jl_uniontype_t*)t)->a, v);
        int b = count_occurs(((jl_uniontype_t*)t)->b, v);
        return a > b ? a : b;
    }
    if (jl_is_unionall(t)) {
        if (((jl_unionall_t*)t)->var == v)
            return 0;
        return count_occurs(((jl_unionall_t*)t)->body, v);
    }
    if (jl_is_vararg(t)) {
        jl_vararg_t *vm = (jl_vararg_t*)t;
        if (vm->T) {
            return count_occurs(vm->T, v) + (vm->N ? count_occurs(vm->N, v) : 0);
        }
    }
    if (jl_is_typeeq(t))
        return count_occurs(jl_typeeq_T(t), v);
    if (jl_is_datatype(t)) {
        int i, c=0;
        for(i=0; i < jl_nparams(t); i++)
            c += count_occurs(jl_tparam(t,i), v);
        return c;
    }
    return 0;
}

static int num_occurs(jl_tvar_t *v, jl_typeenv_t *env)
{
    while (env != NULL) {
        if (env->var == v)
            return (int)(ssize_t)env->val;
        env = env->prev;
    }
    return 0;
}

int tuple_cmp_typeofbottom(jl_datatype_t *a, jl_datatype_t *b)
{
    size_t i, la = jl_nparams(a), lb = jl_nparams(b);
    for (i = 0; i < la || i < lb; i++) {
        jl_value_t *pa = i < la ? jl_tparam(a, i) : NULL;
        jl_value_t *pb = i < lb ? jl_tparam(b, i) : NULL;
        assert(jl_typeofbottom_type); // for clang-sa
        int xa = is_typeofbottom_typealias(pa);
        int xb = is_typeofbottom_typealias(pb);
        if (xa != xb)
            return xa - xb;
    }
    return 0;
}


#define HANDLE_UNIONALL_A                                               \
    jl_unionall_t *ua = (jl_unionall_t*)a;                              \
    jl_typeenv_t newenv = { ua->var, 0x0, env };                        \
    newenv.val = (jl_value_t*)(intptr_t)count_occurs(ua->body, ua->var); \
    return type_morespecific_(ua->body, b, a0, b0, invariant, &newenv)

#define HANDLE_UNIONALL_B                                               \
    jl_unionall_t *ub = (jl_unionall_t*)b;                              \
    jl_typeenv_t newenv = { ub->var, 0x0, env };                        \
    newenv.val = (jl_value_t*)(intptr_t)count_occurs(ub->body, ub->var); \
    return type_morespecific_(a, ub->body, a0, b0, invariant, &newenv)

static int type_morespecific_(jl_value_t *a, jl_value_t *b, jl_value_t *a0, jl_value_t *b0, int invariant, jl_typeenv_t *env)
{
    if (a == b)
        return 0;

    if (jl_is_tuple_type(a) && jl_is_tuple_type(b)) {
        // compare whether a and b have Type{Union{}} included,
        // which makes them instantly the most specific, regardless of all else,
        // for whichever is left most (the left-to-right behavior here ensures
        // we do not need to keep track of conflicts with multiple methods).
        int msp = tuple_cmp_typeofbottom((jl_datatype_t*)a, (jl_datatype_t*)b);
        if (msp)
            return msp > 0;
        // When one is JL_VARARG_BOUND and the other has fixed length,
        // allow the argument length to fix the tvar
        jl_vararg_kind_t akind = jl_va_tuple_kind((jl_datatype_t*)a);
        jl_vararg_kind_t bkind = jl_va_tuple_kind((jl_datatype_t*)b);
        int ans = -1;
        if (akind == JL_VARARG_BOUND && bkind < JL_VARARG_BOUND) {
            ans = args_morespecific_fix1(a, b, a0, b0, 0, env);
            if (ans == 1) return 1;
        }
        if (bkind == JL_VARARG_BOUND && akind < JL_VARARG_BOUND) {
            ans = args_morespecific_fix1(b, a, b0, a0, 1, env);
            if (ans == 0) return 0;
        }
        return tuple_morespecific((jl_datatype_t*)a, (jl_datatype_t*)b, a0, b0, invariant, env);
    }

    if (!invariant) {
        if ((jl_datatype_t*)a == jl_any_type) return 0;
        if ((jl_datatype_t*)b == jl_any_type && !jl_is_typevar(a)) return 1;
    }

    if (jl_is_uniontype(a)) {
        if (jl_is_unionall(b)) {
            HANDLE_UNIONALL_B;
        }
        // Union a is more specific than b if some element of a is more specific than b, but
        // not vice-versa.
        if (sub_msp(b, a, a0, env))
            return 0;
        jl_uniontype_t *u = (jl_uniontype_t*)a;
        if (type_morespecific_(u->a, b, a0, b0, invariant, env) || type_morespecific_(u->b, b, a0, b0, invariant, env)) {
            if (jl_is_uniontype(b)) {
                jl_uniontype_t *v = (jl_uniontype_t*)b;
                if (type_morespecific_(v->a, a, b0, a0, invariant, env) || type_morespecific_(v->b, a, b0, a0, invariant, env))
                    return 0;
            }
            return 1;
        }
        return 0;
    }

    if (jl_is_typeeq(a) && !invariant) {
        if (b == (jl_value_t*)jl_typeofbottom_type)
            return 0;
        jl_value_t *tp0a = jl_typeeq_T(a);
        if (jl_is_typevar(tp0a)) {
            jl_value_t *ub = ((jl_tvar_t*)tp0a)->ub;
            if (jl_is_kind(b) && !sub_msp((jl_value_t*)jl_any_type, ub, b0, env))
                return 1;
        }
        else if (tp0a == jl_bottom_type) {
            if (sub_msp(b, (jl_value_t*)jl_type_type, (jl_value_t*)jl_type_type, env))
                return 1;
        }
        else if (b == (jl_value_t*)jl_datatype_type || b == (jl_value_t*)jl_unionall_type ||
                 b == (jl_value_t*)jl_uniontype_type) {
            return 1;
        }
    }

    if (jl_is_uniontype(b)) {
        if (jl_is_unionall(a)) {
            HANDLE_UNIONALL_A;
        }
        jl_uniontype_t *u = (jl_uniontype_t*)b;
        if (type_morespecific_(a, u->a, a0, b0, invariant, env) || type_morespecific_(a, u->b, a0, b0, invariant, env))
            return !type_morespecific_(b, a, b0, a0, invariant, env);
        return 0;
    }

    if (jl_is_typeeq(a) && jl_is_typeeq(b)) {
        jl_value_t *apara = jl_typeeq_T(a);
        jl_value_t *bpara = jl_typeeq_T(b);
        int afree = jl_has_free_typevars(apara);
        int bfree = jl_has_free_typevars(bpara);
        if (!afree && !bfree && !jl_types_equal(apara, bpara))
            return 0;
        if (type_morespecific_(apara, bpara, a0, b0, 1, env) && (jl_is_typevar(apara) || !afree || bfree))
            return 1;
        if (type_morespecific_(bpara, apara, b0, a0, 1, env) && (jl_is_typevar(bpara) || !bfree || afree))
            return 0;
        if (eq_msp(apara, bpara, a0, b0, env))
            return !afree && bfree;
        return 0;
    }

    if (jl_is_kind(a) && jl_is_typeeq(b) && !invariant) {
        // a kind (e.g. `DataType`) is more specific than an unbounded `Type{T}`
        jl_value_t *tp0b = jl_typeeq_T(b);
        if (jl_is_typevar(tp0b) && sub_msp((jl_value_t*)jl_any_type, ((jl_tvar_t*)tp0b)->ub, b0, env))
            return 1;
    }

    if (jl_is_datatype(a) && jl_is_datatype(b)) {
        jl_datatype_t *tta = (jl_datatype_t*)a, *ttb = (jl_datatype_t*)b;
        // Type{Union{}} is more specific than other types, so TypeofBottom must be too
        if (tta == jl_typeofbottom_type && (is_kind_or_anytype(b) || jl_is_typeeq(b)))
            return 1;
        int super = 0;
        while (tta != jl_any_type) {
            if (tta->name == ttb->name) {
                if (super) {
                    if (!jl_is_typeeq(b)) return 1;
                    jl_value_t *tp0 = jl_typeeq_T(b);
                    if (jl_is_typevar(tp0)) {
                        if (sub_msp((jl_value_t*)jl_any_type, ((jl_tvar_t*)tp0)->ub, b0, env))
                            return 1;
                    }
                }
                assert(jl_nparams(tta) == jl_nparams(ttb));
                int ascore=0, bscore=0, ascore1=0, bscore1=0, adiag=0, bdiag=0;
                for(size_t i=0; i < jl_nparams(tta); i++) {
                    jl_value_t *apara = jl_tparam(tta,i);
                    jl_value_t *bpara = jl_tparam(ttb,i);
                    int afree = jl_has_free_typevars(apara);
                    int bfree = jl_has_free_typevars(bpara);
                    if (!afree && !bfree && !jl_types_equal(apara, bpara))
                        return 0;
                    if (type_morespecific_(apara, bpara, a0, b0, 1, env) && (jl_is_typevar(apara) || !afree || bfree))
                        ascore += 1;
                    else if (type_morespecific_(bpara, apara, b0, a0, 1, env) && (jl_is_typevar(bpara) || !bfree || afree))
                        bscore += 1;
                    else if (eq_msp(apara, bpara, a0, b0, env)) {
                        if (!afree && bfree)
                            ascore += 1;
                        else if (afree && !bfree)
                            bscore += 1;
                    }
                    if (jl_is_typevar(bpara) && !jl_is_typevar(apara) && !jl_is_type(apara))
                        ascore1 = 1;
                    else if (jl_is_typevar(apara) && !jl_is_typevar(bpara) && !jl_is_type(bpara))
                        bscore1 = 1;
                    if (!adiag && jl_is_typevar(apara)) {
                        for(int j=i+1; j < jl_nparams(tta); j++) {
                            if (jl_has_typevar(jl_tparam(tta,j), (jl_tvar_t*)apara)) {
                                adiag = 1; break;
                            }
                        }
                    }
                    if (!bdiag && jl_is_typevar(bpara)) {
                        for(int j=i+1; j < jl_nparams(ttb); j++) {
                            if (jl_has_typevar(jl_tparam(ttb,j), (jl_tvar_t*)bpara)) {
                                bdiag = 1; break;
                            }
                        }
                    }
                }
                if (ascore1 > bscore1)
                    return 1;
                if (bscore1 > ascore1 || bscore > ascore || bdiag > adiag)
                    return 0;
                return ascore > bscore || adiag > bdiag;
            }
            tta = tta->super; super = 1;
        }
        return 0;
    }

    if (jl_is_typevar(a)) {
        if (jl_is_typevar(b)) {
            return (( type_morespecific_((jl_value_t*)((jl_tvar_t*)a)->ub,
                                         (jl_value_t*)((jl_tvar_t*)b)->ub, a0, b0, 0, env) &&
                     !type_morespecific_((jl_value_t*)((jl_tvar_t*)a)->lb,
                                         (jl_value_t*)((jl_tvar_t*)b)->lb, a0, b0, 0, env)) ||
                    ( type_morespecific_((jl_value_t*)((jl_tvar_t*)b)->lb,
                                         (jl_value_t*)((jl_tvar_t*)a)->lb, b0, a0, 0, env) &&
                     !type_morespecific_((jl_value_t*)((jl_tvar_t*)b)->ub,
                                         (jl_value_t*)((jl_tvar_t*)a)->ub, b0, a0, 0, env)));
        }
        if (!jl_is_type(b))
            return 0;
        if (invariant) {
            if (((jl_tvar_t*)a)->ub == jl_bottom_type)
                return 1;
            if (!jl_has_free_typevars(b))
                return 0;
            if (eq_msp(((jl_tvar_t*)a)->ub, b, a0, b0, env))
                return num_occurs((jl_tvar_t*)a, env) >= 2;
        }
        else {
            // need `{T,T} where T` more specific than `{Any, Any}`
            if (b == (jl_value_t*)jl_any_type && ((jl_tvar_t*)a)->ub == (jl_value_t*)jl_any_type &&
                num_occurs((jl_tvar_t*)a, env) >= 2)
                return 1;
        }
        return type_morespecific_(((jl_tvar_t*)a)->ub, b, a0, b0, 0, env);
    }
    if (jl_is_typevar(b)) {
        if (!jl_is_type(a))
            return 1;
        if (invariant) {
            if (((jl_tvar_t*)b)->ub == jl_bottom_type)
                return 0;
            if (jl_has_free_typevars(a)) {
                if (type_morespecific_(a, ((jl_tvar_t*)b)->ub, a0, b0, 0, env))
                    return 1;
                if (eq_msp(a, ((jl_tvar_t*)b)->ub, a0, b0, env))
                    return num_occurs((jl_tvar_t*)b, env) < 2;
                return 0;
            }
            else {
                if (obviously_disjoint(a, ((jl_tvar_t*)b)->ub, 1))
                    return 0;
                if (type_morespecific_(((jl_tvar_t*)b)->ub, a, b0, a0, 0, env))
                    return 0;
                return 1;
            }
        }
        return type_morespecific_(a, ((jl_tvar_t*)b)->ub, a0, b0, 0, env);
    }

    if (jl_is_unionall(a)) {
        HANDLE_UNIONALL_A;
    }
    if (jl_is_unionall(b)) {
        HANDLE_UNIONALL_B;
    }

    return 0;
}

JL_DLLEXPORT int jl_type_morespecific(jl_value_t *a, jl_value_t *b)
{
    if (obviously_disjoint(a, b, 1))
        return 0;
    if (jl_has_free_typevars(a) || jl_has_free_typevars(b))
        return 0;
    if (jl_subtype(b, a))
        return 0;
    if (jl_subtype(a, b))
        return 1;
    return type_morespecific_(a, b, a, b, 0, NULL);
}

JL_DLLEXPORT int jl_type_morespecific_no_subtype(jl_value_t *a, jl_value_t *b)
{
    return type_morespecific_(a, b, a, b, 0, NULL);
}

// Equivalent to `jl_type_morespecific` of the signatures, except that more recent
// methods are more specific, iff the methods signatures are type-equal
JL_DLLEXPORT int jl_method_morespecific(jl_method_t *ma, jl_method_t *mb)
{
    jl_value_t *a = (jl_value_t*)ma->sig;
    jl_value_t *b = (jl_value_t*)mb->sig;
    if (obviously_disjoint(a, b, 1))
        return 0;
    if (jl_has_free_typevars(a) || jl_has_free_typevars(b))
        return 0;
    if (jl_subtype(b, a)) {
        if (jl_types_equal(a, b))
            return jl_atomic_load_relaxed(&ma->primary_world) > jl_atomic_load_relaxed(&mb->primary_world);
        return 0;
    }
    if (jl_subtype(a, b))
        return 1;
    return type_morespecific_(a, b, a, b, 0, NULL);
}

#ifdef __cplusplus
}
#endif
