[dialyzer] Re-work the handling of opaque types

It is now OK to inspect and modify the internals of opaque types within
the scope of the module.

The contracts are used for decorating types with opaqueness when it is
harmless to do so. The opaqueness is propagated by the typesig module
and also by the dataflow module.

A lot of details have been fixed or updated. In particular the modules
erl_types and erl_bif_types have been modified extensively.

The version in vsn.mk has been updated to 2.7. The reason is a
modification of #opaque{} in erl_types.

Dialyzer seems to be about five percent slower than it used to be.

8 files changed, 1081 insertions, 0 deletions

diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/simple/exact_adt.erl b/lib/dialyzer/test/opaque_SUITE_data/src/simple/exact_adt.erl
new file mode 100644
index 0000000000..7103847ae7
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/simple/exact_adt.erl
@@ -0,0 +1,17 @@
+-module(exact_adt).
+
+-export([exact_adt_set_type/1, exact_adt_set_type2/1]).
+
+-export_type([exact_adt/0]).
+
+-record(exact_adt, {}).
+
+-opaque exact_adt() :: #exact_adt{}.
+
+-spec exact_adt_set_type(_) -> exact_adt().
+
+exact_adt_set_type(G) -> G.
+
+-spec exact_adt_set_type2(exact_adt()) -> exact_adt().
+
+exact_adt_set_type2(G) -> G.
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/simple/exact_api.erl b/lib/dialyzer/test/opaque_SUITE_data/src/simple/exact_api.erl
new file mode 100644
index 0000000000..5f7ab4f3aa
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/simple/exact_api.erl
@@ -0,0 +1,60 @@
+-module(exact_api).
+
+-export([new/0, exact_api_test/1, exact_api_new/1,
+         exact_adt_test/1, exact_adt_new/1]).
+
+-export_type([exact_api/0]).
+
+-record(digraph, {vtab = notable :: ets:tab(),
+		  etab = notable :: ets:tab(),
+		  ntab = notable :: ets:tab(),
+	          cyclic = true  :: boolean()}).
+
+-spec new() -> digraph().
+
+new() ->
+    A = #digraph{},
+    set_type(A), % does not have an opaque term as 1st argument
+    A.
+
+-spec set_type(digraph()) -> true.
+
+set_type(G) ->
+    digraph:delete(G).
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% The derived spec of exact_api_new() is
+%%% -spec exact_api_new(exact_api:exact_api()) -> exact_api:exact_api().
+%%% This won't happen unless dialyzer_typesig uses
+%%% t_is_exactly_equal() rather than t_is_equal().
+%%% [As of R17B the latter considers two types equal if nothing but
+%%%  their ?opaque tags differ.]
+
+-record(exact_api, {}).
+
+-opaque exact_api() :: #exact_api{}.
+
+exact_api_test(X) ->
+    #exact_api{} = exact_api_set_type(X). % OK
+
+exact_api_new(A) ->
+    A = #exact_api{},
+    _ = exact_api_set_type(A), % OK (the opaque type is local)
+    A.
+
+-spec exact_api_set_type(exact_api()) -> exact_api().
+
+exact_api_set_type(#exact_api{}=E) -> E.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+-record(exact_adt, {}).
+
+exact_adt_test(X) ->
+    #exact_adt{} = exact_adt:exact_adt_set_type(X). % breaks the opaqueness
+
+exact_adt_new(A) ->
+    A = #exact_adt{},
+    _ = exact_adt:exact_adt_set_type2(A), % does not have an opaque term as 1st argument
+    A.
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/simple/is_rec.erl b/lib/dialyzer/test/opaque_SUITE_data/src/simple/is_rec.erl
new file mode 100644
index 0000000000..2b157483bc
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/simple/is_rec.erl
@@ -0,0 +1,65 @@
+-module(is_rec).
+
+-export([ri1/0, ri11/0, ri13/0, ri14/0, ri2/0, ri3/0, ri4/0, ri5/0,
+         ri6/0, ri7/0, ri8/0]).
+
+-record(r, {f1 :: integer()}).
+
+ri1() ->
+    A = simple1_adt:d1(),
+    is_record(A, r). % opaque term 1
+
+ri11() ->
+    A = simple1_adt:d1(),
+    I = '1-3'(),
+    is_record(A, r, I). % opaque term 1
+
+ri13() ->
+    A = simple1_adt:d1(),
+    if is_record(A, r) -> true end. % breaks the opaqueness
+
+ri14() ->
+    A = simple1_adt:d1(),
+    if is_record({A, 1}, r) -> true end. % breaks the opaqueness
+
+-type '1-3-t'() :: 1..3.
+
+-spec '1-3'() -> '1-3-t'().
+
+'1-3'() ->
+    random:uniform(3).
+
+
+-spec 'Atom'() -> atom().
+
+'Atom'() ->
+    a.
+
+ri2() ->
+    A = simple1_adt:d1(),
+    R = 'Atom'(),
+    is_record(A, R). % opaque term 1
+
+ri3() ->
+    A = simple1_adt:d1(),
+    is_record(A, A, 1). % opaque term 2
+
+ri4() ->
+    A = simple1_adt:d1(),
+    is_record(A, hipp:hopp(), 1). % opaque term 1
+
+ri5() ->
+    A = simple1_adt:d1(),
+    is_record(A, A, hipp:hopp()). % opaque term 2
+
+ri6() ->
+    A = simple1_adt:d1(),
+    if is_record(A, r) -> true end. % breaks opaqueness
+
+ri7() ->
+    A = simple1_adt:d1(),
+    if is_record({r, A}, r) -> true end. % A violates #r{}
+
+ri8() ->
+    A = simple1_adt:d1(),
+    is_record({A, 1}, r). % opaque term 1
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/simple/rec_adt.erl b/lib/dialyzer/test/opaque_SUITE_data/src/simple/rec_adt.erl
new file mode 100644
index 0000000000..ff80d6e99b
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/simple/rec_adt.erl
@@ -0,0 +1,28 @@
+-module(rec_adt).
+
+-export([f/0, r1/0]).
+
+-export_type([r1/0]).
+
+-export_type([f/0, op_t/0, a/0]).
+
+-opaque a() :: a | b.
+
+-record(r1,
+        {f1 :: a()}).
+
+-opaque r1() :: #r1{}.
+
+-opaque f() :: fun((_) -> _).
+
+-opaque op_t() :: integer().
+
+-spec f() -> f().
+
+f() ->
+    fun(_) -> 3 end.
+
+-spec r1() -> r1().
+
+r1() ->
+    #r1{f1 = a}.
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/simple/rec_api.erl b/lib/dialyzer/test/opaque_SUITE_data/src/simple/rec_api.erl
new file mode 100644
index 0000000000..d9b1d59f0c
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/simple/rec_api.erl
@@ -0,0 +1,77 @@
+-module(rec_api).
+
+-export([t1/0, t2/0, adt_t1/0, adt_t1/1, adt_r1/0,
+         t/1, t_adt/0, r/0, r_adt/0]).
+
+-export_type([{a,0},{r1,0}]).
+
+-export_type([f/0, op_t/0, r/0, tup/0]).
+
+-opaque a() :: a | b.
+
+-record(r1,
+        {f1 :: a()}).
+
+-opaque r1() :: #r1{}.
+
+t1() ->
+    A = #r1{f1 = a},
+    {r1, a} = A.
+
+t2() ->
+    A = {r1, 10}, % violates the type of #r1{}
+    {r1, 10} = A. % violates the type of #r1{}
+
+adt_t1() ->
+    R = rec_adt:r1(),
+    {r1, a} = R. % breaks the opaqueness
+
+-spec adt_t1(rec_adt:r1()) -> rec_adt:r1(). % invalid type spec
+
+adt_t1(R) ->
+    {r1, a} = R.
+
+-spec adt_r1() -> rec_adt:r1(). % invalid type spec
+
+adt_r1() ->
+    #r1{f1 = a}.
+
+-opaque f() :: fun((_) -> _).
+
+-opaque op_t() :: integer().
+
+-spec t(f()) -> _.
+
+t(A) ->
+    T = term(),
+    %% 3(T), % cannot test this: dialyzer_dep deliberately crashes
+    A(T).
+
+-spec term() -> op_t().
+
+term() ->
+    3.
+
+t_adt() ->
+    A = rec_adt:f(),
+    T = term(),
+    A(T).
+
+-record(r, {f = fun(_) -> 3 end :: f(), o = 1 :: op_t()}).
+
+-opaque r() :: #r{}.
+
+-opaque tup() :: {'r', f(), op_t()}.
+
+-spec r() -> _.
+
+r() ->
+    {r, f(), 2}. % OK, f() is a local opaque type
+
+-spec f() -> f().
+
+f() ->
+    fun(_) -> 3 end.
+
+r_adt() ->
+    {r, rec_adt:f(), 2}. % breaks the opaqueness
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_adt.erl b/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_adt.erl
new file mode 100644
index 0000000000..21a277c1e9
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_adt.erl
@@ -0,0 +1,138 @@
+-module(simple1_adt).
+
+-export([d1/0, d2/0, i/0, n1/0, n2/0, o1/0, o2/0,
+         c1/0, c2/0, bit1/0, a/0, i1/0, tuple/0,
+         b1/0, b2/0, ty_i1/0]).
+
+-export_type([o1/0, o2/0, d1/0, d2/0]).
+
+-export_type([i1/0, i2/0, di1/0, di2/0]).
+
+-export_type([ty_i1/0, c1/0, c2/0]).
+
+-export_type([b1/0, b2/0]).
+
+-export_type([bit1/0]).
+
+-export_type([tuple1/0, a/0, i/0]).
+
+%% Equal:
+
+-opaque o1() :: a | b | c.
+
+-opaque o2() :: a | b | c.
+
+%% Disjoint:
+
+-opaque d1() :: a | b | c.
+
+-opaque d2() :: d | e | f.
+
+%% One common element:
+
+-opaque c1() :: a | b | c.
+
+-opaque c2() :: c | e | f.
+
+%% Equal integer range:
+
+-opaque i1() :: 1 | 2.
+
+-opaque i2() :: 1 | 2.
+
+%% Disjoint integer range:
+
+-opaque di1() :: 1 | 2.
+
+-opaque di2() :: 3 | 4.
+
+
+-type ty_i1() :: 1 | 2.
+
+%% Boolean types
+
+-opaque b1() :: boolean().
+
+-opaque b2() :: boolean().
+
+%% Binary types
+
+-opaque bit1() :: binary().
+
+%% Tuple types
+
+-opaque tuple1() :: tuple().
+
+%% Atom type
+
+-opaque a() :: atom().
+
+-opaque i() :: integer().
+
+-spec d1() -> d1().
+
+d1() -> a.
+
+-spec d2() -> d2().
+
+d2() -> d.
+
+-spec i() -> i().
+
+i() ->
+    1.
+
+-spec n1() -> o1().
+
+n1() -> a.
+
+-spec n2() -> o2().
+
+n2() -> a.
+
+-spec o1() -> o1().
+
+o1() -> a.
+
+-spec o2() -> o2().
+
+o2() -> a.
+
+-spec c1() -> c1().
+
+c1() -> a.
+
+-spec c2() -> c2().
+
+c2() -> e.
+
+-spec bit1() -> bit1().
+
+bit1() ->
+    <<"hej">>.
+
+-spec a() -> a().
+
+a() ->
+    e.
+
+-spec i1() -> i1().
+
+i1() -> 1.
+
+-spec tuple() -> tuple1().
+
+tuple() -> {1,2}.
+
+-spec b1() -> b1().
+
+b1() -> true.
+
+-spec b2() -> b2().
+
+b2() -> false.
+
+-spec ty_i1() -> ty_i1().
+
+ty_i1() ->
+    1.
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
new file mode 100644
index 0000000000..5135eb8e59
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_api.erl
@@ -0,0 +1,571 @@
+-module(simple1_api).
+
+-export([t1/1, adt_t1/1, t2/1, adt_t2/1, tup/0, t3/0, t4/0, t5/0, t6/0, t7/0,
+         t8/0, adt_t3/0, adt_t4/0, adt_t7/0, adt_t8/0, adt_t5/0,
+         c1/2, c2/2, c2/0, c3/0, c4/0, tt1/0, tt2/0,
+         cmp1/0, cmp2/0, cmp3/0, cmp4/0,
+         ty_cmp1/0, ty_cmp2/0, ty_cmp3/0, ty_cmp4/0,
+         f1/0, f2/0, adt_f1/0, adt_f2/0, f3/0, f4/0, adt_f3/0, adt_f4/0,
+         adt_f4_a/0, adt_f4_b/0,
+         bool_t1/0, bool_t2/0, bool_t3/0, bool_t4/0, bool_t5/1, bool_t6/1,
+         bool_t7/0, bool_adt_t1/0, bool_adt_t2/0, bool_adt_t5/1,
+         bool_adt_t6/1, bool_t8/0, bool_adt_t8/2, bool_t9/0, bool_adt_t9/2,
+         bit_t1/0, bit_adt_t1/0, bit_t3/1, bit_adt_t2/0, bit_adt_t3/1,
+         bit_t5/1, bit_t4/1, bit_adt_t4/1, bit_t5/0, bit_adt_t5/0,
+         call_f/1, call_f_adt/1, call_m_adt/1, call_m/1, call_f_i/1,
+         call_m_i/1, call_m_adt_i/1, call_f_adt_i/1,
+         eq1/0, eq2/0, c5/0, c6/2, c7/2, c8/0]).
+
+%%% Equal opaque types
+
+-export_type([o1/0, o2/0]).
+
+-export_type([d1/0, d2/0]).
+
+-opaque o1() :: a | b | c.
+
+-opaque o2() :: a | b | c.
+
+-export_type([i1/0, i2/0, di1/0, di2/0]).
+
+-export_type([b1/0, b2/0]).
+
+-export_type([bit1/0]).
+
+-export_type([a/0, i/0]).
+
+%% The derived spec is
+%%  -spec t1('a' | 'b') -> simple1_api:o1('a') | simple1_api:o2('a').
+%% but that is not tested...
+
+t1(a) ->
+    o1();
+t1(b) ->
+    o2().
+
+-spec o1() -> o1().
+
+o1() -> a.
+
+-spec o2() -> o2().
+
+o2() -> a.
+
+%% The derived spec is
+%% -spec adt_t1('a' | 'b') -> simple1_adt:o1('a') | simple1_adt:o2('a').
+%% but that is not tested...
+
+adt_t1(a) ->
+    simple1_adt:o1();
+adt_t1(b) ->
+    simple1_adt:o2().
+
+%%% Disjunct opaque types
+
+-opaque d1() :: a | b | c.
+
+-opaque d2() :: d | e | f.
+
+%% -spec t2('a' | 'b') -> simple1_api:d1('a') | simple1_api:d2('d').
+
+t2(a) ->
+    d1();
+t2(b) ->
+    d2().
+
+-spec d1() -> d1().
+
+d1() -> a.
+
+-spec d2() -> d2().
+
+d2() -> d.
+
+%% -spec adt_t2('a' | 'b') -> simple1_adt:d1('a') | simple1_adt:d2('d').
+
+adt_t2(a) ->
+    simple1_adt:d1();
+adt_t2(b) ->
+    simple1_adt:d2().
+
+-spec tup() -> simple1_adt:tuple1(). % invalid type spec
+
+tup() ->
+    {a, b}.
+
+%%% Matching equal opaque types with different names
+
+t3() ->
+    A = n1(),
+    B = n2(),
+    A = A, % OK, of course
+    A = B. % OK since o1() and o2() are local opaque types
+
+t4() ->
+    A = n1(),
+    B = n2(),
+    true = A =:= A, % OK, of course
+    A =:= B. % OK since o1() and o2() are local opaque types
+
+t5() ->
+    A = d1(),
+    B = d2(),
+    A =:= B. % can never evaluate to true
+
+t6() ->
+    A = d1(),
+    B = d2(),
+    A = B. % can never succeed
+
+t7() ->
+    A = d1(),
+    B = d2(),
+    A =/= B. % OK (always true?)
+
+t8() ->
+    A = d1(),
+    B = d2(),
+    A /= B. % OK (always true?)
+
+-spec n1() -> o1().
+
+n1() -> a.
+
+-spec n2() -> o2().
+
+n2() -> a.
+
+adt_t3() ->
+    A = simple1_adt:n1(),
+    B = simple1_adt:n2(),
+    true = A =:= A, % OK.
+    A =:= B. % opaque test, not OK
+
+adt_t4() ->
+    A = simple1_adt:n1(),
+    B = simple1_adt:n2(),
+    A = A, % OK
+    A = B. % opaque term
+
+adt_t7() ->
+    A = simple1_adt:n1(),
+    B = simple1_adt:n2(),
+    false = A =/= A, % OK
+    A =/= B. % opaque test, not OK
+
+adt_t8() ->
+    A = simple1_adt:n1(),
+    B = simple1_adt:n2(),
+    false = A /= A, % OK
+    A /= B. % opaque test, not OK
+
+adt_t5() ->
+    A = simple1_adt:c1(),
+    B = simple1_adt:c2(),
+    A =:= B. % opaque test, not OK
+
+%% Comparison in guard
+
+-spec c1(simple1_adt:d1(), simple1_adt:d2()) -> boolean().
+
+c1(A, B) when A =< B -> true. % succ type of A and B is any() (type spec is OK)
+
+-spec c2(simple1_adt:d1(), simple1_adt:d2()) -> boolean().
+
+c2(A, B) ->
+    if A =< B -> true end. % succ type of A and B is any() (type spec is OK)
+
+c2() ->
+    A = simple1_adt:d1(),
+    B = simple1_adt:d2(),
+    if A =< B -> ok end. % opaque term
+
+c3() ->
+    B = simple1_adt:d2(),
+    if a =< B -> ok end. % opaque term
+
+c4() ->
+    A = simple1_adt:d1(),
+    if A =< d -> ok end. % opaque term
+
+tt1() ->
+    A = o1(),
+    is_integer(A). % OK
+
+tt2() ->
+    A = simple1_adt:d1(),
+    is_integer(A). % breaks the opaqueness
+
+%% Comparison with integers
+
+-opaque i1() :: 1 | 2.
+
+-opaque i2() :: 1 | 2.
+
+-opaque di1() :: 1 | 2.
+
+-opaque di2() :: 3 | 4.
+
+-spec i1() -> i1().
+
+i1() -> 1.
+
+-type ty_i1() :: 1 | 2.
+
+-spec ty_i1() -> ty_i1().
+
+ty_i1() -> 1.
+
+cmp1() ->
+    A = i1(),
+    if A > 3 -> ok end. % can never succeed
+
+cmp2() ->
+    A = simple1_adt:i1(),
+    if A > 3 -> ok end. % opaque term
+
+cmp3() ->
+    A = i1(),
+    if A < 3 -> ok end.
+
+cmp4() ->
+    A = simple1_adt:i1(),
+    if A < 3 -> ok end. % opaque term
+
+%% -type
+
+ty_cmp1() ->
+    A = ty_i1(),
+    if A > 3 -> ok end. % can never succeed
+
+ty_cmp2() ->
+    A = simple1_adt:ty_i1(),
+    if A > 3 -> ok end. % can never succeed
+
+ty_cmp3() ->
+    A = ty_i1(),
+    if A < 3 -> ok end.
+
+ty_cmp4() ->
+    A = simple1_adt:ty_i1(),
+    if A < 3 -> ok end.
+
+%% is_function
+
+f1() ->
+    T = n1(),
+    if is_function(T) -> ok end. % can never succeed
+
+f2() ->
+    T = n1(),
+    is_function(T). % ok
+
+adt_f1() ->
+    T = simple1_adt:n1(),
+    if is_function(T) -> ok end. % breaks the opaqueness
+
+adt_f2() ->
+    T = simple1_adt:n1(),
+    is_function(T). % breaks the opaqueness
+
+f3() ->
+    A = i1(),
+    T = n1(),
+    if is_function(T, A) -> ok end. % can never succeed
+
+f4() ->
+    A = i1(),
+    T = n1(),
+    is_function(T, A). % ok
+
+adt_f3() ->
+    A = simple1_adt:i1(),
+    T = simple1_adt:n1(),
+    if is_function(T, A) -> ok end. % breaks the opaqueness
+
+adt_f4() ->
+    A = simple1_adt:i1(),
+    T = simple1_adt:n1(),
+    is_function(T, A). % breaks the opaqueness
+
+adt_f4_a() ->
+    A = simple1_adt:i1(),
+    T = n1(),
+    is_function(T, A). % opaque term
+
+
+adt_f4_b() ->
+    A = i1(),
+    T = simple1_adt:n1(),
+    is_function(T, A). % breaks the opaqueness
+
+%% A few Boolean examples
+
+bool_t1() ->
+    B = b2(),
+    if B -> ok end. % B =:= true can never succeed
+
+bool_t2() ->
+    A = b1(),
+    B = b2(),
+    if A and not B -> ok end.
+
+bool_t3() ->
+    A = b1(),
+    if not A -> ok end. % can never succeed
+
+bool_t4() ->
+    A = n1(),
+    if not ((A >= 1) and not (A < 1)) -> ok end. % can never succeed
+
+-spec bool_t5(i1()) -> integer().
+
+bool_t5(A) ->
+    if [not (A > 1)] =:=
+       [false]-> 1 end.
+
+-spec bool_t6(b1()) -> integer().
+
+bool_t6(A) ->
+    if [not A] =:=
+       [false]-> 1 end.
+
+-spec bool_t7() -> integer().
+
+bool_t7() ->
+    A = i1(),
+    if [not A] =:= % cannot succeed
+       [false]-> 1 end.
+
+bool_adt_t1() ->
+    B = simple1_adt:b2(),
+    if B -> ok end. % opaque term
+
+bool_adt_t2() ->
+    A = simple1_adt:b1(),
+    B = simple1_adt:b2(),
+    if A and not B -> ok end. % opaque term
+
+-spec bool_adt_t5(simple1_adt:i1()) -> integer().
+
+bool_adt_t5(A) ->
+    if [not (A > 1)] =:= % succ type of A is any() (type spec is OK)
+       [false]-> 1 end.
+
+-spec bool_adt_t6(simple1_adt:b1()) -> integer(). % invalid type spec
+
+bool_adt_t6(A) ->
+    if [not A] =:= % succ type of A is 'true'
+       [false]-> 1 end.
+
+-spec bool_t8() -> integer().
+
+bool_t8() ->
+    A = i1(),
+    if [A and A] =:= % cannot succeed
+       [false]-> 1 end.
+
+-spec bool_adt_t8(simple1_adt:b1(), simple1_adt:b2()) -> integer(). % invalid
+
+bool_adt_t8(A, B) ->
+    if [A and B] =:=
+       [false]-> 1 end.
+
+-spec bool_t9() -> integer().
+
+bool_t9() ->
+    A = i1(),
+    if [A or A] =:= % cannot succeed
+       [false]-> 1 end.
+
+-spec bool_adt_t9(simple1_adt:b1(), simple1_adt:b2()) -> integer(). % invalid
+
+bool_adt_t9(A, B) ->
+    if [A or B] =:=
+       [false]-> 1 end.
+
+-opaque b1() :: boolean().
+
+-opaque b2() :: boolean().
+
+-spec b1() -> b1().
+
+b1() -> true.
+
+-spec b2() -> b2().
+
+b2() -> false.
+
+%% Few (very few...) examples with bit syntax
+
+bit_t1() ->
+    A = i1(),
+    <<100:(A)>>.
+
+bit_adt_t1() ->
+    A = simple1_adt:i1(),
+    <<100:(A)>>. % breaks the opaqueness
+
+bit_t3(A) ->
+    B = i1(),
+    case none:none() of
+        <<A:B>> -> 1
+    end.
+
+bit_adt_t2() ->
+    A = simple1_adt:i1(),
+    case <<"hej">> of
+        <<_:A>> -> ok % breaks the opaqueness (but the message is strange)
+    end.
+
+
+bit_adt_t3(A) ->
+    B = simple1_adt:i1(),
+    case none:none() of
+        <<A:  % breaks the opaqueness (the message is less than perfect)
+          B>> -> 1
+    end.
+
+bit_t5(A) ->
+    B = o1(),
+    case none:none() of
+        <<A:B>> -> 1 % breaks the opaqueness
+    end.
+
+-spec bit_t4(<<_:1>>) -> integer().
+
+bit_t4(A) ->
+    Sz = i1(),
+    case A of
+        <<_:Sz>> -> 1
+    end.
+
+-spec bit_adt_t4(<<_:1>>) -> integer().
+
+bit_adt_t4(A) ->
+    Sz = simple1_adt:i1(),
+    case A of
+        <<_:Sz>> -> 1 % breaks the opaqueness
+    end.
+
+bit_t5() ->
+    A = bit1(),
+    case A of
+        <<_/binary>> -> 1
+    end.
+
+bit_adt_t5() ->
+    A = simple1_adt:bit1(),
+    case A of
+        <<_/binary>> -> 1 % breaks the opaqueness
+    end.
+
+-opaque bit1() :: binary().
+
+-spec bit1() -> bit1().
+
+bit1() ->
+    <<"hej">>.
+
+%% Calls with variable module or function
+
+call_f(A) ->
+    A = a(),
+    foo:A(A).
+
+call_f_adt(A) ->
+    A = simple1_adt:a(),
+    foo:A(A). % breaks the opaqueness
+
+call_m(A) ->
+    A = a(),
+    A:foo(A).
+
+call_m_adt(A) ->
+    A = simple1_adt:a(),
+    A:foo(A). % breaks the opaqueness
+
+-opaque a() :: atom().
+
+-opaque i() :: integer().
+
+-spec a() -> a().
+
+a() ->
+    e.
+
+call_f_i(A) ->
+    A = i(),
+    foo:A(A). % A is not atom() but i()
+
+call_f_adt_i(A) ->
+    A = simple1_adt:i(),
+    foo:A(A). % A is not atom() but simple1_adt:i()
+
+call_m_i(A) ->
+    A = i(),
+    A:foo(A). % A is not atom() but i()
+
+call_m_adt_i(A) ->
+    A = simple1_adt:i(),
+    A:foo(A). % A is not atom() but simple1_adt:i()
+
+-spec eq1() -> integer().
+
+eq1() ->
+    A = simple1_adt:d2(),
+    B = simple1_adt:d1(),
+    if
+        A == B -> % opaque term
+            0;
+        A == A ->
+            1;
+        A =:= A -> % compiler finds this one cannot match
+            2;
+        true -> % compiler finds this one cannot match
+            3
+    end.
+
+eq2() ->
+    A = simple1_adt:d1(),
+    if
+        {A} >= {A} ->
+            1;
+        A >= 3 -> % opaque term
+            2;
+        A == 3 -> % opaque term
+            3;
+        A =:= 3 -> % opaque term
+            4;
+        A == A ->
+            5;
+        A =:= A -> % compiler finds this one cannot match
+            6
+    end.
+
+c5() ->
+    A = simple1_adt:d1(),
+    A < 3. % opaque term
+
+c6(A, B) ->
+    A = simple1_adt:d1(),
+    B = simple1_adt:d1(),
+    A =< B. % same type - no warning
+
+c7(A, B) ->
+    A = simple1_adt:d1(),
+    B = simple1_adt:d2(),
+    A =< B. % opaque term
+
+c8() ->
+    D = digraph:new(),
+    E = ets:new(foo, []),
+    if {D, a} > {D, E} -> true; % OK
+       {1.0, 2} > {{D}, {E}} -> true; % OK
+       {D, 3} > {D, E} -> true  % opaque term 2
+    end.
+
+-spec i() -> i().
+
+i() ->
+    1.
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple2_api.erl b/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple2_api.erl
new file mode 100644
index 0000000000..c86f6fd0b5
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple2_api.erl
@@ -0,0 +1,125 @@
+-module(simple2_api).
+
+-export([c1/2, c2/0, c3/0, c4/1, c5/1, c6/0, c6_b/0, c7/0, c7_b/0,
+         c7_c/0, c8/0, c9/0, c10/0, c11/0, c12/0, c13/0, c14/0, c15/0,
+         c16/0, c17/0, c18/0, c19/0, c20/0, c21/0, c22/0, c23/0,
+         c24/0, c25/0, c26/0]).
+
+-spec c1(simple1_adt:d1(), simple1_adt:d2()) -> boolean().
+
+c1(A, B) ->
+    {A} =< {B}. % succ type of A and B is any()
+
+c2() ->
+    A = simple1_adt:d1(),
+    erlang:make_tuple(1, A). % ok
+
+c3() ->
+    A = simple1_adt:d1(),
+    setelement(1, {A}, A). % ok
+
+c4(_) ->
+    A = simple1_adt:d1(),
+    halt(A). % ok (BIF fails...)
+
+c5(_) ->
+    A = simple1_adt:d1(),
+    [A] -- [A]. % ok
+
+c6() ->
+    A = simple1_adt:d1(),
+    A ! foo. % opaque term
+
+c6_b() ->
+    A = simple1_adt:d1(),
+    erlang:send(A, foo). % opaque term
+
+c7() ->
+    A = simple1_adt:d1(),
+    foo ! A. % ok
+
+c7_b() ->
+    A = simple1_adt:d1(),
+    erlang:send(foo, A). % ok
+
+c7_c() ->
+    A = simple1_adt:d1(),
+    erlang:send(foo, A, []). % ok
+
+c8() ->
+    A = simple1_adt:d1(),
+    A < 3. % opaque term
+
+c9() ->
+    A = simple1_adt:d1(),
+    lists:keysearch(A, 1, []). % ok
+
+c10() ->
+    A = simple1_adt:d1(),
+    lists:keysearch(1, A, []). % opaque term 2
+
+c11() ->
+    A = simple1_adt:tuple(),
+    lists:keysearch(key, 1, [A]). % ok
+
+c12() ->
+    A = simple1_adt:tuple(),
+    lists:keysearch(key, 1, A). % opaque term 3
+
+c13() ->
+    A = simple1_adt:tuple(),
+    lists:keysearch(key, 1, [{A,2}]). % ok
+
+c14() ->
+    A = simple1_adt:tuple(),
+    lists:keysearch(key, 1, [{2,A}]). % ok
+
+c15() ->
+    A = simple1_adt:d1(),
+    lists:keysearch(key, 1, [A]). % ok
+
+c16() ->
+    A = simple1_adt:tuple(),
+    erlang:send(foo, A). % ok
+
+c17() ->
+    A = simple1_adt:tuple(),
+    lists:reverse([A]). % ok
+
+c18() ->
+    A = simple1_adt:tuple(),
+    lists:keyreplace(a, 1, [A], {1,2}). % ok
+
+c19() ->
+    A = simple1_adt:tuple(),
+    %% Problem. The spec says argument 4 is a tuple(). Fix that!
+    lists:keyreplace(a, 1, [{1,2}], A). % opaque term 4
+
+c20() ->
+    A = simple1_adt:tuple(),
+    lists:flatten(A). % opaque term 1
+
+c21() ->
+    A = simple1_adt:tuple(),
+    lists:flatten([[{A}]]). % ok
+
+c22() ->
+    A = simple1_adt:tuple(),
+    lists:flatten([[A]]). % ok
+
+c23() ->
+    A = simple1_adt:tuple(),
+    lists:flatten([A]). % ok
+
+c24() ->
+    A = simple1_adt:tuple(),
+    lists:flatten({A}). % will never return
+
+c25() ->
+    A = simple1_adt:d1(),
+    B = simple1_adt:tuple(),
+    if {A,3} > {A,B} -> true end. % opaque 2nd argument
+
+c26() ->
+    B = simple1_adt:tuple(),
+    tuple_to_list(B). % opaque term 1