Merge branch 'hb/dialyzer/fix_opaque_types/OTP-12493'

* hb/dialyzer/fix_opaque_types/OTP-12493:
  dialyzer: Fix a minor bug concerning opaque types
  dialyzer: Modify warning for comparison of opaque types
  dialyzer: Modify the handling of parametrized opaque types

22 files changed, 398 insertions, 93 deletions

diff --git a/lib/dialyzer/test/opaque_SUITE_data/results/para b/lib/dialyzer/test/opaque_SUITE_data/results/para
index 3aaa238de6..8fe67e39ad 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/results/para
+++ b/lib/dialyzer/test/opaque_SUITE_data/results/para
@@ -7,15 +7,27 @@ para1.erl:38: Attempt to test for equality between a term of type para1_adt:t(in
 para1.erl:43: Attempt to test for equality between a term of type para1_adt:t() and a term of opaque type para1_adt:t(atom())
 para1.erl:48: Attempt to test for equality between a term of type para1_adt:t(integer()) and a term of opaque type para1_adt:t()
 para1.erl:53: The test {3,2} =:= {'a','b'} can never evaluate to 'true'
-para2.erl:103: Attempt to test for equality between a term of type para2_adt:circ({{integer(),integer()},{integer(),integer()}},{{integer(),integer()},{integer(),integer()}}) and a term of opaque type para2_adt:circ({{integer(),integer()},{integer(),integer()}})
+para2.erl:103: Attempt to test for equality between a term of type para2_adt:circ(integer(),integer()) and a term of opaque type para2_adt:circ(integer())
 para2.erl:117: Attempt to test for equality between a term of type para2_adt:un(atom(),integer()) and a term of opaque type para2_adt:un(integer(),atom())
 para2.erl:31: The test 'a' =:= 'b' can never evaluate to 'true'
 para2.erl:61: Attempt to test for equality between a term of type para2_adt:c2() and a term of opaque type para2_adt:c1()
 para2.erl:66: The test 'a' =:= 'b' can never evaluate to 'true'
-para2.erl:88: The test para2:circ({{integer(),integer()},{integer(),integer()}}) =:= para2:circ({{integer(),integer()},{integer(),integer()}},{{integer(),integer()},{integer(),integer()}}) can never evaluate to 'true'
+para2.erl:88: The test para2:circ(integer()) =:= para2:circ(integer(),integer()) can never evaluate to 'true'
 para3.erl:28: Invalid type specification for function para3:ot2/0. The success typing is () -> 'foo'
 para3.erl:36: The pattern {{{17}}} can never match the type {{{{{{_,_,_,_,_}}}}}}
 para3.erl:55: Invalid type specification for function para3:t2/0. The success typing is () -> 'foo'
 para3.erl:65: The attempt to match a term of type {{{{{para3_adt:ot1(_,_,_,_,_)}}}}} against the pattern {{{{{17}}}}} breaks the opaqueness of para3_adt:ot1(_,_,_,_,_)
 para3.erl:68: The pattern {{{{17}}}} can never match the type {{{{{para3_adt:ot1(_,_,_,_,_)}}}}}
 para3.erl:74: Invalid type specification for function para3:exp_adt/0. The success typing is () -> 3
+para4.erl:21: Invalid type specification for function para4:a/1. The success typing is (dict:dict(atom() | integer(),atom() | integer()) | para4:d_all()) -> [{atom() | integer(),atom() | integer()}]
+para4.erl:26: Invalid type specification for function para4:i/1. The success typing is (dict:dict(atom() | integer(),atom() | integer()) | para4:d_all()) -> [{atom() | integer(),atom() | integer()}]
+para4.erl:31: Invalid type specification for function para4:t/1. The success typing is (dict:dict(atom() | integer(),atom() | integer()) | para4:d_all()) -> [{atom() | integer(),atom() | integer()}]
+para4.erl:59: Attempt to test for equality between a term of type para4_adt:t(atom() | integer()) and a term of opaque type para4_adt:t(integer())
+para4.erl:64: Attempt to test for equality between a term of type para4_adt:t(atom() | integer()) and a term of opaque type para4_adt:t(atom())
+para4.erl:69: Attempt to test for equality between a term of type para4_adt:int(1 | 2 | 3 | 4) and a term of opaque type para4_adt:int(1 | 2)
+para4.erl:74: 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(1 | 2)
+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/para2.erl b/lib/dialyzer/test/opaque_SUITE_data/src/para/para2.erl
index 09b2235fa5..4461ff291c 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/src/para/para2.erl
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/para/para2.erl
@@ -85,7 +85,7 @@ ct2_adt() ->
 tcirc() ->
     A = circ1(),
     B = circ2(),
-    A =:= B. % can never evaluate to 'true' (but the types are not OK, or?)
+    A =:= B. % can never evaluate to 'true'
 
 -spec circ1() -> circ(integer()).
 
@@ -100,7 +100,7 @@ circ2() ->
 tcirc_adt() ->
     A = circ1_adt(),
     B = circ2_adt(),
-    A =:= B. % opaque attempt (one would expect them to be the same...)
+    A =:= B. % opaque attempt (number of parameters differs)
 
 circ1_adt() ->
     para2_adt:circ1().
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/para/para3.erl b/lib/dialyzer/test/opaque_SUITE_data/src/para/para3.erl
index 792ae40d39..102215b28d 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/src/para/para3.erl
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/para/para3.erl
@@ -71,7 +71,7 @@ t2_adt() ->
 
 -type exp() :: para3_adt:exp1(para3_adt:exp2()).
 
--spec exp_adt() -> exp().
+-spec exp_adt() -> exp(). % invalid type spec
 
 exp_adt() ->
     3.
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/para/para4.erl b/lib/dialyzer/test/opaque_SUITE_data/src/para/para4.erl
new file mode 100644
index 0000000000..b9794672a9
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/para/para4.erl
@@ -0,0 +1,134 @@
+-module(para4).
+
+-compile(export_all).
+
+-export_type([d_atom/0, d_integer/0, d_tuple/0, d_all/0]).
+
+-export_type([t/1]).
+
+-type ai() :: atom() | integer().
+
+-type d(T) :: dict:dict(T, T).
+
+-opaque d_atom() :: d(atom()).
+-opaque d_integer() :: d(integer()).
+-opaque d_tuple() :: d(tuple()).
+-opaque d_all() :: d(ai()).
+
+b(D) ->
+    a(D) ++ i(D).
+
+-spec a(d_atom()) -> [{atom(), atom()}]. % Invalid type spec
+
+a(D) ->
+    c(D).
+
+-spec i(d_integer()) -> [{integer(), integer()}]. % Invalid type spec
+
+i(D) ->
+    c(D).
+
+-spec t(d_tuple()) -> [{tuple(), tuple()}]. % Invalid type spec.
+
+t(D) ->
+    c(D).
+
+-spec c(d_all()) -> [{ai(), ai()}].
+
+c(D) ->
+    dict:to_list(D).
+
+
+
+
+-opaque t(A) :: {A, A}.
+
+adt_tt5() ->
+    I1 = adt_y1(),
+    I2 = adt_y3(),
+    I1 =:= I2.
+
+adt_tt6() ->
+    I1 = adt_y2(),
+    I2 = adt_y3(),
+    I1 =:= I2.
+
+adt_tt7() ->
+    I1 = adt_t1(),
+    I2 = adt_t3(),
+    I1 =:= I2. % opaque attempt
+
+adt_tt8() ->
+    I1 = adt_t2(),
+    I2 = adt_t3(),
+    I1 =:= I2. % opaque attempt
+
+adt_tt9() ->
+    I1 = adt_int2(),
+    I2 = adt_int4(),
+    I1 =:= I2. % opaque attempt
+
+adt_tt10() ->
+    I1 = adt_int2(),
+    I2 = adt_int2_4(),
+    I1 =:= I2. % opaque attempt
+
+adt_tt11() ->
+    I1 = adt_int5_7(),
+    I2 = adt_int2_4(),
+    I1 =:= I2. % opaque attempt
+
+adt_tt12() ->
+    I1 = adt_un1_2(),
+    I2 = adt_un3_4(),
+    I1 =:= I2. % opaque attempt
+
+adt_tt13() ->
+    I1 = adt_tup(),
+    I2 = adt_tup2(),
+    I1 =:= I2. % opaque attempt
+
+y3() ->
+    {a, 3}.
+
+adt_t1() ->
+    para4_adt:t1().
+
+adt_t2() ->
+    para4_adt:t2().
+
+adt_t3() ->
+    para4_adt:t3().
+
+adt_y1() ->
+    para4_adt:y1().
+
+adt_y2() ->
+    para4_adt:y2().
+
+adt_y3() ->
+    para4_adt:y3().
+
+adt_int2() ->
+    para4_adt:int2().
+
+adt_int4() ->
+    para4_adt:int4().
+
+adt_int2_4() ->
+    para4_adt:int2_4().
+
+adt_int5_7() ->
+    para4_adt:int5_7().
+
+adt_un1_2() ->
+    para4_adt:un1_2().
+
+adt_un3_4() ->
+    para4_adt:un3_4().
+
+adt_tup() ->
+    para4_adt:tup().
+
+adt_tup2() ->
+    para4_adt:tup2().
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/para/para4_adt.erl b/lib/dialyzer/test/opaque_SUITE_data/src/para/para4_adt.erl
new file mode 100644
index 0000000000..407dd198a7
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/para/para4_adt.erl
@@ -0,0 +1,108 @@
+-module(para4_adt).
+
+-export([t1/0, t2/0, t3/0, y1/0, y2/0, y3/0]).
+
+-export([int2/0, int4/0, int2_4/0, int5_7/0]).
+
+-export([un1_2/0, un3_4/0]).
+
+-export([tup/0, tup2/0]).
+
+-export_type([t/1, y/1, int/1, tup/1, un/1]).
+
+-type ai() :: atom() | integer().
+
+-opaque t(A) :: {A, A}.
+
+-type y(A) :: {A, A}.
+
+-opaque int(I) :: I.
+
+-opaque un(I) :: atom() | I.
+
+-opaque tup(T) :: T.
+
+-spec t1() -> t(integer()).
+
+t1() ->
+    {i(), i()}.
+
+-spec t2() -> t(atom()).
+
+t2() ->
+    {a(), a()}.
+
+-spec t3() -> t(ai()).
+
+t3() ->
+    {ai(), ai()}.
+
+-spec y1() -> y(integer()).
+
+y1() ->
+    {i(), i()}.
+
+-spec y2() -> y(atom()).
+
+y2() ->
+    {a(), a()}.
+
+-spec y3() -> y(ai()).
+
+y3() ->
+    {ai(), ai()}.
+
+-spec a() -> atom().
+
+a() ->
+    foo:a().
+
+-spec i() -> integer().
+
+i() ->
+    foo:i().
+
+-spec ai() -> ai().
+
+ai() ->
+    foo:ai().
+
+-spec int2() -> int(1..2).
+
+int2() ->
+    foo:int2().
+
+-spec int4() -> int(1..4).
+
+int4() ->
+    foo:int4().
+
+-spec int2_4() -> int(2..4).
+
+int2_4() ->
+    foo:int2_4().
+
+-spec int5_7() -> int(5..7).
+
+int5_7() ->
+    foo:int5_7().
+
+-spec un1_2() -> un(1..2).
+
+un1_2() ->
+    foo:un1_2().
+
+-spec un3_4() -> un(3..4).
+
+un3_4() ->
+    foo:un3_4().
+
+-spec tup() -> tup(tuple()).
+
+tup() ->
+    foo:tup().
+
+-spec tup2() -> tup({_, _}).
+
+tup2() ->
+    foo:tup2().
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 e7823a596a..d39f350c0f 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().
@@ -755,9 +753,9 @@ t_opaque_from_records(RecDict) ->
                  %% List = lists:zip(ArgNames, Args),
                  %% TmpVarDict = dict:from_list(List),
                  %% Rep = t_from_form(Type, RecDict, TmpVarDict),
-                 Rep = t_none(), % not used for anything right now
+                 Rep = t_any(), % not used for anything right now
                  Args = [t_any() || _ <- ArgNames],
-                 skip_opaque_alias(Rep, Module, Name, Args)
+                 t_opaque(Module, Name, Args, Rep)
 	     end, OpaqueRecDict),
   [OpaqueType || {_Key, OpaqueType} <- dict:to_list(OpaqueTypeDict)].
 
