Map difference fast path break set algebra laws

[lukaszsamson]

Existing issue

• I have searched existing issues and could not find a duplicate.

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 code shows the bug:

# build map types `a`, `b`, `c`
a = closed_map(b: atom([:x, :y]), c: pid())
b =
  closed_map(
    b: if_set(opt_union(atom([:y]), float())),
    c: opt_union(pid(), opt_union(binary(), integer()))
  )
c = open_map(c: if_set(opt_union(pid(), binary())))

# `a` is a subtype of `c`
subtype?(a, c)
true

# so `(a \ b) \ c` must be empty for any `b`

ab = opt_difference(a, b)
abc = opt_difference(ab, c)

# `a \ b` is a subtype of `a` (and hence of `c`)
subtype?(ab, a)
true

# ((a \ b) \ c) and c must be disjoint
empty?(opt_intersection(abc, c))
false # should be true

# `a` is a subtype of `c`, (a \ b) \ c must be empty
empty?(abc)
false # should be true

Likely reason (as stated by GPT 5.5):
I do not understand the implementation well enough to verify the statement below so I present it as is

elixir/lib/elixir/lib/module/types/descr.ex

Line 5700 in 73cf46d

{:one_key_difference, a_diff, a_union} ->

The bug is BDD-variable-ordering dependent. In the node \ leaf one-key fast path, a_union is treated as exact a1 ∪ a2 for the dual branch D1 \ a_union. But the map leaf code builds it as “same tag/fields as the positive literal, with key -> v1 ∪ v2”. That equals the true union only in the exact-shape case where the positive literal is an open single-key map on the same key. For closed or multi-key positives, a_union is too small, so D1 \ a_union subtracts too little and the difference is too large.

Note: Pre #15433 there were more failing cases that the refactor addressed

Expected behavior

Set algebra laws preserved in fast path