Merge pull request #524 from xxdavid/fix_map_exhaustiveness

Improve map exhaustiveness checking

src/gradualizer_type.erl

@@ -25,6 +25,7 @@
 %% Export the additional types that gradualizer uses
 -export_type([abstract_pattern/0,
               af_assoc_type/0,
+              af_map_type/0,
               af_atom/0,
               af_binary_op/1,
               af_constrained_function_type/0,

test/known_problems/should_fail/map_refinement_fancy.erl

@@ -1,14 +1,20 @@
 -module(map_refinement_fancy).
 
--export([map_refinement_fancy/1]).
+-export([map_refinement_fancy/1, just_a_bit_less_fancy/1]).
 
-%% Expected exhustiveness error: Values of type #{1 := 3, 2 := 4} not covered.
+%% Expected exhaustiveness error: Values of type #{1 := 3, 2 := 4} not covered.
 %%
-%% Explanation: Currently, during refinement, after clause 1 a type with
-%% overlapping keys #{1..2 := 3, 2 := 3..4} is produced, which prevents
-%% exhaustiveness checking. It almost works. :)
+%% Explanation: exhaustiveness checking is disabled for maps with non-singleton
+%% required (exact assoc) keys.
 -spec map_refinement_fancy(#{1..2 := 3..4}) -> ok.
 map_refinement_fancy(#{1 := 4}) ->
     ok;
 map_refinement_fancy(#{2 := 3}) ->
     ok.
+
+%% Expected exhaustiveness error: Values #{x => a} and #{y => a} not covered.
+%%
+%% Explanation: exhaustiveness checking is disabled for maps with non-singleton
+%% required (exact assoc) keys.
+-spec just_a_bit_less_fancy(#{x|y := a}) -> ok.
+just_a_bit_less_fancy(#{x := a, y := a}) -> ok.

test/known_problems/should_pass/inner_union_subtype_of_root_union.erl

@@ -0,0 +1,22 @@
+-module(inner_union_subtype_of_root_union).
+
+-export([tuple_case/0, map_case/1]).
+
+% The problem is that {t, a|b} is not subtype of {t, a} | {t, b}.
+
+% It has surfaced because
+%     {'type', anno(), 'map_field_assoc' | 'map_field_exact', [abstract_type()]}
+% is not a subtype of
+%     {'type', anno(), 'map_field_assoc', [abstract_type()]}
+%   | {'type', anno(), 'map_field_exact', [abstract_type()]}
+
+-spec g() -> a | b.
+g() -> a.
+
+-spec tuple_case() -> {t, a} | {t, b}.
+tuple_case() ->
+    {t, g()}.
+
+% The same thing holds for maps.
+-spec map_case(#{a => b | c}) -> #{a => b} | #{a => c}.
+map_case(M) -> M.

test/known_problems/should_pass/map_pattern_duplicate_key.erl

@@ -0,0 +1,7 @@
+-module(map_pattern_duplicate_key).
+
+-export([f/1]).
+
+% Fails with: The expression x on line 6 at column 13 is not a valid key in the map type #{x := a}
+-spec f(#{x := a}) -> true.
+f(#{x := a, x := a}) -> true.

test/should_fail/map_refinement_fail.erl

@@ -8,3 +8,56 @@ map_value_type_refinement(#{x := a}) ->
     ok;
 map_value_type_refinement(#{x := b}) ->
     ok.
+
+% Expected error: Nonexhaustive patterns. #{x => a} not covered.
+-spec optional_key(#{x := a, y => b}) -> ok.
+optional_key(#{x := a, y := b}) -> ok.
+
+% Expected error: Nonexhaustive patterns. #{x => b, y => c} not covered.
+-spec multiple_values(#{x := a|b, y := c|d}) -> ok.
+multiple_values(#{x := a, y := c}) -> ok;
+multiple_values(#{x := a, y := d}) -> ok;
+multiple_values(#{x := b, y := d}) -> ok.
+
+%% Expected error: Nonexhaustive patterns. Empty map not covered.
+-spec multiple_keys(#{x|y => a}) -> ok.
+multiple_keys(#{x := a, y := a}) -> ok;
+multiple_keys(#{x := a}) -> ok;
+multiple_keys(#{y := a}) -> ok.
+
+% Expected error: Nonexhaustive patterns. #{x => b} (and others) not covered.
+-spec multiple_keys_and_values(#{x|y => a|b}) -> ok.
+multiple_keys_and_values(#{x := a, y := a}) -> ok;
+multiple_keys_and_values(#{x := a, y := b}) -> ok;
+multiple_keys_and_values(#{x := b, y := a}) -> ok;
+multiple_keys_and_values(#{x := b, y := b}) -> ok;
+multiple_keys_and_values(#{x := a}) -> ok.
+
+%% Expected error: Invalid key. (The pattern #{x => a, y => a) has
+%% already been covered by the first clause.)
+-spec multiple_keys_2(#{x|y => a}) -> ok.
+multiple_keys_2(#{x := a}) -> ok;
+multiple_keys_2(#{y := a}) -> ok;
+multiple_keys_2(#{x := a, y := a}) -> ok.
+
+% Expected error: Nonexhaustive patterns. #{x => 0} not covered.
+-spec infinite_value_type(#{x := integer()}) -> ok.
+infinite_value_type(#{x := 1}) -> ok;
+infinite_value_type(#{x := 2}) -> ok.
+
+% Expected error: Nonexhaustive patterns. #{0 => true} not covered.
+-spec infinite_key_type(#{integer() => true}) -> ok.
+infinite_key_type(#{1 := true}) -> ok;
+infinite_key_type(#{2 := true}) -> ok.
+
+% Expected error: Nonexhaustive patterns. #{x => b} not covered.
+-spec union_of_maps(#{x := a} | #{x := b}) -> ok.
+union_of_maps(#{x := a}) -> ok.
+
+% Expected error: Nonexhaustive patterns. #{y => b} not covered.
+-spec union_of_maps_2(#{x := a} | #{y := b}) -> ok.
+union_of_maps_2(#{x := a}) -> ok.
+
+% Expected error: Nonexhaustive patterns. #{x => b} not covered.
+-spec union_of_maps_3(#{x := a} | #{x := a|b}) -> ok.
+union_of_maps_3(#{x := a}) -> ok.

test/should_pass/map_refinement.erl

@@ -17,3 +17,60 @@ map_value_type_refinement(#{x := b}) ->
     ok;
 map_value_type_refinement(#{}) ->
     ok.
+
+-spec optional_key(#{x := a, y => b}) -> ok.
+optional_key(#{x := a, y := b}) -> ok;
+optional_key(#{x := a}) -> ok.
+
+-spec optional_key_2(#{x := a, y => b}) -> ok.
+optional_key_2(#{x := a}) -> ok.
+
+-spec catch_all_map_pattern(#{x := a|b, y => c|d|e, z := integer()}) -> ok.
+catch_all_map_pattern(#{}) -> ok.
+
+-spec any_map(map()) -> ok.
+any_map(#{x := a}) -> ok;
+any_map(#{y := b}) -> ok.
+
+-spec multiple_values(#{x := a|b, y := c|d}) -> ok.
+multiple_values(#{x := a, y := c}) -> ok;
+multiple_values(#{x := a, y := d}) -> ok;
+multiple_values(#{x := b, y := d}) -> ok;
+multiple_values(#{x := b, y := c}) -> ok.
+
+-spec multiple_keys(#{x|y => a}) -> ok.
+multiple_keys(#{x := a, y := a}) -> ok;
+multiple_keys(#{x := a}) -> ok;
+multiple_keys(#{y := a}) -> ok;
+multiple_keys(#{}) -> ok.
+
+-spec multiple_keys_and_values(#{x|y => a|b}) -> ok.
+multiple_keys_and_values(#{x := a, y := a}) -> ok;
+multiple_keys_and_values(#{x := a, y := b}) -> ok;
+multiple_keys_and_values(#{x := b, y := a}) -> ok;
+multiple_keys_and_values(#{x := b, y := b}) -> ok;
+multiple_keys_and_values(#{x := a}) -> ok;
+multiple_keys_and_values(#{x := b}) -> ok;
+multiple_keys_and_values(#{}) -> ok.
+
+-spec infinite_value_type(#{x := integer()}) -> integer().
+infinite_value_type(#{x := 1}) -> 2;
+infinite_value_type(#{x := 2}) -> 3;
+infinite_value_type(#{x := N}) -> N + 1.
+
+-spec infinite_key_type(#{integer() => true}) -> ok.
+infinite_key_type(#{1 := true}) -> ok;
+infinite_key_type(#{2 := true}) -> ok;
+infinite_key_type(_Map) -> ok.
+
+-spec union_of_maps(#{x := a} | #{x := b}) -> ok.
+union_of_maps(#{x := a}) -> ok;
+union_of_maps(#{x := b}) -> ok.
+
+-spec union_of_maps_2(#{x := a} | #{y := b}) -> ok.
+union_of_maps_2(#{x := a}) -> ok;
+union_of_maps_2(#{y := b}) -> ok.
+
+-spec union_of_maps_3(#{x := a} | #{x := a|b}) -> ok.
+union_of_maps_3(#{x := a}) -> ok;
+union_of_maps_3(#{x := b}) -> ok.

test/typechecker_tests.erl

@@ -10,6 +10,9 @@
 -define(t(T), t(??T)).
 t(T) -> typelib:remove_pos(typelib:parse_type(T)).
 
+%% Macro to convert expression to abstract form
+-define(e(E), merl:quote(??E)).
+
 subtype_test_() ->
     [
      %% The unknown type, both directions
@@ -592,15 +595,184 @@ add_type_pat_test_() ->
       ?_assert(type_check_forms(["f([E|_]) -> E."]))},
      {"Pattern matching record against any()",
       ?_assert(type_check_forms(["-record(r, {f}).",
-                                 "f(#r{f = F}) -> F."]))}
+                                 "f(#r{f = F}) -> F."]))},
+
+      ?_assertEqual(?t(a),                 type_pat(?e(a),                 ?t(a))),
+      ?_assertEqual(?t(a),                 type_pat(?e(Var),               ?t(a))),
+      ?_assertEqual(?t(42),                type_pat(?e(42),                ?t(integer()))),
+      ?_assertEqual(?t(integer()),         type_pat(?e(Var),               ?t(integer()))),
+      ?_assertEqual(?t({3, true}),         type_pat(?e({3, true}),         ?t({integer(), boolean()}))),
+      ?_assertEqual(?t({3, boolean()}),    type_pat(?e({3, _}),            ?t({integer(), boolean()}))),
+
+      ?_assertThrow({type_error, pattern, _, {atom, _, a}, {atom, _, b}},
+                                           type_pat(?e(a),                 ?t(b))),
+
+      %% Maps
+      ?_assertEqual(?t(#{}),               type_pat(?e(#{}),               ?t(#{}))),
+      ?_assertEqual(?t(#{x := a}),         type_pat(?e(#{x := a}),         ?t(#{x := a}))),
+      ?_assertEqual(?t(#{x := a}),         type_pat(?e(Var),               ?t(#{x := a}))),
+      ?_assertEqual(?t(#{x := a}),         type_pat(?e(#{}),               ?t(#{x := a}))),
+
+      ?_assertEqual(?t(#{x := a, y := b}), type_pat(?e(#{}),               ?t(#{x := a, y := b}))),
+      ?_assertEqual(?t(#{x := a, y := b}), type_pat(?e(#{x := a}),         ?t(#{x := a, y := b}))),
+      ?_assertEqual(?t(#{x := a, y := b}), type_pat(?e(#{x := a, y := b}), ?t(#{x := a, y := b}))),
+
+      ?_assertEqual(?t(#{x := a}),         type_pat(?e(#{x := a}),         ?t(#{x => a}))),
+      ?_assertEqual(?t(#{x => a}),         type_pat(?e(Var),               ?t(#{x => a}))),
+      ?_assertEqual(?t(#{x => a}),         type_pat(?e(#{}),               ?t(#{x => a}))),
+
+      ?_assertEqual(?t(#{x := a}),         type_pat(?e(#{x := a}),         ?t(#{x := a|b}))),
+      ?_assertEqual(?t(#{x := a}),         type_pat(?e(#{x := a}),         ?t(#{x => a|b}))),
+      ?_assertEqual(?t(#{x := 1}),         type_pat(?e(#{x := 1}),         ?t(#{x => 1..3}))),
+
+      ?_assertEqual(?t(#{x => a, y := b}), type_pat(?e(#{}),               ?t(#{x => a, y := b}))),
+      ?_assertEqual(?t(#{x := a, y := b}), type_pat(?e(#{x := a}),         ?t(#{x => a, y := b}))),
+      ?_assertEqual(?t(#{y := b, x => a}), type_pat(?e(#{y := b}),         ?t(#{x => a, y := b}))),
+
+      ?_assertEqual(?t(#{x := 42}),        type_pat(?e(#{x := 42}),        ?t(#{x := integer()}))),
+      ?_assertEqual(?t(#{x := integer()}), type_pat(?e(#{x := Var}),       ?t(#{x := integer()}))),
+
+      ?_assertEqual(?t(#{y := b, x => a}), type_pat(?e(#{y := b}),         ?t(#{x => a, y => b} | #{z := c}))),
+      ?_assertEqual(?t(#{y := b, x => a}), type_pat(?e(#{y := b}),         ?t(#{x => a, y => b} | #{y := c, z := c}))),
+      ?_assertEqual(?t(#{y := b, x => a} | #{y := b, z := c}),
+                                           type_pat(?e(#{y := b}),         ?t(#{x => a, y => b} | #{y := b, z := c}))),
+
+      ?_assertEqual(?t(none()),            type_pat(?e(#{x := a}),         ?t(any()))),
+      ?_assertEqual(?t(none()),            type_pat(?e(#{}),               ?t(any()))),
+
+      ?_assertEqual(?t(#{x := a, y => a}), type_pat(?e(#{x := a}),         ?t(#{x|y := a}))),
+      ?_assertEqual(?t(#{x := a, y => a}), type_pat(?e(#{x := a}),         ?t(#{x|y => a}))),
+      ?_assertEqual(?t(#{x := a, atom() => a}),
+                                           type_pat(?e(#{x := a}),         ?t(#{atom() := a}))),
+      ?_assertEqual(?t(#{x := a, atom() => a}),
+                                           type_pat(?e(#{x := a}),         ?t(#{atom() => a}))),
+      ?_assertEqual(?t(#{x := a, y => a|b}),
+                                           type_pat(?e(#{x := a}),         ?t(#{x|y := a|b}))),
+      ?_assertEqual(?t(#{x := a, y => a|b, z => c}),
+                                           type_pat(?e(#{x := a}),         ?t(#{x|y := a|b, z => c}))),
+
+      ?_assertEqual(?t(#{x := a, y := a, atom() => a}),
+                                           type_pat(?e(#{x := a, y := a}), ?t(#{atom() => a}))),
+      ?_assertEqual(?t(#{x := a, y := a}),
+                                           type_pat(?e(#{x := a, y := a}), ?t(#{x|y => a}))),
+      ?_assertEqual(?t(#{x := a, y := a, atom() => a}),
+                                           type_pat(?e(#{x := a, y := a}), ?t(#{x|y => a, atom() => a}))),
+
+      ?_assertEqual(?t(none()),            type_pat(?e(#{"abc" := abc}),    ?t(#{string() => atom()}))),
+
+      ?_assertThrow({type_error, pattern, _, {atom, _, b}, {atom, _, a}},
+                                           type_pat(?e(#{x := b}),         ?t(#{x := a}))),
+      ?_assertThrow({type_error, badkey, {atom, _, y}, _MapTy},
+                                           type_pat(?e(#{y := c}),         ?t(#{x := a})))
     ].
 
 type_diff_test_() ->
+    {setup,
+      fun setup_app/0,
+      fun cleanup_app/1,
+
     [{"Can refine a union with another union",
       ?_assertEqual(?t( a1 | b | b1 | c | c1 | d ),
                     typechecker:type_diff(?t( (a | a1) | (b | b1) | (c | c1) | (d | d1) ),
-                                          ?t( a | d1), gradualizer:env()))}
-    ].
+                                          ?t( a | d1), gradualizer:env()))},
+
+      ?_assertEqual(?t(none()),
+                    typechecker:type_diff(?t(#{x := integer()}),
+                                          ?t(#{x := integer()}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{}),
+                    typechecker:type_diff(?t(#{x => integer()}),
+                                          ?t(#{x := integer()}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(none()),
+                    typechecker:type_diff(?t(#{x => integer()}),
+                                          ?t(#{x => integer()}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{x := b}),
+                    typechecker:type_diff(?t(#{x := a|b}),
+                                          ?t(#{x := a}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{x => b}),
+                    typechecker:type_diff(?t(#{x => a|b}),
+                                          ?t(#{x := a}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{x := 2..3}),
+                    typechecker:type_diff(?t(#{x := 1..3}),
+                                          ?t(#{x := 1}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(none()),
+                    typechecker:type_diff(?t(#{x := a, y := b}),
+                                          ?t(#{x := a, y := b}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(none()),
+                    typechecker:type_diff(?t(#{x := a, y := b}),
+                                          ?t(#{y := b, x := a}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{x := b, y := c}),
+                    typechecker:type_diff(?t(#{x := a|b, y := c}),
+                                          ?t(#{x := a, y := c}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{x := b, y => c} | #{x := a|b}),
+                    typechecker:type_diff(?t(#{x := a|b, y => c}),
+                                          ?t(#{x := a, y := c}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{x := b, y => c|d} | #{x := a|b, y => d}),
+                    typechecker:type_diff(?t(#{x := a|b, y => c|d}),
+                                          ?t(#{x := a, y := c}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{x => b, y := c}),
+                    typechecker:type_diff(?t(#{x => a|b, y := c}),
+                                          ?t(#{x := a, y := c}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{y => b}),
+                    typechecker:type_diff(?t(#{x => a, y => b}),
+                                          ?t(#{x := a, y => b}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{y => a}),
+                    typechecker:type_diff(?t(#{x|y => a}),
+                                          ?t(#{x := a, y => a}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(none()),
+                    typechecker:type_diff(?t(#{x|y => a}),
+                                          ?t(#{x => a, y => a}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{x => a|b, y => b} | #{x => b, y => a|b}),
+                    typechecker:type_diff(?t(#{x|y => a|b}),
+                                          ?t(#{x := a, y := a}),
+                                          gradualizer:env())),
+
+      ?_assertEqual(?t(#{y := b}),
+                    typechecker:type_diff(?t(#{x := atom()} | #{y := b}),
+                                          ?t(#{x := atom()}),
+                                          gradualizer:env())),
+
+      % disjoint
+      ?_assertEqual(?t(#{x := a}),
+                    typechecker:type_diff(?t(#{x := a}),
+                                          ?t(#{y := a}),
+                                          gradualizer:env())),
+
+      % has non-singleton required key
+      ?_assertEqual(?t(#{x|y := a}),
+                    typechecker:type_diff(?t(#{x|y := a}),
+                                          ?t(#{x := a}),
+                                          gradualizer:env()))
+    ]}.
 
 %%
 %% Helper functions
@@ -652,3 +824,8 @@ type_check_expr(EnvStr, ExprString, Opts) ->
     Expr = merl:quote(ExprString),
     {Ty, _VarBinds, _Cs} = typechecker:type_check_expr(Env, Expr),
     typelib:pp_type(Ty).
+
+type_pat(Pat, Ty) ->
+    {[PatTy], _UBounds, _Env, _Css} =
+        typechecker:add_types_pats([Pat], [Ty], gradualizer:env(), capture_vars),
+        PatTy.