7 files changed, 496 insertions, 48 deletions
diff --git a/lib/dialyzer/src/dialyzer.erl b/lib/dialyzer/src/dialyzer.erl
index 9f51dfe356..bcac8afe64 100644
--- a/lib/dialyzer/src/dialyzer.erl
+++ b/lib/dialyzer/src/dialyzer.erl
@@ -336,6 +336,9 @@ message_to_string({guard_fail, []}) ->
   "Clause guard cannot succeed.\n";
 message_to_string({guard_fail, [Arg1, Infix, Arg2]}) ->
   io_lib:format("Guard test ~s ~s ~s can never succeed\n", [Arg1, Infix, Arg2]);
+message_to_string({map_update, [Type, Key]}) ->
+  io_lib:format("A key of type ~s cannot exist "
+		"in a map of type ~s\n", [Key, Type]);
 message_to_string({neg_guard_fail, [Arg1, Infix, Arg2]}) ->
   io_lib:format("Guard test not(~s ~s ~s) can never succeed\n",
 		[Arg1, Infix, Arg2]);
diff --git a/lib/dialyzer/src/dialyzer.hrl b/lib/dialyzer/src/dialyzer.hrl
index 601e2e954b..ea6a71217c 100644
--- a/lib/dialyzer/src/dialyzer.hrl
+++ b/lib/dialyzer/src/dialyzer.hrl
@@ -60,6 +60,7 @@
 -define(WARN_BEHAVIOUR, warn_behaviour).
 -define(WARN_UNDEFINED_CALLBACK, warn_undefined_callbacks).
 -define(WARN_UNKNOWN, warn_unknown).
+-define(WARN_MAP_CONSTRUCTION, warn_map_construction).
 
 %%
 %% The following type has double role:
@@ -75,7 +76,8 @@
                        | ?WARN_CONTRACT_SUPERTYPE | ?WARN_CALLGRAPH
                        | ?WARN_UNMATCHED_RETURN | ?WARN_RACE_CONDITION
                        | ?WARN_BEHAVIOUR | ?WARN_CONTRACT_RANGE
-		       | ?WARN_UNDEFINED_CALLBACK | ?WARN_UNKNOWN.
+		       | ?WARN_UNDEFINED_CALLBACK | ?WARN_UNKNOWN
+		       | ?WARN_MAP_CONSTRUCTION.
 
 %%
 %% This is the representation of each warning as they will be returned
diff --git a/lib/dialyzer/src/dialyzer_contracts.erl b/lib/dialyzer/src/dialyzer_contracts.erl
index e03e4d5bb4..1895a98e96 100644
--- a/lib/dialyzer/src/dialyzer_contracts.erl
+++ b/lib/dialyzer/src/dialyzer_contracts.erl
@@ -277,28 +277,45 @@ check_extraneous_1(Contract, SuccType) ->
   case [CR || CR <- CRngs,
               erl_types:t_is_none(erl_types:t_inf(CR, STRng))] of
     [] ->
-      CRngList = list_part(CRng),
-      STRngList = list_part(STRng),
-      case is_not_nil_list(CRngList) andalso is_not_nil_list(STRngList) of
-        false -> ok;
-        true ->
-          CRngElements = erl_types:t_list_elements(CRngList),
-          STRngElements = erl_types:t_list_elements(STRngList),
-          Inf = erl_types:t_inf(CRngElements, STRngElements),
-          case erl_types:t_is_none(Inf) of
-            true -> {error, invalid_contract};
-            false -> ok
-          end
+      case bad_extraneous_list(CRng, STRng)
+	orelse bad_extraneous_map(CRng, STRng)
+      of
+	true -> {error, invalid_contract};
+	false -> ok
       end;
     CRs -> {error, {extra_range, erl_types:t_sup(CRs), STRng}}
   end.
 
