Skip too complex guards

.github/workflows/proptests.yml

@@ -13,7 +13,7 @@ jobs:
     name: Erlang ${{matrix.otp}}
     strategy:
       matrix:
-        otp: ['24.3.4.4']
+        otp: ['26.2.5']
     steps:
       - uses: actions/checkout@v2
       - uses: erlef/setup-beam@v1

src/typechecker.erl

@@ -417,10 +417,6 @@ compat_ty({type, Anno1, record, [{atom, _, Name} | Fields1]},
           {type, Anno2, record, [{atom, _, Name} | Fields2]}, Seen, Env) ->
     AllFields1 = case Fields1 of [] -> get_record_fields_types(Name, Anno1, Env); _ -> Fields1 end,
     AllFields2 = case Fields2 of [] -> get_record_fields_types(Name, Anno2, Env); _ -> Fields2 end,
-    %% We can assert because we explicitly match {atom, _, Name}
-    %% out of the field list in both cases above.
-    AllFields1 = ?assert_type(AllFields1, [record_field_type()]),
-    AllFields2 = ?assert_type(AllFields2, [record_field_type()]),
     compat_record_tys(AllFields1, AllFields2, Seen, Env);
 compat_ty({type, _, record, _}, {type, _, tuple, any}, Seen, _Env) ->
     ret(Seen);
@@ -440,20 +436,15 @@ compat_ty(Ty1, Ty2, Seen, Env) when ?is_list_type(Ty1), ?is_list_type(Ty2) ->
 compat_ty({type, _, tuple, any}, {type, _, tuple, any}, Seen, _Env) ->
     ret(Seen);
 compat_ty({type, _, tuple, any}, {type, _, tuple, Args2}, Seen, Env) ->
