`list_tl` underapproximates on difference type

[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 proves the bug. Here t is a set of all non empty lists with atom elements where not all of them are :a. This includes lists like [:b], [:a, :b], [:b, :a], [:b, :b], [:b, :a, :a], [:b, :a, :b], ... etc.

t = opt_difference(non_empty_list(atom()), non_empty_list(atom([:a])))

a tail of that difference should be list(atom()) as it includes [], [:b], [:a], [:a, :a], [:a, :b], ...
of which non_empty_list(atom([:a])) is a subtype

subtype?(non_empty_list(atom([:a])), list(atom))
true

yet the returned type is too narrow

{:ok, tl} = list_tl(t)
subtype?(non_empty_list(atom([:a])), tl)
false

Likely reason:

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

Line 2467 in 1d59997

|> Enum.reduce(initial, fn {_list, last, _negs}, acc -> opt_union(acc, last) end)

reuses the original BDD with the negations instead of rebuilding from positive DNF leaves

Expected behavior

subtype?(non_empty_list(atom([:a])), tl) should return true, list_tl should not narrow the type

[gldubc]

The issue is a bit trickier than it seems:

1. the negatives can be discarded after computing tl. It is a safe underapproximation, and should be immediately implemented to replace the current unsafe underapproximation.

2. but there are edge cases where removing them completely is imprecise (though not unsafe). here are two:

a) A simple one

t =
    non_empty_list(:a | :b)
    and not non_empty_list(:a)
    and not non_empty_list(:b)

The lists of this type cannot be of size 1, because it would be either [:a] or [:b] (as if "all possible heads are covered") so the tail cannot be the empty list.

b) A more complex one

t =
    non_empty_list(:a | :b | :c)
    and not non_empty_list(:a | :b)
    and not non_empty_list(:b | :c)

the negative heads cover all possible positive heads:

(:a | :b) or (:b | :c) = :a | :b | :c

but in fact list(:b) tails are impossible, because lists [:a, :b .... :b] and [:c, :b, ..., :b] are removed by the negations already.

So tl(t) = list(:a | :b | :c) and not list(:b)

@josevalim
For now, I propose to use a safe overapproximation that simply discards negatives.

In the future, having exactly tail computation could be solved either by

• a bespoke algorithm that checks all the possible coverage and is able to output the precise type above
• implementing lists using recursive pairs and use snd projection

Can we keep this issue to track the approximation?

[lukaszsamson]

Two more manifestations of the same bug. Both should be fixed automatically by the positive-only rebuild applied at the BDD seed level.

Improper terminators (the suffix dimension is narrowed the same way):

inp = opt_difference(non_empty_list(atom(), opt_union(pid(), port())),
                     non_empty_list(atom([:a]), pid()))
{:ok, tl} = list_tl(inp)
subtype?(non_empty_list(atom([:a]), pid()), tl) # false, should be true: [:b, :a | pid] belongs to inp and its tail is [:a | pid]

Gradual wrapper (the dynamic projection goes through the same helper):

{:ok, tl} = list_tl(dynamic(opt_difference(non_empty_list(atom()),
                                           non_empty_list(atom([:a])))))
subtype?(dynamic(non_empty_list(atom([:a]))), tl)  # false; should be true

the negatives can be discarded after computing tl. It is a safe underapproximation

I believe you meant overapproximation @gldubc

Also, a note on your example (a): on current main@450a24c84037e27062cd2d9be4536b1589f8fa2f it exhibits the unsoundness too, not only the future precision gap

ab = atom([:a, :b])
t =
  non_empty_list(ab)
  |> opt_difference(non_empty_list(atom([:a])))
  |> opt_difference(non_empty_list(atom([:b])))

{:ok, tl} = list_tl(t)

to_quoted_string(tl) # "list(:a or :b) and not (non_empty_list(:b) or non_empty_list(:a))"
#  the input's negations were carried into the tail type

# unsoundness due to underapproximation: [:a, :b, :a] is in t and its tail is [:b, :a] which is in non_empty_list(:a or :b)
subtype?(non_empty_list(ab), tl) # false, invalid underapproximation

# imprecision: t has no size-1 values, so no tail is []; exact tl excludes empty_list(), yet:
subtype?(empty_list(), tl) # true