@@ -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).
 
@@ -2627,13 +2625,13 @@ combine(S, T1, T2) ->
   #opaque{mod = Mod1, name = Name1, args = Args1} = T1,
   #opaque{mod = Mod2, name = Name2, args = Args2} = T2,
   Comb1 = comb(Mod1, Name1, Args1, S, T1),
-  case is_same_type_name({Mod1, Name1, Args1}, {Mod2, Name2, Args2}) of
+  case is_compat_opaque_names({Mod1, Name1, Args1}, {Mod2, Name2, Args2}) of
     true  -> Comb1;
     false -> Comb1 ++ comb(Mod2, Name2, Args2, S, T2)
   end.
 
 comb(Mod, Name, Args, S, T) ->
-  case is_same_name(Mod, Name, Args, S) of
+  case can_combine_opaque_names(Mod, Name, Args, S) of
     true ->
       ?opaque(Set) = S,
       Set;
@@ -2641,17 +2639,17 @@ comb(Mod, Name, Args, S, T) ->
       [T#opaque{struct = S}]
   end.
 
-is_same_name(Mod1, Name1, Args1,
-             ?opaque([#opaque{mod = Mod2, name = Name2, args = Args2}])) ->
-  is_same_type_name({Mod1, Name1, Args1}, {Mod2, Name2, Args2});
-is_same_name(_, _, _, _) -> false.
+can_combine_opaque_names(Mod1, Name1, Args1,
+               ?opaque([#opaque{mod = Mod2, name = Name2, args = Args2}])) ->
+  is_compat_opaque_names({Mod1, Name1, Args1}, {Mod2, Name2, Args2});
+can_combine_opaque_names(_, _, _, _) -> false.
 
 %% Combining two lists this way can be very time consuming...
 %% 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,
@@ -2678,18 +2676,33 @@ inf_opaque_types(IsOpaque1, ModNameArgs1, T1,
   #opaque{struct = S2}=T2,
   case
     Opaques =:= 'universe' orelse
-    is_same_type_name(ModNameArgs1, ModNameArgs2)
+    is_compat_opaque_names(ModNameArgs1, ModNameArgs2)
   of
     true -> t_inf(S1, S2, Opaques);
     false ->
       case {IsOpaque1, IsOpaque2} of
-        {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);
+        {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.
 
+is_compat_opaque_names(ModNameArgs, ModNameArgs) -> true;
+is_compat_opaque_names({Mod,Name,Args1}, {Mod,Name,Args2}) ->
+  is_compat_args(Args1, Args2);
+is_compat_opaque_names(_, _) -> false.
+
+is_compat_args([A1|Args1], [A2|Args2]) ->
+  is_compat_arg(A1, A2) andalso is_compat_args(Args1, Args2);
+is_compat_args([], []) -> true;
+is_compat_args(_, _) -> false.
+
+is_compat_arg(A, A) -> true;
+is_compat_arg(A1, A2) -> t_is_any(A1) orelse t_is_any(A2).
+
 -spec t_inf_lists([erl_type()], [erl_type()]) -> [erl_type()].
 
 t_inf_lists(L1, L2) ->
@@ -2788,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.
 
@@ -2800,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) ->
@@ -2810,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};
@@ -4227,17 +4240,19 @@ type_from_form(Name, Args, TypeNames, ET, M, MR, V, D, L) ->
           false -> {t_any(), L1}
         end,
       Rep1 = choose_opaque_type(Rep, Type),
-      Args2 = [subst_all_vars_to_any(ArgType) || ArgType <- ArgTypes],
-      {skip_opaque_alias(Rep1, Module, Name, Args2), L2};
+      Rep2 = case t_is_none(Rep1) of
+               true -> Rep1;
+               false ->
+                 Args2 = [subst_all_vars_to_any(ArgType) ||
+                           ArgType <- ArgTypes],
+                 t_opaque(Module, Name, Args2, Rep1)
+             end,
+      {Rep2, L2};
     error ->
       Msg = io_lib:format("Unable to find type ~w/~w\n", [Name, ArgsLen]),
       throw({error, Msg})
   end.
 
-skip_opaque_alias(?opaque(_) = T, _Mod, _Name, _Args) -> T;
-skip_opaque_alias(T, Module, Name, Args) ->
-  t_opaque(Module, Name, Args, T).
-
 remote_from_form(RemMod, Name, Args, TypeNames, ET, M, MR, V, D, L) ->
   {ArgTypes, L1} = list_from_form(Args, TypeNames, ET, M, MR, V, D, L),
   if
@@ -4280,7 +4295,11 @@ remote_from_form(RemMod, Name, Args, TypeNames, ET, M, MR, V, D, L) ->
                         {t_any(), L1}
                     end,
                   NewRep1 = choose_opaque_type(NewRep, Type),
-                  {skip_opaque_alias(NewRep1, Mod, Name, ArgTypes), L2};
+                  NewRep2 = case t_is_none(NewRep1) of
+                     true -> NewRep1;
+                     false -> t_opaque(Mod, Name, ArgTypes, NewRep1)
+                   end,
+                  {NewRep2, L2};
                 error ->
                   Msg = io_lib:format("Unable to find remote type ~w:~w()\n",
                                       [RemMod, Name]),
@@ -4680,17 +4699,6 @@ do_opaque(?union(List) = Type, Opaques, Pred) ->
 do_opaque(Type, _Opaques, Pred) ->
   Pred(Type).
 
-is_same_type_name(ModNameArgs, ModNameArgs) -> true;
-is_same_type_name({Mod, Name, Args1}, {Mod, Name, Args2}) ->
-  all_any(Args1) orelse all_any(Args2);
-is_same_type_name(_ModNameArgs1, _ModNameArgs2) ->
-  false.
-
-all_any([]) -> true;
-all_any([T|L]) ->
-  t_is_any(T) andalso all_any(L);
-all_any(_) -> false.
-
 map_keys(?map(Pairs)) ->
   [K || {K, _} <- Pairs].
 
diff --git a/lib/stdlib/doc/src/array.xml b/lib/stdlib/doc/src/array.xml
index b03a2fa0cc..af23cd95d9 100644
--- a/lib/stdlib/doc/src/array.xml
+++ b/lib/stdlib/doc/src/array.xml
@@ -93,9 +93,6 @@ the default value cannot be confused with the values of set entries.</p>
   </datatype>
   <datatype>
     <name name="array" n_vars="0"/>
-    <desc>
-      <p><c>array()</c> is equivalent to <c>array(term())</c>.</p>
-    </desc>
   </datatype>
   <datatype>
     <name name="array_indx"/>
diff --git a/lib/stdlib/doc/src/dict.xml b/lib/stdlib/doc/src/dict.xml
index 0771682a25..b456b97578 100644
--- a/lib/stdlib/doc/src/dict.xml
+++ b/lib/stdlib/doc/src/dict.xml
@@ -46,9 +46,6 @@
     </datatype>
     <datatype>
       <name name="dict" n_vars="0"/>
-      <desc>
-        <p><c>dict()</c> is equivalent to <c>dict(term(), term())</c>.</p>
-      </desc>
     </datatype>
   </datatypes>
   <funcs>
diff --git a/lib/stdlib/doc/src/gb_sets.xml b/lib/stdlib/doc/src/gb_sets.xml
index 405bae5698..99e92d8680 100644
--- a/lib/stdlib/doc/src/gb_sets.xml
+++ b/lib/stdlib/doc/src/gb_sets.xml
@@ -120,9 +120,6 @@
     </datatype>
     <datatype>
       <name name="set" n_vars="0"/>
-      <desc>
-        <p><c>set()</c> is equivalent to <c>set(term())</c>.</p>
-      </desc>
     </datatype>
     <datatype>
       <name name="iter" n_vars="1"/>
@@ -130,9 +127,6 @@
     </datatype>
     <datatype>
       <name name="iter" n_vars="0"/>
-      <desc>
-        <p><c>iter()</c> is equivalent to <c>iter(term())</c>.</p>
-      </desc>
     </datatype>
   </datatypes>
   <funcs>
diff --git a/lib/stdlib/doc/src/gb_trees.xml b/lib/stdlib/doc/src/gb_trees.xml
index 82167e1083..99ca2d6a9a 100644
--- a/lib/stdlib/doc/src/gb_trees.xml
+++ b/lib/stdlib/doc/src/gb_trees.xml
@@ -64,9 +64,6 @@
     </datatype>
     <datatype>
       <name name="tree" n_vars="0"/>
-      <desc>
-        <p><c>tree()</c> is equivalent to <c>tree(term(), term())</c>.</p>
-      </desc>
     </datatype>
     <datatype>
       <name name="iter" n_vars="2"/>
@@ -74,9 +71,6 @@
     </datatype>
     <datatype>
       <name name="iter" n_vars="0"/>
-      <desc>
-        <p><c>iter()</c> is equivalent to <c>iter(term(), term())</c>.</p>
-      </desc>
     </datatype>
   </datatypes>
   <funcs>
diff --git a/lib/stdlib/doc/src/queue.xml b/lib/stdlib/doc/src/queue.xml
index 9c994154d4..f689412988 100644
--- a/lib/stdlib/doc/src/queue.xml
+++ b/lib/stdlib/doc/src/queue.xml
@@ -95,9 +95,6 @@
     </datatype>
     <datatype>
       <name name="queue" n_vars="0"/>
-      <desc>
-        <p><c>queue()</c> is equivalent to <c>queue(term())</c>.</p>
-      </desc>
     </datatype>
   </datatypes>
 
diff --git a/lib/stdlib/doc/src/sets.xml b/lib/stdlib/doc/src/sets.xml
index 4a31648f8f..eecddb7fd4 100644
--- a/lib/stdlib/doc/src/sets.xml
+++ b/lib/stdlib/doc/src/sets.xml
@@ -50,9 +50,6 @@
     </datatype>
     <datatype>
       <name name="set" n_vars="0"/>
-      <desc>
-        <p><c>set()</c> is equivalent to <c>set(term())</c>.</p>
-      </desc>
     </datatype>
   </datatypes>
   <funcs>
diff --git a/lib/stdlib/src/array.erl b/lib/stdlib/src/array.erl
index 10d2ccea45..f98a587c55 100644
--- a/lib/stdlib/src/array.erl
+++ b/lib/stdlib/src/array.erl
@@ -164,7 +164,7 @@
                 elements :: elements(_)         %% the tuple tree
 	       }).
 
--opaque array() :: array(term()).
+-type array() :: array(term()).
 
 -opaque array(Type) ::
           #array{default :: Type, elements :: elements(Type)}.
diff --git a/lib/stdlib/src/dict.erl b/lib/stdlib/src/dict.erl
index 5a9f63c5e2..d2af9554a1 100644
--- a/lib/stdlib/src/dict.erl
+++ b/lib/stdlib/src/dict.erl
@@ -70,7 +70,7 @@
 	}).
 
 
--opaque dict() :: dict(_, _).
+-type dict() :: dict(_, _).
 
 -opaque dict(Key, Value) :: #dict{segs :: segs(Key, Value)}.
 
diff --git a/lib/stdlib/src/gb_sets.erl b/lib/stdlib/src/gb_sets.erl
index d3fbd542f7..d099737d8f 100644
--- a/lib/stdlib/src/gb_sets.erl
+++ b/lib/stdlib/src/gb_sets.erl
@@ -203,11 +203,10 @@
 -export_type([set/0, set/1, iter/0, iter/1]).
 
 -type gb_set_node(Element) :: 'nil' | {Element, _, _}.
--type gb_set_node() :: gb_set_node(_).
 -opaque set(Element) :: {non_neg_integer(), gb_set_node(Element)}.
--opaque set() :: set(_).
+-type set() :: set(_).
 -opaque iter(Element) :: [gb_set_node(Element)].
--opaque iter() :: [gb_set_node()].
+-type iter() :: iter(_).
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
diff --git a/lib/stdlib/src/gb_trees.erl b/lib/stdlib/src/gb_trees.erl
index 259e8f718b..2cbfd8fd2a 100644
--- a/lib/stdlib/src/gb_trees.erl
+++ b/lib/stdlib/src/gb_trees.erl
@@ -160,11 +160,10 @@
 
 -type gb_tree_node(K, V) :: 'nil'
                           | {K, V, gb_tree_node(K, V), gb_tree_node(K, V)}.
--type gb_tree_node() :: gb_tree_node(_, _).
 -opaque tree(Key, Value) :: {non_neg_integer(), gb_tree_node(Key, Value)}.
--opaque tree() :: tree(_, _).
+-type tree() :: tree(_, _).
 -opaque iter(Key, Value) :: [gb_tree_node(Key, Value)].
--opaque iter() :: [gb_tree_node()].
+-type iter() :: iter(_, _).
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
diff --git a/lib/stdlib/src/queue.erl b/lib/stdlib/src/queue.erl
index 472d503b99..d2e6848258 100644
--- a/lib/stdlib/src/queue.erl
+++ b/lib/stdlib/src/queue.erl
@@ -48,7 +48,7 @@
 
 -opaque queue(Item) :: {list(Item), list(Item)}.
 
--opaque queue() :: queue(_).
+-type queue() :: queue(_).
 
 %% Creation, inspection and conversion
 
diff --git a/lib/stdlib/src/sets.erl b/lib/stdlib/src/sets.erl
index 167a676281..041d281148 100644
--- a/lib/stdlib/src/sets.erl
+++ b/lib/stdlib/src/sets.erl
@@ -70,7 +70,7 @@
 	 segs                :: segs(_)			% Segments
 	}).
 
--opaque set() :: set(_).
+-type set() :: set(_).
 
 -opaque set(Element) :: #set{segs :: segs(Element)}.