-    %% We can assert because we match out `any' in previous clauses.
-    %% TODO: it would be perfect if Gradualizer could refine this type automatically in such a case
-    Args2 = ?assert_type(Args2, [type()]),
     Args1 = lists:duplicate(length(Args2), type(any)),
     % We check the argument types because Args2 may contain type variables
     % and in that case, we want to constrain them
     compat_tys(Args1, Args2, Seen, Env);
 compat_ty({type, _, tuple, Args1}, {type, _, tuple, any}, Seen, Env) ->
-    Args1 = ?assert_type(Args1, [type()]),
     Args2 = lists:duplicate(length(Args1), type(any)),
     compat_tys(Args1, Args2, Seen, Env);
 compat_ty({type, _, tuple, Args1}, {type, _, tuple, Args2}, Seen, Env) ->
-    compat_tys(?assert_type(Args1, [type()]),
-               ?assert_type(Args2, [type()]), Seen, Env);
+    compat_tys(Args1, Args2, Seen, Env);
 
 %% Maps
 compat_ty({type, _, map, [?any_assoc]}, {type, _, map, _Assocs}, Seen, _Env) ->
@@ -469,10 +460,6 @@ compat_ty({type, _, map, Assocs1}, {type, _, map, Assocs2}, Seen, Env) ->
                       ({type, _, map_field_exact, _}) -> true;
                       (_) -> false
                   end,
-    %% We can assert because {type, _, map, any} is normalized away by normalize/2,
-    %% whereas ?any_assoc associations are matched out explicitly in the previous clauses.
-    Assocs1 = ?assert_type(Assocs1, [gradualizer_type:af_assoc_type()]),
-    Assocs2 = ?assert_type(Assocs2, [gradualizer_type:af_assoc_type()]),
     MandatoryAssocs1 = lists:filter(IsMandatory, Assocs1),
     MandatoryAssocs2 = lists:filter(IsMandatory, Assocs2),
     {Seen3, Cs3} = lists:foldl(fun ({type, _, map_field_exact, _} = Assoc2, {Seen2, Cs2}) ->
@@ -507,10 +494,6 @@ compat_ty({type, _, AssocTag1, [Key1, Val1]},
              AssocTag1 == map_field_exact, AssocTag2 == map_field_exact;
              AssocTag1 == map_field_exact, AssocTag2 == map_field_assoc ->
     %% For M1 <: M2, mandatory fields in M2 must be mandatory fields in M1
-    Key1 = ?assert_type(Key1, type()),
-    Key2 = ?assert_type(Key2, type()),
-    Val1 = ?assert_type(Val1, type()),
-    Val2 = ?assert_type(Val2, type()),
     {Seen1, Cs1} = compat(Key1, Key2, Seen, Env),
     {Seen2, Cs2} = compat(Val1, Val2, Seen1, Env),
     {Seen2, constraints:combine(Cs1, Cs2, Env)};
@@ -4015,7 +3998,6 @@ disable_exhaustiveness_check(#env{} = Env) ->
 check_arg_exhaustiveness(Env, ArgTys, Clauses, RefinedArgTys) ->
     case exhaustiveness_checking(Env) andalso
          all_refinable(ArgTys, Env) andalso
-         no_clause_has_guards(Clauses) andalso
          some_type_not_none(RefinedArgTys)
     of
         true ->
@@ -4036,10 +4018,6 @@ exhaustiveness_checking(#env{} = Env) ->
 all_refinable(any, _Env) -> false;
 all_refinable(Types, Env) -> lists:all(fun (Ty) -> refinable(Ty, Env) end, Types).
 
--spec no_clause_has_guards(_) -> boolean().
-no_clause_has_guards(Clauses) ->
-    lists:all(fun no_guards/1, Clauses).
-
 -spec some_type_not_none([type()]) -> boolean().
 some_type_not_none(Types) when is_list(Types) ->
     lists:any(fun (T) -> T =/= type(none) end, Types).
@@ -4106,6 +4084,8 @@ refine_mismatch_using_guards(PatTys,
             do_refine_mismatch_using_guards(Guards, PatTys, Pats, VEnv, Env);
         [_|_] ->
             %% we don't know yet how to do this in guard sequences
+            Env#env.no_skip_complex_guards orelse throw({skip, too_complex_guards}),
+            %% TODO: Invalid lack of pattern refinement
             PatTys
     end.
 
@@ -4579,16 +4559,15 @@ mta({user_type, Anno, Name, Args}, Env) ->
 mta(Type, _Env) ->
     Type.
 
--spec no_guards(_) -> boolean().
-no_guards({clause, _, _, Guards, _}) ->
-    Guards == [].
-
 %% Refines the types of bound variables using the assumption that a clause has
 %% mismatched.
 -spec refine_vars_by_mismatching_clause(gradualizer_type:af_clause(), venv(), env()) -> venv().
 refine_vars_by_mismatching_clause({clause, _, Pats, Guards, _Block}, VEnv, Env) ->
     PatternCantFail = are_patterns_matching_all_input(Pats, VEnv),
     case Guards of
+        [] ->
+            %% No guards, so no refinement
+            VEnv;
         [[{call, _, {atom, _, Fun}, Args = [{var, _, Var}]}]] when PatternCantFail ->
             %% Simple case: A single guard on the form `when is_TYPE(Var)'.
             %% If Var was bound before the clause, which failed because of a
@@ -4602,7 +4581,8 @@ refine_vars_by_mismatching_clause({clause, _, Pats, Guards, _Block}, VEnv, Env)
                     VEnv
             end;
         _OtherGuards ->
-            %% No refinement
+            Env#env.no_skip_complex_guards orelse throw({skip, too_complex_guards}),
+            %% TODO: Invalid lack of refinement
             VEnv
     end.
 
