Type checking improvements

* Ensure we do not accumulate previous information across clauses
* Avoid union(a, not a) when building domains
* Ensure union with an open map/tuples returns the open map/tuple
* Remove deep traversal on bdd leaf intersection which was slowing
  compilation of projects like open_api_spex

Closes #15285.

Author: josevalim

lib/elixir/lib/module/types.ex

@@ -321,28 +321,41 @@ defmodule Module.Types do
     stack = stack |> fresh_stack(mode, fun_arity) |> with_file_meta(meta)
     base_info = {:def, kind, fun, expected}
 
-    {_, _, _, mapping, clauses_types, clauses_context} =
-      Enum.reduce(clauses, {0, 0, Pattern.init_previous(), [], [], context}, fn
-        {meta, args, guards, body}, {index, total, previous, mapping, inferred, acc_context} ->
+    {_, _, _, domain, mapping, clauses_types, clauses_context} =
+      Enum.reduce(clauses, {0, 0, Pattern.init_previous(), [], [], [], context}, fn
+        {meta, args, guards, body},
+        {index, total, previous, domain, mapping, inferred, acc_context} ->
           fresh_context = fresh_context(acc_context)
           info = {base_info, args, guards}
 
           try do
-            {trees, previous, context} =
+            {trees, head_no_previous_args_types, previous, head_context} =
               Pattern.of_head(args, guards, expected, previous, info, meta, stack, fresh_context)
 
             {return_type, context} =
-              Expr.of_expr(body, Descr.term(), body, stack, context)
+              Expr.of_expr(body, Descr.term(), body, stack, head_context)
 
             args_types = Pattern.of_domain(trees, stack, context)
 
             {type_index, inferred} =
               add_inferred(inferred, args_types, return_type, total - 1, [])
 
+            domain =
+              case domain do
+                [] ->
+                  args_types
+
+                _ ->
+                  head_args_types = Pattern.of_domain(trees, stack, head_context)
+                  compute_domain(args_types, head_args_types, head_no_previous_args_types, domain)
+              end
+
             if type_index == -1 do
-              {index + 1, total + 1, previous, [{index, total} | mapping], inferred, context}
+              mapping = [{index, total} | mapping]
+              {index + 1, total + 1, previous, domain, mapping, inferred, context}
             else
-              {index + 1, total, previous, [{index, type_index} | mapping], inferred, context}
+              mapping = [{index, type_index} | mapping]
+              {index + 1, total, previous, domain, mapping, inferred, context}
             end
           rescue
             e ->
@@ -352,19 +365,69 @@ defmodule Module.Types do
 
     domain =
       case clauses_types do
-        [_] ->
-          nil
-
-        _ ->
-          clauses_types
-          |> Enum.map(fn {args, _} -> args end)
-          |> Enum.zip_with(fn types -> Enum.reduce(types, &Descr.union/2) end)
+        [_] -> nil
+        _ -> domain
       end
 
     inferred = {:infer, domain, Enum.reverse(clauses_types)}
     {inferred, mapping, restore_context(clauses_context, context)}
   end
 
+  defp compute_domain(
+         [arg | args_types],
+         [head_arg | head_args_types],
+         [no_prev_arg | no_prev_args_types],
+         [d | domain]
+       ) do
+    [
+      # This is an optimization that broadens the domain, but it is acceptable
+      # because the domain is used for reverse arrows and not type checking.
+      #
+      # The overall idea is that, if we have a function with three clauses,
+      # the domain is computed by unioning their inferred types. However, their
+      # inferred types often have the different of the previous clauses:
+      #
+      #     union(r3 ^ (c3 - c2 - c1), r2 ^ (c2 - c1), r1 ^ c1)
+      #
+      # Where `rN` represents the refinement in every function body.
+      #
+      # What this function does is, if the type of a given arg in a clause
+      # before and after the body is the same (meaning r3 is term), then
+      # we replace all of `(c3 - c2 - c1)` by just `c3`, which removes
+      # many of the differences in the node. However, keep in mind that,
+      # because `r2` may have refine `c2` in the previous clause, the domain
+      # may end-up being broader. Take this example:
+      #
+      #     % %{..., foo: integer()} -> binary()
+      #     def example(%{foo: var}), do: Integer.to_string(var)
+      #
+      #     % %{...} and not %{..., foo: term()} -> :error
+      #     def example(%{}), do: :error
+      #
+      # The actual domain is:
+      #
+      #     %{..., foo: not_set()} or %{..., foo: integer()}
+      #     #=> %{..., foo: if_set(integer())}
+      #
+      # But we will infer:
+      #
+      #     %{...} or %{..., foo: integer()}
+      #     #=> %{...}
+      #
+      # We lose precision but this is exactly what we want: to have simpler types.
+      # Furthermore, the signature used in type checking is not refined in any way,
+      # so type checking is still sound.
+      if arg == head_arg do
+        Descr.union(Descr.upper_bound(no_prev_arg), d)
+      else
+        Descr.union(arg, d)
+      end
+      | compute_domain(args_types, head_args_types, no_prev_args_types, domain)
+    ]
+  end
+
+  defp compute_domain([], [], [], []), do: []
+
   # We check for term equality of types as an optimization
   # to reduce the amount of check we do at runtime.
   defp add_inferred([{args, existing_return} | tail], args, return, index, acc),

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

@@ -2870,6 +2870,12 @@ defmodule Module.Types.Descr do
     end
   end
 
+  defp map_union(bdd_leaf(:open, fields) = leaf, _) when is_fields_empty(fields),
+    do: leaf
+
+  defp map_union(_, bdd_leaf(:open, fields) = leaf) when is_fields_empty(fields),
+    do: leaf
+
   defp map_union(bdd_leaf(tag1, fields1), bdd_leaf(tag2, fields2)) do
     case maybe_optimize_map_union(tag1, fields1, tag2, fields2) do
       {tag, fields} -> bdd_leaf(tag, fields)
@@ -3043,6 +3049,9 @@ defmodule Module.Types.Descr do
   defp map_difference(_, bdd_leaf(:open, [])),
     do: :bdd_bot
 
+  defp map_difference(bdd_leaf(:open, []), {_, _, _, _} = bdd2),
+    do: bdd_negation(bdd2)
+
   defp map_difference(bdd1, bdd2),
     do: bdd_difference(bdd1, bdd2, &map_leaf_difference/3)
 
@@ -4961,10 +4970,10 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp tuple_difference(bdd_leaf(:open, []), bdd_leaf(:open, [])),
+  defp tuple_difference(_, bdd_leaf(:open, [])),
     do: :bdd_bot
 
-  defp tuple_difference(bdd_leaf(:open, []), bdd2),
+  defp tuple_difference(bdd_leaf(:open, []), {_, _, _, _} = bdd2),
     do: bdd_negation(bdd2)
 
   defp tuple_difference(bdd1, bdd2),
@@ -5163,6 +5172,12 @@ defmodule Module.Types.Descr do
     end)
   end
 
+  defp tuple_union(bdd_leaf(:open, fields) = leaf, _) when is_fields_empty(fields),
+    do: leaf
+
+  defp tuple_union(_, bdd_leaf(:open, fields) = leaf) when is_fields_empty(fields),
+    do: leaf
+
   defp tuple_union(
          bdd_leaf(tag1, elements1) = tuple1,
          bdd_leaf(tag2, elements2) = tuple2
@@ -5845,8 +5860,8 @@ defmodule Module.Types.Descr do
   defp bdd_difference_union(i, u1, u2),
     do: bdd_difference(i, bdd_union(u1, u2))
 
-  # We avoid unions because they are lazy and we prune
-  # intersections more actively.
+  # We avoid bdd_negation(bdd_union(u1, u2)) because the negation
+  # would spread the unions across constrained and dual parts anyway.
   defp bdd_negation_union(u1, u2) do
     bdd_intersection(bdd_negation(u1), bdd_negation(u2))
   end
@@ -6049,109 +6064,70 @@ defmodule Module.Types.Descr do
 
   # Intersections are great because they allow us to cut down
   # the number of nodes in the tree. So whenever we have a leaf,
-  # we actually propagate it throughout the whole tree, cutting
-  # down nodes.
-  defguardp is_not_open(leaf) when elem(leaf, 0) != :open
-
+  # we propagate it throughout the whole tree, cutting down nodes.
   defp bdd_intersection(bdd_leaf(_, _) = leaf1, bdd_leaf(_, _) = leaf2, leaf_intersection) do
     leaf_intersection.(leaf1, leaf2)
   end
 
-  defp bdd_intersection(bdd_leaf(_, _) = leaf, bdd, leaf_intersection) when is_not_open(leaf) do
-    bdd_leaf_intersection(leaf, bdd, leaf_intersection)
+  defp bdd_intersection(bdd, bdd_leaf(tag, _) = leaf, leaf_intersection) when tag != :open do
+    bdd_non_open_leaf_intersection(leaf, bdd, leaf_intersection)
   end
 
-  defp bdd_intersection(bdd, bdd_leaf(_, _) = leaf, leaf_intersection) when is_not_open(leaf) do
-    bdd_leaf_intersection(leaf, bdd, leaf_intersection)
+  defp bdd_intersection(bdd_leaf(tag, _) = leaf, bdd, leaf_intersection) when tag != :open do
+    bdd_non_open_leaf_intersection(leaf, bdd, leaf_intersection)
   end
 
-  # Take two BDDs, B1 = {a1, C1, U2, D2} and B2.
-  #
-  # When C1 = :bdd_top, we have:
+  defp bdd_intersection(bdd1, bdd2, _leaf_intersection) do
+    bdd_intersection(bdd1, bdd2)
+  end
+
+  # Take two BDDs, B1 = {a1, C1, U1, D1} and B2 = a2.
   #
-  #     ((a1 and C1) or U2 or (not a1 and D2)) and B2
-  #     (a1 and B2) or (B2 and U2) or (B2 and not a1 and D2)
+  # We have:
   #
-  # When C1 = :bdd_bot, we have:
+  #     ((a1 and C1) or U1 or (not a1 and D1)) and a2
+  #     (a1 and a2 and C1) or (a2 and U1) or (a2 and not a1 and D1)
   #
-  #     (U2 or (not a1 and D2)) and B2
-  #     (B2 and U2) or (B2 and not a1 and D2)
-  defp bdd_intersection({leaf, :bdd_top, u, d}, bdd, leaf_intersection) when is_not_open(leaf) do
-    bdd_leaf_intersection(leaf, bdd, leaf_intersection)
-    |> bdd_union(bdd_intersection(u, bdd, leaf_intersection))
-    |> case do
-      result when d == :bdd_bot -> result
-      result -> bdd_union(result, bdd_intersection(bdd, {leaf, :bdd_bot, :bdd_bot, d}))
-    end
+  # When C1 = :bdd_top, (a1 and a2) or (a2 and U2) or (a2 and not a1 and D2)
+  # When C2 = :bdd_bot, (a2 and U2) or (a2 and not a1 and D2)
+  defp bdd_non_open_leaf_intersection(leaf1, bdd_leaf(_, _) = leaf2, leaf_intersection) do
+    leaf_intersection.(leaf1, leaf2)
   end
 
-  defp bdd_intersection(bdd, {leaf, :bdd_top, u, d}, leaf_intersection) when is_not_open(leaf) do
-    bdd_leaf_intersection(leaf, bdd, leaf_intersection)
-    |> bdd_union(bdd_intersection(u, bdd, leaf_intersection))
+  defp bdd_non_open_leaf_intersection(leaf, {a, :bdd_top, u, d}, leaf_intersection) do
+    leaf_intersection.(a, leaf)
+    |> bdd_union(bdd_non_open_leaf_intersection(leaf, u, leaf_intersection))
     |> case do
-      result when d == :bdd_bot -> result
-      result -> bdd_union(result, bdd_intersection(bdd, {leaf, :bdd_bot, :bdd_bot, d}))
-    end
-  end
+      result when d == :bdd_bot ->
+        result
 
-  defp bdd_intersection({leaf, :bdd_bot, u, d}, bdd, leaf_intersection) when is_not_open(leaf) do
-    case bdd_intersection(u, bdd, leaf_intersection) do
-      result when d == :bdd_bot -> result
-      result -> bdd_union(result, bdd_intersection(bdd, {leaf, :bdd_bot, :bdd_bot, d}))
+      result ->
+        leaf
+        |> bdd_non_open_leaf_intersection(d, leaf_intersection)
+        |> bdd_difference(a)
+        |> bdd_union(result)
     end
   end
 
-  defp bdd_intersection(bdd, {leaf, :bdd_bot, u, d}, leaf_intersection) when is_not_open(leaf) do
-    case bdd_intersection(u, bdd, leaf_intersection) do
-      result when d == :bdd_bot -> result
-      result -> bdd_union(result, bdd_intersection(bdd, {leaf, :bdd_bot, :bdd_bot, d}))
+  defp bdd_non_open_leaf_intersection(leaf, {a, :bdd_bot, u, d}, leaf_intersection) do
+    case bdd_non_open_leaf_intersection(leaf, u, leaf_intersection) do
+      result when d == :bdd_bot ->
+        result
+
+      result ->
+        leaf
+        |> bdd_non_open_leaf_intersection(d, leaf_intersection)
+        |> bdd_difference(a)
+        |> bdd_union(result)
     end
   end
 
-  defp bdd_intersection(bdd1, bdd2, _leaf_intersection) do
+  defp bdd_non_open_leaf_intersection(bdd1, bdd2, _leaf_intersection) do
     bdd_intersection(bdd1, bdd2)
   end
 
-  defp bdd_leaf_intersection(leaf, bdd, intersection) do
-    case bdd do
-      :bdd_top ->
-        leaf
-
-      :bdd_bot ->
-        :bdd_bot
-
-      bdd_leaf(_, _) ->
-        intersection.(leaf, bdd)
-
-      {bdd_leaf(:open, _), _, _, _} ->
-        bdd_intersection(leaf, bdd)
-
-      {lit, c, u, _} when lit == leaf ->
-        case bdd_union(c, u) do
-          :bdd_bot -> :bdd_bot
-          cu -> {lit, cu, :bdd_bot, :bdd_bot}
-        end
-
-      {lit, c, u, d} ->
-        rest =
-          bdd_union(
-            bdd_leaf_intersection(leaf, u, intersection),
-            bdd_difference(bdd_leaf_intersection(leaf, d, intersection), lit)
-          )
-
-        if c == :bdd_bot do
-          rest
-        else
-          case intersection.(leaf, lit) do
-            :bdd_bot -> rest
-            new_leaf -> bdd_union(bdd_leaf_intersection(new_leaf, c, intersection), rest)
-          end
-        end
-    end
-  end
-
-  # {lit, c, u, d} = (lit and c) or u or (not lit and d), so
-  # its negation is ((lit and not c) or (not lit and not d)) and not u.
+  # {lit, c, u, d} = (lit and c) or u or (not lit and d),
+  # so its negation is ((lit and not c) or (not lit and not d)) and not u.
   def bdd_negation(:bdd_top), do: :bdd_bot
   def bdd_negation(:bdd_bot), do: :bdd_top
   def bdd_negation({_, _} = pair), do: {pair, :bdd_bot, :bdd_bot, :bdd_top}

lib/elixir/lib/module/types/expr.ex

@@ -834,7 +834,7 @@ defmodule Module.Types.Expr do
           {patterns, guards} = extract_head(head)
           info = {base_info, head}
 
-          {trees, previous, context} =
+          {trees, _, previous, context} =
             Pattern.of_head(patterns, guards, domain, previous, info, meta, stack, context)
 
           {result, context} = of_body.(trees, body, context)

lib/elixir/lib/module/types/pattern.ex

@@ -50,7 +50,9 @@ defmodule Module.Types.Pattern do
   end
 
   defp previous_to_string({list, _}) do
-    Enum.map_join(list, "\n    ", fn types ->
+    list
+    |> Enum.reverse()
+    |> Enum.map_join("\n    ", fn types ->
       types
       |> Enum.map_join(", ", &(&1 |> upper_bound() |> to_quoted_string()))
       |> indent(4)
@@ -190,27 +192,28 @@ defmodule Module.Types.Pattern do
       # First we check if it fails without previous, if it doesn't, check if it is redundant.
       case of_precise_head(patterns, guards, expected, init_previous(), tag, stack, original) do
         {other_trees, _, _, _, %{failed: true} = other_context} ->
-          {other_trees, previous, other_context}
+          {other_trees, args_types, previous, other_context}
 
         {other_trees, _, _, args_types, other_context} ->
           if previous_subtype?(args_types, previous) do
             warning = {:redundant, tag, expected, args_types, previous, other_context}
-            {other_trees, previous, warn(__MODULE__, warning, meta, stack, other_context)}
+            context = warn(__MODULE__, warning, meta, stack, other_context)
+            {other_trees, args_types, previous, context}
           else
-            {trees, previous, context}
+            {trees, args_types, previous, context}
           end
       end
     else
       cond do
         check_previous? and previous_subtype?(args_types, previous) ->
           warning = {:redundant, tag, expected, args_types, previous, context}
-          {trees, previous, warn(__MODULE__, warning, meta, stack, context)}
+          {trees, args_types, previous, warn(__MODULE__, warning, meta, stack, context)}
 
         precise? ->
-          {trees, concat_previous(args_types, previous), context}
+          {trees, args_types, concat_previous(args_types, previous), context}
 
         true ->
-          {trees, previous, context}
+          {trees, args_types, previous, context}
       end
     end
   end
@@ -235,7 +238,7 @@ defmodule Module.Types.Pattern do
            of_pattern_intersect(trees, 0, [], pattern_info, tag, stack, context),
          # We compute the args types before we do the intersection with previous clauses
          args_types =
-           (with [_ | _] <- previous,
+           (with false <- empty_previous?(previous),
                  {:ok, _types, context} <-
                    of_pattern_refine(types, changed, pattern_info, tag, stack, context) do
               trees_to_args_types(trees, stack, context)