+bad_extraneous_list(CRng, STRng) ->
+  CRngList = list_part(CRng),
+  STRngList = list_part(STRng),
+  case is_not_nil_list(CRngList) andalso is_not_nil_list(STRngList) of
+    false -> false;
+    true ->
+      CRngElements = erl_types:t_list_elements(CRngList),
+      STRngElements = erl_types:t_list_elements(STRngList),
+      Inf = erl_types:t_inf(CRngElements, STRngElements),
+      erl_types:t_is_none(Inf)
+  end.
+
 list_part(Type) ->
   erl_types:t_inf(erl_types:t_list(), Type).
 
 is_not_nil_list(Type) ->
   erl_types:t_is_list(Type) andalso not erl_types:t_is_nil(Type).
 
+bad_extraneous_map(CRng, STRng) ->
+  CRngMap = map_part(CRng),
+  STRngMap = map_part(STRng),
+  (not is_empty_map(CRngMap)) andalso (not is_empty_map(STRngMap))
+    andalso is_empty_map(erl_types:t_inf(CRngMap, STRngMap)).
+
+map_part(Type) ->
+  erl_types:t_inf(erl_types:t_map(), Type).
+
+is_empty_map(Type) ->
+  erl_types:t_is_equal(Type, erl_types:t_from_term(#{})).
+
 %% This is the heart of the "range function"
 -spec process_contracts([contract_pair()], [erl_types:erl_type()]) ->
                            erl_types:erl_type().
diff --git a/lib/dialyzer/src/dialyzer_dataflow.erl b/lib/dialyzer/src/dialyzer_dataflow.erl
index 6e49043551..f0fa9fbb4e 100644
--- a/lib/dialyzer/src/dialyzer_dataflow.erl
+++ b/lib/dialyzer/src/dialyzer_dataflow.erl
@@ -72,7 +72,7 @@
 	 t_tuple/0, t_tuple/1, t_tuple_args/1, t_tuple_args/2,
          t_tuple_subtypes/2,
 	 t_unit/0, t_unopaque/2,
-	 t_map/1
+	 t_map/0, t_map/1, t_is_singleton/2
      ]).
 
 %%-define(DEBUG, true).
@@ -342,8 +342,6 @@ traverse(Tree, Map, State) ->
       handle_tuple(Tree, Map, State);
     map ->
       handle_map(Tree, Map, State);
-    map_pair ->
-      handle_map_pair(Tree, Map, State);
     values ->
       Elements = cerl:values_es(Tree),
       {State1, Map1, EsType} = traverse_list(Elements, Map, State),
@@ -1102,15 +1100,54 @@ handle_try(Tree, Map, State) ->
 %%----------------------------------------
 
 handle_map(Tree,Map,State) ->
-    Pairs = cerl:map_es(Tree),
-    {State1, Map1, TypePairs} = traverse_list(Pairs,Map,State),
-    {State1, Map1, t_map(TypePairs)}.
+  Pairs = cerl:map_es(Tree),
+  Arg = cerl:map_arg(Tree),
+  {State1, Map1, ArgType} = traverse(Arg, Map, State),
+  ArgType1 = t_inf(t_map(), ArgType),
+  case t_is_none_or_unit(ArgType1) of
+    true ->
+      {State1, Map1, ArgType1};
+    false ->
+      {State2, Map2, TypePairs, ExactKeys} =
+	traverse_map_pairs(Pairs, Map1, State1, t_none(), [], []),
+      InsertPair = fun({KV,assoc,_},Acc) -> erl_types:t_map_put(KV,Acc);
+		      ({KV,exact,KVTree},Acc) ->
+		       case t_is_none(T=erl_types:t_map_update(KV,Acc)) of
+			 true -> throw({none, Acc, KV, KVTree});
+			 false -> T
+		       end
+		   end,
+      try lists:foldl(InsertPair, ArgType1, TypePairs)
+      of ResT ->
+	  BindT = t_map([{K, t_any()} || K <- ExactKeys]),
+	  case bind_pat_vars_reverse([Arg], [BindT], [], Map2, State2) of
+	    {error, _, _, _, _} -> {State2, Map2, ResT};
+	    {Map3, _} ->           {State2, Map3, ResT}
+	  end
+      catch {none, MapType, {K,_}, KVTree} ->
+	  Msg2 = {map_update, [format_type(MapType, State2),
+			       format_type(K, State2)]},
+	  {state__add_warning(State2, ?WARN_MAP_CONSTRUCTION, KVTree, Msg2),
+	   Map2, t_none()}
+      end
+  end.
 
