dialyzer_typesig: Add map support

28 files changed, 568 insertions, 11 deletions

diff --git a/lib/dialyzer/src/dialyzer_dataflow.erl b/lib/dialyzer/src/dialyzer_dataflow.erl
index 6e49043551..48eaf8510b 100644
--- a/lib/dialyzer/src/dialyzer_dataflow.erl
+++ b/lib/dialyzer/src/dialyzer_dataflow.erl
@@ -2421,7 +2421,9 @@ filter_fail_clauses([Clause|Left]) ->
   case (cerl:clause_pats(Clause) =:= []) of
     true ->
       Body = cerl:clause_body(Clause),
-      case cerl:is_literal(Body) andalso (cerl:concrete(Body) =:= fail) of
+      case cerl:is_literal(Body) andalso (cerl:concrete(Body) =:= fail) orelse
+	cerl:is_c_primop(Body) andalso
+	(cerl:atom_val(cerl:primop_name(Body)) =:= match_fail) of
 	true -> filter_fail_clauses(Left);
 	false -> [Clause|filter_fail_clauses(Left)]
       end;
diff --git a/lib/dialyzer/src/dialyzer_typesig.erl b/lib/dialyzer/src/dialyzer_typesig.erl
index 5f0881bbcd..12d6673d28 100644
--- a/lib/dialyzer/src/dialyzer_typesig.erl
+++ b/lib/dialyzer/src/dialyzer_typesig.erl
@@ -48,6 +48,7 @@
 	 t_is_float/1, t_is_fun/1,
 	 t_is_integer/1, t_non_neg_integer/0,
 	 t_is_list/1, t_is_nil/1, t_is_none/1, t_is_number/1,
+	 t_is_singleton/1,
 
          t_limit/2, t_list/0, t_list/1,
 	 t_list_elements/1, t_nonempty_list/1, t_maybe_improper_list/0,
@@ -57,7 +58,7 @@
 	 t_timeout/0, t_tuple/0, t_tuple/1,
          t_var/1, t_var_name/1,
 	 t_none/0, t_unit/0,
-	 t_map/1
+	 t_map/0, t_map/1, t_map_get/2, t_map_put/2
      ]).
 
 -include("dialyzer.hrl").
@@ -476,7 +477,111 @@ traverse(Tree, DefinedVars, State) ->
 	[] -> {State2, TupleType}
       end;
     map ->
