Skip to content

Commit 74305bf

Browse files
authored
fix #31703, type intersection bug with chains of vars in invariant position (#31747)
1 parent 4dd91fa commit 74305bf

File tree

2 files changed

+68
-18
lines changed

2 files changed

+68
-18
lines changed

src/subtype.c

+33-18
Original file line numberDiff line numberDiff line change
@@ -1617,6 +1617,33 @@ static void set_bound(jl_value_t **bound, jl_value_t *val, jl_tvar_t *v, jl_sten
16171617
*bound = val;
16181618
}
16191619

1620+
// subtype, treating all vars as existential
1621+
static int subtype_in_env_existential(jl_value_t *x, jl_value_t *y, jl_stenv_t *e)
1622+
{
1623+
jl_varbinding_t *v = e->vars;
1624+
int len = 0;
1625+
while (v != NULL) {
1626+
len++;
1627+
v = v->prev;
1628+
}
1629+
int8_t *rs = (int8_t*)malloc(len);
1630+
int n = 0;
1631+
v = e->vars;
1632+
while (v != NULL) {
1633+
rs[n++] = v->right;
1634+
v->right = 1;
1635+
v = v->prev;
1636+
}
1637+
int issub = subtype_in_env(x, y, e);
1638+
n = 0; v = e->vars;
1639+
while (v != NULL) {
1640+
v->right = rs[n++];
1641+
v = v->prev;
1642+
}
1643+
free(rs);
1644+
return issub;
1645+
}
1646+
16201647
static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int8_t R, int param)
16211648
{
16221649
jl_varbinding_t *bb = lookup(e, b);
@@ -1629,30 +1656,19 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
16291656
int d = bb->depth0;
16301657
jl_value_t *root=NULL; jl_savedenv_t se;
16311658
if (param == 2) {
1632-
jl_value_t *ub = R ? intersect_aside(a, bb->ub, e, d) : intersect_aside(bb->ub, a, e, d);
1633-
JL_GC_PUSH2(&ub, &root);
1634-
if (!jl_has_free_typevars(ub) && !jl_has_free_typevars(bb->lb)) {
1635-
save_env(e, &root, &se);
1636-
int issub = subtype_in_env(bb->lb, ub, e);
1637-
restore_env(e, root, &se);
1638-
free(se.buf);
1639-
if (!issub) {
1640-
JL_GC_POP();
1641-
return jl_bottom_type;
1642-
}
1643-
}
1659+
if (!(subtype_in_env_existential(bb->lb, a, e) && subtype_in_env_existential(a, bb->ub, e)))
1660+
return jl_bottom_type;
1661+
jl_value_t *ub = a;
16441662
if (ub != (jl_value_t*)b) {
16451663
if (jl_has_free_typevars(ub)) {
16461664
// constraint X == Ref{X} is unsatisfiable. also check variables set equal to X.
16471665
if (var_occurs_inside(ub, b, 0, 0)) {
1648-
JL_GC_POP();
16491666
return jl_bottom_type;
16501667
}
16511668
jl_varbinding_t *btemp = e->vars;
16521669
while (btemp != NULL) {
16531670
if (btemp->lb == (jl_value_t*)b && btemp->ub == (jl_value_t*)b &&
16541671
var_occurs_inside(ub, btemp->var, 0, 0)) {
1655-
JL_GC_POP();
16561672
return jl_bottom_type;
16571673
}
16581674
btemp = btemp->prev;
@@ -1661,7 +1677,6 @@ static jl_value_t *intersect_var(jl_tvar_t *b, jl_value_t *a, jl_stenv_t *e, int
16611677
bb->ub = ub;
16621678
bb->lb = ub;
16631679
}
1664-
JL_GC_POP();
16651680
return ub;
16661681
}
16671682
else if (bb->constraintkind == 0) {
@@ -1768,7 +1783,7 @@ static jl_value_t *finish_unionall(jl_value_t *res JL_MAYBE_UNROOTED, jl_varbind
17681783
// given x<:T<:x, substitute x for T
17691784
varval = vb->ub;
17701785
}
1771-
else if (!var_occurs_inside(res, vb->var, 0, 1) && is_leaf_bound(vb->ub)) {
1786+
else if (!vb->occurs_inv && is_leaf_bound(vb->ub)) {
17721787
// replace T<:x with x in covariant position when possible
17731788
varval = vb->ub;
17741789
}
@@ -2517,7 +2532,7 @@ static jl_value_t *intersect_types(jl_value_t *x, jl_value_t *y, int emptiness_o
25172532
if (obviously_disjoint(x, y, 0))
25182533
return jl_bottom_type;
25192534
init_stenv(&e, NULL, 0);
2520-
e.intersection = 1;
2535+
e.intersection = e.ignore_free = 1;
25212536
e.emptiness_only = emptiness_only;
25222537
return intersect_all(x, y, &e);
25232538
}
@@ -2637,7 +2652,7 @@ jl_value_t *jl_type_intersection_env_s(jl_value_t *a, jl_value_t *b, jl_svec_t *
26372652
goto bot;
26382653
jl_stenv_t e;
26392654
init_stenv(&e, NULL, 0);
2640-
e.intersection = 1;
2655+
e.intersection = e.ignore_free = 1;
26412656
e.envout = env;
26422657
if (szb)
26432658
memset(env, 0, szb*sizeof(void*));

test/subtype.jl

+35
Original file line numberDiff line numberDiff line change
@@ -1471,3 +1471,38 @@ CovType{T} = Union{AbstractArray{T,2},
14711471
@testintersect(Pair{<:Any, <:AbstractMatrix},
14721472
Pair{T, <:CovType{T}} where T<:AbstractFloat,
14731473
Pair{T,S} where S<:AbstractArray{T,2} where T<:AbstractFloat)
1474+
1475+
# issue #31703
1476+
@testintersect(Pair{<:Any, Ref{Tuple{Ref{Ref{Tuple{Int}}},Ref{Float64}}}},
1477+
Pair{T, S} where S<:(Ref{A} where A<:(Tuple{C,Ref{T}} where C<:(Ref{D} where D<:(Ref{E} where E<:Tuple{FF}) where FF<:B)) where B) where T,
1478+
Pair{Float64, Ref{Tuple{Ref{Ref{Tuple{Int}}},Ref{Float64}}}})
1479+
1480+
module I31703
1481+
using Test, LinearAlgebra
1482+
import Base: OneTo, Slice
1483+
1484+
struct BandedMatrix{T, CONTAINER, RAXIS} end
1485+
struct Ones{T, N, Axes} end
1486+
const RestrictionMatrix = BandedMatrix{<:Int, <:Ones}
1487+
struct Applied{Style, Args<:Tuple} end
1488+
const Mul = Applied{Style,Factors} where Factors<:Tuple where Style
1489+
const RestrictedBasis{B} = Mul{<:Any,<:Tuple{B, <:RestrictionMatrix}}
1490+
struct ApplyQuasiArray{T, N, App<:Applied} end
1491+
const MulQuasiArray = ApplyQuasiArray{T,N,MUL} where MUL<:(Applied{Style,Factors} where Factors<:Tuple where Style) where N where T
1492+
const RestrictedQuasiArray{T,N,B} = MulQuasiArray{T,N,<:RestrictedBasis{B}}
1493+
const BasisOrRestricted{B} = Union{B,RestrictedBasis{<:B},<:RestrictedQuasiArray{<:Any,<:Any,<:B}}
1494+
struct QuasiAdjoint{T,S} end
1495+
const AdjointRestrictedBasis{B} = Mul{<:Any,<:Tuple{<:Adjoint{<:Any,<:RestrictionMatrix}, <:QuasiAdjoint{<:Any,B}}}
1496+
const AdjointRestrictedQuasiArray{T,N,B} = MulQuasiArray{T,N,<:AdjointRestrictedBasis{B}}
1497+
const AdjointBasisOrRestricted{B} = Union{<:QuasiAdjoint{<:Any,B},AdjointRestrictedBasis{<:B},<:AdjointRestrictedQuasiArray{<:Any,<:Any,<:B}}
1498+
const RadialOperator{T,B,M<:AbstractMatrix{T}} = Mul{<:Any,<:Tuple{<:BasisOrRestricted{B},M,<:AdjointBasisOrRestricted{B}}}
1499+
const HFPotentialOperator{T,B} = RadialOperator{T,B,Diagonal{T,Vector{T}}}
1500+
struct HFPotential{kind,T,B,RO<:HFPotentialOperator{T,B},P<:Integer} end
1501+
1502+
T = HFPotential{_A,Float64,Any,Applied{Int,Tuple{ApplyQuasiArray{Float64,2,Applied{Int,Tuple{Any,BandedMatrix{Int,Ones{Int,2,Tuple{OneTo{Int},OneTo{Int}}},OneTo{Int}}}}},Diagonal{Float64,Array{Float64,1}},ApplyQuasiArray{Float64,2,Applied{Int,Tuple{Adjoint{Int,BandedMatrix{Int,Ones{Int,2,Tuple{OneTo{Int},OneTo{Int}}},OneTo{Int}}},QuasiAdjoint{Float64,Any}}}}}},_B} where _B where _A
1503+
1504+
let A = typeintersect(HFPotential, T),
1505+
B = typeintersect(T, HFPotential)
1506+
@test A == B == HFPotential{kind,Float64,Any,Applied{Int,Tuple{ApplyQuasiArray{Float64,2,Applied{Int,Tuple{Any,BandedMatrix{Int,Ones{Int,2,Tuple{OneTo{Int},OneTo{Int}}},OneTo{Int}}}}},Diagonal{Float64,Array{Float64,1}},ApplyQuasiArray{Float64,2,Applied{Int,Tuple{Adjoint{Int,BandedMatrix{Int,Ones{Int,2,Tuple{OneTo{Int},OneTo{Int}}},OneTo{Int}}},QuasiAdjoint{Float64,Any}}}}}},P} where P<:Integer where kind
1507+
end
1508+
end

0 commit comments

Comments
 (0)