-handle_map_pair(Tree,Map,State) ->
-  Key = cerl:map_pair_key(Tree),
-  Val = cerl:map_pair_val(Tree),
+traverse_map_pairs([], Map, State, _ShadowKeys, PairAcc, KeyAcc) ->
+  {State, Map, lists:reverse(PairAcc), KeyAcc};
+traverse_map_pairs([Pair|Pairs], Map, State, ShadowKeys, PairAcc, KeyAcc) ->
+  Key = cerl:map_pair_key(Pair),
+  Val = cerl:map_pair_val(Pair),
+  Op = cerl:map_pair_op(Pair),
   {State1, Map1, [K,V]} = traverse_list([Key,Val],Map,State),
-  {State1, Map1, {K,V}}.
+  KeyAcc1 =
+    case cerl:is_literal(Op) andalso cerl:concrete(Op) =:= exact andalso
+      t_is_singleton(K, State#state.opaques) andalso
+      t_is_none(t_inf(ShadowKeys, K)) of
+      true -> [K|KeyAcc];
+      false -> KeyAcc
+  end,
+  traverse_map_pairs(Pairs, Map1, State1, t_sup(K, ShadowKeys),
+		     [{{K,V},cerl:concrete(Op),Pair}|PairAcc], KeyAcc1).
 
 %%----------------------------------------
 
@@ -1445,7 +1482,9 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
   {NewMap, TypeOut} =
     case cerl:type(Pat) of
       alias ->
-	AliasPat = cerl:alias_pat(Pat),
+	%% Map patterns are more allowing than the type of their literal. We
+	%% must unfold AliasPat if it is a literal.
+	AliasPat = dialyzer_utils:refold_pattern(cerl:alias_pat(Pat)),
 	Var = cerl:alias_var(Pat),
 	Map1 = enter_subst(Var, AliasPat, Map),
 	{Map2, [PatType]} = bind_pat_vars([AliasPat], [Type], [],
@@ -1486,14 +1525,59 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	    {Map1, t_cons(HdType, TlType)}
 	end;
       literal ->
-	Literal = literal_type(Pat),
-	case t_is_none(t_inf(Literal, Type, Opaques)) of
+	Pat0 = dialyzer_utils:refold_pattern(Pat),
+	case cerl:is_literal(Pat0) of
 	  true ->
-	    bind_opaque_pats(Literal, Type, Pat, State);
-	  false -> {Map, Literal}
+	    Literal = literal_type(Pat),
+	    case t_is_none(t_inf(Literal, Type, Opaques)) of
+	      true ->
+		bind_opaque_pats(Literal, Type, Pat, State);
+	      false -> {Map, Literal}
+	    end;
+	  false ->
+	    %% Retry with the unfolded pattern
+	    {Map1, [PatType]}
+	      = bind_pat_vars([Pat0], [Type], [], Map, State, Rev),
+	    {Map1, PatType}
 	end;
       map ->
-	  {Map, t_map([])};
+	MapT = t_inf(Type, t_map(), Opaques),
+	case t_is_none(MapT) of
+	  true ->
+	    bind_opaque_pats(t_map(), Type, Pat, State);
+	  false ->
+	    case Rev of
+	      %% TODO: Reverse matching (propagating a matched subset back to a value)
+	      true -> {Map, MapT};
+	      false ->
+		FoldFun =
+		  fun(Pair, {MapAcc, ListAcc}) ->
+		      %% Only exact (:=) can appear in patterns
+		      exact = cerl:concrete(cerl:map_pair_op(Pair)),
+		      Key = cerl:map_pair_key(Pair),
+		      KeyType =
+			case cerl:type(Key) of
+			  var ->
+			    case state__lookup_type_for_letrec(Key, State) of
+			      error -> lookup_type(Key, MapAcc);
+			      {ok, RecType} -> RecType
+			    end;
+			  literal ->
+			    literal_type(Key)
+			end,
+		      Bind = erl_types:t_map_get(KeyType, MapT),
+		      {MapAcc1, [ValType]} =
+			bind_pat_vars([cerl:map_pair_val(Pair)],
+				      [Bind], [], MapAcc, State, Rev),
+		      case t_is_singleton(KeyType, Opaques) of
+			true  -> {MapAcc1, [{KeyType, ValType}|ListAcc]};
+			false -> {MapAcc1, ListAcc}
+		      end
+		  end,
+		{Map1, Pairs} = lists:foldl(FoldFun, {Map, []}, cerl:map_es(Pat)),
+		{Map1, t_inf(MapT, t_map(Pairs))}
+	    end
+	end;
       tuple ->
 	Es = cerl:tuple_es(Pat),
 	{TypedRecord, Prototype} =
@@ -1710,15 +1794,58 @@ bind_guard(Guard, Map, Env, Eval, State) ->
     'try' ->
       Arg = cerl:try_arg(Guard),
       [Var] = cerl:try_vars(Guard),
+      EVars = cerl:try_evars(Guard),
       %%?debug("Storing: ~w\n", [Var]),
-      NewEnv = dict:store(get_label(Var), Arg, Env),
-      bind_guard(cerl:try_body(Guard), Map, NewEnv, Eval, State);
+      Map1 = join_maps_begin(Map),
+      Map2 = mark_as_fresh(EVars, Map1),
+      %% Visit handler first so we know if it should be ignored
+      {{HandlerMap, HandlerType}, HandlerE} =
+	try {bind_guard(cerl:try_handler(Guard), Map2, Env, Eval, State), none}
+	catch throw:HE ->
+	    {{Map2, t_none()}, HE}
+	end,
+      BodyEnv = dict:store(get_label(Var), Arg, Env),
+      Wanted = case Eval of pos -> t_atom(true); neg -> t_atom(false);
+		 dont_know -> t_any() end,
+      case t_is_none(t_inf(HandlerType, Wanted)) of
+	%% Handler won't save us; pretend it does not exist
+	true -> bind_guard(cerl:try_body(Guard), Map, BodyEnv, Eval, State);
+	false ->
+	  {{BodyMap, BodyType}, BodyE} =
+	    try {bind_guard(cerl:try_body(Guard), Map1, BodyEnv,
+			    Eval, State), none}
+	    catch throw:BE ->
+		{{Map1, t_none()}, BE}
+	    end,
+	  Map3 = join_maps_end([BodyMap, HandlerMap], Map1),
+	  case t_is_none(Sup = t_sup(BodyType, HandlerType)) of
+	    true ->
+	      %% Pick a reason. N.B. We assume that the handler is always
+	      %% compiler-generated if the body is; that way, we won't need to
+	      %% check.
+	      Fatality = case {BodyE, HandlerE} of
+			   {{fatal_fail, _}, _} -> fatal_fail;
+			   {_, {fatal_fail, _}} -> fatal_fail;
+			   _ -> fail
+			 end,
+	      throw({Fatality,
+		     case {BodyE, HandlerE} of
+		       {{_, Rsn}, _} when Rsn =/= none -> Rsn;
+		       {_, {_,Rsn}} -> Rsn;
+		       _ -> none
+		     end});
+	    false -> {Map3, Sup}
+	  end
+      end;
     tuple ->
       Es0 = cerl:tuple_es(Guard),
       {Map1, Es} = bind_guard_list(Es0, Map, Env, dont_know, State),
       {Map1, t_tuple(Es)};
     map ->
-      {Map, t_map([])};
+      case Eval of
+	dont_know -> handle_guard_map(Guard, Map, Env, State);
+	_PosOrNeg -> {Map, t_none()}  %% Map exprs do not produce bools
+      end;
     'let' ->
       Arg = cerl:let_arg(Guard),
       [Var] = cerl:let_vars(Guard),
@@ -1761,7 +1888,7 @@ handle_guard_call(Guard, Map, Env, Eval, State) ->
     {erlang, F, 1} when F =:= is_atom; F =:= is_boolean;
 			F =:= is_binary; F =:= is_bitstring;
 			F =:= is_float; F =:= is_function;
-			F =:= is_integer; F =:= is_list;
+			F =:= is_integer; F =:= is_list; F =:= is_map;
 			F =:= is_number; F =:= is_pid; F =:= is_port;
 			F =:= is_reference; F =:= is_tuple ->
       handle_guard_type_test(Guard, F, Map, Env, Eval, State);
@@ -1841,6 +1968,7 @@ bind_type_test(Eval, TypeTest, ArgType, State) ->
 	   is_function -> t_fun();
 	   is_integer -> t_integer();
 	   is_list -> t_maybe_improper_list();
+	   is_map -> t_map();
 	   is_number -> t_number();
 	   is_pid -> t_pid();
 	   is_port -> t_port();
@@ -2349,6 +2477,30 @@ bind_guard_list([G|Gs], Map, Env, Eval, State, Acc) ->
 bind_guard_list([], Map, _Env, _Eval, _State, Acc) ->
   {Map, lists:reverse(Acc)}.
 
+handle_guard_map(Guard, Map, Env, State) ->
+  Pairs = cerl:map_es(Guard),
+  Arg = cerl:map_arg(Guard),
+  {Map1, ArgType0} = bind_guard(Arg, Map, Env, dont_know, State),
+  ArgType1 = t_inf(t_map(), ArgType0),
+  case t_is_none_or_unit(ArgType1) of
+    true -> {Map1, t_none()};
+    false ->
+      {Map2, TypePairs} = bind_guard_map_pairs(Pairs, Map1, Env, State, []),
+      {Map2, lists:foldl(fun({KV,assoc},Acc) -> erl_types:t_map_put(KV,Acc);
+			    ({KV,exact},Acc) -> erl_types:t_map_update(KV,Acc)
+			 end, ArgType1, TypePairs)}
+  end.
+
+bind_guard_map_pairs([], Map, _Env, _State, PairAcc) ->
+  {Map, lists:reverse(PairAcc)};
+bind_guard_map_pairs([Pair|Pairs], Map, Env, State, PairAcc) ->
+  Key = cerl:map_pair_key(Pair),
+  Val = cerl:map_pair_val(Pair),
+  Op = cerl:map_pair_op(Pair),
+  {Map1, [K,V]} = bind_guard_list([Key,Val],Map,Env,dont_know,State),
+  bind_guard_map_pairs(Pairs, Map1, Env, State,
+		       [{{K,V},cerl:concrete(Op)}|PairAcc]).
+
 -type eval() :: 'pos' | 'neg' | 'dont_know'.
 
 -spec signal_guard_fail(eval(), cerl:c_call(), [type()],
@@ -2421,7 +2573,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;
@@ -2639,8 +2793,9 @@ store_map(Key, Val, #map{dict = Dict, ref = undefined} = Map) ->
 store_map(Key, Val, #map{dict = Dict, modified = Mod} = Map) ->
   Map#map{dict = dict:store(Key, Val, Dict), modified = [Key | Mod]}.
 
-enter_subst(Key, Val, #map{subst = Subst} = MS) ->
+enter_subst(Key, Val0, #map{subst = Subst} = MS) ->
   KeyLabel = get_label(Key),
+  Val = dialyzer_utils:refold_pattern(Val0),
   case cerl:is_literal(Val) of
     true ->
       store_map(KeyLabel, literal_type(Val), MS);
@@ -2703,6 +2858,9 @@ mark_as_fresh([Tree|Left], Map) ->
       bitstr ->
 	%% The Size field is not fresh.
 	{SubTrees1 -- [cerl:bitstr_size(Tree)], Map};
+      map_pair ->
+	%% The keys are not fresh
+	{SubTrees1 -- [cerl:map_pair_key(Tree)], Map};
       var ->
 	{SubTrees1, enter_type(Tree, t_any(), Map)};
       _ ->
diff --git a/lib/dialyzer/src/dialyzer_options.erl b/lib/dialyzer/src/dialyzer_options.erl
index dd81dd01ed..add660eae9 100644
--- a/lib/dialyzer/src/dialyzer_options.erl
+++ b/lib/dialyzer/src/dialyzer_options.erl
@@ -47,6 +47,7 @@ build(Opts) ->
 		  ?WARN_CALLGRAPH,
 		  ?WARN_FAILING_CALL,
 		  ?WARN_BIN_CONSTRUCTION,
+		  ?WARN_MAP_CONSTRUCTION,
 		  ?WARN_CONTRACT_RANGE,
 		  ?WARN_CONTRACT_TYPES,
 		  ?WARN_CONTRACT_SYNTAX,
diff --git a/lib/dialyzer/src/dialyzer_typesig.erl b/lib/dialyzer/src/dialyzer_typesig.erl
index 5f0881bbcd..50fcbc555b 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").
@@ -126,6 +127,8 @@
                 solvers     = []                :: [solver()]
 	       }).
 
+-type state() :: #state{}.
+
 %%-----------------------------------------------------------------------------
 
 -define(TYPE_LIMIT, 4).
@@ -311,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)};
@@ -392,8 +395,18 @@ traverse(Tree, DefinedVars, State) ->
       {State2, _} = traverse_list(Funs, DefinedVars1, State1),
       traverse(Body, DefinedVars1, State2);
     literal ->
-      Type = t_from_term(cerl:concrete(Tree)),
-      {State, Type};
+      %% Maps are special; a literal pattern matches more than just the value
+      %% constructed by the literal. For example #{} constructs the empty map,
+      %% but matches every map.
+      case state__is_in_match(State) of
+	true ->
+	  Tree1 = dialyzer_utils:refold_pattern(Tree),
+	  case cerl:is_literal(Tree1) of
+	    false -> traverse(Tree1, DefinedVars, State);
+	    true -> {State, t_from_term(cerl:concrete(Tree))}
+	  end;
+	_ -> {State, t_from_term(cerl:concrete(Tree))}
+      end;
     module ->
       Defs = cerl:module_defs(Tree),
       Funs = [Fun || {_Var, Fun} <- Defs],
@@ -437,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)};
@@ -476,7 +489,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 +1065,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()};
@@ -1004,7 +1122,9 @@ bitstr_val_constr(SizeType, UnitVal, Flags) ->
       end
   end.
 