-	{State, t_map([])};
+      Entries = cerl:map_es(Tree),
+      MapFoldFun = fun(Entry, AccState) ->
+		       AccState1 = state__set_in_match(AccState, false),
+		       {AccState2, KeyVar} = traverse(cerl:map_pair_key(Entry),
+						      DefinedVars, AccState1),
+		       AccState3 = state__set_in_match(
+				     AccState2, state__is_in_match(AccState)),
+		       {AccState4, ValVar} = traverse(cerl:map_pair_val(Entry),
+						      DefinedVars, AccState3),
+		       {{KeyVar, ValVar}, AccState4}
+		   end,
+      {Pairs, State1} = lists:mapfoldl(MapFoldFun, State, Entries),
+      %% We mustn't recurse into map arguments to matches. Not only are they
+      %% syntactically only allowed to be the literal #{}, but that would also
+      %% cause an infinite recursion, since traverse/3 unfolds literals with
+      %% maps in them using dialyzer_utils:reflow_pattern/1.
+      {State2, ArgVar} =
+	case state__is_in_match(State) of
+	  false -> traverse(cerl:map_arg(Tree), DefinedVars, State1);
+	  true -> {State1, t_map()}
+	end,
+      MapVar = mk_var(Tree),
+      MapType = ?mk_fun_var(
+		   fun(Map) ->
+		       lists:foldl(
+			 fun({K,V}, TypeAcc) ->
+			     t_map_put({lookup_type(K, Map),
+					lookup_type(V, Map)},
+				       TypeAcc)
+			 end, t_inf(t_map(), lookup_type(ArgVar, Map)),
+			 Pairs)
+		   end, [ArgVar | lists:append([[K,V] || {K,V} <- Pairs])]),
+      %% TODO: does the "same element appearing several times" problem apply
+      %% here too?
+      Fun =
+	fun({KeyVar, ValVar}, {AccState, ShadowKeys}) ->
+	    %% If Val is known to be the last association of Key (i.e. Key
+	    %% is not in ShadowKeys), Val must be a subtype of what is
+	    %% associated to Key in Tree
+	    TypeFun =
+	      fun(Map) ->
+		  KeyType = lookup_type(KeyVar, Map),
+		  case t_is_singleton(KeyType) of
+		    false -> t_any();
+		    true ->
+		      MT = t_inf(lookup_type(MapVar, Map), t_map()),
+		      case t_is_none(MT) of
+			true -> t_none();
+			false ->
+			  DisjointFromKeyType =
+			    fun(ShadowKey) ->
+				t_is_none(t_inf(lookup_type(ShadowKey, Map),
+						KeyType))
+			    end,
+			  case lists:all(DisjointFromKeyType, ShadowKeys) of
+			    true -> t_map_get(KeyType, MT);
+			    %% A later association might shadow this one
+			    false -> t_any()
+			  end
+		      end
+		  end
+	      end,
+	    ValType = ?mk_fun_var(TypeFun, [KeyVar, MapVar | ShadowKeys]),
+	    {state__store_conj(ValVar, sub, ValType, AccState),
+	     [KeyVar | ShadowKeys]}
+	end,
+      %% Accumulate shadowing keys right-to-left
+      {State3, _} = lists:foldr(Fun, {State2, []}, Pairs),
+      %% In a map expression, Arg must contain all keys that are inserted with
+      %% the exact (:=) operator, and are known (i.e. are not in ShadowedKeys)
+      %% to not have been introduced by a previous association
+      State4 =
+	case state__is_in_match(State) of
+	  true -> State3;
+	  false ->
+	    ArgFun =
+	      fun(Map) ->
+		  FoldFun =
+		    fun({{KeyVar, _}, Entry}, {AccType, ShadowedKeys}) ->
+			OpTree = cerl:map_pair_op(Entry),
+			KeyType = lookup_type(KeyVar, Map),
+			AccType1 =
+			  case cerl:is_literal(OpTree) andalso
+			    cerl:concrete(OpTree) =:= exact of
+			    true ->
+			      case t_is_none(t_inf(ShadowedKeys, KeyType)) of
+				true ->
+				  t_map_put({KeyType, t_any()}, AccType);
+				false ->
+				  AccType
+			      end;
+			    false ->
+			      AccType
+			  end,
+			{AccType1, t_sup(KeyType, ShadowedKeys)}
+		    end,
+		  %% Accumulate shadowed keys left-to-right
+		  {ResType, _} = lists:foldl(FoldFun, {t_map(), t_none()},
+					     lists:zip(Pairs, Entries)),
+		  ResType
+	      end,
+	    ArgType = ?mk_fun_var(ArgFun, [KeyVar || {KeyVar, _} <- Pairs]),
+	    state__store_conj(ArgVar, sub, ArgType, State3)
+	end,
+      {state__store_conj(MapVar, sub, MapType, State4), MapVar};
     values ->
       %% We can get into trouble when unifying products that have the
       %% same element appearing several times. Handle these cases by
@@ -948,6 +1053,7 @@ get_type_test({erlang, is_float, 1}) ->     {ok, t_float()};
 get_type_test({erlang, is_function, 1}) ->  {ok, t_fun()};
 get_type_test({erlang, is_integer, 1}) ->   {ok, t_integer()};
 get_type_test({erlang, is_list, 1}) ->      {ok, t_list()};
+get_type_test({erlang, is_map, 1}) ->       {ok, t_map()};
 get_type_test({erlang, is_number, 1}) ->    {ok, t_number()};
 get_type_test({erlang, is_pid, 1}) ->       {ok, t_pid()};
 get_type_test({erlang, is_port, 1}) ->      {ok, t_port()};
@@ -1048,8 +1154,35 @@ get_safe_underapprox_1([Pat|Left], Acc, Map) ->
       Type = t_tuple(Ts),
       get_safe_underapprox_1(Left, [Type|Acc], Map1);
     map ->
-      %% TODO: Can maybe do something here
-      throw(dont_know);
+      %% Some assertions in case the syntax gets more premissive in the future
+      true = #{} =:= cerl:concrete(cerl:map_arg(Pat)),
+      true = lists:all(fun(P) ->
+			   cerl:is_literal(Op = cerl:map_pair_op(P)) andalso
+			     exact =:= cerl:concrete(Op)
+		       end, cerl:map_es(Pat)),
+      KeyTrees = lists:map(fun cerl:map_pair_key/1, cerl:map_es(Pat)),
+      ValTrees = lists:map(fun cerl:map_pair_val/1, cerl:map_es(Pat)),
+      %% Keys must not be underapproximated. Overapproximations are safe.
+      Keys = get_safe_overapprox(KeyTrees),
+      {Vals, Map1} = get_safe_underapprox_1(ValTrees, [], Map),
+      case lists:all(fun erl_types:t_is_singleton/1, Keys) of
+	false -> throw(dont_know);
+	true -> ok
+      end,
+      SortedPairs = lists:sort(lists:zip(Keys, Vals)),
+      %% We need to deal with duplicates ourselves
+      SquashDuplicates =
+	fun SquashDuplicates([{K,First},{K,Second}|List]) ->
+	    case t_is_none(Inf = t_inf(First, Second)) of
+	      true -> throw(dont_know);
+	      false -> [{K, Inf}|SquashDuplicates(List)]
+	    end;
+	    SquashDuplicates([Good|Rest]) ->
+	    [Good|SquashDuplicates(Rest)];
+	    SquashDuplicates([]) -> []
+	end,
+      Type = t_map(SquashDuplicates(SortedPairs)),
+      get_safe_underapprox_1(Left, [Type|Acc], Map1);
     values ->
       Es = cerl:values_es(Pat),
       {Ts, Map1} = get_safe_underapprox_1(Es, [], Map),
