Disjunctive normal form attempt

notes.1.md

@@ -0,0 +1,72 @@
+These are some experiments with the disjunctive normal form we mentioned
+in https://github.com/josefs/Gradualizer/pull/524#discussion_r1200493035.
+
+First, https://typex.fly.dev/ seems to actually call CDuce under the hood.
+This can be inferred from the following error message generated based on some invalid input.
+Input:
+
+```
+g :: (_ -> {:t, :a} | {:t, :b})
+def g(_), do: {:t, :b}
+
+tuple_case :: (_ -> {:t, :a or :b})
+def tuple_case(arg), do: g(arg)
+
+tuple_case(:z)
+```
+
+Message:
+
+```
+Typing error:
+After extracting domain types from
+	{ _fun =[Any] -> |({ _tup=[`t `a] ; _size=2 }, { _tup=[`t `b] ; _size=2 }) ; _ari = 1 }
+Failed to parse the result:
+	Cduce_core.Parser.MenhirBasics.Error  <-------------- Cduce error
+```
+
+Second, let's consider:
+
+```erlang
+-spec g() -> {t, a | b}.
+g() -> {t, a}.
+
+-spec tuple_case1() -> {t, a} | {t, b}.
+tuple_case1() ->
+    R = g(),
+    R.
+
+-spec tuple_case2() -> {t, a} | {t, b}.
+tuple_case2() ->
+    g().
+```
+
+The following equivalent examples were tested with https://typex.fly.dev/:
+
+```
+g :: (_ -> {:t, :a or :b})
+def g(_), do: {:t, :b}
+
+tuple_case :: (_ -> {:t, :a} or {:t, :b})
+def tuple_case(arg), do: g(arg)
+
+tuple_case(:z)
+```
+
+```
+g :: (_ -> {:t, :a} or {:t, :b})
+def g(_), do: {:t, :b}
+
+tuple_case :: (_ -> {:t, :a or :b})
+def tuple_case(arg), do: g(arg)
+
+tuple_case(:z)
+```
+
+They both typecheck.
+This means that the Elixir prototype based on CDuce does indeed
+treat {t, a | b} :: {t, a} | {t, b}
+as well as {t, a} | {t, b} :: {t, a | b}.
+
+This can be achieved to some extent in Gradualizer, too,
+but it comes with significant breakage of tests.

src/typechecker.erl

@@ -1022,6 +1022,7 @@ expand_builtin_aliases({type, Ann, iolist, []}) ->
              {type, Ann, iolist, []}],
     Tail = [{type, Ann, nil, []},
             {type, Ann, binary, []}],
+    %% TODO: dnf
     {type, Ann, maybe_improper_list, [{type, Ann, union, Union},
                                       {type, Ann, union, Tail}]};
 expand_builtin_aliases({type, Ann, map, any}) ->
@@ -1055,6 +1056,34 @@ expand_builtin_aliases({type, Ann, no_return, []}) ->
 %% TODO: This is a kludge by which lists of types slip through calls to normalize().
 %%       Specifically, lists of Types representing bounded fun clauses.
 expand_builtin_aliases(Type) ->
+    dnf(Type).
+    %Type.
+
+-spec dnf(_) -> any().
+dnf(?type(union, _) = Ty) ->
+    Ty;
+dnf({type, _, _, any} = Ty) ->
+    Ty;
+%% A list of unions is not the same as a union of lists.
+dnf({type, _, list, _} = Ty) ->
+    Ty;
+dnf({type, Anno, Tag, Args} = Ty0) ->
+    {ArgExpandedUnions, AnyExpanded} =
+        lists:foldr(fun
+                        (?type(union, Tys), {Acc, _}) ->
+                            {[Tys | Acc], true};
+                        (Ty, {Acc, AnyExpanded}) ->
+                            {[[Ty] | Acc], AnyExpanded}
+                    end,
+                    {[], false}, Args),
+    ArgTyCombinations = gradualizer_lib:cartesian_product(ArgExpandedUnions),
+    if
+        AnyExpanded ->
+            {type, Anno, union, [ {type, Anno, Tag, A} || A <- ArgTyCombinations ]};
+        not AnyExpanded ->
+            Ty0
+    end;
+dnf(Type) ->
     Type.
 
 %% Flattens nested unions