-get_safe_underapprox_1([Pat|Left], Acc, Map) ->
+get_safe_underapprox_1([Pat0|Left], Acc, Map) ->
+  %% Maps should be treated as patterns, not as literals
+  Pat = dialyzer_utils:refold_pattern(Pat0),
   case cerl:type(Pat) of
     alias ->
       APat = cerl:alias_pat(Pat),
@@ -1048,8 +1168,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 +1211,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 +1419,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) ->
@@ -1900,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},
@@ -2975,13 +3133,24 @@ mk_constraint_ref(Id, Deps) ->
 
 mk_constraint_list(Type, List) ->
   List1 = ordsets:from_list(lift_lists(Type, List)),
-  List2 = ordsets:filter(fun(X) -> get_deps(X) =/= [] end, List1),
-  Deps = calculate_deps(List2),
+  case Type of
+    conj ->
+      List2 = ordsets:filter(fun(X) -> get_deps(X) =/= [] end, List1),
+      mk_constraint_list_cont(Type, List2);
+    disj ->
+      case lists:any(fun(X) -> get_deps(X) =:= [] end, List1) of
+	true -> mk_constraint_list_cont(Type, [mk_constraint_any(eq)]);
+	false -> mk_constraint_list_cont(Type, List1)
+      end
+  end.
+
+mk_constraint_list_cont(Type, List) ->
+  Deps = calculate_deps(List),
   case Deps =:= [] of
     true -> #constraint_list{type = conj,
 			     list = [mk_constraint_any(eq)],
 			     deps = []};