@@ -1064,6 +1197,15 @@ get_safe_underapprox_1([Pat|Left], Acc, Map) ->
 get_safe_underapprox_1([], Acc, Map) ->
   {lists:reverse(Acc), Map}.
 
+get_safe_overapprox(Pats) ->
+  lists:map(fun get_safe_overapprox_1/1, Pats).
+
+get_safe_overapprox_1(Pat) ->
+  case cerl:is_literal(Lit = cerl:fold_literal(Pat)) of
+    true  -> t_from_term(cerl:concrete(Lit));
+    false -> t_any()
+  end.
+
 %%----------------------------------------
 %% Guards
 %%
@@ -1263,6 +1405,8 @@ get_bif_constr({erlang, is_integer, 1}, Dst, [Arg], State) ->
   get_bif_test_constr(Dst, Arg, t_integer(), State);
 get_bif_constr({erlang, is_list, 1}, Dst, [Arg], State) ->
   get_bif_test_constr(Dst, Arg, t_maybe_improper_list(), State);
+get_bif_constr({erlang, is_map, 1}, Dst, [Arg], State) ->
+  get_bif_test_constr(Dst, Arg, t_map(), State);
 get_bif_constr({erlang, is_number, 1}, Dst, [Arg], State) ->
   get_bif_test_constr(Dst, Arg, t_number(), State);
 get_bif_constr({erlang, is_pid, 1}, Dst, [Arg], State) ->
