Existing issue
Elixir and Erlang/OTP versions
Erlang/OTP 28 [erts-16.4.0.1] [source] [64-bit] [smp:12:12] [ds:12:12:10] [async-threads:1] [jit]
Interactive Elixir (1.21.0-dev)
Operating system
any
Current behavior
The following 5 repros are manifestations of the same underlying bug:
- negated closed leaf
d = opt_difference(open_map(), empty_map())
{:ok, res} = map_put(d, atom(), atom([:x]))
to_quoted_string(res)
"map() and not %{atom() => :x}" # wrong
subtype?(closed_map(a: atom([:x])), res)
false # wrong
- negated domains
d2 = opt_difference(open_map([{[:integer], atom()}]),
closed_map([{[:integer], atom([:y])}]))
{:ok, res2} = map_put(d2, integer(), atom([:y]))
x = opt_difference(closed_map([{[:integer], atom([:y])}]), empty_map())
empty?(opt_intersection(x, res2))
true # wrong
- negated empty map
w = opt_difference(closed_map([{[:integer], atom([:z])}]), empty_map())
{:ok, pw} = map_put(w, integer(), atom([:y]))
to_quoted_string(pw)
"%{integer() => :y or :z} and not %{integer() => :y}" # wrong
empty?(pw)
false
x = opt_difference(closed_map([{[:integer], atom([:y])}]), empty_map())
empty?(opt_intersection(pw, x))
true # wrong
- map_update path
d = opt_difference(open_map(), empty_map())
{_v, resu, _e} = map_update(d, atom(), atom([:x]), false, true)
to_quoted_string(resu)
"map() and not %{atom() => :x}" # wrong
subtype?(closed_map(a: atom([:x])), resu)
false # wrong
- dynamic path
{:ok, resd} = map_put(dynamic(d), atom(), atom([:x]))
to_quoted_string(resd)
"dynamic(map() and not %{atom() => :x})" # wrong
subtype?(dynamic(closed_map(a: atom([:x]))), resd)
false # wrong
{_v2, resud, _e2} = map_update(dynamic(d), atom(), atom([:x]), false, true)
subtype?(dynamic(closed_map(a: atom([:x]))), resud)
false # wrong
Likely reason:
|
defp map_update_put_domains(bdd, domain_keys, type_fun, force?) do |
bdd_map rewrites every leaf label, including negated ones. The comment on
map_update_put_domains is not true as proven by the repros above.
For negations, we count on the idea that a negation will not remove any
type from a domain unless it completely cancels out the type.
Rewriting not(N) to not(put(N)) changes what is excluded. put(N) >= N, so not(put(N)) <= not(N). The result type can exclude reachable values even when nothing is cancelled.
Note: this is a different bug than #15507
Expected behavior
No unsound rewrite of negated BDD
Existing issue
Elixir and Erlang/OTP versions
Erlang/OTP 28 [erts-16.4.0.1] [source] [64-bit] [smp:12:12] [ds:12:12:10] [async-threads:1] [jit]
Interactive Elixir (1.21.0-dev)
Operating system
any
Current behavior
The following 5 repros are manifestations of the same underlying bug:
Likely reason:
elixir/lib/elixir/lib/module/types/descr.ex
Line 3786 in 4215bbe
bdd_maprewrites every leaf label, including negated ones. The comment onmap_update_put_domainsis not true as proven by the repros above.Rewriting
not(N)tonot(put(N))changes what is excluded.put(N)>=N, sonot(put(N))<=not(N). The result type can exclude reachable values even when nothing is cancelled.Note: this is a different bug than #15507
Expected behavior
No unsound rewrite of negated BDD