`tuple_insert_at` loses the inserted element and misapplies it at wrong index

[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

Let's create an open tuple by difference operation (any tuple of size >= 2)

t2 = opt_difference(open_tuple([]), opt_union(tuple([]), tuple([term()])))

# equality holds
equal?(t2, open_tuple([term(), term()])) 
true

# now insert a float at index 2
t3 = tuple_insert_at(t2, 2, float())

to_quoted_string(t3)
"{...} and not {term(), float()} and not {float()}" # wrong, why is float type in negations? I'd expect the representation to be `{...} and not {term()} and not {}`

# this shows over-approximation
subtype?(tuple([integer(), integer(), atom()]), t3)
true # should be false

While over-approximation is accepted in this case it breaks congruence wrt equal? and the element layout is clearly wrong.

Open tuple constructed directly is not affected:

to_quoted_string(tuple_insert_at(open_tuple([term(), term()]), 2, float()))
"{term(), term(), float(), ...}"

subtype?(tuple([integer(), integer(), atom()]), tuple_insert_at(open_tuple([term(), term()]), 2, float()))
false

Reason:

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

Line 5320 in 34c7f21

bdd_map(bdd, fn bdd_leaf(tag, elements) ->

tuple_insert_static uses bdd_map which rewrites only explicit literal leaves. bdd_top and bdd_bot are not updated. In the repro bdd_map:

• rewrites the negated closed {} into {float()}
• rewrites the negated closed {:term} into {term(), float()}
• reaches the :bdd_top and leaves it unchanged - the inserted float() is never placed

Expected behavior

Correct application of inserted constraint