From 86d5f76019846512d566780c13e18a39f8ea8267 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Thu, 12 Jan 2023 23:01:45 +0100 Subject: [PATCH 1/3] Add test to test/known_problems/should_pass/poly_should_pass.erl This is modelled after the same error in gradualizer_db:collects_specs/2. --- .../should_pass/poly_should_pass.erl | 39 ++++++++++++++++++- 1 file changed, 38 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 05a685b5..ef8511a0 100644 --- a/test/known_problems/should_pass/poly_should_pass.erl +++ b/test/known_problems/should_pass/poly_should_pass.erl @@ -2,7 +2,8 @@ -gradualizer([solve_constraints]). --export([find1/0]). +-export([find1/0, + l/0]). -spec lookup(T1, [{T1, T2}]) -> (none | T2). lookup(_, []) -> none; @@ -15,3 +16,39 @@ 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 `takes_an_intersection/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. +-spec l() -> [t1() | t2()]. +l() -> + lists:map(fun takes_an_intersection/1, return_list_of_unions([])). + +-spec takes_an_intersection(t1() | t2()) -> t1() | t2(); + (list()) -> [t1() | t2()]. +takes_an_intersection([]) -> []; +takes_an_intersection([_|_] = L) -> lists:map(fun takes_an_intersection/1, L); +takes_an_intersection(T) -> T. + +-spec return_list_of_unions(list_of_unions()) -> list_of_unions(). +return_list_of_unions(_L) -> []. From 0fd78c86de927bf470acbfb2fa34e5c33c53da56 Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Thu, 12 Jan 2023 23:05:28 +0100 Subject: [PATCH 2/3] Add test to test/should_pass/poly_pass.erl --- .../should_pass/poly_should_pass.erl | 2 ++ test/should_pass/poly_pass.erl | 17 ++++++++++++++++- 2 files changed, 18 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 ef8511a0..709a00d7 100644 --- a/test/known_problems/should_pass/poly_should_pass.erl +++ b/test/known_problems/should_pass/poly_should_pass.erl @@ -40,6 +40,8 @@ find1() -> %% 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 takes_an_intersection/1, return_list_of_unions([])). diff --git a/test/should_pass/poly_pass.erl b/test/should_pass/poly_pass.erl index dcf99940..c357f726 100644 --- a/test/should_pass/poly_pass.erl +++ b/test/should_pass/poly_pass.erl @@ -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]). @@ -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) -> []. From efb8072272904588985311d25e55d835115f9e5e Mon Sep 17 00:00:00 2001 From: Radek Szymczyszyn Date: Fri, 13 Jan 2023 15:30:05 +0100 Subject: [PATCH 3/3] Rename test functions which have, not take, an intersection type --- test/known_problems/should_pass/poly_should_pass.erl | 12 ++++++------ test/should_fail/poly_union_lower_bound_fail.erl | 10 +++++----- test/should_pass/poly_lists_map_constraints_pass.erl | 8 ++++---- 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/test/known_problems/should_pass/poly_should_pass.erl b/test/known_problems/should_pass/poly_should_pass.erl index 709a00d7..b40a313e 100644 --- a/test/known_problems/should_pass/poly_should_pass.erl +++ b/test/known_problems/should_pass/poly_should_pass.erl @@ -28,7 +28,7 @@ find1() -> %% %% Now, why is that the case? %% `return_list_of_unions/1' returns just that - a list of `t1() | t2()' unions. -%% This means that `takes_an_intersection/1' passed in to `lists:map/2' would be called with +%% 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()]'. @@ -44,13 +44,13 @@ find1() -> %% See also `l/0' in `test/should_pass/poly_pass.erl'. -spec l() -> [t1() | t2()]. l() -> - lists:map(fun takes_an_intersection/1, return_list_of_unions([])). + lists:map(fun has_intersection_spec/1, return_list_of_unions([])). --spec takes_an_intersection(t1() | t2()) -> t1() | t2(); +-spec has_intersection_spec(t1() | t2()) -> t1() | t2(); (list()) -> [t1() | t2()]. -takes_an_intersection([]) -> []; -takes_an_intersection([_|_] = L) -> lists:map(fun takes_an_intersection/1, L); -takes_an_intersection(T) -> T. +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) -> []. diff --git a/test/should_fail/poly_union_lower_bound_fail.erl b/test/should_fail/poly_union_lower_bound_fail.erl index 73c974f8..9f065580 100644 --- a/test/should_fail/poly_union_lower_bound_fail.erl +++ b/test/should_fail/poly_union_lower_bound_fail.erl @@ -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). diff --git a/test/should_pass/poly_lists_map_constraints_pass.erl b/test/should_pass/poly_lists_map_constraints_pass.erl index 08b5d6f5..c3752010 100644 --- a/test/should_pass/poly_lists_map_constraints_pass.erl +++ b/test/should_pass/poly_lists_map_constraints_pass.erl @@ -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.