Preserve left element types in list subtraction

[lukaszsamson]

Teach the type system that list -- returns a possibly empty sublist of its left operand while preserving proper-list validation for both operands.

Assisted-by: Codex:GPT-5.6 Sol, Claude Fable 5

[josevalim]

Isn't this the same as left?

[lukaszsamson]

No. Trivial counterexample [:foo] -- [:foo] === []. If left is nonempty the result may be empty list. But even if we returned union(left, empty_list()) it would be unsound with negations. Given left as non_empty_list(atom()) and not list(atom([:a])), in [:b, :a] -- [:b] the result [:a] would fall outside the union type (credit Fable for this one counterexample).

[josevalim]

Fascinating example where list(a), list(term()) -> list(a) when a: term() gives a different result than a, list(term()) -> a when a: list(term()), which I would expect them to be equivalent. Does this make sense to you @gldubc?

[lukaszsamson]

Fascinating sure but currently purely synthetic. I don't think elixir can produce such type negation via guards/patterns. Guards do not allow expressing whole list properties and patterns only match on empty or list head. It may not be synthetic when type definition syntax lands.
Are they equivalent - it boils down to what -- actually preserves. Contains some type or is empty: yes, Is the list proper: yes, is the list not empty: no, contains at least one sth: no, contains at least one not sth: no

[josevalim]

@lukaszsamson ideally, we don't want to implement most of those, except for:

1. our type signatures are not expressive enough to type them
2. the functions are common enough that typing them now justify it

In that case, I am thinking the type signature of this would be a, list(term()) -> a when a: list(term()), right? And because it is not common, I think we can skip it for now.

[lukaszsamson]

The negation case can be covered with a hacky test. I'm not comfortable adding that. Would be easier with new_stack/1 and new_context/0 being public.

test "-- widens negated list types to their element type" do
  # List types are not closed under sublists: left admits [:b, :a]
  # (an atom list containing a non-:a element), but its sublist
  # [:b, :a] -- [:b] == [:a] escapes left and left ∪ empty_list(),
  # so returning either as the result type would be unsound.
  left = opt_difference(non_empty_list(atom()), list(atom([:a])))
  escaped_sublist = non_empty_list(atom([:a]))
  refute subtype?(escaped_sublist, opt_union(left, empty_list()))

  {result, context} =
    Module.Types.Apply.remote_apply(
      Module.Types.Apply.signature(:erlang, :--, 2),
      :erlang, :--,
      [left, non_empty_list(atom([:b]))],
      quote(do: [:b, :a] -- [:b]),
      %{mode: :static},
      Module.Types.context()
    )

  assert context.warnings == []
  assert subtype?(escaped_sublist, result)
  assert result == list(atom())
end

[lukaszsamson]

Added one more test and TODO matching ++