dialyzer: Fix another pattern literal bug

dialyzer_typesig:traverse/3 would perform an unsafe optimisation when
given a cons pattern that contained a map and could be folded into a
literal with cerl:fold_literal/1. In this case, when traversing the map
a type variable would be generated, but this variable would be dropped
by the erl_types:t_cons/2 constructor by in turn calling t_sup(),
producing the overapproximation any(). However, in this particular case,
dialyzer_typesig:traverse/3 is not allowed to overapproximate, since its
result is used in an EQ-constraint.

Although erl_types:t_tuple/1 does not overapproximate like t_cons/2,
which makes the bug unlikely to affect tuples too, the fix was
nevertheless applied defensively to the case of tuples as well.

Also, fix a bug where dialyzer_utils:refold_pattern/1 would generate
syntax nodes with two {label, _} attributes.

3 files changed, 73 insertions, 6 deletions

diff --git a/lib/dialyzer/src/dialyzer_typesig.erl b/lib/dialyzer/src/dialyzer_typesig.erl
index 5b40376352..ae8b195345 100644
--- a/lib/dialyzer/src/dialyzer_typesig.erl
+++ b/lib/dialyzer/src/dialyzer_typesig.erl
@@ -127,6 +127,8 @@
                 solvers     = []                :: [solver()]
 	       }).
 
+-type state() :: #state{}.
+
 %%-----------------------------------------------------------------------------
 
 -define(TYPE_LIMIT, 4).
@@ -312,7 +314,7 @@ traverse(Tree, DefinedVars, State) ->
       Hd = cerl:cons_hd(Tree),
       Tl = cerl:cons_tl(Tree),
       {State1, [HdVar, TlVar]} = traverse_list([Hd, Tl], DefinedVars, State),
-      case cerl:is_literal(cerl:fold_literal(Tree)) of
+      case cerl:is_literal(fold_literal_maybe_match(Tree, State)) of
 	true ->
 	  %% We do not need to do anything more here.
 	  {State, t_cons(HdVar, TlVar)};
@@ -448,7 +450,7 @@ traverse(Tree, DefinedVars, State) ->
       Elements = cerl:tuple_es(Tree),
       {State1, EVars} = traverse_list(Elements, DefinedVars, State),
       {State2, TupleType} =
-	case cerl:is_literal(cerl:fold_literal(Tree)) of
+	case cerl:is_literal(fold_literal_maybe_match(Tree, State1)) of
 	  true ->
 	    %% We do not need to do anything more here.
 	    {State, t_tuple(EVars)};
@@ -2056,7 +2058,7 @@ sane_maps(Map1, Map2, Keys, _S1, _S2) ->
 %% Solver v2
 
 -record(v2_state, {constr_data = dict:new() :: dict:dict(),
-                   state :: #state{}}).
+		   state :: state()}).
 
 v2_solve_ref(Fun, Map, State) ->
   V2State = #v2_state{state = State},
@@ -3430,6 +3432,15 @@ find_constraint(Tuple, [#constraint_list{list = List}|Cs]) ->
 find_constraint(Tuple, [_|Cs]) ->
   find_constraint(Tuple, Cs).
 
+-spec fold_literal_maybe_match(cerl:tree(), state()) -> cerl:tree().
+
+fold_literal_maybe_match(Tree0, State) ->
+  Tree1 = cerl:fold_literal(Tree0),
+  case state__is_in_match(State) of
+    false -> Tree1;
+    true -> dialyzer_utils:refold_pattern(Tree1)
+  end.
+
 lookup_record(Records, Tag, Arity) ->
   case erl_types:lookup_record(Tag, Arity, Records) of
     {ok, Fields} ->
diff --git a/lib/dialyzer/src/dialyzer_utils.erl b/lib/dialyzer/src/dialyzer_utils.erl
index 721c2c000a..d37701f03b 100644
--- a/lib/dialyzer/src/dialyzer_utils.erl
+++ b/lib/dialyzer/src/dialyzer_utils.erl
@@ -873,8 +873,15 @@ refold_pattern(Pat) ->
   case cerl:is_literal(Pat) andalso find_map(cerl:concrete(Pat)) of
     true ->
       Tree = refold_concrete_pat(cerl:concrete(Pat)),
-      [{label, Label}] = cerl:get_ann(Tree),
-      cerl:set_ann(Tree, [{label, Label}|cerl:get_ann(Pat)]);
+      PatAnn = cerl:get_ann(Pat),
+      case proplists:is_defined(label, PatAnn) of
+	%% Literals are not normally annotated with a label, but can be if, for
+	%% example, they were created by cerl:fold_literal/1.
+	true -> cerl:set_ann(Tree, PatAnn);
+	false ->
+	  [{label, Label}] = cerl:get_ann(Tree),
+	  cerl:set_ann(Tree, [{label, Label}|PatAnn])
+      end;
     false -> Pat
   end.
 
diff --git a/lib/dialyzer/test/map_SUITE_data/src/bug.erl b/lib/dialyzer/test/map_SUITE_data/src/bug.erl
index 9e152bf461..fc32f5641a 100644
--- a/lib/dialyzer/test/map_SUITE_data/src/bug.erl
+++ b/lib/dialyzer/test/map_SUITE_data/src/bug.erl
@@ -1,6 +1,11 @@
 -module(bug).
 
--export([t1/0, f1/1]).
+-export([t1/0, f1/1
+	,t2/0, f2/1
+	,t3/0, f3/1
+	,t4/0, f4/1
+	,t5/0, f5/1
+	]).
 
 t1() ->
     V = f1(#{a=>b}),
@@ -12,3 +17,47 @@ t1() ->
 
 f1(M) -> %% Should get map() succ typing
     #{} = M.
+
+t2() ->
+    V = f2([#{a=>b}]),
+    case V of
+	[#{a := P}] -> P; %% Must not warn here
+	_ -> ok
+    end,
+    ok.
+
+f2(M) -> %% Should get [map(),...] succ typing
+    [#{}] = M.
+
+t3() ->
+    V = f3([#{a=>b},a]),
+    case V of
+	[#{a := P}, _Q] -> P; %% Must not warn here
+	_ -> ok
+    end,
+    ok.
+
+f3(M) -> %% Should get [map()|a,...] succ typing
+    [#{},a] = M.
+
+t4() ->
+    V = f4({#{a=>b},{}}),
+    case V of
+	{#{a := P},{}} -> P; %% Must not warn here
+	_ -> ok
+    end,
+    ok.
+
+f4(M) -> %% Should get {map(),{}} succ typing
+    {#{},{}} = M.
+
+t5() ->
+    V = f5(#{k=>q,a=>b}),
+    case V of
+	#{k := q, a := P} -> P; %% Must not warn here
+	_ -> ok
+    end,
+    ok.
+
+f5(M) -> %% Should get #{k:=q, ...} succ typing
+    #{k:=q} = M.