Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Constraint solver limitation known problem test and a workaround #503

Merged
merged 3 commits into from
Jan 13, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 40 additions & 1 deletion test/known_problems/should_pass/poly_should_pass.erl
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,8 @@

-gradualizer([solve_constraints]).

-export([find1/0]).
-export([find1/0,
l/0]).

-spec lookup(T1, [{T1, T2}]) -> (none | T2).
lookup(_, []) -> none;
Expand All @@ -15,3 +16,41 @@ find1() ->
none -> "default";
V -> V
end.

-type t1() :: {}.
-type t2() :: binary().
-type list_of_unions() :: [t1() | t2()].

%% This fails with:
%%
%% Lower bound [t1() | t2()] of type variable B_typechecker_3529_12 on line 25
%% is not a subtype of t1() | t2()
%%
%% Now, why is that the case?
%% `return_list_of_unions/1' returns just that - a list of `t1() | t2()' unions.
%% This means that `has_intersection_spec/1' passed in to `lists:map/2' would be called with
%% a union as the arg, not a list.
%% This should mean that it would also return a `t1() | t2()' union, so the final return value from
%% `l/0' should be `[t1() | t2()]'.
%% However, the constraint solver is not able to tell that only one clause of the
%% multi-clause spec would suffice and it uses both clauses' return types as lower bound on `B'.
%%
%% In practice, this means that we should avoid functions
%% with intersection types like `(a()) -> b() & ([a()]) -> [b()]',
%% because the constraint solver can't cope with them.
%% We should instead define two separate functions: `(a()) -> b()' and `([a()]) -> [b()]',
%% and check outside of them which to call based on the type of the parameter.
%%
%% See also `l/0' in `test/should_pass/poly_pass.erl'.
-spec l() -> [t1() | t2()].
l() ->
lists:map(fun has_intersection_spec/1, return_list_of_unions([])).

-spec has_intersection_spec(t1() | t2()) -> t1() | t2();
(list()) -> [t1() | t2()].
has_intersection_spec([]) -> [];
has_intersection_spec([_|_] = L) -> lists:map(fun has_intersection_spec/1, L);
has_intersection_spec(T) -> T.

-spec return_list_of_unions(list_of_unions()) -> list_of_unions().
return_list_of_unions(_L) -> [].
10 changes: 5 additions & 5 deletions test/should_fail/poly_union_lower_bound_fail.erl
Original file line number Diff line number Diff line change
Expand Up @@ -28,13 +28,13 @@ takes_a_union(I) when is_integer(I) -> I.
%% on line 456 is not a subtype of binary() | integer()
-spec k([binary() | integer() | string()]) -> list().
k(L) ->
lists:map(fun takes_an_intersection/1, L).
lists:map(fun has_intersection_spec/1, L).

-spec takes_an_intersection(binary()) -> binary();
-spec has_intersection_spec(binary()) -> binary();
(integer()) -> integer().
takes_an_intersection(B) when is_binary(B) -> B;
takes_an_intersection(I) when is_integer(I) -> I.
has_intersection_spec(B) when is_binary(B) -> B;
has_intersection_spec(I) when is_integer(I) -> I.

-spec l([binary() | integer()]) -> [integer()].
l(L) ->
lists:map(fun takes_an_intersection/1, L).
lists:map(fun has_intersection_spec/1, L).
8 changes: 4 additions & 4 deletions test/should_pass/poly_lists_map_constraints_pass.erl
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,9 @@ map_specific_list(List) ->

-spec j([binary() | integer()]) -> list().
j(L) ->
lists:map(fun takes_an_intersection/1, L).
lists:map(fun has_intersection_spec/1, L).

-spec takes_an_intersection(binary()) -> binary();
-spec has_intersection_spec(binary()) -> binary();
(integer()) -> integer().
takes_an_intersection(B) when is_binary(B) -> B;
takes_an_intersection(I) when is_integer(I) -> I.
has_intersection_spec(B) when is_binary(B) -> B;
has_intersection_spec(I) when is_integer(I) -> I.
17 changes: 16 additions & 1 deletion test/should_pass/poly_pass.erl
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,8 @@
poly_pass/3]).

%% These examples don't come from the above paper.
-export([f/1]).
-export([f/1,
l/0]).

-gradualizer([solve_constraints]).

Expand All @@ -18,3 +19,17 @@ poly_pass(F, B1, B2) -> {F(B2), F(B1)}.
-spec f([integer(), ...]) -> integer().
f(L) ->
hd(L).

-type t1() :: {}.
-type t2() :: binary().
-type list_of_unions() :: [t1() | t2()].

-spec l() -> [t1() | t2()].
l() ->
lists:map(fun helper/1, return_list_of_unions([])).

-spec helper(t1() | t2()) -> t1() | t2().
helper(T) -> T.

-spec return_list_of_unions(list_of_unions()) -> list_of_unions().
return_list_of_unions(_L) -> [].