-    false -> #constraint_list{type = Type, list = List2, deps = Deps}
+    false -> #constraint_list{type = Type, list = List, deps = Deps}
   end.
 
 lift_lists(Type, List) ->
@@ -3263,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:cerl(), state()) -> cerl:cerl().
+
+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 5fc1c0e691..d37701f03b 100644
--- a/lib/dialyzer/src/dialyzer_utils.erl
+++ b/lib/dialyzer/src/dialyzer_utils.erl
@@ -49,6 +49,7 @@
 	 process_record_remote_types/1,
          sets_filter/2,
 	 src_compiler_opts/0,
+	 refold_pattern/1,
 	 parallelism/0,
          family/1
 	]).
@@ -752,6 +753,13 @@ pp_hook(Node, Ctxt, Cont) ->
       pp_binary(Node, Ctxt, Cont);
     bitstr ->
       pp_segment(Node, Ctxt, Cont);
+    map ->
+      pp_map(Node, Ctxt, Cont);
+    literal ->
+      case is_map(cerl:concrete(Node)) of
+	true -> pp_map(Node, Ctxt, Cont);
+	false -> Cont(Node, Ctxt)
+      end;
     _ ->
       Cont(Node, Ctxt)
   end.
@@ -832,6 +840,87 @@ pp_atom(Atom) ->
   String = atom_to_list(cerl:atom_val(Atom)),
   prettypr:text(String).
 
