dialyzer: Improve a warning message

Messages like "Invalid type specification for function
para3:exp_adt/0. The success typing is () -> 3" now look like
"The specification for para3:exp_adt/0 has an opaque subtype
para3_adt:exp1(para3_adt:exp2()) which is violated by the success
typing () -> 3".

The old message did not give any clue as to what invalidated the
contract, namely the opaque subtype.

4 files changed, 36 insertions, 9 deletions

diff --git a/lib/dialyzer/src/dialyzer.erl b/lib/dialyzer/src/dialyzer.erl
index 7f86520c06..aaa2f358d6 100644
--- a/lib/dialyzer/src/dialyzer.erl
+++ b/lib/dialyzer/src/dialyzer.erl
@@ -407,6 +407,10 @@ message_to_string({contract_range, [Contract, M, F, ArgStrings, Line, CRet]}) ->
 message_to_string({invalid_contract, [M, F, A, Sig]}) ->
   io_lib:format("Invalid type specification for function ~w:~w/~w."
 		" The success typing is ~s\n", [M, F, A, Sig]);
+message_to_string({contract_with_opaque, [M, F, A, OpaqueType, SigType]}) ->
+  io_lib:format("The specification for ~w:~w/~w"
+                " has an opaque subtype ~s which is violated by the"
+                " success typing ~s\n", [M, F, A, OpaqueType, SigType]);
 message_to_string({extra_range, [M, F, A, ExtraRanges, SigRange]}) ->
   io_lib:format("The specification for ~w:~w/~w states that the function"
 		" might also return ~s but the inferred return is ~s\n",
diff --git a/lib/dialyzer/src/dialyzer_contracts.erl b/lib/dialyzer/src/dialyzer_contracts.erl
index a72368f9f8..73b04b305b 100644
--- a/lib/dialyzer/src/dialyzer_contracts.erl
+++ b/lib/dialyzer/src/dialyzer_contracts.erl
@@ -232,7 +232,7 @@ check_contract(#contract{contracts = Contracts}, SuccType, Opaques) ->
       error ->
 	{error, {overlapping_contract, []}};
       ok ->
-	InfList = [erl_types:t_inf(Contract, SuccType, Opaques)
+	InfList = [{Contract, erl_types:t_inf(Contract, SuccType, Opaques)}
 		   || Contract <- Contracts2],
 	case check_contract_inf_list(InfList, SuccType, Opaques) of
 	  {error, _} = Invalid -> Invalid;
@@ -256,10 +256,21 @@ check_domains([Dom|Doms]) ->
 %% Allow a contract if one of the overloaded contracts is possible.
 %% We used to be more strict, e.g., all overloaded contracts had to be
 %% possible.
-check_contract_inf_list([FunType|Left], SuccType, Opaques) ->
+check_contract_inf_list(List, SuccType, Opaques) ->
+  case check_contract_inf_list(List, SuccType, Opaques, []) of
+    ok -> ok;
+    {error, []} -> {error, invalid_contract};
+    {error, [{SigRange, ContrRange}|_]} ->
+      case erl_types:t_find_opaque_mismatch(SigRange, ContrRange, Opaques) of
+        error -> {error, invalid_contract};
+        {ok, _T1, T2} -> {error, {opaque_mismatch, T2}}
+      end
+  end.
+
+check_contract_inf_list([{Contract, FunType}|Left], SuccType, Opaques, OM) ->
   FunArgs = erl_types:t_fun_args(FunType),
   case lists:any(fun erl_types:t_is_none_or_unit/1, FunArgs) of
-    true -> check_contract_inf_list(Left, SuccType, Opaques);
+    true -> check_contract_inf_list(Left, SuccType, Opaques, OM);
     false ->
       STRange = erl_types:t_fun_range(SuccType),
       case erl_types:t_is_none_or_unit(STRange) of
@@ -267,13 +278,16 @@ check_contract_inf_list([FunType|Left], SuccType, Opaques) ->
 	false ->
 	  Range = erl_types:t_fun_range(FunType),
 	  case erl_types:t_is_none(erl_types:t_inf(STRange, Range)) of
-	    true -> check_contract_inf_list(Left, SuccType, Opaques);
+	    true ->
+              CR = erl_types:t_fun_range(Contract),
+              NewOM = [{STRange, CR}|OM],
+              check_contract_inf_list(Left, SuccType, Opaques, NewOM);
 	    false -> ok
 	  end
       end
   end;
-check_contract_inf_list([], _SuccType, _Opaques) ->
-  {error, invalid_contract}.
+check_contract_inf_list([], _SuccType, _Opaques, OM) ->
+  {error, OM}.
 
 check_extraneous([], _SuccType) -> ok;
 check_extraneous([C|Cs], SuccType) ->
@@ -687,6 +701,9 @@ get_invalid_contract_warnings_funs([{MFA, {FileLine, Contract, _Xtra}}|Left],
 	case check_contract(Contract, Sig, Opaques) of
 	  {error, invalid_contract} ->
 	    [invalid_contract_warning(MFA, WarningInfo, Sig, RecDict)|Acc];
+          {error, {opaque_mismatch, T2}} ->
+            W = contract_opaque_warning(MFA, WarningInfo, T2, Sig, RecDict),
+            [W|Acc];
 	  {error, {overlapping_contract, []}} ->
 	    [overlapping_contract_warning(MFA, WarningInfo)|Acc];
 	  {error, {extra_range, ExtraRanges, STRange}} ->
@@ -740,6 +757,12 @@ invalid_contract_warning({M, F, A}, WarningInfo, SuccType, RecDict) ->
   SuccTypeStr = dialyzer_utils:format_sig(SuccType, RecDict),
   {?WARN_CONTRACT_TYPES, WarningInfo, {invalid_contract, [M, F, A, SuccTypeStr]}}.
 
+contract_opaque_warning({M, F, A}, WarningInfo, OpType, SuccType, RecDict) ->
+  OpaqueStr = erl_types:t_to_string(OpType),
+  SuccTypeStr = dialyzer_utils:format_sig(SuccType, RecDict),
+  {?WARN_CONTRACT_TYPES, WarningInfo,
+   {contract_with_opaque, [M, F, A, OpaqueStr, SuccTypeStr]}}.
+
 overlapping_contract_warning({M, F, A}, WarningInfo) ->
   {?WARN_CONTRACT_TYPES, WarningInfo, {overlapping_contract, [M, F, A]}}.
 
diff --git a/lib/dialyzer/test/opaque_SUITE_data/results/para b/lib/dialyzer/test/opaque_SUITE_data/results/para
index b23d0cae3a..a490de2d43 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/results/para
+++ b/lib/dialyzer/test/opaque_SUITE_data/results/para
@@ -18,7 +18,7 @@ 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
+para3.erl:74: The specification for para3:exp_adt/0 has an opaque subtype para3_adt:exp1(para3_adt:exp2()) which is violated by the success typing () -> 3
 para4.erl:21: Invalid type specification for function para4:a/1. The success typing is (para4:d_all() | para4:d_atom()) -> [{atom() | integer(),atom() | integer()}]
 para4.erl:26: Invalid type specification for function para4:i/1. The success typing is (para4:d_all() | para4:d_integer()) -> [{atom() | integer(),atom() | integer()}]
 para4.erl:31: Invalid type specification for function para4:t/1. The success typing is (para4:d_all() | para4:d_tuple()) -> [{atom() | integer(),atom() | integer()}]
diff --git a/lib/dialyzer/test/opaque_SUITE_data/results/simple b/lib/dialyzer/test/opaque_SUITE_data/results/simple
index 5a7f006d8c..0fdf07d1fe 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/results/simple
+++ b/lib/dialyzer/test/opaque_SUITE_data/results/simple
@@ -22,7 +22,7 @@ rec_api.erl:24: Record construction #r1{f1::10} violates the declared type of fi
 rec_api.erl:29: Matching of pattern {'r1', 10} tagged with a record name violates the declared type of #r1{f1::10}
 rec_api.erl:33: The attempt to match a term of type rec_adt:r1() against the pattern {'r1', 'a'} breaks the opaqueness of the term
 rec_api.erl:35: Invalid type specification for function rec_api:adt_t1/1. The success typing is (#r1{f1::'a'}) -> #r1{f1::'a'}
-rec_api.erl:40: Invalid type specification for function rec_api:adt_r1/0. The success typing is () -> #r1{f1::'a'}
+rec_api.erl:40: The specification for rec_api:adt_r1/0 has an opaque subtype rec_adt:r1() which is violated by the success typing () -> #r1{f1::'a'}
 rec_api.erl:85: The attempt to match a term of type rec_adt:f() against the record field 'f' declared to be of type rec_api:f() breaks the opaqueness of the term
 rec_api.erl:99: Record construction #r2{f1::10} violates the declared type of field f1::rec_api:a()
 simple1_api.erl:113: The test simple1_api:d1() =:= simple1_api:d2() can never evaluate to 'true'
@@ -79,7 +79,7 @@ simple1_api.erl:538: Guard test A::simple1_adt:d1() =:= 3 contains an opaque ter
 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 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'}
+simple1_api.erl:91: The specification for simple1_api:tup/0 has an opaque subtype simple1_adt:tuple1() which is violated by the success typing () -> {'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
 simple2_api.erl:116: The call lists:flatten({simple1_adt:tuple1()}) will never return since it differs in the 1st argument from the success typing arguments: ([any()])
 simple2_api.erl:121: Guard test {simple1_adt:d1(),3} > {simple1_adt:d1(),simple1_adt:tuple1()} contains an opaque term as 2nd argument