@@ -4746,17 +4726,23 @@ type_check_function(Env, {function, _Anno, Name, NArgs, Clauses}) ->
     ?verbose(Env, "Checking function ~p/~p~n", [Name, NArgs]),
     case maps:find({Name, NArgs}, Env#env.fenv) of
         {ok, FunTy} ->
-            NewEnv = Env#env{current_spec = FunTy},
-            FunTyNoPos = [ typelib:remove_pos(?assert_type(Ty, type())) || Ty <- FunTy ],
-            Arity = clause_arity(hd(Clauses)),
-            case expect_fun_type(NewEnv, FunTyNoPos, Arity) of
-                {type_error, NotFunTy} ->
-                    %% This can only happen if `create_fenv/2' creates garbage.
-                    erlang:error({invalid_function_type, NotFunTy});
-                FTy ->
-                    FTy1 = make_rigid_type_vars(FTy),
-                    _Vars = check_clauses_fun(NewEnv, FTy1, Clauses),
-                    NewEnv
+            try
+                NewEnv = Env#env{current_spec = FunTy},
+                FunTyNoPos = [ typelib:remove_pos(?assert_type(Ty, type())) || Ty <- FunTy ],
+                Arity = clause_arity(hd(Clauses)),
+                case expect_fun_type(NewEnv, FunTyNoPos, Arity) of
+                    {type_error, NotFunTy} ->
+                        %% This can only happen if `create_fenv/2' creates garbage.
+                        erlang:error({invalid_function_type, NotFunTy});
+                    FTy ->
+                        FTy1 = make_rigid_type_vars(FTy),
+                        _Vars = check_clauses_fun(NewEnv, FTy1, Clauses),
+                        NewEnv
+                end
+            catch
+                throw:{skip, Reason} ->
+                    ?verbose(Env, "Skipping function ~p/~p due to ~s~n", [Name, NArgs, Reason]),
+                    Env
             end;
         error ->
             throw(internal_error(missing_type_spec, Name, NArgs))
@@ -4771,18 +4757,17 @@ arity(I) ->
     ?assert(I < 256, arity_overflow),
     ?assert_type(I, arity()).
 
--spec position_info_from_spec(form() | forms() | none) -> erl_anno:anno().
+-spec position_info_from_spec(none | form() | forms()) -> erl_anno:anno().
 position_info_from_spec(none) ->
     %% This simplifies testing internal functions.
     %% In these cases we don't go through type_check_function,
     %% but call deeper into the typechecker directly.
     erl_anno:new(0);
+position_info_from_spec(Form) when is_tuple(Form) ->
+    element(2, Form);
 position_info_from_spec([_|_] = Forms) ->
     %% TODO: https://github.com/josefs/Gradualizer/issues/388
-    position_info_from_spec(hd(Forms));
-position_info_from_spec(Form) ->
-    Form = ?assert_type(Form, form()),
-    element(2, Form).
+    position_info_from_spec(hd(Forms)).
 
 %% Type check patterns against types (P1 :: T1, P2 :: T2, ...)
 %% and add variable bindings for the patterns.
@@ -5835,7 +5820,8 @@ create_env(#parsedata{module    = Module
          verbose = proplists:get_bool(verbose, Opts),
          union_size_limit = proplists:get_value(union_size_limit, Opts,
                                                 default_union_size_limit()),
-         solve_constraints = proplists:get_bool(solve_constraints, Opts)}.
+         solve_constraints = proplists:get_bool(solve_constraints, Opts),
+         no_skip_complex_guards = proplists:get_bool(no_skip_complex_guards, Opts)}.
 
 -spec default_union_size_limit() -> non_neg_integer().
 default_union_size_limit() -> 30.

src/typechecker.hrl

@@ -3,23 +3,26 @@
 
 -record(clauses_controls, {exhaust}).
 
