Non-trivial sum type exhaustiveness checking

Makefile

@@ -132,7 +132,7 @@ test/arg.beam: test/should_fail/arg.erl
 test_data_erls = $(wildcard test/known_problems/**/*.erl test/should_fail/*.erl test/should_pass/*.erl)
 build_test_data:
 	mkdir -p "test_data"
-	erlc -o test_data $(test_data_erls)
+	erlc $(ERLC_OPTS) -o test_data $(test_data_erls)
 
 EUNIT_OPTS =
 

src/gradualizer_lib.erl

@@ -2,7 +2,8 @@
 
 -module(gradualizer_lib).
 
--export([merge_with/3, top_sort/1, pick_value/1, fold_ast/3, get_ast_children/1,
+-export([merge_with/3, top_sort/1, get_type_definition/3,
+         pick_value/2, fold_ast/3, get_ast_children/1,
          empty_tenv/0, create_tenv/3]).
 -export_type([graph/1, tenv/0]).
 
@@ -90,58 +91,114 @@ reverse_graph(G) ->
     from_edges(maps:keys(G), [ {J, I} || {I, Js} <- maps:to_list(G), J <- Js ]).
 
 
-% Given a type, pick a value of that type.
-% Used in exhaustiveness checking to show an example value
-% which is not covered by the cases.
-pick_value(List) when is_list(List) ->
-    [pick_value(Ty) || Ty <- List ];
-pick_value(?type(integer)) ->
+%% Look up `UserTy' definition:
+%% first in `gradualizer_db', then, if not found, in provided `Types' map.
+%% `UserTy' is actually an unexported `gradualizer_type:af_user_defined_type()'.
+
+-spec get_type_definition(UserTy, TEnv, Opts) -> {ok, Ty} | opaque | not_found when
+      UserTy :: gradualizer_type:abstract_type(),
+      TEnv :: tenv(),
+      Opts :: [annotate_user_types],
+      Ty :: gradualizer_type:abstract_type().
+get_type_definition({remote_type, _Anno, [{atom, _, Module}, {atom, _, Name}, Args]}, _TEnv, _Opts) ->
+    gradualizer_db:get_type(Module, Name, Args);
+get_type_definition({user_type, Anno, Name, Args}, TEnv, Opts) ->
+    %% Let's check if the type is a known remote type.
+    case typelib:get_module_from_annotation(Anno) of
+        {ok, Module} ->
+            gradualizer_db:get_type(Module, Name, Args);
+        none ->
+            %% Let's check if the type is defined in the context of this module.
+            case maps:get({Name, length(Args)}, maps:get(types, TEnv), not_found) of
+                {Params, Type0} ->
+                    VarMap = maps:from_list(lists:zip(Params, Args)),
+                    Type2 = case proplists:is_defined(annotate_user_types, Opts) of
+                                true ->
+                                    Type1 = typelib:annotate_user_types(maps:get(module, TEnv), Type0),
+                                    typelib:substitute_type_vars(Type1, VarMap);
+                                false ->
+                                    typelib:substitute_type_vars(Type0, VarMap)
+                            end,
+                    {ok, Type2};
+                not_found ->
+                    not_found
+            end
+    end.
+
+
+%% Given a type `Ty', pick a value of that type.
+%% Used in exhaustiveness checking to show an example value
+%% which is not covered by the cases.
+
+-spec pick_value(Ty, TEnv) -> AbstractVal when
+      Ty :: gradualizer_type:abstract_type(),
+      TEnv :: tenv(),
+      AbstractVal :: gradualizer_type:abstract_expr().
+pick_value(List, TEnv) when is_list(List) ->
+    [pick_value(Ty, TEnv) || Ty <- List ];
+pick_value(?type(integer), _TEnv) ->
     {integer, erl_anno:new(0), 0};
-pick_value(?type(char)) ->
+pick_value(?type(char), _TEnv) ->
     {char, erl_anno:new(0), $a};
-pick_value(?type(non_neg_integer)) ->
+pick_value(?type(non_neg_integer), _TEnv) ->
     {integer, erl_anno:new(0), 0};
-pick_value(?type(pos_integer)) ->
+pick_value(?type(pos_integer), _TEnv) ->
     {integer, erl_anno:new(0), 0};
-pick_value(?type(neg_integer)) ->
+pick_value(?type(neg_integer), _TEnv) ->
     {integer, erl_anno:new(0), -1};
-pick_value(?type(float)) ->
+pick_value(?type(float), _TEnv) ->
     {float, erl_anno:new(0), -1};
-pick_value(?type(atom)) ->
+pick_value(?type(atom), _TEnv) ->
     {atom, erl_anno:new(0), a};
-pick_value({atom, _, A}) ->
+pick_value({atom, _, A}, _TEnv) ->
     {atom, erl_anno:new(0), A};
-pick_value({ann_type, _, [_, Ty]}) ->
-    pick_value(Ty);
-pick_value(?type(union, [Ty|_])) ->
-    pick_value(Ty);
-pick_value(?type(tuple, any)) ->
+pick_value({ann_type, _, [_, Ty]}, TEnv) ->
+    pick_value(Ty, TEnv);
+pick_value(?type(union, [Ty|_]), TEnv) ->
+    pick_value(Ty, TEnv);
+pick_value(?type(tuple, any), _TEnv) ->
     {tuple, erl_anno:new(0), []};
-pick_value(?type(tuple, Tys)) ->
-    {tuple, erl_anno:new(0), [pick_value(Ty) || Ty <- Tys]};
-pick_value(?type(record, [{atom, _, RecordName}])) ->
+pick_value(?type(tuple, Tys), TEnv) ->
+    {tuple, erl_anno:new(0), [pick_value(Ty, TEnv) || Ty <- Tys]};
+pick_value(?type(record, [{atom, _, RecordName}]), _TEnv) ->
     {record, erl_anno:new(0), RecordName, []};
-pick_value(?type(record, [{atom, _, RecordName} | Tys])) ->
+pick_value(?type(record, [{atom, _, RecordName} | Tys]), TEnv) ->
     MFields = [
-        {record_field, erl_anno:new(0), {atom, erl_anno:new(0), FieldName}, pick_value(Ty)}
+        {record_field, erl_anno:new(0), {atom, erl_anno:new(0), FieldName}, pick_value(Ty, TEnv)}
         || ?type(field_type, [{atom, _, FieldName}, Ty]) <- Tys
     ],
     {record, erl_anno:new(0), RecordName, MFields};
-pick_value(?type(list)) ->
+pick_value(?type(list), _TEnv) ->
     {nil, erl_anno:new(0)};
-pick_value(?type(list,_)) ->
+pick_value(?type(list,_), _TEnv) ->
     {nil, erl_anno:new(0)};
-pick_value(?type(nil)) ->
+pick_value(?type(nil), _TEnv) ->
     {nil, erl_anno:new(0)};
 %% The ?type(range) is a different case because the type range
 %% ..information is not encoded as an abstract_type()
 %% i.e. {type, Anno, range, [{integer, Anno2, Low}, {integer, Anno3, High}]}
-pick_value(?type(range, [{_TagLo, _, neg_inf}, Hi = {_TagHi, _, _Hi}])) ->
-    %% pick_value(Hi);
+pick_value(?type(range, [{_TagLo, _, neg_inf}, Hi = {_TagHi, _, _Hi}]), _TEnv) ->
+    %% pick_value(Hi, TEnv);
     Hi;
-pick_value(?type(range, [Lo = {_TagLo, _, _Lo}, {_TagHi, _, _Hi}])) ->
-    %% pick_value(Lo).
-    Lo.
+pick_value(?type(range, [Lo = {_TagLo, _, _Lo}, {_TagHi, _, _Hi}]), _TEnv) ->
+    %% pick_value(Lo, TEnv).
+    Lo;
+pick_value(Type, TEnv)
+  when element(1, Type) =:= remote_type; element(1, Type) =:= user_type ->
+    {Kind, Anno, Name, Args} = case Type of
+                                   {remote_type, Anno, [_, {atom, _, Name}, Args]} ->
+                                       {remote_type, Anno, Name, Args};
+                                   {user_type, Anno, Name, Args} ->
+                                       {user_type, Anno, Name, Args}
+                               end,
+    case get_type_definition(Type, TEnv, [annotate_user_types]) of
+        {ok, Ty} ->
+            pick_value(Ty, TEnv);
+        opaque ->
+            {var, Anno, '_Opaque'};
+        not_found ->
+            throw({undef, Kind, Anno, {Name, length(Args)}})
+    end.
 
 
 %% ------------------------------------------------

src/typechecker.erl

@@ -617,28 +617,13 @@ normalize({type, _, union, Tys}, TEnv) ->
         Ts  -> type(union, Ts)
     end;
 normalize({user_type, P, Name, Args} = Type, TEnv) ->
-    case typelib:get_module_from_annotation(P) of
-        {ok, Module} ->
-            %% Local type in another module, from an expanded remote type
-            case gradualizer_db:get_type(Module, Name, Args) of
-                {ok, T} ->
-                    normalize(typelib:remove_pos(T), TEnv);
-                opaque ->
-                    Type;
-                not_found ->
-                    throw({undef, user_type, P, {Module, Name, length(Args)}})
-            end;
-        none ->
-            %% Local user-defined type
-            TypeId = {Name, length(Args)},
-            case maps:get(types, TEnv) of
-                #{TypeId := {Vars, Type0}} ->
-                    VarMap = maps:from_list(lists:zip(Vars, Args)),
-                    Type1 = typelib:substitute_type_vars(Type0, VarMap),
-                    normalize(Type1, TEnv);
-                _NotFound ->
-                    throw({undef, user_type, P, {Name, length(Args)}})
-            end
+    case gradualizer_lib:get_type_definition(Type, TEnv, []) of
+        {ok, T} ->
+            normalize(typelib:remove_pos(T), TEnv);
+        opaque ->
+            Type;
+        not_found ->
+            throw({undef, user_type, P, {Name, length(Args)}})
     end;
 normalize(T = ?top(), _TEnv) ->
     %% Don't normalize gradualizer:top().
@@ -3203,16 +3188,17 @@ check_clauses(Env = #env{tenv = TEnv}, ArgsTy, ResTy, Clauses, Caps) ->
                     end,
                     {[], [], ArgsTy, Env#env.venv},
                     Clauses),
-    % Checking for exhaustive patternmatching
-    case {Env#env.exhaust
-         ,ArgsTy =/= any andalso
-          lists:all(fun refinable/1, ArgsTy)
-         ,lists:all(fun no_guards/1, Clauses)
-         ,is_list(RefinedArgsTy) andalso
-          lists:any(fun (T) -> T =/= type(none) end, RefinedArgsTy)} of
+    % Checking for exhaustive pattern matching
+    check_exhaustiveness(Env, ArgsTy, Clauses, RefinedArgsTy, VarBindsList, Css).
+
+check_exhaustiveness(Env = #env{tenv = TEnv}, ArgsTy, Clauses, RefinedArgsTy, VarBindsList, Css) ->
+    case {Env#env.exhaust,
+          ArgsTy =/= any andalso lists:all(fun (Ty) -> refinable(Ty, TEnv) end, ArgsTy),
+          lists:all(fun no_guards/1, Clauses),
+          is_list(RefinedArgsTy) andalso lists:any(fun (T) -> T =/= type(none) end, RefinedArgsTy)} of
         {true, true, true, true} ->
             [{clause, P, _, _, _}|_] = Clauses,
-            throw({nonexhaustive, P, gradualizer_lib:pick_value(RefinedArgsTy)});
+            throw({nonexhaustive, P, gradualizer_lib:pick_value(RefinedArgsTy, TEnv)});
         _ ->
             ok
     end,
@@ -3449,27 +3435,50 @@ pick_one_refinement_each([Ty|Tys], [RefTy|RefTys]) ->
     RefHeadCombinations ++ RefTailCombinations.
 
 %% Is a type refinable to the point that we do exhaustiveness checking on it?
-refinable(?type(integer)) ->
+refinable(Ty, TEnv) ->
+    refinable(Ty, TEnv, sets:new()).
+
+refinable(?type(integer), _TEnv, _Trace) ->
     true;
-refinable(?type(char)) ->
+refinable(?type(char), _TEnv, _Trace) ->
     true;
-refinable(?type(non_neg_integer)) ->
+refinable(?type(non_neg_integer), _TEnv, _Trace) ->
     true;
-refinable(?type(pos_integer)) ->
+refinable(?type(pos_integer), _TEnv, _Trace) ->
     true;
-refinable(?type(neg_integer)) ->
+refinable(?type(neg_integer), _TEnv, _Trace) ->
     true;
-refinable({atom, _, _}) ->
+refinable({atom, _, _}, _TEnv, _Trace) ->
     true;
-refinable(?type(nil)) ->
+refinable(?type(nil), _TEnv, _Trace) ->
     true;
-refinable(?type(union,Tys)) when is_list(Tys) ->
-    lists:all(fun refinable/1, Tys);
-refinable(?type(tuple, Tys)) when is_list(Tys) ->
-    lists:all(fun refinable/1, Tys);
-refinable(?type(record, [_ | Fields])) ->
-    lists:all(fun refinable/1, [X || ?type(field_type, X) <- Fields]);
-refinable(_) ->
+refinable(?type(union,Tys), TEnv, Trace) when is_list(Tys) ->
+    lists:all(fun (Ty) -> refinable(Ty, TEnv, Trace) end, Tys);
+refinable(?type(tuple, Tys), TEnv, Trace) when is_list(Tys) ->
+    lists:all(fun (Ty) -> refinable(Ty, TEnv, Trace) end, Tys);
+refinable(?type(record, [_ | Fields]), TEnv, Trace) ->
+    lists:all(fun (Ty) -> refinable(Ty, TEnv, Trace) end, [X || ?type(field_type, X) <- Fields]);
+refinable(?top(), _TEnv, _Trace) ->
+    %% This clause prevents incorrect exhaustiveness warnings
+    %% when `gradualizer:top()' is used explicitly.
+    false;
+refinable(RefinableTy, TEnv, Trace)
+  when element(1, RefinableTy) =:= remote_type; element(1, RefinableTy) =:= user_type ->
+    case sets:is_element(RefinableTy, Trace) of
+        true ->
+            %% We're searching down the variants of a recursive type and we've
+            %% reached this recursive type again (that is, it's found in `Trace').
+            %% We assume it's refinable to terminate recursion.
+            %% Refinability will be determined by the variants which are not (mutually) recursive.
+            true;
+        false ->
+            case gradualizer_lib:get_type_definition(RefinableTy, TEnv, [annotate_user_types]) of
+                {ok, Ty} -> refinable(Ty, TEnv, sets:add_element(RefinableTy, Trace));
+                opaque -> true;
+                not_found -> false
+            end
+    end;
+refinable(_, _, _) ->
     false.
 
 no_guards({clause, _, _, Guards, _}) ->

test/known_problems/should_fail/exhaustive_map_variants.erl

@@ -0,0 +1,16 @@
+-module(exhaustive_map_variants).
+
+%% This extends cases from test/should_fail/exhaustive_user_type.erl to variants defined as maps.
+
+-export([map_variants/1]).
+
+-export_type([map_sum_t/0]).
+
+-type map_sum_t() :: #{field_one := _}
+                   | #{field_two := _}.
+
+-spec map_variants(map_sum_t()) -> ok.
+map_variants(T) ->
+    case T of
+        #{field_one := _} -> ok
+    end.

test/known_problems/should_fail/exhaustive_remote_map_variants.erl

@@ -0,0 +1,15 @@
+-module(exhaustive_remote_map_variants).
+
+%% This is the remote type counterpart
+%% of test/known_problems/should_fail/exhaustive_map_variants.erl
+%%
+%% See also test/should_fail/exhaustive_user_type.erl
+%% and test/should_fail/exhaustive_remote_user_type.erl
+
+-export([remote_map_variants/1]).
+
+-spec remote_map_variants(exhaustive_user_type:map_sum_t()) -> ok.
+remote_map_variants(T) ->
+    case T of
+        #{field_one := _} -> ok
+    end.

test/should_fail/exhaustive_remote_user_type.erl

@@ -0,0 +1,51 @@
+-module(exhaustive_remote_user_type).
+
+-export([local_alias/1,
+         local_alias_to_recursive_type/1,
+         remote/1,
+         generic_with_remote_opaque/1,
+         remote_opaque/1,
+         remote_record_variants/1]).
+
+-type alias_t() :: exhaustive_user_type:t().
+-type recursive_t() :: exhaustive_user_type:recursive_t().
+
+-spec local_alias(alias_t()) -> ok.
+local_alias(T) ->
+    case T of
+        {true, _} -> ok
+    end.
+
+-spec local_alias_to_recursive_type(recursive_t()) -> ok.
+local_alias_to_recursive_type(T) ->
+    case T of
+        ok -> ok
+    end.
+
+-spec remote(exhaustive_user_type:t()) -> ok.
+remote(T) ->
+    case T of
+        {true, _} -> ok
+    end.
+
+-type g(T) :: ok | {generic, T}.
+
+-spec generic_with_remote_opaque(g(exhaustive_user_type:opaque_t())) -> ok.
+generic_with_remote_opaque(T) ->
+    case T of
+        ok -> ok
+    end.
+
+-spec remote_opaque(exhaustive_user_type:opaque_t()) -> ok.
+remote_opaque(T) ->
+    case T of
+        left -> ok
+    end.
+
+-include("exhaustive_user_type.hrl").
+
+-spec remote_record_variants(exhaustive_user_type:record_sum_t()) -> ok.
+remote_record_variants(T) ->
+    case T of
+        #variant1{} -> ok
+    end.