Skip to content

Commit

Permalink
Also record chained innervars
Browse files Browse the repository at this point in the history 
At present we only record direct `innervars` (`T` -> `S<:Val{T}`). And chained `innervars` might be ignored (`T` -> `S<:Val{V<:T}`\
This commit fix it.
  • Loading branch information
@N5N3
N5N3 committed Jul 15, 2023
1 parent 22ac24a commit cd74337
Show file tree
Hide file tree
Showing 2 changed files with 128 additions and 39 deletions.
160 changes: 122 additions & 38 deletions src/subtype.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2721,32 +2721,33 @@ static jl_value_t *omit_bad_union(jl_value_t *u, jl_tvar_t *t)
jl_tvar_t *var = ((jl_unionall_t *)u)->var;
jl_value_t *ub = var->ub, *body = ((jl_unionall_t *)u)->body;
assert(var != t);
if (!jl_has_typevar(var->lb, t)) {
JL_GC_PUSH3(&ub, &body, &var);
body = omit_bad_union(body, t);
if (!jl_has_typevar(body, var)) {
res = body;
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 {
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)) {
JL_TRY {
res = jl_substitute_var(body, var, ub);
}
else if (obviously_egal(var->lb, ub)) {
JL_TRY {
res = jl_substitute_var(body, var, ub);
}
JL_CATCH {
res = jl_bottom_type;
}
JL_CATCH {
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);
}
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();
Expand All @@ -2770,9 +2771,9 @@ static jl_value_t *omit_bad_union(jl_value_t *u, jl_tvar_t *t)
// 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;
jl_value_t *varval = NULL, *ilb = NULL, *iub = NULL, *nivar = NULL;
jl_tvar_t *newvar = vb->var;
JL_GC_PUSH2(&res, &newvar);
JL_GC_PUSH5(&res, &newvar, &ilb, &iub, &nivar);
// try to reduce var to a single value
if (jl_is_long(vb->ub) && jl_is_typevar(vb->lb)) {
varval = vb->ub;
Expand Down Expand Up @@ -2806,19 +2807,99 @@ static jl_value_t *finish_unionall(jl_value_t *res JL_MAYBE_UNROOTED, jl_varbind
newvar = jl_new_typevar(vb->var->name, vb->lb, vb->ub);

// remove/replace/rewrap free occurrences of this var in the environment

// I. Handle indirect innervars (make them behave like direct innervars).
// 1) record if btemp->lb/ub has indirect innervars.
// 2) subtitute `vb->var` with `varval`/`varval`
// note: We only store the innervar in the outmost `varbinding`,
// thus we must check all inner env to ensure the recording/subtitution
// is complete
int len = current_env_length(e);
int8_t *blinding_has_innerdep = (int8_t *)alloca(len);
memset(blinding_has_innerdep, 0, len);
for (jl_varbinding_t *btemp = e->vars; btemp != NULL; btemp = btemp->prev) {
if (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);
ilb = ivar->lb; iub = ivar->ub;
int has_innerdep = 0;
if (jl_has_typevar(ilb, vb->var)) {
has_innerdep = 1;
if (varval) {
JL_TRY {
ilb = jl_substitute_var(ilb, vb->var, varval);
}
JL_CATCH {
res = jl_bottom_type;
}
}
else if (newvar != vb->var) {
ilb = jl_substitute_var(ilb, vb->var, (jl_value_t*)newvar);
}
}
if (jl_has_typevar(iub, vb->var)) {
has_innerdep = 1;
if (varval) {
JL_TRY {
iub = jl_substitute_var(iub, vb->var, varval);
}
JL_CATCH {
res = jl_bottom_type;
}
}
else if (newvar != vb->var) {
iub = jl_substitute_var(iub, vb->var, (jl_value_t*)newvar);
}
}
if (!has_innerdep) continue;
int need_subtitution = 0;
if (ilb != ivar->lb || iub != ivar->ub) {
need_subtitution = 1;
nivar = (jl_value_t *)jl_new_typevar(ivar->name, ilb, iub);
jl_array_ptr_set(btemp->innervars, i, nivar);
if (jl_has_typevar(res, ivar))
res = jl_substitute_var(res, ivar, nivar);
}
int envind = 0;
for (jl_varbinding_t *btemp2 = e->vars; btemp2 != btemp->prev; btemp2 = btemp2->prev) {
if (jl_has_typevar(btemp2->lb, ivar)) {
if (need_subtitution)
btemp2->lb = jl_substitute_var(btemp2->lb, ivar, nivar);
blinding_has_innerdep[envind] |= 1;
}
if (jl_has_typevar(btemp2->ub, ivar)) {
if (need_subtitution)
btemp2->ub = jl_substitute_var(btemp2->ub, ivar, nivar);
blinding_has_innerdep[envind] |= 2;
}
envind++;
}
}
}
}
// II. Handle direct innervars.
jl_varbinding_t *wrap = NULL;
int envind = 0;
for (jl_varbinding_t *btemp = e->vars; btemp != NULL; btemp = btemp->prev) {
if (jl_has_typevar(btemp->lb, vb->var)) {
int has_innerdep = blinding_has_innerdep[envind++];
int lb_has_innerdep = has_innerdep & 1;
int ub_has_innerdep = has_innerdep & 2;
assert(!has_innerdep || btemp->depth0 == vb->depth0);
int lb_has_dep = jl_has_typevar(btemp->lb, vb->var);
int ub_has_dep = jl_has_typevar(btemp->ub, vb->var);
if (lb_has_innerdep || lb_has_dep) {
if (vb->lb == (jl_value_t*)btemp->var) {
JL_GC_POP();
return jl_bottom_type;
}
if (varval) {
JL_TRY {
btemp->lb = jl_substitute_var(btemp->lb, vb->var, varval);
}
JL_CATCH {
res = jl_bottom_type;
if (lb_has_dep) { // inner substitution has been handled
JL_TRY {
btemp->lb = jl_substitute_var(btemp->lb, vb->var, varval);
}
JL_CATCH {
res = jl_bottom_type;
}
}
}
else if (btemp->lb == (jl_value_t*)vb->var) {
Expand All @@ -2827,7 +2908,7 @@ static jl_value_t *finish_unionall(jl_value_t *res JL_MAYBE_UNROOTED, jl_varbind
else if (btemp->depth0 == vb->depth0 && !jl_has_typevar(vb->lb, btemp->var) && !jl_has_typevar(vb->ub, btemp->var)) {
// 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 (newvar != vb->var && lb_has_dep) // inner substitution has been handled
btemp->lb = jl_substitute_var(btemp->lb, vb->var, (jl_value_t*)newvar);
wrap = btemp;
}
Expand All @@ -2836,20 +2917,23 @@ static jl_value_t *finish_unionall(jl_value_t *res JL_MAYBE_UNROOTED, jl_varbind
}
assert((jl_value_t*)btemp->var != btemp->lb);
}
if (jl_has_typevar(btemp->ub, vb->var)) {
if (ub_has_innerdep || ub_has_dep) {
if (vb->ub == (jl_value_t*)btemp->var) {
// TODO: handle `omit_bad_union` correctly if `ub_has_innerdep`
btemp->ub = omit_bad_union(btemp->ub, vb->var);
if (btemp->ub == jl_bottom_type && btemp->ub != btemp->lb) {
JL_GC_POP();
return jl_bottom_type;
}
}
if (varval) {
JL_TRY {
btemp->ub = jl_substitute_var(btemp->ub, vb->var, varval);
}
JL_CATCH {
res = jl_bottom_type;
if (ub_has_dep) { // inner substitution has been handled
JL_TRY {
btemp->ub = jl_substitute_var(btemp->ub, vb->var, varval);
}
JL_CATCH {
res = jl_bottom_type;
}
}
}
else if (btemp->ub == (jl_value_t*)vb->var) {
Expand All @@ -2860,7 +2944,7 @@ static jl_value_t *finish_unionall(jl_value_t *res JL_MAYBE_UNROOTED, jl_varbind
btemp->ub = vb->ub;
}
else if (btemp->depth0 == vb->depth0 && !jl_has_typevar(vb->lb, btemp->var) && !jl_has_typevar(vb->ub, btemp->var)) {
if (newvar != vb->var)
if (newvar != vb->var && ub_has_dep) // inner substitution has been handled
btemp->ub = jl_substitute_var(btemp->ub, vb->var, (jl_value_t*)newvar);
wrap = btemp;
}
Expand Down
7 changes: 6 additions & 1 deletion test/subtype.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2552,8 +2552,13 @@ end
@test !<:(Type{Vector{Union{Base.BitInteger, Base.IEEEFloat, StridedArray, Missing, Nothing, Val{T}}}} where {T}, Type{Array{T}} where {T})

#issue 50195
T50195{S} = Pair{S,Set{S}}
let a = Tuple{Type{X} where X<:Union{Nothing, Val{X1} where {X4, X1<:(Pair{X2, Val{X2}} where X2<:Val{X4})}}},
b = Tuple{Type{Y} where Y<:(Val{Y1} where {Y4<:Src, Y1<:(Pair{Y2, Val{Y2}} where Y2<:Union{Val{Y4}, Y4})})} where Src
@test typeintersect(a, b) <: Any
end

#issue 50195
let a = Tuple{Union{Nothing, Type{Pair{T1}} where T1}}
b = Tuple{Type{X2} where X2<:(Pair{T2, Y2} where {Src, Z2<:Src, Y2<:Union{Val{Z2}, Z2}})} where T2
@test !Base.has_free_typevars(typeintersect(a, b))
end

0 comments on commit cd74337

Please sign in to comment.