--record(env, {fenv              = #{}   :: #{{atom(), arity()} =>
-                                                  [gradualizer_type:af_constrained_function_type()]
-                                                | [gradualizer_type:gr_any_type()]
-                                            },
-              imported          = #{}   :: #{{atom(), arity()} => module()},
-              venv              = #{}   :: typechecker:venv(),
-              tenv                      :: gradualizer_lib:tenv(),
-              infer             = false :: boolean(),
-              verbose           = false :: boolean(),
-              exhaust           = true  :: boolean(),
+-record(env, {fenv              = #{}           :: #{{atom(), arity()} =>
+                                                          [gradualizer_type:af_constrained_function_type()]
+                                                        | [gradualizer_type:gr_any_type()]
+                                                    },
+              imported          = #{}           :: #{{atom(), arity()} => module()},
+              venv              = #{}           :: typechecker:venv(),
+              tenv                              :: gradualizer_lib:tenv(),
+              infer             = false         :: boolean(),
+              verbose           = false         :: boolean(),
+              exhaust           = true          :: boolean(),
               %% Controls driving the type checking algorithm
               %% per clauses-list (fun/case/try-catch/receive).
-              clauses_stack     = []    :: [#clauses_controls{}],
+              clauses_stack     = []            :: [#clauses_controls{}],
               %% Performance hack: Unions larger than this limit are replaced by any() in normalization.
-              union_size_limit          :: non_neg_integer(),
-              current_spec      = none  :: erl_parse:abstract_form() | none,
-              solve_constraints = false :: boolean()
+              union_size_limit                  :: non_neg_integer(),
+              current_spec      = none          :: erl_parse:abstract_form() | none,
+              solve_constraints = false         :: boolean(),
+              %% Skip functions whose guards are too complex to be handled yet,
+              %% which might result in false positives when checking rest of the functions
+              no_skip_complex_guards = false    :: boolean()
              }).
 
 -endif. %% __TYPECHECKER_HRL__

src/typelib.erl

@@ -232,11 +232,15 @@ annotate_user_type_(_Filename, Type) ->
 -spec get_module_from_annotation(erl_anno:anno()) -> {ok, module()} | none.
 get_module_from_annotation(Anno) ->
     case erl_anno:file(Anno) of
-        File when is_list(File) ->
-            Basename = filename:basename(File, ".erl"),
-            {ok, list_to_existing_atom(?assert_type(Basename, string()))};
         undefined ->
-            none
+            none;
+        File ->
+            case unicode:characters_to_binary(filename:basename(File, ".erl")) of
+                Basename when is_binary(Basename) ->
+                    {ok, binary_to_existing_atom(Basename)};
+                _ ->
+                    erlang:error({malformed_anno, Anno})
+            end
     end.
 
 -spec substitute_type_vars(type(),

test/known_problems/should_fail/type_refinement_should_fail.erl

@@ -0,0 +1,21 @@
+-module(type_refinement_should_fail).
+
+-export([guard_prevents_refinement/2,
+         guard_prevents_refinement2/1,
+         pattern_prevents_refinement/2]).
+
+-spec guard_prevents_refinement(1..2, boolean()) -> 2.
+guard_prevents_refinement(N, Guard) ->
+    case N of
+        1 when Guard -> 2;
+        M            -> M  %% 1 cannot be eliminated
+    end.
+
+-spec guard_prevents_refinement2(integer()) -> ok.
+guard_prevents_refinement2(X) when is_integer(X), X rem 7 == 0 -> ok;
+guard_prevents_refinement2(X) -> ok. % X can still be an integer
+
+-spec pattern_prevents_refinement(integer(), any()) -> atom().
+pattern_prevents_refinement(X, X)    when is_integer(X) -> ok;
+pattern_prevents_refinement(X, {_Y}) when is_integer(X) -> ok;
+pattern_prevents_refinement(Inf, _) -> Inf. % Inf can still be an integer

test/known_problems/should_pass/refine_bound_var_with_guard_should_pass.erl

@@ -1,6 +1,9 @@
 -module(refine_bound_var_with_guard_should_pass).
 
--export([f/1]).
+-export([f/1,
+         too_complex_guards/1]).
+
+-gradualizer([no_skip_complex_guards]).
 
 %% This type is simpler than gradualizer_type:abstract_type() by having less variants
 %% and by using tuples to contain deeper nodes. The latter frees us from having to deal
@@ -35,3 +38,12 @@ g({type, nonempty_list, {InnerNode}}) ->
     InnerNode;
 g({type, atom, {_InnerNode}}) ->
     a.
+
+%% See too_complex_guards thrown in src/typechecker.erl.
+-spec too_complex_guards(integer() | [integer()] | none) -> number().
+too_complex_guards([_|_] = Ints) ->
+    lists:sum(Ints);
+too_complex_guards(EmptyOrNone) when EmptyOrNone =:= none orelse is_list(EmptyOrNone) ->
+    0;
+too_complex_guards(Int) ->
+    Int.

test/should_fail/type_refinement_fail.erl

@@ -1,15 +1,7 @@
 -module(type_refinement_fail).
--export([guard_prevents_refinement/2, imprecision_prevents_refinement/2,
-         multi_pat_fail_1/2,
-         guard_prevents_refinement2/1,
-         pattern_prevents_refinement/2]).
 
--spec guard_prevents_refinement(1..2, boolean()) -> 2.
-guard_prevents_refinement(N, Guard) ->
-    case N of
-        1 when Guard -> 2;
-        M            -> M  %% 1 cannot be eliminated
-    end.
+-export([imprecision_prevents_refinement/2,
+         multi_pat_fail_1/2]).
 
 -spec imprecision_prevents_refinement(float(), a|b) -> b.
 imprecision_prevents_refinement(3.14, a) -> b;
@@ -18,12 +10,3 @@ imprecision_prevents_refinement(_, X) -> X.
 -spec multi_pat_fail_1(a|b, a|b) -> {b, b}.
 multi_pat_fail_1(a, a) -> {b, b};
 multi_pat_fail_1(A, B) -> {A, B}. %% Not only {b, b} here
-
--spec guard_prevents_refinement2(erlang:timestamp()) -> ok.
-guard_prevents_refinement2(X) when is_integer(X), X rem 7 == 0 -> ok;
-guard_prevents_refinement2(infinity) -> ok. % can still be an integer
-
--spec pattern_prevents_refinement(erlang:timestamp(), any()) -> atom().
-pattern_prevents_refinement(X, X)    when is_integer(X) -> ok;
-pattern_prevents_refinement(X, {_Y}) when is_integer(X) -> ok;
-pattern_prevents_refinement(Inf, _) -> Inf. % Inf can still be an integer

test/should_pass/type_refinement_pass.erl

@@ -11,7 +11,11 @@
          beside_match_all/2,
          beside_singleton/2,
          refine_bound_var_by_guard_bifs/1,
-         refine_literals_by_guards/1]).
+         refine_literals_by_guards/1,
+         too_complex_guards/1,
+         no_guards/1,
+         no_complex_guards1/1,
+         no_complex_guards2/1]).
 
 %% Test that Value is not considered to be string() | false.
 -spec basic_type_refinement(string()) -> string().