+pp_map(Node, Ctxt, Cont) ->
+  Arg = cerl:map_arg(Node),
+  Before = case cerl:is_c_map_empty(Arg) of
+	     true -> prettypr:floating(prettypr:text("#{"));
+	     false ->
+	       prettypr:beside(Cont(Arg,Ctxt),
+			       prettypr:floating(prettypr:text("#{")))
+	   end,
+  prettypr:beside(
+    Before, prettypr:beside(
+	      prettypr:par(seq(cerl:map_es(Node),
+			       prettypr:floating(prettypr:text(",")),
+			       Ctxt, Cont)),
+	      prettypr:floating(prettypr:text("}")))).
+
+seq([H | T], Separator, Ctxt, Fun) ->
+  case T of
+    [] -> [Fun(H, Ctxt)];
+    _  -> [prettypr:beside(Fun(H, Ctxt), Separator)
+	   | seq(T, Separator, Ctxt, Fun)]
+  end;
+seq([], _, _, _) ->
+  [prettypr:empty()].
+
+%%------------------------------------------------------------------------------
+
+-spec refold_pattern(cerl:cerl()) -> cerl:cerl().
+
+refold_pattern(Pat) ->
+  %% Avoid the churn of unfolding and refolding
+  case cerl:is_literal(Pat) andalso find_map(cerl:concrete(Pat)) of
+    true ->
+      Tree = refold_concrete_pat(cerl:concrete(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.
+
+find_map(#{}) -> true;
+find_map(Tuple) when is_tuple(Tuple) -> find_map(tuple_to_list(Tuple));
+find_map([H|T]) -> find_map(H) orelse find_map(T);
+find_map(_) -> false.
+
+refold_concrete_pat(Val) ->
+  case Val of
+    _ when is_tuple(Val) ->
+      Els = lists:map(fun refold_concrete_pat/1, tuple_to_list(Val)),
+      case lists:all(fun cerl:is_literal/1, Els) of
+	true -> cerl:abstract(Val);
+	false -> label(cerl:c_tuple_skel(Els))
+      end;
+    [H|T] ->
+      case  cerl:is_literal(HP=refold_concrete_pat(H))
+	and cerl:is_literal(TP=refold_concrete_pat(T))
+      of
+	true -> cerl:abstract(Val);
+	false -> label(cerl:c_cons_skel(HP, TP))
+      end;
+    M when is_map(M) ->
+      %% Map patterns are not generated by the parser(!), but they have a
+      %% property we want, namely that they are never folded into literals.
+      %% N.B.: The key in a map pattern is an expression, *not* a pattern.
+      label(cerl:c_map_pattern([cerl:c_map_pair_exact(cerl:abstract(K),
+						      refold_concrete_pat(V))
+				|| {K, V} <- maps:to_list(M)]));
+    _ ->
+      cerl:abstract(Val)
+  end.
+
+label(Tree) ->
+      %% Sigh
+      Label = -erlang:unique_integer([positive]),
+      cerl:set_ann(Tree, [{label, Label}]).
+
 %%------------------------------------------------------------------------------
 
 -spec parallelism() -> integer().