diff --git a/lib/dialyzer/test/map_SUITE_data/dialyzer_options b/lib/dialyzer/test/map_SUITE_data/dialyzer_options
new file mode 100644
index 0000000000..50991c9bc5
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/dialyzer_options
@@ -0,0 +1 @@
+{dialyzer_options, []}.
diff --git a/lib/dialyzer/test/map_SUITE_data/results/bad_argument b/lib/dialyzer/test/map_SUITE_data/results/bad_argument
new file mode 100644
index 0000000000..8d76ae5e3f
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/results/bad_argument
@@ -0,0 +1,4 @@
+
+bad_argument.erl:14: Function t3/0 has no local return
+bad_argument.erl:15: Guard test is_map('not_a_map') can never succeed
+bad_argument.erl:5: Function t/0 has no local return
diff --git a/lib/dialyzer/test/map_SUITE_data/results/contract b/lib/dialyzer/test/map_SUITE_data/results/contract
new file mode 100644
index 0000000000..0f6e1d0c65
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/results/contract
@@ -0,0 +1,7 @@
+
+contract.erl:10: Function t2/0 has no local return
+contract.erl:10: The call missing:f(#{'a':=1, 'c':=4}) breaks the contract (#{'a':=1,'b'=>2,'c'=>3}) -> 'ok'
+contract.erl:12: Function t3/0 has no local return
+contract.erl:12: The call missing:f(#{'a':=1, 'b':=2, 'e':=3}) breaks the contract (#{'a':=1,'b'=>2,'c'=>3}) -> 'ok'
+contract.erl:8: Function t1/0 has no local return
+contract.erl:8: The call missing:f(#{'b':=2}) breaks the contract (#{'a':=1,'b'=>2,'c'=>3}) -> 'ok'
diff --git a/lib/dialyzer/test/map_SUITE_data/results/is_map_guard b/lib/dialyzer/test/map_SUITE_data/results/is_map_guard
new file mode 100644
index 0000000000..6ab464d865
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/results/is_map_guard
@@ -0,0 +1,5 @@
+
+is_map_guard.erl:13: Function t2/0 has no local return
+is_map_guard.erl:15: The call is_map_guard:explicit('still_not_map') will never return since it differs in the 1st argument from the success typing arguments: (map())
+is_map_guard.erl:6: Function t1/0 has no local return
+is_map_guard.erl:8: The call is_map_guard:implicit('not_a_map') will never return since it differs in the 1st argument from the success typing arguments: (map())
diff --git a/lib/dialyzer/test/map_SUITE_data/results/map_in_guard b/lib/dialyzer/test/map_SUITE_data/results/map_in_guard
new file mode 100644
index 0000000000..8ba8594b0e
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/results/map_in_guard
@@ -0,0 +1,5 @@
+
+map_in_guard.erl:10: The call map_in_guard:assoc_update('not_a_map') will never return since it differs in the 1st argument from the success typing arguments: (#{})
+map_in_guard.erl:13: The call map_in_guard:assoc_guard_clause('not_a_map') will never return since it differs in the 1st argument from the success typing arguments: (#{})
+map_in_guard.erl:20: The call map_in_guard:exact_guard_clause(#{}) will never return since it differs in the 1st argument from the success typing arguments: (#{'a':='q'})
+map_in_guard.erl:35: Function raw_expr/0 has no local return
diff --git a/lib/dialyzer/test/map_SUITE_data/results/map_in_guard2 b/lib/dialyzer/test/map_SUITE_data/results/map_in_guard2
new file mode 100644
index 0000000000..e3202badbe
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/results/map_in_guard2
@@ -0,0 +1,10 @@
+
+map_in_guard2.erl:10: The call map_in_guard2:assoc_guard_clause('not_a_map') will never return since it differs in the 1st argument from the success typing arguments: (map())
+map_in_guard2.erl:12: The pattern 'true' can never match the type 'false'
+map_in_guard2.erl:17: Clause guard cannot succeed. The variable M was matched against the type 'not_a_map'
+map_in_guard2.erl:20: Function assoc_update/1 has no local return
+map_in_guard2.erl:20: Guard test is_map(M::'not_a_map') can never succeed
+map_in_guard2.erl:22: Clause guard cannot succeed. The variable M was matched against the type 'not_a_map'
+map_in_guard2.erl:22: Function assoc_guard_clause/1 has no local return
+map_in_guard2.erl:27: Function exact_guard_clause/1 has no local return
+map_in_guard2.erl:8: The call map_in_guard2:assoc_update('not_a_map') will never return since it differs in the 1st argument from the success typing arguments: (map())
diff --git a/lib/dialyzer/test/map_SUITE_data/results/map_size b/lib/dialyzer/test/map_SUITE_data/results/map_size
new file mode 100644
index 0000000000..fc6c1f028c
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/results/map_size
@@ -0,0 +1,13 @@
+
+map_size.erl:11: The pattern 1 can never match the type 0
+map_size.erl:13: Function t2/0 has no local return
+map_size.erl:15: Function p/1 has no local return
+map_size.erl:15: Guard test 1 =:= 0 can never succeed
+map_size.erl:17: Function t3/0 has no local return
+map_size.erl:21: The pattern 4 can never match the type 1 | 2 | 3
+map_size.erl:23: Function t4/0 has no local return
+map_size.erl:24: The pattern 0 can never match the type 1 | 2 | 3
+map_size.erl:26: Function t5/1 has no local return
+map_size.erl:5: Function t1/0 has no local return
+map_size.erl:7: The pattern 1 can never match the type 0
+map_size.erl:9: Function e1/0 has no local return
diff --git a/lib/dialyzer/test/map_SUITE_data/results/order b/lib/dialyzer/test/map_SUITE_data/results/order
new file mode 100644
index 0000000000..7be789a11a
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/results/order
@@ -0,0 +1,17 @@
+
+order.erl:12: Function t2/0 has no local return
+order.erl:14: Guard test is_integer(Int::'b') can never succeed
+order.erl:16: The variable _Else can never match since previous clauses completely covered the type 'b'
+order.erl:19: Function t3/0 has no local return
+order.erl:21: Guard test is_integer(Int::'b') can never succeed
+order.erl:23: The variable _Else can never match since previous clauses completely covered the type 'b'
+order.erl:30: The variable _Else can never match since previous clauses completely covered the type 'b' | 1
+order.erl:33: Function t5/0 has no local return
+order.erl:36: The variable Atom can never match since previous clauses completely covered the type 1
+order.erl:37: The variable _Else can never match since previous clauses completely covered the type 1
+order.erl:40: Function t6/0 has no local return
+order.erl:42: Guard test is_integer(Int::'b') can never succeed
+order.erl:44: The variable _Else can never match since previous clauses completely covered the type 'b'
+order.erl:5: Function t1/0 has no local return
+order.erl:7: Guard test is_integer(Int::'b') can never succeed
+order.erl:9: The variable _Else can never match since previous clauses completely covered the type 'b'
diff --git a/lib/dialyzer/test/map_SUITE_data/results/subtract_value_flip b/lib/dialyzer/test/map_SUITE_data/results/subtract_value_flip
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/results/subtract_value_flip
diff --git a/lib/dialyzer/test/map_SUITE_data/results/typeflow b/lib/dialyzer/test/map_SUITE_data/results/typeflow
new file mode 100644
index 0000000000..12f5f1459d
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/results/typeflow
@@ -0,0 +1,6 @@
+
+typeflow.erl:12: Function a_is_integer/1 has no local return
+typeflow.erl:14: Function t2/1 has no local return
+typeflow.erl:19: Function t3/1 has no local return
+typeflow.erl:20: The call maps:get('a',M::#{}) will never return since the success typing arguments are (any(),map())
+typeflow.erl:5: Function t1/1 has no local return
diff --git a/lib/dialyzer/test/map_SUITE_data/results/typeflow2 b/lib/dialyzer/test/map_SUITE_data/results/typeflow2
new file mode 100644
index 0000000000..b93a8599b7
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/results/typeflow2
@@ -0,0 +1,6 @@
+
+typeflow2.erl:26: Function t2/1 has no local return
+typeflow2.erl:29: The call lists:sort(integer()) will never return since it differs in the 1st argument from the success typing arguments: ([any()])
+typeflow2.erl:42: The pattern ~{'a':=X}~ can never match since previous clauses completely covered the type #{'a':=integer()}
+typeflow2.erl:43: The variable _ can never match since previous clauses completely covered the type #{'a':=integer()}
+typeflow2.erl:48: The pattern ~{}~ can never match the type #{'a':=atom() | maybe_improper_list() | integer()}
diff --git a/lib/dialyzer/test/map_SUITE_data/results/typesig b/lib/dialyzer/test/map_SUITE_data/results/typesig
new file mode 100644
index 0000000000..f5c7dacdbc
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/results/typesig
@@ -0,0 +1,5 @@
+
+typesig.erl:5: Function t1/0 has no local return
+typesig.erl:5: The call typesig:test(#{'a':=1}) will never return since it differs in the 1st argument from the success typing arguments: (#{'a':={number()}, ...})
+typesig.erl:6: Function t2/0 has no local return
+typesig.erl:6: The call typesig:test(#{'a':={'b'}, ...}) will never return since it differs in the 1st argument from the success typing arguments: (#{'a':={number()}, ...})
diff --git a/lib/dialyzer/test/map_SUITE_data/src/bad_argument.erl b/lib/dialyzer/test/map_SUITE_data/src/bad_argument.erl
new file mode 100644
index 0000000000..95e2b32ddc
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/src/bad_argument.erl
@@ -0,0 +1,19 @@
+-module(bad_argument).
+
+-export([t/0, t2/0, t3/0]).
+
+t() ->
+    _=(id1(#{a=>q}))#{b:=9}.
+
+t2() ->
+    _ = id2(4),
+    X = id2(3),
+    _ = (#{ X => q})#{3 := p},
+    X.
+
+t3() ->
+    (id3(not_a_map))#{a => b}.
+
+id1(X) -> X.
+id2(X) -> X.
+id3(X) -> X.
diff --git a/lib/dialyzer/test/map_SUITE_data/src/contract.erl b/lib/dialyzer/test/map_SUITE_data/src/contract.erl
new file mode 100644
index 0000000000..2b31be0d58
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/src/contract.erl
@@ -0,0 +1,14 @@
+-module(missing).
+
+-export([t1/0, t2/0, t3/0, t4/0]).
+
+-spec f(#{a := 1, b => 2, c => 3}) -> ok.
+f(_) -> ok.
+
+t1() -> f(#{b => 2}).
+
+t2() -> f(#{a => 1, c => 4}).
+
+t3() -> f(#{a => 1, b => 2, e => 3}).
+
+t4() -> f(#{a => 1, b => 2}).
diff --git a/lib/dialyzer/test/map_SUITE_data/src/is_map_guard.erl b/lib/dialyzer/test/map_SUITE_data/src/is_map_guard.erl
new file mode 100644
index 0000000000..ceb4a8763a
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/src/is_map_guard.erl
@@ -0,0 +1,17 @@
+-module(is_map_guard).
+
+-export([t1/0, t2/0, implicit/1, explicit/1
+	]).
+
+t1() ->
+    _ = implicit(#{}),
+    implicit(not_a_map).
+
+implicit(M) ->
+    M#{}.
+
+t2() ->
+    explicit(#{q=>d}),
+    explicit(still_not_map).
+
+explicit(M) when is_map(M) -> ok.
diff --git a/lib/dialyzer/test/map_SUITE_data/src/map_in_guard.erl b/lib/dialyzer/test/map_SUITE_data/src/map_in_guard.erl
new file mode 100644
index 0000000000..6176ef1fdf
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/src/map_in_guard.erl
@@ -0,0 +1,35 @@
+-module(map_in_guard).
+
+-export([test/0, raw_expr/0]).
+
+test() ->
+    false = assoc_guard(#{}),
+    true  = assoc_guard(not_a_map),
+    #{a := true} = assoc_update(#{}),
+    {'EXIT', {{badmap, not_a_map}, [{?MODULE, assoc_update, 1, _}|_]}}
+	= (catch assoc_update(not_a_map)),
+    ok = assoc_guard_clause(#{}),
+    {'EXIT', {function_clause, [{?MODULE, assoc_guard_clause, _, _}|_]}}
+	= (catch assoc_guard_clause(not_a_map)),
+    true = exact_guard(#{a=>1}),
+    {'EXIT', {function_clause, [{?MODULE, assoc_guard_clause, _, _}|_]}}
+    %% There's nothing we can do to find the error here, is there?
+	= (catch (begin true = exact_guard(#{}) end)),
+    ok = exact_guard_clause(#{a => q}),
+    {'EXIT', {function_clause, [{?MODULE, exact_guard_clause, _, _}|_]}}
+	= (catch exact_guard_clause(#{})),
+    ok.
+
+assoc_guard(M) when is_map(M#{a => b}) -> true;
+assoc_guard(Q) -> false.
+
+assoc_update(M) -> M#{a => true}.
+
+assoc_guard_clause(M) when is_map(M#{a => 3}) -> ok.
+
+exact_guard(M) when (false =/= M#{a := b}) -> true;
+exact_guard(_) -> false.
+
+exact_guard_clause(M) when (false =/= M#{a := b}) -> ok.
+
+raw_expr() when #{}; true -> ok. %% Must not warn here!
diff --git a/lib/dialyzer/test/map_SUITE_data/src/map_in_guard2.erl b/lib/dialyzer/test/map_SUITE_data/src/map_in_guard2.erl
new file mode 100644
index 0000000000..ac2205e8fa
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/src/map_in_guard2.erl
@@ -0,0 +1,27 @@
+-module(map_in_guard2).
+
+-export([test/0]).
+
+test() ->
+    false = assoc_guard(not_a_map),
+    {'EXIT', {{badmap, not_a_map}, [{?MODULE, assoc_update, 1, _}|_]}}
+	= (catch assoc_update(not_a_map)),
+    {'EXIT', {function_clause, [{?MODULE, assoc_guard_clause, _, _}|_]}}
+	= (catch assoc_guard_clause(not_a_map)),
+    {'EXIT', {function_clause, [{?MODULE, assoc_guard_clause, _, _}|_]}}
+	= (catch (begin true = exact_guard(#{}) end)),
+    {'EXIT', {function_clause, [{?MODULE, exact_guard_clause, _, _}|_]}}
+	= (catch exact_guard_clause(#{})),
+    ok.
+
+assoc_guard(M) when is_map(M#{a => b}) -> true;
+assoc_guard(_) -> false.
+
+assoc_update(M) -> M#{a => true}.
+
+assoc_guard_clause(M) when is_map(M#{a => 3}) -> ok.
+
+exact_guard(M) when (false =/= M#{a := b}) -> true;
+exact_guard(_) -> false.
+
+exact_guard_clause(M) when (false =/= M#{a := b}) -> ok.
diff --git a/lib/dialyzer/test/map_SUITE_data/src/map_size.erl b/lib/dialyzer/test/map_SUITE_data/src/map_size.erl
new file mode 100644
index 0000000000..2da4f6904e
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/src/map_size.erl
@@ -0,0 +1,36 @@
+-module(map_size).
+
+-export([t1/0, e1/0, t2/0, t3/0, t4/0, t5/1, t6/1, t7/1]).
+
+t1() ->
+    0 = maps:size(#{}),
+    1 = maps:size(#{}).
+
+e1() ->
+    0 = map_size(#{}),
+    1 = map_size(#{}).
+
+t2() -> p(#{a=>x}).
+
+p(M) when map_size(M) =:= 0 -> ok.
+
+t3() ->
+    1 = map_size(cio()),
+    2 = map_size(cio()),
+    3 = map_size(cio()),
+    4 = map_size(cio()).
+
+t4() ->
+    0 = map_size(cio()).
+
+t5(M) when map_size(M) =:= 0 ->
+    #{a := _} = M. %% Only t5 has no local return; want better message
+
+t6(M) when map_size(M) =:= 0 ->
+    #{} = M.
+
+t7(M=#{a := _}) when map_size(M) =:= 1 ->
+    #{b := _} = M. %% We should warn here too
+
+-spec cio() -> #{3 := ok, 9 => _, 11 => x}.
+cio() -> binary_to_term(<<131,116,0,0,0,2,97,3,100,0,2,111,107,97,9,97,6>>).
diff --git a/lib/dialyzer/test/map_SUITE_data/src/order.erl b/lib/dialyzer/test/map_SUITE_data/src/order.erl
new file mode 100644
index 0000000000..51868d7e94
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/src/order.erl
@@ -0,0 +1,56 @@
+-module(order).
+
+-export([t1/0, t2/0, t3/0, t4/0, t5/0, t6/0]).
+
+t1() ->
+    case maps:get(a, #{a=>1, a=>b}) of
+	Int when is_integer(Int) -> fail;
+	Atom when is_atom(Atom) -> error(ok);
+	_Else -> fail
+    end.
+
+t2() ->
+    case maps:get(a, #{a=>id_1(1), a=>id_b(b)}) of
+	Int when is_integer(Int) -> fail;
+	Atom when is_atom(Atom) -> error(ok);
+	_Else -> fail
+    end.
+
+t3() ->
+    case maps:get(a, #{a=>id_1(1), id_a(a)=>id_b(b)}) of
+	Int when is_integer(Int) -> fail;
+	Atom when is_atom(Atom) -> error(ok);
+	_Else -> fail
+    end.
+
+t4() ->
+    case maps:get(a, #{a=>id_1(1), a_or_b()=>id_b(b)}) of
+	Int when is_integer(Int) -> ok;
+	Atom when is_atom(Atom) -> ok;
+	_Else -> fail
+    end.
+
+t5() ->
+    case maps:get(c, #{c=>id_1(1), a_or_b()=>id_b(b)}) of
+	Int when is_integer(Int) -> error(ok);
+	Atom when is_atom(Atom) -> fail;
+	_Else -> fail
+    end.
+
+t6() ->
+    case maps:get(a, #{a_or_b()=>id_1(1), id_a(a)=>id_b(b)}) of
+	Int when is_integer(Int) -> fail;
+	Atom when is_atom(Atom) -> error(ok);
+	_Else -> fail
+    end.
+
+id_1(X) -> X.
+
+id_a(X) -> X.
+
+id_b(X) -> X.
+
+any() -> binary_to_term(<<>>).
+
+-spec a_or_b() -> a | b.
+a_or_b() -> any().
diff --git a/lib/dialyzer/test/map_SUITE_data/src/subtract_value_flip.erl b/lib/dialyzer/test/map_SUITE_data/src/subtract_value_flip.erl
new file mode 100644
index 0000000000..97e6b54e3c
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/src/subtract_value_flip.erl
@@ -0,0 +1,9 @@
+-module(subtract_value_flip).
+
+-export([t1/1]).
+
+t1(#{type := _Smth} = Map) ->
+    case Map of
+	#{type := a} -> ok;
+	#{type := b} -> error
+    end.
diff --git a/lib/dialyzer/test/map_SUITE_data/src/typeflow.erl b/lib/dialyzer/test/map_SUITE_data/src/typeflow.erl
new file mode 100644
index 0000000000..b43fd6897b
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/src/typeflow.erl
@@ -0,0 +1,25 @@
+-module(typeflow).
+
+-export([t1/1, t2/1, t3/1, t4/1]).
+
+t1(M = #{}) ->
+    a_is_integer(M),
+    case M of
+	#{a := X} when is_integer(X) -> ok;
+	_ -> fail
+    end.
+
+a_is_integer(#{a := X}) when is_integer(X) -> ok.
+
+t2(M = #{}) ->
+    a_is_integer(M),
+    lists:sort(maps:get(a, M)),
+    ok.
+
+t3(M = #{}) ->
+    lists:sort(maps:get(a, M)),
+    ok.
+
+t4(M) ->
+    lists:sort(maps:get(a, M)),
+    ok.
diff --git a/lib/dialyzer/test/map_SUITE_data/src/typeflow2.erl b/lib/dialyzer/test/map_SUITE_data/src/typeflow2.erl
new file mode 100644
index 0000000000..71a9657a60
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/src/typeflow2.erl
@@ -0,0 +1,88 @@
+-module(typeflow2).
+
+-export([t1/1, t2/1, t3/1, t4/1, t5/1, t6/1, t7/1, optional3/1]).
+
+t1(L) ->
+    M = only_integers_and_lists(L),
+    optional(M),
+    case M of
+	#{a := X} when is_integer(X) -> ok;
+	#{a := X} when is_list(X) -> ok; %% Must warn here
+	#{a := X} when is_pid(X) -> ok;
+	_ -> fail
+    end.
+
+optional(#{a:=X}) ->
+    true = is_integer(X);
+optional(#{}) ->
+    true.
+
+only_integers_and_lists(L) -> only_integers_and_lists(L, #{}).
+
+only_integers_and_lists([], M) -> M;
+only_integers_and_lists([{K,V}|T], M) when is_integer(V); is_list(V)->
+    only_integers_and_lists(T, M#{K => V}).
+
+t2(L) ->
+    M = only_integers_and_lists(L),
+    optional(M),
+    lists:sort(maps:get(a, M)),
+    ok.
+
+t3(L) ->
+    M = only_integers_and_lists(L),
+    lists:sort(maps:get(a, M)),
+    ok.
+
+t4(V) ->
+    M=map_with(a,V),
+    optional2(M),
+    case M of
+	#{a := X} when is_integer(X) -> ok;
+	#{a := X} when is_list(X) -> ok; %% Must warn here
+	_ -> fail
+    end.
+
+optional2(#{a:=X}) ->
+    true = is_integer(X);
+optional2(#{}) ->
+    true.
+
+map_with(K, V) when is_integer(V); is_list(V); is_atom(V) -> #{K => V}.
+
+t5(L) ->
+    M = only_integers_and_lists(L),
+    optional3(M),
+    case M of
+	#{a := X} when is_integer(X) -> ok;
+	#{a := X} when is_list(X) -> ok; %% Must warn here
+	#{a := X} when is_pid(X) -> ok; %% Must warn here
+	#{a := X} when is_atom(X) -> ok;
+	_ -> fail
+    end.
+
+t6(L) ->
+    M = only_integers_and_lists(L),
+    case M of
+	#{a := X} when is_integer(X) -> ok;
+	#{a := X} when is_list(X) -> ok; %% Must not warn here
+	_ -> fail
+    end.
+
+optional3(#{a:=X}) ->
+    true = is_integer(X);
+optional3(#{}) ->
+    true.
+
+t7(M) ->
+    optional4(M),
+    case M of
+	#{a := X} when is_integer(X) -> ok;
+	#{a := X} when is_list(X) -> ok;
+	#{a := X} when is_pid(X) -> ok; %% Must warn here
+	#{a := X} when is_atom(X) -> ok; %% Must warn here
+	_ -> fail %% Must not warn here (requires parsing)
+    end.
+
+-spec optional4(#{a=>integer()|list()}) -> true.
+optional4(#{}) -> true.
diff --git a/lib/dialyzer/test/map_SUITE_data/src/typesig.erl b/lib/dialyzer/test/map_SUITE_data/src/typesig.erl
new file mode 100644
index 0000000000..b50511af41
--- /dev/null
+++ b/lib/dialyzer/test/map_SUITE_data/src/typesig.erl
@@ -0,0 +1,9 @@
+-module(typesig).
+
+-export([t1/0, t2/0, t3/0, test/1]).
+
+t1() -> test(#{a=>1}).
+t2() -> test(#{a=>{b}}).
+t3() -> test(#{a=>{3}}).
+
+test(#{a:={X}}) -> X+1.
diff --git a/lib/dialyzer/test/small_SUITE_data/results/literals b/lib/dialyzer/test/small_SUITE_data/results/literals
index 5d611f520b..883e982134 100644
--- a/lib/dialyzer/test/small_SUITE_data/results/literals
+++ b/lib/dialyzer/test/small_SUITE_data/results/literals
@@ -13,3 +13,4 @@ literals.erl:26: Function m2/1 has no local return
 literals.erl:26: Matching of pattern {'r', 'a'} tagged with a record name violates the declared type of #r{id::'integer'}
 literals.erl:29: Function m3/1 has no local return
 literals.erl:29: The pattern {{'r', 'a'}} can never match the type any()
+literals.erl:32: Function m4/1 has no local return
diff --git a/lib/dialyzer/test/small_SUITE_data/results/maps1 b/lib/dialyzer/test/small_SUITE_data/results/maps1
index 773f037c47..3e076326d2 100644
--- a/lib/dialyzer/test/small_SUITE_data/results/maps1
+++ b/lib/dialyzer/test/small_SUITE_data/results/maps1
@@ -1,8 +1,4 @@
 
-maps1.erl:20: Function recv/3 has no local return
-maps1.erl:25: Function decode/1 has no local return
-maps1.erl:31: Function t1/0 has no local return
-maps1.erl:40: Function update/2 has no local return
 maps1.erl:43: Function t3/0 has no local return
 maps1.erl:46: Function foo/2 has no local return
 maps1.erl:52: The call Mod:'function'(~{'literal'=>'map'}~,'another_arg') requires that Mod is of type atom() not #{}
diff --git a/lib/dialyzer/test/small_SUITE_data/src/literals.erl b/lib/dialyzer/test/small_SUITE_data/src/literals.erl
index 3aefbf1a4e..354a0f4cdc 100644
--- a/lib/dialyzer/test/small_SUITE_data/src/literals.erl
+++ b/lib/dialyzer/test/small_SUITE_data/src/literals.erl
@@ -2,7 +2,7 @@
 
 %% Bad records inside structures used to be ignored. The reason:
 %% v3_core:unfold() does not annotate the parts of a literal.
-%% This example does not work perfectly yet, in particular Maps.
+%% This example does not work perfectly yet.
 
 -export([t1/0, t2/0, t3/0, t4/0, m1/1, m2/1, m3/1, m4/1]).
 
@@ -29,5 +29,5 @@ m2([#r{id = a}]) -> % violation
 m3({#r{id = a}}) -> % can never match; not so good
     ok.
 
-m4(#{a := #r{id = a}}) -> % violation not found
+m4(#{a := #r{id = a}}) -> % violation
     ok.