@@ -99,3 +103,44 @@ refine_literals_by_guards(X) when is_integer(X) -> self();
 refine_literals_by_guards(X) when is_tuple(X)   -> self();
 refine_literals_by_guards(X) when is_list(X)    -> self();
 refine_literals_by_guards(X)                    -> X.
+
+%% See also refine_bound_var_with_guard_should_pass known problem.
+-spec too_complex_guards(integer() | [integer()] | none) -> number().
+too_complex_guards([_|_] = Ints) ->
+    lists:sum(Ints);
+%% Passes thanks to the whole function being skipped, but these guards are not handled yet.
+%% See too_complex_guards thrown in src/typechecker.erl.
+too_complex_guards(EmptyOrNone) when EmptyOrNone =:= none orelse is_list(EmptyOrNone) ->
+    0;
+too_complex_guards(Int) ->
+    Int.
+
+%% This is based on dog-fooding typechecker:position_info_from_spec/1 @ 3bdca60,
+%% where we know that the list will never be empty.
+%% This is one way to refactor `too_complex_guards' to get typechecked with a little bit of
+%% programmer input.
+-spec no_guards(integer() | [integer()] | none) -> number().
+no_guards(none) ->
+    0;
+no_guards([] = Ints) ->
+    0;
+no_guards([_|_] = Ints) ->
+    lists:sum(Ints);
+no_guards(Int) ->
+    Int.
+
+-spec no_complex_guards1(integer() | [integer()] | none) -> number().
+no_complex_guards1(none) ->
+    0;
+no_complex_guards1(Ints) when is_list(Ints) ->
+    lists:sum(Ints);
+no_complex_guards1(Num) ->
+    Num.
+
+-spec no_complex_guards2(integer() | [integer()] | none) -> number().
+no_complex_guards2(none) ->
+    0;
+no_complex_guards2(Num) when is_integer(Num) ->
+    Num;
+no_complex_guards2(List) ->
+    lists:sum(List).