Enhance list type handling and add list_proper? function (#15002)

- Refactor list_bdd_to_pos_dnf to improve handling of negations and last types.
- Introduce list_proper? function to check if a list type is a proper list.
- Update list_hd and list_tl to fix wrong cases.
- Simplify list_bdd_to_pos_dnf by removing unnecessary checks.

Author: gldubc

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

@@ -1795,13 +1795,12 @@ defmodule Module.Types.Descr do
             #
             # A negation only matters when the negated list type is a supertype of the
             # corresponding positive list type; in that case we subtract the negated
-            # variant from the positive one.
+            # variant from the positive one. This is done in list_bdd_to_pos_dnf/1.
             {list_type, last_type} =
               list_bdd_to_pos_dnf(bdd)
               |> Enum.reduce({list_type, last_type_no_list}, fn
-                {head, tail}, {acc_head, acc_tail} ->
-                  tail = list_tail_unfold(tail)
-                  {union(head, acc_head), union(tail, acc_tail)}
+                {list, last, _negs}, {acc_list, acc_last} ->
+                  {union(list, acc_list), union(last, acc_last)}
               end)
 
             list_new(list_type, last_type)
@@ -1829,40 +1828,34 @@ defmodule Module.Types.Descr do
     end
   end
 
-  # Takes all the lines from the root to the leaves finishing with a 1,
-  # and compile into tuples of positive and negative nodes. Positive nodes are
-  # those followed by a left path, negative nodes are those followed by a right path.
-  defp list_bdd_to_dnf(bdd) do
-    bdd_to_dnf(bdd)
-    |> Enum.reduce([], fn {pos_list, neg_list}, acc ->
-      case non_empty_list_literals_intersection(pos_list) do
-        :empty ->
-          acc
-
-        {list, last} ->
-          if list_line_empty?(list, last, neg_list),
-            do: acc,
-            else: [{{list, last}, neg_list} | acc]
-      end
-    end)
-  end
-
   # Takes all the lines from the root to the leaves finishing with a 1,
   # and compile into tuples of positive and negative nodes. Keep only the non-empty positives,
   # and include the impact of negations on the last type.
   # To see if a negation changes the last type or the list type, we just need to check
   # if the negative list type is a supertype of the positive list type. In that case,
   # we can remove the negative last type from the positive one.
+
   # (If this subtracted type was empty, the whole type would be empty)
   defp list_bdd_to_pos_dnf(bdd) do
     bdd_to_dnf(bdd)
-    |> Enum.reduce([], fn {pos_list, neg_list}, acc ->
+    |> Enum.reduce([], fn {pos_list, negs}, acc ->
       case non_empty_list_literals_intersection(pos_list) do
         :empty ->
           acc
 
         {list, last} ->
-          if list_line_empty?(list, last, neg_list), do: acc, else: [{list, last} | acc]
+          Enum.reduce_while(negs, {last, []}, fn {neg_type, neg_last}, {acc_last, acc_negs} ->
+            if subtype?(list, neg_type) do
+              difference = difference(acc_last, neg_last)
+              if empty?(difference), do: {:halt, nil}, else: {:cont, {difference, acc_negs}}
+            else
+              {:cont, {acc_last, [{neg_type, neg_last} | acc_negs]}}
+            end
+          end)
+          |> case do
+            nil -> acc
+            {last, negs} -> [{list, last, Enum.reverse(negs)} | acc]
+          end
       end
     end)
   end
@@ -1885,6 +1878,38 @@ defmodule Module.Types.Descr do
   defp list_top?(bdd_leaf(:term, :term)), do: true
   defp list_top?(_), do: false
 
+  @doc """
+  Checks if a list type is a proper list (terminated by empty list).
+  """
+  def list_proper?(:term), do: false
+  def list_proper?(%{} = descr), do: Map.get(descr, :dynamic, descr) |> list_proper_static?()
+
+  defp list_proper_static?(:term), do: false
+
+  defp list_proper_static?(%{} = descr) do
+    # A list is proper if it's either the empty list alone, or all non-empty
+    # list types have tails that are subtypes of empty list
+    case descr do
+      %{bitmap: bitmap, list: bdd} ->
+        (bitmap &&& @bit_empty_list) != 0 and empty?(Map.drop(descr, [:list, :bitmap])) and
+          list_bdd_proper?(bdd)
+
+      %{bitmap: bitmap} ->
+        (bitmap &&& @bit_empty_list) != 0 and empty?(Map.delete(descr, :bitmap))
+
+      %{list: bdd} ->
+        empty?(Map.delete(descr, :list)) and list_bdd_proper?(bdd)
+
+      %{} ->
+        empty?(descr)
+    end
+  end
+
+  defp list_bdd_proper?(bdd) do
+    list_bdd_to_pos_dnf(bdd)
+    |> Enum.all?(fn {_list, last, _negs} -> subtype?(last, @empty_list) end)
+  end
+
   defp list_intersection(bdd_leaf(list1, last1), bdd_leaf(list2, last2)) do
     try do
       list = non_empty_intersection!(list1, list2)
@@ -1914,10 +1939,16 @@ defmodule Module.Types.Descr do
   # The result may be larger than the initial bdd1, which is maintained in the accumulator.
   defp list_difference(bdd_leaf(list1, last1) = bdd1, bdd_leaf(list2, last2) = bdd2) do
     cond do
-      disjoint?(list1, list2) or disjoint?(last1, last2) -> bdd_leaf(list1, last1)
-      subtype?(list1, list2) and subtype?(last1, last2) -> :bdd_bot
-      equal?(list1, list2) -> bdd_leaf(list1, difference(last1, last2))
-      true -> bdd_difference(bdd1, bdd2)
+      disjoint?(list1, list2) or disjoint?(last1, last2) ->
+        bdd_leaf(list1, last1)
+
+      subtype?(list1, list2) ->
+        if subtype?(last1, last2),
+          do: :bdd_bot,
+          else: bdd_leaf(list1, difference(last1, last2))
+
+      true ->
+        bdd_difference(bdd1, bdd2)
     end
   end
 
@@ -1991,20 +2022,17 @@ defmodule Module.Types.Descr do
 
   defp list_hd_static(%{list: bdd}) do
     list_bdd_to_pos_dnf(bdd)
-    |> Enum.reduce(none(), fn {list, _}, acc ->
-      union(list, acc)
-    end)
+    |> Enum.reduce(none(), fn {list, _last, _negs}, acc -> union(acc, list) end)
   end
 
   defp list_hd_static(%{}), do: none()
 
   @doc """
-  Returns the tail of a list.
+   Returns the tail of a list.
 
-  Errors on a possibly empty list.
-  On a non empty list of integers, it returns a (possibly empty) list of integers.
-  On a non empty list of integers, with an atom tail element, it returns either an atom,
-  or a (possibly empty) list of integers with an atom tail element.
+   For a `non_empty_list(t)`, the tail type is `list(t)`.
+  For an improper list `non_empty_list(t, s)`, the tail type is
+  `list(t, s) or s` (either the rest of the list or the terminator)
   """
   def list_tl(:term), do: :badnonemptylist
 
@@ -2042,7 +2070,8 @@ defmodule Module.Types.Descr do
           %{list: bdd}
       end
 
-    list_bdd_to_pos_dnf(bdd) |> Enum.reduce(initial, fn {_, tail}, acc -> union(tail, acc) end)
+    list_bdd_to_pos_dnf(bdd)
+    |> Enum.reduce(initial, fn {_list, last, _negs}, acc -> union(acc, last) end)
   end
 
   defp list_tl_static(%{}), do: none()
@@ -2054,12 +2083,19 @@ defmodule Module.Types.Descr do
       dnf
       |> Enum.reduce({[], false}, fn {list_type, last_type, negs}, {acc, list_rendered?} ->
         {name, arguments, list_rendered?} =
-          if subtype?(last_type, @empty_list) do
-            name = if empty?, do: :list, else: :non_empty_list
-            {name, [to_quoted(list_type, opts)], empty?}
-          else
-            args = [to_quoted(list_type, opts), to_quoted(last_type, opts)]
-            {:non_empty_list, args, list_rendered?}
+          cond do
+            subtype?(last_type, @empty_list) ->
+              name = if empty?, do: :list, else: :non_empty_list
+              {name, [to_quoted(list_type, opts)], empty?}
+
+            # Sugar: print the last type as term() if it only misses non empty lists.
+            subtype?(@not_non_empty_list, last_type) ->
+              args = [to_quoted(list_type, opts), {:term, [], []}]
+              {:non_empty_list, args, list_rendered?}
+
+            true ->
+              args = [to_quoted(list_type, opts), to_quoted(last_type, opts)]
+              {:non_empty_list, args, list_rendered?}
           end
 
         acc =
@@ -2096,27 +2132,19 @@ defmodule Module.Types.Descr do
   end
 
   # Eliminate empty lists from the union, and redundant types (that are subtypes of others,
-  # or that can be merged with others).
+  # or that can be merged with others). List_bdd_to_pos_dnf already takes into account the
+  # impact of negations on the last type.
   defp list_normalize(bdd) do
-    list_bdd_to_dnf(bdd)
-    |> Enum.reduce([], fn {{list, last}, negs}, acc ->
-      # First, try to eliminate the negations from the existing type.
-      {list, last, negs} =
+    list_bdd_to_pos_dnf(bdd)
+    |> Enum.reduce([], fn {list, last, negs}, acc ->
+      # Prune negations from those with empty intersections.
+      negs =
         Enum.uniq(negs)
-        |> Enum.reduce({list, last, []}, fn {nlist, nlast}, {acc_list, acc_last, acc_negs} ->
-          last = list_tail_unfold(last)
-          new_list = intersection(list, nlist)
-          new_last = intersection(last, nlast)
-
-          cond do
-            # No intersection between the list and the negative
-            empty?(new_list) or empty?(new_last) -> {acc_list, acc_last, acc_negs}
-            subtype?(list, nlist) -> {acc_list, difference(acc_last, nlast), acc_negs}
-            true -> {acc_list, acc_last, [{nlist, nlast} | acc_negs]}
-          end
+        |> Enum.filter(fn {nlist, nlast} ->
+          not empty?(intersection(list, nlist)) and not empty?(intersection(last, nlast))
         end)
 
-      add_to_list_normalize(acc, list, last, negs |> Enum.reverse())
+      add_to_list_normalize(acc, list, last, negs)
     end)
   end
 

lib/elixir/test/elixir/module/types/descr_test.exs

@@ -1249,6 +1249,7 @@ defmodule Module.Types.DescrTest do
       assert list_hd(non_empty_list(term())) == {:ok, term()}
       assert list_hd(non_empty_list(integer())) == {:ok, integer()}
       assert list_hd(difference(list(number()), list(integer()))) == {:ok, number()}
+      assert list_hd(non_empty_list(atom(), float())) == {:ok, atom()}
 
       assert list_hd(dynamic()) == {:ok, dynamic()}
       assert list_hd(dynamic(list(integer()))) == {:ok, dynamic(integer())}
@@ -1267,6 +1268,27 @@ defmodule Module.Types.DescrTest do
       assert list_hd(non_empty_list(atom(), negation(list(term(), term())))) == {:ok, atom()}
     end
 
+    test "list_proper?" do
+      assert list_proper?(term()) == false
+      assert list_proper?(none()) == true
+      assert list_proper?(empty_list()) == true
+      assert list_proper?(non_empty_list(integer())) == true
+      assert list_proper?(non_empty_list(integer(), atom())) == false
+      assert list_proper?(non_empty_list(integer(), term())) == false
+      assert list_proper?(non_empty_list(integer(), list(term()))) == true
+      assert list_proper?(list(integer()) |> union(list(integer(), integer()))) == false
+      assert list_proper?(dynamic(list(integer()))) == true
+      assert list_proper?(dynamic(list(integer(), atom()))) == false
+
+      # An empty list
+      list_with_tail =
+        non_empty_list(atom(), union(integer(), empty_list()))
+        |> difference(non_empty_list(atom([:ok]), integer()))
+        |> difference(non_empty_list(atom(), term()))
+
+      assert list_proper?(list_with_tail) == true
+    end
+
     test "list_tl" do
       assert list_tl(none()) == :badnonemptylist
       assert list_tl(term()) == :badnonemptylist
@@ -1284,11 +1306,9 @@ defmodule Module.Types.DescrTest do
       # integers with an atom tail, or a (possibly empty) list of tuples with a float tail.
       assert list_tl(union(non_empty_list(integer(), atom()), non_empty_list(tuple(), float()))) ==
                {:ok,
-                atom()
-                |> union(float())
-                |> union(
-                  union(non_empty_list(integer(), atom()), non_empty_list(tuple(), float()))
-                )}
+                union(atom(), float())
+                |> union(non_empty_list(integer(), atom()))
+                |> union(non_empty_list(tuple(), float()))}
 
       assert list_tl(dynamic()) == {:ok, dynamic()}
       assert list_tl(dynamic(list(integer()))) == {:ok, dynamic(list(integer()))}
@@ -2394,6 +2414,14 @@ defmodule Module.Types.DescrTest do
       assert union(dynamic(list(integer(), float())), dynamic(list(integer(), pid())))
              |> to_quoted_string() ==
                "dynamic(empty_list() or non_empty_list(integer(), float() or pid()))"
+
+      list_with_tail =
+        non_empty_list(atom(), union(integer(), empty_list()))
+        |> difference(non_empty_list(atom([:ok]), integer()))
+        |> difference(non_empty_list(atom(), integer()))
+
+      # Check that simplifications occur.
+      assert to_quoted_string(list_with_tail) == "non_empty_list(atom())"
     end
 
     test "tuples" do