From 45757f72d7e6f3e8bdda91296658ebd309791f36 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Tue, 14 Mar 2023 17:41:30 +0100 Subject: [PATCH 01/18] Copy af_maybe() from erlang/otp#7013 --- src/gradualizer_type.erl | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/gradualizer_type.erl b/src/gradualizer_type.erl index 2c1906e7..e9441818 100644 --- a/src/gradualizer_type.erl +++ b/src/gradualizer_type.erl @@ -47,6 +47,7 @@ -type abstract_expr() :: af_literal() | af_match(abstract_expr()) + | af_maybe_match() | af_variable() | af_tuple(abstract_expr()) | af_nil() @@ -73,7 +74,9 @@ | af_local_fun() | af_remote_fun() | af_fun() - | af_named_fun(). + | af_named_fun() + | af_maybe() + | af_maybe_else(). -type af_record_update(T) :: {'record', anno(), @@ -220,6 +223,9 @@ -type af_map_pattern() :: {'map', anno(), [af_assoc_exact(af_pattern())]}. +-type af_maybe() :: {'maybe', anno(), af_body()}. +-type af_maybe_else() :: {'maybe', anno(), af_body(), {'else', anno(), af_clause_seq()}}. + -type abstract_type() :: af_annotated_type() | af_atom() | af_bitstring_type() @@ -357,6 +363,8 @@ -type af_match(T) :: {'match', anno(), af_pattern(), T}. +-type af_maybe_match() :: {'maybe_match', anno(), af_pattern(), abstract_expr()}. + -type af_variable() :: {'var', anno(), atom()}. % | af_anon_variable() %-type af_anon_variable() :: {'var', anno(), '_'}. From fc54501e447df0334d4c22df7f0ecaaa1c383bd9 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Tue, 14 Mar 2023 17:45:12 +0100 Subject: [PATCH 02/18] Fix a self-check error in gradualizer_db:get_beam_map/0 --- src/gradualizer_db.erl | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/gradualizer_db.erl b/src/gradualizer_db.erl index a2c06428..4c740353 100644 --- a/src/gradualizer_db.erl +++ b/src/gradualizer_db.erl @@ -609,7 +609,8 @@ get_beam_map() -> fun (Filename) -> case re:run(Filename, RE, [{capture, all_but_first, list}]) of {match, [Mod]} -> - {list_to_atom(Mod), Filename}; + %% We can assert because we request re:run() to return a `list` + {list_to_atom(?assert_type(Mod, string())), Filename}; nomatch -> {false, false}; _ -> From b990d6bdea52b02ac0eb9724240f01a30d26581f Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Tue, 14 Mar 2023 17:54:26 +0100 Subject: [PATCH 03/18] Fix a self-check error in typechecker:compat_ty(record, record, ...) --- src/typechecker.erl | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/typechecker.erl b/src/typechecker.erl index 7046fe47..3ed68198 100644 --- a/src/typechecker.erl +++ b/src/typechecker.erl @@ -358,10 +358,14 @@ compat_ty({type, P1, record, [{atom, _, Name}]}, compat_record_fields(Fields1, Fields2, Seen, Env); %% Records that have been refined on one side or the other -compat_ty({type, Anno1, record, [{atom, _, Name}|Fields1]}, - {type, Anno2, record, [{atom, _, Name}|Fields2]}, Seen, Env) -> +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); @@ -460,7 +464,7 @@ compat_tys(_Tys1, _Tys2, _, _) -> throw(nomatch). --spec compat_record_tys([type()], [type()], map(), env()) -> compat_acc(). +-spec compat_record_tys(list(), list(), map(), env()) -> compat_acc(). compat_record_tys([], [], Seen, _Env) -> ret(Seen); compat_record_tys([?type_field_type(Name, Field1)|Fields1], [?type_field_type(Name, Field2)|Fields2], Seen, Env) -> @@ -4059,7 +4063,7 @@ refine(OrigTy, Ty, Trace, Env) -> end end. --spec get_record_fields_types(atom(), erl_anno:anno(), env()) -> [_]. +-spec get_record_fields_types(atom(), erl_anno:anno(), env()) -> [record_field_type()]. get_record_fields_types(Name, Anno, Env) -> RecordFields = get_maybe_remote_record_fields(Name, Anno, Env), [type_field_type(FieldName, Type) || ?typed_record_field(FieldName, Type) <- RecordFields]. From fc1c5b49e76dd134c8627648fe1b052ea9161fe5 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Tue, 14 Mar 2023 17:56:55 +0100 Subject: [PATCH 04/18] Fix a self-check error in compat_ty(tuple, tuple, ...) --- src/typechecker.erl | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/typechecker.erl b/src/typechecker.erl index 3ed68198..802a8669 100644 --- a/src/typechecker.erl +++ b/src/typechecker.erl @@ -387,7 +387,10 @@ compat_ty({type, _, tuple, any}, {type, _, tuple, _Args}, Seen, _Env) -> compat_ty({type, _, tuple, _Args}, {type, _, tuple, any}, Seen, _Env) -> ret(Seen); compat_ty({type, _, tuple, Args1}, {type, _, tuple, Args2}, Seen, Env) -> - compat_tys(Args1, 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 + compat_tys(?assert_type(Args1, [type()]), + ?assert_type(Args2, [type()]), Seen, Env); %% Maps compat_ty({type, _, map, [?any_assoc]}, {type, _, map, _Assocs}, Seen, _Env) -> From ef6750cf699e1cebedc62a59330730afb413f193 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Tue, 14 Mar 2023 18:02:26 +0100 Subject: [PATCH 05/18] Fix a self-check error in compat_ty(map, map, ...) --- src/typechecker.erl | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/typechecker.erl b/src/typechecker.erl index 802a8669..adb0010b 100644 --- a/src/typechecker.erl +++ b/src/typechecker.erl @@ -406,6 +406,10 @@ 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}) -> From 10d5f64f4d2095bb114561c32fd893bf485b0b60 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Tue, 14 Mar 2023 18:06:05 +0100 Subject: [PATCH 06/18] Fix a self-check error in compat_ty(map_assoc, map_assoc, ...) --- src/typechecker.erl | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/typechecker.erl b/src/typechecker.erl index adb0010b..d30a792c 100644 --- a/src/typechecker.erl +++ b/src/typechecker.erl @@ -443,6 +443,10 @@ 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)}; From 4bb2090d8368a1f5aa153380d074b70a98bc741e Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Tue, 14 Mar 2023 18:17:47 +0100 Subject: [PATCH 07/18] Fix a self-check error in absform:normalize_function_type/1 --- src/absform.erl | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/src/absform.erl b/src/absform.erl index f9a90f55..59668521 100644 --- a/src/absform.erl +++ b/src/absform.erl @@ -35,10 +35,20 @@ normalize_record_field({typed_record_field, normalize_function_type_list(FunTypeList) -> ?assert_type(lists:map(fun normalize_function_type/1, FunTypeList), nonempty_list()). --spec normalize_function_type(BoundedFun | Fun) -> BoundedFun when - BoundedFun :: gradualizer_type:af_constrained_function_type(), - Fun :: gradualizer_type:af_fun_type(). +-type bounded_fun() :: gradualizer_type:af_constrained_function_type(). + +-spec normalize_function_type(bounded_fun()) -> bounded_fun(); + (gradualizer_type:af_fun_type()) -> bounded_fun(). +normalize_function_type({type, _, 'bounded_fun', [_FunType, _FunConst]} = BoundedFun) -> + BoundedFun; +normalize_function_type({type, _, 'bounded_fun', _}) -> + %% This will never happen if the code in question compiles, + %% but to avoid a "Nonexhaustive patterns" error we handle it explicitly. + %% TODO: if the type representation inherited from erl_parse didn't use lists for inner nodes we + %% wouldn't have to bother with matching empty lists here :( + erlang:error(unreachable); normalize_function_type({type, L, 'fun', [{type, _, product, _ArgTypes}, _RetType]} = FunType) -> {type, L, bounded_fun, [FunType, _EmptyConst = []]}; -normalize_function_type({type, _, 'bounded_fun', [_FunType, _FunConst]} = BoundedFun) -> - BoundedFun. +normalize_function_type({type, _, 'fun', _}) -> + %% TODO: same story as for bounded_fun above + erlang:error(unreachable). From 1b8046def0c9af7ce161a680cfb6a8fbe22a4232 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Tue, 14 Mar 2023 18:29:58 +0100 Subject: [PATCH 08/18] Add a TODO about solving constraints --- src/typechecker.erl | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/typechecker.erl b/src/typechecker.erl index d30a792c..6af1e86e 100644 --- a/src/typechecker.erl +++ b/src/typechecker.erl @@ -3168,6 +3168,8 @@ type_check_list_op_in(Env, ResTy, {op, P, Op, Arg1, Arg2} = Expr) -> {union_var_binds(VarBinds1, VarBinds2, Env), constraints:combine([Cs, Cs1, Cs2])}; false -> + %% TODO: we're getting this because of a type var, so if we solve constraints + %% here and get a substitution for this type var, we should be able to tell more throw(type_error(op_type_too_precise, Op, P, ResTy1)) end end. From b934fc34f3911d97731243702d33b02a2d2d2283 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Tue, 14 Mar 2023 18:34:11 +0100 Subject: [PATCH 09/18] Fix a self-check error in gradualizer_int:int_type_to_range/1 --- src/gradualizer_int.erl | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/gradualizer_int.erl b/src/gradualizer_int.erl index bffe5c5a..d3fce004 100644 --- a/src/gradualizer_int.erl +++ b/src/gradualizer_int.erl @@ -109,7 +109,10 @@ int_type_to_range({type, _, range, [{Tag1, _, I1}, {Tag2, _, I2}]}) Tag2 =:= integer orelse Tag2 =:= char orelse (Tag2 =:= atom andalso - (I2 =:= neg_inf orelse I2 =:= pos_inf)) -> {I1, I2}; + (I2 =:= neg_inf orelse I2 =:= pos_inf)) -> + I1 = ?assert_type(I1, integer() | neg_inf | pos_inf), + I2 = ?assert_type(I2, integer() | neg_inf | pos_inf), + {I1, I2}; int_type_to_range({char, _, I}) -> {I, I}; int_type_to_range({integer, _, I}) -> {I, I}. From 5efbb021811b7a15142c47550578173f11199f29 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Tue, 14 Mar 2023 23:51:17 +0100 Subject: [PATCH 10/18] Fix a self-check error in gradualizer_lib:get_type_definition/3 --- src/gradualizer_lib.erl | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/gradualizer_lib.erl b/src/gradualizer_lib.erl index da16c9d1..3c318d97 100644 --- a/src/gradualizer_lib.erl +++ b/src/gradualizer_lib.erl @@ -122,7 +122,11 @@ get_type_definition({user_type, Anno, Name, Args}, Env, Opts) -> 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, Env#env.tenv), not_found) of + case maps:get({Name, length(Args)}, maps:get(types, Env#env.tenv), {not_, found}) of + %% TODO: the constraint solver requires the "shape" of a Default to be the same as + %% of an actual Value + {not_, found} -> + not_found; {Params, Type0} -> VarMap = maps:from_list(lists:zip(Params, Args)), Type2 = case proplists:is_defined(annotate_user_types, Opts) of @@ -133,9 +137,7 @@ get_type_definition({user_type, Anno, Name, Args}, Env, Opts) -> false -> typelib:substitute_type_vars(Type0, VarMap) end, - {ok, Type2}; - not_found -> - not_found + {ok, Type2} end end. From 1c8d073090a08c1134b2210a47e005f39f22c90e Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Tue, 14 Mar 2023 23:55:52 +0100 Subject: [PATCH 11/18] Fix a self-check error in gradualizer_int:int_range_to_types/1 --- src/gradualizer_int.erl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/gradualizer_int.erl b/src/gradualizer_int.erl index d3fce004..a1c269f3 100644 --- a/src/gradualizer_int.erl +++ b/src/gradualizer_int.erl @@ -161,7 +161,7 @@ int_range_to_types({I, pos_inf}) when I > 1 -> [{type, erl_anno:new(0), range, [{integer, erl_anno:new(0), I} ,{integer, erl_anno:new(0), pos_inf}]}]; int_range_to_types({I, I}) -> - [range_bound(I)]; + [range_bound(?assert_type(I, integer()))]; int_range_to_types({pos_inf, _}) -> []; int_range_to_types({_, neg_inf}) -> []; int_range_to_types({I, J}) when is_integer(I) andalso is_integer(J) -> From edab7d35a7404450700fc089c829df2c29ee75eb Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Wed, 15 Mar 2023 00:14:16 +0100 Subject: [PATCH 12/18] Fix a self-check error in normalize_rec/2 and expand_builtin_aliases/1 --- src/typechecker.erl | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/typechecker.erl b/src/typechecker.erl index 6af1e86e..be56e4f1 100644 --- a/src/typechecker.erl +++ b/src/typechecker.erl @@ -888,7 +888,7 @@ normalize(Ty, Env) -> %% The third argument is a set of user types that we've already unfolded. %% It's important that we don't keep unfolding such types because it will %% lead to infinite recursion. --spec normalize_rec(type() | gradualizer_type:gr_range_bound(), env()) -> type(). +-spec normalize_rec(type(), env()) -> type(). normalize_rec({type, _, union, Tys}, Env) -> UnionSizeLimit = Env#env.union_size_limit, Types = flatten_unions(Tys, Env), @@ -933,13 +933,16 @@ normalize_rec({op, _, _, _Arg} = Op, _Env) -> normalize_rec({op, _, _, _Arg1, _Arg2} = Op, _Env) -> erl_eval:partial_eval(Op); normalize_rec({type, Ann, range, [T1, T2]}, Env) -> - {type, Ann, range, [normalize_rec(T1, Env), - normalize_rec(T2, Env)]}; + %% We can assert that T1 and T2 are valid type() instances, because they must be expressed in + %% Erlang type syntax. Infinities are not allowed there - it's a Gradualizer extension to allow + %% them as range bounds. + {type, Ann, range, [normalize_rec(?assert_type(T1, type()), Env), + normalize_rec(?assert_type(T2, type()), Env)]}; normalize_rec(Type, _Env) -> expand_builtin_aliases(Type). %% Replace built-in type aliases --spec expand_builtin_aliases(type() | gradualizer_type:gr_range_bound()) -> type(). +-spec expand_builtin_aliases(type()) -> type(). expand_builtin_aliases({var, Ann, '_'}) -> {type, Ann, any, []}; expand_builtin_aliases({type, Ann, term, []}) -> From 48962db103404fcd052fc795528ee8f525bdba41 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Wed, 15 Mar 2023 00:17:01 +0100 Subject: [PATCH 13/18] Fix a self-check error in compat_ty/4 --- src/typechecker.erl | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/typechecker.erl b/src/typechecker.erl index be56e4f1..5b46605e 100644 --- a/src/typechecker.erl +++ b/src/typechecker.erl @@ -418,16 +418,19 @@ compat_ty({type, _, map, Assocs1}, {type, _, map, Assocs2}, Seen, Env) -> %% if that's not the case, let's throw now. length(MandatoryAssocs1) == 0 andalso throw(nomatch), case lists:foldl(fun - (_Assoc1, {Seen1, Cs1}) -> {Seen1, Cs1}; - (Assoc1, nomatch) -> + %% TODO: {no, match} is yet another case of + %% the constraint solver "shape" limitation + (Assoc1, {no, match}) -> try compat(Assoc1, Assoc2, Seen2, Env) catch - nomatch -> nomatch - end - end, nomatch, MandatoryAssocs1) + nomatch -> {no, match} + end; + (_Assoc1, {Seen1, Cs1}) -> + {Seen1, Cs1} + end, {no, match}, MandatoryAssocs1) of - nomatch -> throw(nomatch); + {no, match} -> throw(nomatch); {Seen1, Cs1} -> {Seen1, constraints:combine(Cs1, Cs2)} end end, ret(Seen), MandatoryAssocs2), From 38639152fc50be0434fcc0ca05b08138598199f2 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Wed, 15 Mar 2023 00:48:13 +0100 Subject: [PATCH 14/18] Fix a self-check error in expect_fun_type1/3 --- src/typechecker.erl | 42 +++++++++++++++++------------------------- 1 file changed, 17 insertions(+), 25 deletions(-) diff --git a/src/typechecker.erl b/src/typechecker.erl index 5b46605e..d58e659a 100644 --- a/src/typechecker.erl +++ b/src/typechecker.erl @@ -1366,7 +1366,7 @@ allow_empty_list(Ty) -> -type fun_ty_simple() :: {fun_ty, [type()], type(), constraints()}. -type fun_ty_intersection() :: {fun_ty_intersection, [fun_ty_simple()], constraints()}. --type fun_ty_union() :: {fun_ty_union, [fun_ty_simple()], constraints()}. +-type fun_ty_union() :: {fun_ty_union, [fun_ty()], constraints()}. %% Categorizes a function type. %% Normalizes the type (expand user-def and remote types). Errors for non-fun @@ -1390,22 +1390,12 @@ expect_fun_type(Env, Type, Arity) -> expect_fun_type1(Env, BTy = {type, _, bounded_fun, [Ft, _Fc]}, Arity) -> Sub = bounded_type_subst(Env, BTy), Ft = ?assert_type(Ft, type()), - case expect_fun_type1(Env, Ft, Arity) of - {fun_ty, ArgsTy, ResTy, Cs} -> - {{Args, Res}, CsI} = instantiate_fun_type(subst_ty(Sub, ArgsTy), - subst_ty(Sub, ResTy)), - {fun_ty, Args, Res, constraints:combine(Cs, CsI)}; - {fun_ty_intersection, Tys, Cs} -> - {InstTys, CsI} = instantiate_fun_type(subst_ty(Sub, Tys)), - {fun_ty_intersection, InstTys, constraints:combine(Cs, CsI)}; - {fun_ty_union, Tys, Cs} -> - {InstTys, CsI} = instantiate_fun_type(subst_ty(Sub, Tys)), - {fun_ty_union, InstTys, constraints:combine(Cs, CsI)}; - Err -> - Err - end; + {fun_ty, ArgsTy, ResTy, Cs} = expect_fun_type1(Env, Ft, Arity), + {{Args, Res}, CsI} = instantiate_fun_type(subst_ty(Sub, ArgsTy), + subst_ty(Sub, ResTy)), + {fun_ty, Args, Res, constraints:combine(Cs, CsI)}; expect_fun_type1(_Env, {type, _, 'fun', [{type, _, product, ArgsTy}, ResTy]}, _Arity) -> - {fun_ty, ArgsTy, ResTy, constraints:empty()}; + {fun_ty, ArgsTy, ?assert_type(ResTy, type()), constraints:empty()}; expect_fun_type1(_Env, {type, _, 'fun', []}, Arity) -> ArgsTy = lists:duplicate(Arity, type(any)), ResTy = type(any), @@ -1439,8 +1429,8 @@ expect_fun_type1(_Env, {var, _, Var}, Arity) -> ArgsTy = lists:duplicate(Arity, type(any)), ResTyVar = gradualizer_tyvar:new(Var, ?MODULE, ?LINE), ResTy = {var, erl_anno:new(0), ResTyVar}, - ResTyUpper = {type, erl_anno:new(0), 'fun', [{type, erl_anno:new(0), any}, - {var, erl_anno:new(0), ResTy}]}, + AnyArgs = {type, erl_anno:new(0), any}, + ResTyUpper = {type, erl_anno:new(0), 'fun', [AnyArgs, ResTy]}, Cs = constraints:add_var(ResTyVar, constraints:upper(Var, ResTyUpper)), {fun_ty, ArgsTy, ResTy, Cs}; expect_fun_type1(_Env, {type, _, any, []}, Arity) -> @@ -1453,19 +1443,26 @@ expect_fun_type1(_Env, ?top(), Arity) -> expect_fun_type1(_Env, _Ty, _Arity) -> type_error. --spec expect_intersection_type(env(), [tuple()], arity()) -> [fun_ty()] | type_error. +-spec expect_intersection_type(env(), [tuple()], arity()) -> [fun_ty_simple()] | type_error. expect_intersection_type(_Env, [], _Arity) -> []; expect_intersection_type(Env, [FunTy|Tys], Arity) -> case expect_fun_type1(Env, FunTy, Arity) of type_error -> type_error; + {fun_ty_intersection, _, _} -> + %% We can't have a multi-clause spec clause within a multi-clause spec + type_error; + {fun_ty_union, _, _} -> + %% We can't have a union of functions as a spec clause + type_error; Ty -> + Ty = ?assert_type(Ty, fun_ty_simple()), case expect_intersection_type(Env, Tys, Arity) of type_error -> type_error; Tyss -> - [Ty|Tyss] + [Ty | Tyss] end end. @@ -3624,11 +3621,6 @@ instantiate_fun_type(Args, Res) -> {NewRes , ResVars, _Map} = instantiate(Res, Map), {{NewArgs, NewRes}, constraints:vars(maps:merge(ArgVars, ResVars))}. --spec instantiate_fun_type([type()]) -> {[type()], constraints:t()}. -instantiate_fun_type(Tys) -> - {NewTys, Vars, _Map} = instantiate_inner(Tys, #{}), - {NewTys, constraints:vars(Vars)}. - -type instantiate_retval(T) :: {T, constraints:mapset(constraints:var()), #{constraints:var() => type()}}. From 57a07c2da7017d49d3f1d975b0b823411e05b870 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Wed, 15 Mar 2023 09:52:27 +0100 Subject: [PATCH 15/18] Fix a self-check error in type_check_list_op_in/3 and add test/should_pass/list_op_pass.erl --- src/typechecker.erl | 4 ++++ test/should_fail/list_op.erl | 14 -------------- test/should_pass/list_op_pass.erl | 14 ++++++++++++++ 3 files changed, 18 insertions(+), 14 deletions(-) create mode 100644 test/should_pass/list_op_pass.erl diff --git a/src/typechecker.erl b/src/typechecker.erl index d58e659a..24a67602 100644 --- a/src/typechecker.erl +++ b/src/typechecker.erl @@ -3191,6 +3191,10 @@ list_op_arg_types(ListOp, {type, _, union, Tys}) -> {Arg1Tys, Arg2Tys} = lists:unzip(Pairs), {type(union, Arg1Tys), type(union, Arg2Tys)} end; +list_op_arg_types(_ListOp, {var, _, _TyVar}) -> + %% TODO: we should create new type vars for the operands like arith_op_arg_types/2 does + %% and constrain them appropriately, but for now we just approximate with any() + {type(any), type(any)}; list_op_arg_types('++', Ty) -> case list_view(Ty) of false -> false; diff --git a/test/should_fail/list_op.erl b/test/should_fail/list_op.erl index 0409197c..7d67b0fb 100644 --- a/test/should_fail/list_op.erl +++ b/test/should_fail/list_op.erl @@ -1,10 +1,8 @@ -module(list_op). -export([append_right_error/1, append_left_error/1, - append/0, subtract/1, subtract/2, - subtract/0, subtract2/1, subtract2/2]). @@ -14,12 +12,6 @@ append_right_error(X) -> [1] ++ X. -spec append_left_error(integer()) -> _ | integer(). append_left_error(X) -> X ++ [1]. -%% FIXME checking this function used to crash -%% now it returns the following error -%% "The operator '++' is expected to have type _TyVar-* which is too precise to be statically checked" -append() -> - lists:foldl(fun(X, A) -> A ++ [X] end, [], []). - -spec subtract([a]) -> {ok, [a]}. subtract(Xs) -> Xs -- Xs. @@ -35,9 +27,3 @@ subtract2(Xs) -> subtract2(Xs, Ys) -> A = Xs -- Ys, A. - -%% FIXME checking this function used to crash -%% now it returns the following error -%% "The operator '--' is expected to have type _TyVar-* which is too precise to be statically checked" -subtract() -> - lists:foldl(fun(X, A) -> A -- [X] end, [], []). diff --git a/test/should_pass/list_op_pass.erl b/test/should_pass/list_op_pass.erl new file mode 100644 index 00000000..167d639a --- /dev/null +++ b/test/should_pass/list_op_pass.erl @@ -0,0 +1,14 @@ +-module(list_op_pass). + +-export([append/0, + subtract/0]). + +%% Checking this function used to crash. +%% Now that we approximate type vars for list ops with any, it passes. +append() -> + lists:foldl(fun(X, A) -> A ++ [X] end, [], []). + +%% Checking this function used to crash. +%% Now that we approximate type vars for list ops with any, it passes. +subtract() -> + lists:foldl(fun(X, A) -> A -- [X] end, [], []). From 5a68b968cb020131b7031f3ed43da52191cd1047 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Wed, 15 Mar 2023 10:08:33 +0100 Subject: [PATCH 16/18] Fail CI if ERROR_LINES is non-zero --- .github/workflows/self-check.yml | 6 +++--- Makefile | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/self-check.yml b/.github/workflows/self-check.yml index 656680e3..4369d141 100644 --- a/.github/workflows/self-check.yml +++ b/.github/workflows/self-check.yml @@ -26,10 +26,10 @@ jobs: - name: "Assess self check result" run: | ERROR_LINES=$(wc -l gradualize.log | awk '{print $1}') - if [ $ERROR_LINES -lt 100 ]; then - echo "ok, self reported errors are in check: $ERROR_LINES < 100" + if [ $ERROR_LINES -eq 0 ]; then + echo "ok, there are no self-check errors: $ERROR_LINES == 0" exit 0 else - echo "we've regressed, failing the job: $ERROR_LINES >= 100" + echo "we've regressed, failing the job: $ERROR_LINES != 0" exit 1 fi diff --git a/Makefile b/Makefile index ab91441d..8485ff54 100644 --- a/Makefile +++ b/Makefile @@ -90,7 +90,7 @@ bin/gradualizer: $(beams) ebin/gradualizer.app .PHONY: gradualize gradualize: escript - bin/gradualizer --infer --solve_constraints --specs_override_dir priv/extra_specs/ \ + @bin/gradualizer --infer --solve_constraints --specs_override_dir priv/extra_specs/ \ -pa ebin --color ebin | grep -v -f gradualize-ignore.lst .PHONY: nocrashongradualize From 3e3123916ac9486ee8fbd6e78ddceecec24b10e0 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Wed, 15 Mar 2023 15:21:35 +0100 Subject: [PATCH 17/18] Explain gradualizer_type.erl direct inheritance from OTP's erl_parse.yrl --- src/gradualizer_type.erl | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/gradualizer_type.erl b/src/gradualizer_type.erl index e9441818..b7e096d8 100644 --- a/src/gradualizer_type.erl +++ b/src/gradualizer_type.erl @@ -1,7 +1,9 @@ %% @private -%% This file was automatically generated from the file "erl_parse.yrl". +%% This file is closely resembles Erlang/OTP's "erl_parse.yrl", the Erlang yecc grammar. +%% However, it contains Gradualizer-specific modifications. +%% These are denoted by a `gr_' prefix, instead of an `af_' prefix. %% -%% Copyright Ericsson AB 1996-2018. All Rights Reserved. +%% Copyright Ericsson AB 1996-2023. All Rights Reserved. %% %% Licensed under the Apache License, Version 2.0 (the "License"); %% you may not use this file except in compliance with the License. From 49e695b2253c04232a859c7f361a67d9c4f1af3e Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Wed, 15 Mar 2023 15:39:40 +0100 Subject: [PATCH 18/18] Add a test for the solver 'shape sensitivity' to test/known_problems/should_pass/poly_should_pass.erl --- test/known_problems/should_pass/poly_should_pass.erl | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/test/known_problems/should_pass/poly_should_pass.erl b/test/known_problems/should_pass/poly_should_pass.erl index b40a313e..b4fa014a 100644 --- a/test/known_problems/should_pass/poly_should_pass.erl +++ b/test/known_problems/should_pass/poly_should_pass.erl @@ -3,7 +3,8 @@ -gradualizer([solve_constraints]). -export([find1/0, - l/0]). + l/0, + solver_sensitive_to_shape/1]). -spec lookup(T1, [{T1, T2}]) -> (none | T2). lookup(_, []) -> none; @@ -54,3 +55,10 @@ has_intersection_spec(T) -> T. -spec return_list_of_unions(list_of_unions()) -> list_of_unions(). return_list_of_unions(_L) -> []. + +-spec solver_sensitive_to_shape(#{tuple := {a, b}}) -> ok. +solver_sensitive_to_shape(M) -> + case maps:get(tuple, M, not_found) of + not_found -> ok; + {a, b} -> ok + end.