dialyzer: Modify warning for comparison of opaque types

Comparing two operands for (in)equality is allowed if both operands
are of the same unknown opaque type. Since OTP 17, there is a warning
if the types of the operands have nothing in common (this cannot
happen before OTP 17). However, the warning says there is a test
between opaque types, which is wrong. The warning now states that the
comparison cannot evaluate to 'true', which is more consistent.

6 files changed, 95 insertions, 24 deletions

diff --git a/lib/dialyzer/test/opaque_SUITE_data/results/para b/lib/dialyzer/test/opaque_SUITE_data/results/para
index e50979e2f0..8fe67e39ad 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/results/para
+++ b/lib/dialyzer/test/opaque_SUITE_data/results/para
@@ -29,3 +29,5 @@ para4.erl:74: Attempt to test for equality between a term of type para4_adt:int(
 para4.erl:79: Attempt to test for equality between a term of type para4_adt:int(2 | 3 | 4) and a term of opaque type para4_adt:int(5 | 6 | 7)
 para4.erl:84: Attempt to test for equality between a term of type para4_adt:un(3 | 4) and a term of opaque type para4_adt:un(1 | 2)
 para4.erl:89: Attempt to test for equality between a term of type para4_adt:tup({_,_}) and a term of opaque type para4_adt:tup(tuple())
+para5.erl:13: Attempt to test for inequality between a term of type para5_adt:dd(atom()) and a term of opaque type para5_adt:d()
+para5.erl:8: The test para5_adt:d() =:= para5_adt:d() can never evaluate to 'true'
diff --git a/lib/dialyzer/test/opaque_SUITE_data/results/simple b/lib/dialyzer/test/opaque_SUITE_data/results/simple
index 29864d6065..1a7a139d6e 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/results/simple
+++ b/lib/dialyzer/test/opaque_SUITE_data/results/simple
@@ -28,11 +28,11 @@ rec_api.erl:99: Record construction #r2{f1::10} violates the declared type of fi
 simple1_api.erl:113: The test simple1_api:d1() =:= simple1_api:d2() can never evaluate to 'true'
 simple1_api.erl:118: Guard test simple1_api:d2() =:= A::simple1_api:d1() can never succeed
 simple1_api.erl:142: Attempt to test for equality between a term of type simple1_adt:o2() and a term of opaque type simple1_adt:o1()
-simple1_api.erl:148: Guard test simple1_adt:o2() =:= A::simple1_adt:o1() contains an opaque term as 1st argument
+simple1_api.erl:148: Guard test simple1_adt:o2() =:= A::simple1_adt:o1() contains opaque terms as 1st and 2nd arguments
 simple1_api.erl:154: Attempt to test for inequality between a term of type simple1_adt:o2() and a term of opaque type simple1_adt:o1()
 simple1_api.erl:160: Attempt to test for inequality between a term of type simple1_adt:o2() and a term of opaque type simple1_adt:o1()
 simple1_api.erl:165: Attempt to test for equality between a term of type simple1_adt:c2() and a term of opaque type simple1_adt:c1()
-simple1_api.erl:181: Guard test A::simple1_adt:d1() =< B::simple1_adt:d2() contains an opaque term as 1st argument
+simple1_api.erl:181: Guard test A::simple1_adt:d1() =< B::simple1_adt:d2() contains opaque terms as 1st and 2nd arguments
 simple1_api.erl:185: Guard test 'a' =< B::simple1_adt:d2() contains an opaque term as 2nd argument
 simple1_api.erl:189: Guard test A::simple1_adt:d1() =< 'd' contains an opaque term as 1st argument
 simple1_api.erl:197: The type test is_integer(A::simple1_adt:d1()) breaks the opaqueness of the term A::simple1_adt:d1()
@@ -72,12 +72,12 @@ simple1_api.erl:499: The call 'foo':A(A::simple1_api:i()) requires that A is of
 simple1_api.erl:503: The call 'foo':A(A::simple1_adt:i()) requires that A is of type atom() not simple1_adt:i()
 simple1_api.erl:507: The call A:'foo'(A::simple1_api:i()) requires that A is of type atom() | tuple() not simple1_api:i()
 simple1_api.erl:511: The call A:'foo'(A::simple1_adt:i()) requires that A is of type atom() | tuple() not simple1_adt:i()
-simple1_api.erl:519: Guard test A::simple1_adt:d2() == B::simple1_adt:d1() contains an opaque term as 1st argument
+simple1_api.erl:519: Guard test A::simple1_adt:d2() == B::simple1_adt:d1() contains opaque terms as 1st and 2nd arguments
 simple1_api.erl:534: Guard test A::simple1_adt:d1() >= 3 contains an opaque term as 1st argument
 simple1_api.erl:536: Guard test A::simple1_adt:d1() == 3 contains an opaque term as 1st argument
 simple1_api.erl:538: Guard test A::simple1_adt:d1() =:= 3 contains an opaque term as 1st argument
 simple1_api.erl:548: The call erlang:'<'(A::simple1_adt:d1(),3) contains an opaque term as 1st argument when terms of different types are expected in these positions
-simple1_api.erl:558: The call erlang:'=<'(A::simple1_adt:d1(),B::simple1_adt:d2()) contains an opaque term as 1st argument when terms of different types are expected in these positions
+simple1_api.erl:558: The call erlang:'=<'(A::simple1_adt:d1(),B::simple1_adt:d2()) contains opaque terms as 1st and 2nd arguments when terms of different types are expected in these positions
 simple1_api.erl:565: Guard test {digraph:graph(),3} > {digraph:graph(),atom() | ets:tid()} contains an opaque term as 2nd argument
 simple1_api.erl:91: Invalid type specification for function simple1_api:tup/0. The success typing is () -> {'a','b'}
 simple2_api.erl:100: The call lists:flatten(A::simple1_adt:tuple1()) contains an opaque term as 1st argument when a structured term of type [any()] is expected
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/para/para5.erl b/lib/dialyzer/test/opaque_SUITE_data/src/para/para5.erl
new file mode 100644
index 0000000000..76ea3e76b5
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/para/para5.erl
@@ -0,0 +1,33 @@
+-module(para5).
+
+-export([d/0, dd/0, da1/0]).
+
+d() ->
+    I1 = adt_d1(),
+    I2 = adt_d2(),
+    I1 =:= I2. % can never evaluate to true
+
+dd() ->
+    I1 = adt_d1(),
+    I2 = adt_dd(),
+    I1 =/= I2. % incompatible opaque types
+
+da1() ->
+    I1 = adt_da1(),
+    I2 = adt_da2(),
+    I1 =:= I2.
+
+adt_d1() ->
+    para5_adt:d1().
+
+adt_d2() ->
+    para5_adt:d2().
+
+adt_dd() ->
+    para5_adt:dd().
+
+adt_da1() ->
+    para5_adt:da1().
+
+adt_da2() ->
+    para5_adt:da2().
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/para/para5_adt.erl b/lib/dialyzer/test/opaque_SUITE_data/src/para/para5_adt.erl
new file mode 100644
index 0000000000..a62e0488e0
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/para/para5_adt.erl
@@ -0,0 +1,36 @@
+-module(para5_adt).
+
+-export([d1/0, d2/0, dd/0, da1/0, da2/0]).
+
+-export_type([d/0, dd/1, da/2]).
+
+-opaque d() :: 1 | 2.
+
+-spec d1() -> d().
+
+d1() ->
+    1.
+
+-spec d2() -> d().
+
+d2() ->
+    2.
+
+-opaque dd(A) :: A.
+
+-spec dd() -> dd(atom()).
+
+dd() ->
+    foo:atom().
+
+-opaque da(A, B) :: {A, B}.
+
+-spec da1() -> da(any(), atom()).
+
+da1() ->
+    {3, a}.
+
+-spec da2() -> da(integer(), any()).
+
+da2() ->
+    {3, a}.
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_api.erl b/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_api.erl
index eef2074e0c..7db1100597 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_api.erl
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_api.erl
@@ -145,7 +145,7 @@ adt_t4() ->
     A = simple1_adt:n1(),
     B = simple1_adt:n2(),
     A = A, % OK
-    A = B. % opaque term
+    A = B. % opaque terms
 
 adt_t7() ->
     A = simple1_adt:n1(),
@@ -178,7 +178,7 @@ c2(A, B) ->
 c2() ->
     A = simple1_adt:d1(),
     B = simple1_adt:d2(),
-    if A =< B -> ok end. % opaque term
+    if A =< B -> ok end. % opaque terms
 
 c3() ->
     B = simple1_adt:d2(),
@@ -516,7 +516,7 @@ eq1() ->
     A = simple1_adt:d2(),
     B = simple1_adt:d1(),
     if
-        A == B -> % opaque term
+        A == B -> % opaque terms
             0;
         A == A ->
             1;
@@ -555,7 +555,7 @@ c6(A, B) ->
 c7(A, B) ->
     A = simple1_adt:d1(),
     B = simple1_adt:d2(),
-    A =< B. % opaque term
+    A =< B. % opaque terms
 
 c8() ->
     D = digraph:new(),
diff --git a/lib/hipe/cerl/erl_types.erl b/lib/hipe/cerl/erl_types.erl
index c7440e5ce3..1531d96324 100644
--- a/lib/hipe/cerl/erl_types.erl
+++ b/lib/hipe/cerl/erl_types.erl
@@ -583,13 +583,11 @@ t_find_opaque_mismatch_list([H|T]) ->
 %% calling t_contains_opaque/2 is that the traversal stops when
 %% there is a mismatch which means that unknown opaque types "below"
 %% the mismatch are not found.
-%% XXX. Returns one element even if both oparands contain opaque types.
-%% XXX. Slow since t_inf() is called but the results are ignored.
 t_find_unknown_opaque(_T1, _T2, 'universe') -> [];
 t_find_unknown_opaque(T1, T2, Opaques) ->
   try t_inf(T1, T2, {match, Opaques}) of
     _ -> []
-  catch throw:N when is_integer(N) -> [N]
+  catch throw:{pos, Ns} -> Ns
   end.
 
 -spec t_decorate_with_opaque(erl_type(), erl_type(), [erl_type()]) -> erl_type().
@@ -2608,7 +2606,7 @@ inf_opaque1(T1, ?opaque(Set2)=T2, Pos, Opaques) ->
   end.
 
 inf_is_opaque_type(T, Pos, {match, Opaques}) ->
-  is_opaque_type(T, Opaques) orelse throw(Pos);
+  is_opaque_type(T, Opaques) orelse throw({pos, [Pos]});
 inf_is_opaque_type(T, _Pos, Opaques) ->
   is_opaque_type(T, Opaques).
 
@@ -2650,8 +2648,8 @@ can_combine_opaque_names(_, _, _, _) -> false.
 %% Note: two parameterized opaque types are not the same if their
 %% actual parameters differ
 inf_opaque(Set1, Set2, Opaques) ->
-  List1 = inf_look_up(Set1, 1, Opaques),
-  List2 = inf_look_up(Set2, 2, Opaques),
+  List1 = inf_look_up(Set1, Opaques),
+  List2 = inf_look_up(Set2, Opaques),
   List0 = [combine(Inf, T1, T2) ||
             {Is1, ModNameArgs1, T1} <- List1,
             {Is2, ModNameArgs2, T2} <- List2,
@@ -2662,14 +2660,14 @@ inf_opaque(Set1, Set2, Opaques) ->
   sup_opaque(List).
 
 %% Optimization: do just one lookup.
-inf_look_up(Set, Pos, Opaques) ->
-  [{Opaques =:= 'universe' orelse inf_is_opaque_type2(T, Pos, Opaques),
+inf_look_up(Set, Opaques) ->
+  [{Opaques =:= 'universe' orelse inf_is_opaque_type2(T, Opaques),
     {M, N, Args}, T} ||
     #opaque{mod = M, name = N, args = Args} = T <- set_to_list(Set)].
 
-inf_is_opaque_type2(T, Pos, {match, Opaques}) ->
-  is_opaque_type2(T, Opaques) orelse throw(Pos);
-inf_is_opaque_type2(T, _Pos, Opaques) ->
+inf_is_opaque_type2(T, {match, Opaques}) ->
+  is_opaque_type2(T, Opaques);
+inf_is_opaque_type2(T, Opaques) ->
   is_opaque_type2(T, Opaques).
 
 inf_opaque_types(IsOpaque1, ModNameArgs1, T1,
@@ -2686,6 +2684,8 @@ inf_opaque_types(IsOpaque1, ModNameArgs1, T1,
         {true, true}  -> t_inf(S1, S2, Opaques);
         {true, false} -> t_inf(S1, ?opaque(set_singleton(T2)), Opaques);
         {false, true} -> t_inf(?opaque(set_singleton(T1)), S2, Opaques);
+        {false, false} when element(1, Opaques) =:= match ->
+          throw({pos, [1, 2]});
         {false, false} -> t_none()
       end
   end.
@@ -2801,7 +2801,7 @@ inf_union(U1, U2, Opaques) ->
   {Union, ThrowList3} = inf_union(U1, U2, 0, [], [], Opaques),
   ThrowList = lists:merge3(ThrowList1, ThrowList2, ThrowList3),
   case t_sup([O1, O2, Union]) of
-    ?none when ThrowList =/= [] -> throw(hd(ThrowList));
+    ?none when ThrowList =/= [] -> throw({pos, lists:usort(ThrowList)});
     Sup -> Sup
   end.
 
@@ -2813,8 +2813,8 @@ inf_union_collect([E|L], Opaque, InfFun, InfList, ThrowList) ->
   try InfFun(E, Opaque)of
     Inf ->
       inf_union_collect(L, Opaque, InfFun, [Inf|InfList], ThrowList)
-  catch throw:N when is_integer(N) ->
-      inf_union_collect(L, Opaque, InfFun, InfList, [N|ThrowList])
+  catch throw:{pos, Ns} ->
+      inf_union_collect(L, Opaque, InfFun, InfList, Ns ++ ThrowList)
   end.
 
 inf_union([?none|Left1], [?none|Left2], N, Acc, ThrowList, Opaques) ->
@@ -2823,8 +2823,8 @@ inf_union([T1|Left1], [T2|Left2], N, Acc, ThrowList, Opaques) ->
   try t_inf(T1, T2, Opaques) of
     ?none -> inf_union(Left1, Left2, N, [?none|Acc], ThrowList, Opaques);
     T     -> inf_union(Left1, Left2, N+1, [T|Acc], ThrowList, Opaques)
-  catch throw:N when is_integer(N) ->
-      inf_union(Left1, Left2, N, [?none|Acc], [N|ThrowList], Opaques)
+  catch throw:{pos, Ns} ->
+      inf_union(Left1, Left2, N, [?none|Acc], Ns ++ ThrowList, Opaques)
   end;
 inf_union([], [], N, Acc, ThrowList, _Opaques) ->
   if N =:= 0 -> {?none, ThrowList};