@@ -2601,14 +2630,16 @@ do_type_check_expr_in(Env, ResTy, {tuple, _, TS} = Tup) ->
             {VBs, Css} = lists:unzip([ type_check_expr_in(Env, Ty, Expr)
                                     || {Ty, Expr} <- lists:zip(Tys, TS) ]),
             {union_var_binds(VBs, Env), constraints:combine([Cs|Css])};
-        {elem_tys, Tyss, Cs} ->
-            case type_check_tuple_union_in(Env, Tyss, TS) of
-                none ->
-                    {Ty, _VB, _Cs} = type_check_expr(Env#env{infer = true}, Tup),
-                    throw(type_error(Tup, Ty, ResTy));
-                {VBs, Css} ->
-                    {union_var_binds(VBs, Env), constraints:combine([Cs|Css])}
-            end;
+        {elem_tys, _Tyss, Cs1} ->
+            %% ResTy dictates that we expect a union of tuples.
+            {TupTy, VB, Cs2} = type_check_expr(Env, Tup),
+            Cs3 = case subtype(TupTy, ResTy, Env) of
+                      {true, Cs} ->
+                          Cs;
+                      false ->
+                          throw(type_error(Tup, TupTy, ResTy))
+                  end,
+            {VB, constraints:combine([Cs1, Cs2, Cs3])};
         any ->
             {_Tys, VBs, Css} = lists:unzip3([type_check_expr(Env, Expr)
                                            || Expr <- TS ]),
@@ -3583,19 +3614,6 @@ type_check_union_in1(Env, [Ty|Tys], Expr) ->
 type_check_union_in1(_Env, [], _Expr) ->
     none.
 
--spec type_check_tuple_union_in(env(), [[type()]], [expr()]) -> R when
-      R :: {[env()], [constraints:t()]} | none.
-type_check_tuple_union_in(Env, [Tys|Tyss], Elems) ->
-    try
-        lists:unzip([type_check_expr_in(Env, Ty, Expr)
-                   || {Ty, Expr} <- lists:zip(Tys, Elems)])
-    catch
-        E when element(1,E) == type_error ->
-            type_check_tuple_union_in(Env, Tyss, Elems)
-    end;
-type_check_tuple_union_in(_Env, [], _Elems) ->
-    none.
-
 -spec get_bounded_fun_type_list(atom(), arity(), env(), anno()) -> [type()].
 get_bounded_fun_type_list(Name, Arity, Env, P) ->
     case maps:find({Name, Arity}, Env#env.fenv) of

test/known_problems/should_pass/inner_union_subtype_of_root_union.erl

@@ -1,6 +1,6 @@
 -module(inner_union_subtype_of_root_union).
 
--export([tuple_case/0, map_case/1]).
+-export([map_case/1]).
 
 % The problem is that {t, a|b} is not subtype of {t, a} | {t, b}.
 
@@ -10,13 +10,11 @@
 %     {'type', anno(), 'map_field_assoc', [abstract_type()]}
 %   | {'type', anno(), 'map_field_exact', [abstract_type()]}
 
+% See also test/should_pass/inner_union_subtype_of_root_union_pass.erl
+
 -spec g() -> a | b.
 g() -> a.
 
--spec tuple_case() -> {t, a} | {t, b}.
-tuple_case() ->
-    {t, g()}.
-
 % The same thing holds for maps.
 -spec map_case(#{a => b | c}) -> #{a => b} | #{a => c}.
-map_case(M) -> M.
+map_case(M) -> M.

test/known_problems/should_pass/refine_bound_var_with_guard_should_pass.erl

@@ -1,6 +1,6 @@
 -module(refine_bound_var_with_guard_should_pass).
 
--export([f/1]).
+-export([f/1, g/1]).
 
 %% This type is simpler than gradualizer_type:abstract_type() by having less variants
 %% and by using tuples to contain deeper nodes. The latter frees us from having to deal

test/should_fail/tuple_union_fail.erl

@@ -3,6 +3,8 @@
 -export([f/0]).
 -export([tuple_union/0]).
 
+-gradualizer([infer]).
+
 -spec f() -> {integer()} | {boolean()}.
 f() ->
     {apa}.

test/should_pass/inner_union_subtype_of_root_union_pass.erl

@@ -0,0 +1,26 @@
+-module(inner_union_subtype_of_root_union_pass).
+
+-export([tuple_case1/0,
+         tuple_case2/0]).
+
+% The problem is that {t, a|b} is not subtype of {t, a} | {t, b}.
+
+% It has surfaced because
+%     {'type', anno(), 'map_field_assoc' | 'map_field_exact', [abstract_type()]}
+% is not a subtype of
+%     {'type', anno(), 'map_field_assoc', [abstract_type()]}
+%   | {'type', anno(), 'map_field_exact', [abstract_type()]}
+
+% See also test/known_problems/should_pass/inner_union_subtype_of_root_union.erl
+
+-spec g() -> a | b.
+g() -> a.
+
+-spec tuple_case1() -> {t, a} | {t, b}.
+tuple_case1() ->
+    R = {t, g()},
+    R.
+
+-spec tuple_case2() -> {t, a} | {t, b}.
+tuple_case2() ->
+    {t, g()}.

test/typechecker_tests.erl

@@ -76,7 +76,14 @@ subtype_test_() ->
      ?_assert(subtype(?t( 1..5              ), ?t( 1..3|4..6        ))),
      ?_assert(subtype(?t( 1..5|a            ), ?t( 1..3|4..6|atom() ))),
      ?_assert(subtype(?t( a|b               ), ?t( atom()           ))),
-     ?_assert(subtype(?t( (A :: boolean())|(B :: boolean()) ), ?t( boolean() ))),
+     ?_assert(subtype(?t( (A :: boolean())|(B :: boolean()) ),
+                      ?t( boolean() ))),
+     ?_assert(subtype(?t( {t, a|b}          ), ?t( {t, a} | {t, b}  ))),
+     ?_assert(subtype(?t( {t, a} | {t, b}   ), ?t( {t, a|b}         ))),
+     ?_assert(subtype(?t( {t, a|b, 1|2}     ),
+                      ?t( {t, a, 1} | {t, a, 2} | {t, b, 1} | {t, b, 2} ))),
+     ?_assert(subtype(?t( {t, a, 1} | {t, a, 2} | {t, b, 1} | {t, b, 2} ),
+                      ?t( {t, a|b, 1|2} ))),
 
      %% Lists
      ?_assert(subtype(?t( [a]               ), ?t( list()           ))),
@@ -164,6 +171,13 @@ not_subtype_test_() ->
      ?_assertNot(subtype(?t( {}             ), ?t( {any()}          ))),
      ?_assertNot(subtype(?t( {1..2, 3..4}   ), ?t( {1, 3}           ))),
 
+     ?_assertNot(subtype(?t( {t, a|b}           ), ?t( {t, a}       ))),
+     ?_assertNot(subtype(?t( {t, a} | {t, b}    ), ?t( {t, a}       ))),
+     ?_assertNot(subtype(?t( {t, a|b, 1|2}      ),
+                         ?t( {t, a, 1} | {t, b, 1}                  ))),
+     ?_assertNot(subtype(?t( {t, a, 1} | {t, a, 2} | {t, b, 1} | {t, b, 2} ),
+                         ?t( {t, a|b, 1}                            ))),
+
      %% Maps
      ?_assertNot(subtype(?t( #{}            ), ?t( #{a := b}                            ))),
      ?_assertNot(subtype(?t( #{a => b}      ), ?t( #{a := b}                            ))),