diff --git a/.github/workflows/proptests.yml b/.github/workflows/proptests.yml index 2eebb9b1..ccffd410 100644 --- a/.github/workflows/proptests.yml +++ b/.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 diff --git a/src/typechecker.erl b/src/typechecker.erl index 9e9337c6..9aa8c06a 100644 --- a/src/typechecker.erl +++ b/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. diff --git a/src/typechecker.hrl b/src/typechecker.hrl index 91540cbc..1f268d26 100644 --- a/src/typechecker.hrl +++ b/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__ diff --git a/src/typelib.erl b/src/typelib.erl index 670c4924..bae3d2dc 100644 --- a/src/typelib.erl +++ b/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(), diff --git a/test/known_problems/should_fail/type_refinement_should_fail.erl b/test/known_problems/should_fail/type_refinement_should_fail.erl new file mode 100644 index 00000000..8b0e8e66 --- /dev/null +++ b/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 diff --git a/test/known_problems/should_pass/refine_bound_var_with_guard_should_pass.erl b/test/known_problems/should_pass/refine_bound_var_with_guard_should_pass.erl index 2d4d18ce..e0ce3082 100644 --- a/test/known_problems/should_pass/refine_bound_var_with_guard_should_pass.erl +++ b/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. diff --git a/test/should_fail/type_refinement_fail.erl b/test/should_fail/type_refinement_fail.erl index cb83c751..33de910c 100644 --- a/test/should_fail/type_refinement_fail.erl +++ b/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 diff --git a/test/should_pass/type_refinement_pass.erl b/test/should_pass/type_refinement_pass.erl index 462276c3..429cebbb 100644 --- a/test/should_pass/type_refinement_pass.erl +++ b/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).