diff --git a/notes.1.md b/notes.1.md new file mode 100644 index 00000000..68d5a75f --- /dev/null +++ b/notes.1.md @@ -0,0 +1,72 @@ +These are some experiments with the disjunctive normal form we mentioned +in https://github.com/josefs/Gradualizer/pull/524#discussion_r1200493035. + +First, https://typex.fly.dev/ seems to actually call CDuce under the hood. +This can be inferred from the following error message generated based on some invalid input. +Input: + +``` +g :: (_ -> {:t, :a} | {:t, :b}) +def g(_), do: {:t, :b} + +tuple_case :: (_ -> {:t, :a or :b}) +def tuple_case(arg), do: g(arg) + +tuple_case(:z) +``` + +Message: + +``` +Typing error: +After extracting domain types from + { _fun =[Any] -> |({ _tup=[`t `a] ; _size=2 }, { _tup=[`t `b] ; _size=2 }) ; _ari = 1 } +Failed to parse the result: + Cduce_core.Parser.MenhirBasics.Error <-------------- Cduce error +``` + +Second, let's consider: + +```erlang +-spec g() -> {t, a | b}. +g() -> {t, a}. + +-spec tuple_case1() -> {t, a} | {t, b}. +tuple_case1() -> + R = g(), + R. + +-spec tuple_case2() -> {t, a} | {t, b}. +tuple_case2() -> + g(). +``` + +The following equivalent examples were tested with https://typex.fly.dev/: + +``` +g :: (_ -> {:t, :a or :b}) +def g(_), do: {:t, :b} + +tuple_case :: (_ -> {:t, :a} or {:t, :b}) +def tuple_case(arg), do: g(arg) + +tuple_case(:z) +``` + +``` +g :: (_ -> {:t, :a} or {:t, :b}) +def g(_), do: {:t, :b} + +tuple_case :: (_ -> {:t, :a or :b}) +def tuple_case(arg), do: g(arg) + +tuple_case(:z) +``` + +They both typecheck. +This means that the Elixir prototype based on CDuce does indeed +treat {t, a | b} :: {t, a} | {t, b} +as well as {t, a} | {t, b} :: {t, a | b}. + +This can be achieved to some extent in Gradualizer, too, +but it comes with significant breakage of tests. diff --git a/src/typechecker.erl b/src/typechecker.erl index 873dc9d9..9c3df3e6 100644 --- a/src/typechecker.erl +++ b/src/typechecker.erl @@ -1022,6 +1022,7 @@ expand_builtin_aliases({type, Ann, iolist, []}) -> {type, Ann, iolist, []}], Tail = [{type, Ann, nil, []}, {type, Ann, binary, []}], + %% TODO: dnf {type, Ann, maybe_improper_list, [{type, Ann, union, Union}, {type, Ann, union, Tail}]}; expand_builtin_aliases({type, Ann, map, any}) -> @@ -1055,6 +1056,34 @@ expand_builtin_aliases({type, Ann, no_return, []}) -> %% TODO: This is a kludge by which lists of types slip through calls to normalize(). %% Specifically, lists of Types representing bounded fun clauses. expand_builtin_aliases(Type) -> + dnf(Type). + %Type. + +-spec dnf(_) -> any(). +dnf(?type(union, _) = Ty) -> + Ty; +dnf({type, _, _, any} = Ty) -> + Ty; +%% A list of unions is not the same as a union of lists. +dnf({type, _, list, _} = Ty) -> + Ty; +dnf({type, Anno, Tag, Args} = Ty0) -> + {ArgExpandedUnions, AnyExpanded} = + lists:foldr(fun + (?type(union, Tys), {Acc, _}) -> + {[Tys | Acc], true}; + (Ty, {Acc, AnyExpanded}) -> + {[[Ty] | Acc], AnyExpanded} + end, + {[], false}, Args), + ArgTyCombinations = gradualizer_lib:cartesian_product(ArgExpandedUnions), + if + AnyExpanded -> + {type, Anno, union, [ {type, Anno, Tag, A} || A <- ArgTyCombinations ]}; + not AnyExpanded -> + Ty0 + end; +dnf(Type) -> Type. %% Flattens nested unions @@ -2601,14 +2630,16 @@ do_type_check_expr_in(Env, ResTy, {tuple, _, TS} = Tup) -> {VBs, Css} = lists:unzip([ type_check_expr_in(Env, Ty, Expr) || {Ty, Expr} <- lists:zip(Tys, TS) ]), {union_var_binds(VBs, Env), constraints:combine([Cs|Css])}; - {elem_tys, Tyss, Cs} -> - case type_check_tuple_union_in(Env, Tyss, TS) of - none -> - {Ty, _VB, _Cs} = type_check_expr(Env#env{infer = true}, Tup), - throw(type_error(Tup, Ty, ResTy)); - {VBs, Css} -> - {union_var_binds(VBs, Env), constraints:combine([Cs|Css])} - end; + {elem_tys, _Tyss, Cs1} -> + %% ResTy dictates that we expect a union of tuples. + {TupTy, VB, Cs2} = type_check_expr(Env, Tup), + Cs3 = case subtype(TupTy, ResTy, Env) of + {true, Cs} -> + Cs; + false -> + throw(type_error(Tup, TupTy, ResTy)) + end, + {VB, constraints:combine([Cs1, Cs2, Cs3])}; any -> {_Tys, VBs, Css} = lists:unzip3([type_check_expr(Env, Expr) || Expr <- TS ]), @@ -3583,19 +3614,6 @@ type_check_union_in1(Env, [Ty|Tys], Expr) -> type_check_union_in1(_Env, [], _Expr) -> none. --spec type_check_tuple_union_in(env(), [[type()]], [expr()]) -> R when - R :: {[env()], [constraints:t()]} | none. -type_check_tuple_union_in(Env, [Tys|Tyss], Elems) -> - try - lists:unzip([type_check_expr_in(Env, Ty, Expr) - || {Ty, Expr} <- lists:zip(Tys, Elems)]) - catch - E when element(1,E) == type_error -> - type_check_tuple_union_in(Env, Tyss, Elems) - end; -type_check_tuple_union_in(_Env, [], _Elems) -> - none. - -spec get_bounded_fun_type_list(atom(), arity(), env(), anno()) -> [type()]. get_bounded_fun_type_list(Name, Arity, Env, P) -> case maps:find({Name, Arity}, Env#env.fenv) of diff --git a/test/known_problems/should_pass/inner_union_subtype_of_root_union.erl b/test/known_problems/should_pass/inner_union_subtype_of_root_union.erl index bdb92baa..20a8b0f4 100644 --- a/test/known_problems/should_pass/inner_union_subtype_of_root_union.erl +++ b/test/known_problems/should_pass/inner_union_subtype_of_root_union.erl @@ -1,6 +1,6 @@ -module(inner_union_subtype_of_root_union). --export([tuple_case/0, map_case/1]). +-export([map_case/1]). % The problem is that {t, a|b} is not subtype of {t, a} | {t, b}. @@ -10,13 +10,11 @@ % {'type', anno(), 'map_field_assoc', [abstract_type()]} % | {'type', anno(), 'map_field_exact', [abstract_type()]} +% See also test/should_pass/inner_union_subtype_of_root_union_pass.erl + -spec g() -> a | b. g() -> a. --spec tuple_case() -> {t, a} | {t, b}. -tuple_case() -> - {t, g()}. - % The same thing holds for maps. -spec map_case(#{a => b | c}) -> #{a => b} | #{a => c}. -map_case(M) -> M. \ No newline at end of file +map_case(M) -> M. 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..1fa02266 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,6 @@ -module(refine_bound_var_with_guard_should_pass). --export([f/1]). +-export([f/1, g/1]). %% 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 diff --git a/test/should_fail/tuple_union_fail.erl b/test/should_fail/tuple_union_fail.erl index a510e3ff..1bb6f847 100644 --- a/test/should_fail/tuple_union_fail.erl +++ b/test/should_fail/tuple_union_fail.erl @@ -3,6 +3,8 @@ -export([f/0]). -export([tuple_union/0]). +-gradualizer([infer]). + -spec f() -> {integer()} | {boolean()}. f() -> {apa}. diff --git a/test/should_pass/inner_union_subtype_of_root_union_pass.erl b/test/should_pass/inner_union_subtype_of_root_union_pass.erl new file mode 100644 index 00000000..de237e2e --- /dev/null +++ b/test/should_pass/inner_union_subtype_of_root_union_pass.erl @@ -0,0 +1,26 @@ +-module(inner_union_subtype_of_root_union_pass). + +-export([tuple_case1/0, + tuple_case2/0]). + +% The problem is that {t, a|b} is not subtype of {t, a} | {t, b}. + +% It has surfaced because +% {'type', anno(), 'map_field_assoc' | 'map_field_exact', [abstract_type()]} +% is not a subtype of +% {'type', anno(), 'map_field_assoc', [abstract_type()]} +% | {'type', anno(), 'map_field_exact', [abstract_type()]} + +% See also test/known_problems/should_pass/inner_union_subtype_of_root_union.erl + +-spec g() -> a | b. +g() -> a. + +-spec tuple_case1() -> {t, a} | {t, b}. +tuple_case1() -> + R = {t, g()}, + R. + +-spec tuple_case2() -> {t, a} | {t, b}. +tuple_case2() -> + {t, g()}. diff --git a/test/typechecker_tests.erl b/test/typechecker_tests.erl index e48b60e2..2429ff20 100644 --- a/test/typechecker_tests.erl +++ b/test/typechecker_tests.erl @@ -76,7 +76,14 @@ subtype_test_() -> ?_assert(subtype(?t( 1..5 ), ?t( 1..3|4..6 ))), ?_assert(subtype(?t( 1..5|a ), ?t( 1..3|4..6|atom() ))), ?_assert(subtype(?t( a|b ), ?t( atom() ))), - ?_assert(subtype(?t( (A :: boolean())|(B :: boolean()) ), ?t( boolean() ))), + ?_assert(subtype(?t( (A :: boolean())|(B :: boolean()) ), + ?t( boolean() ))), + ?_assert(subtype(?t( {t, a|b} ), ?t( {t, a} | {t, b} ))), + ?_assert(subtype(?t( {t, a} | {t, b} ), ?t( {t, a|b} ))), + ?_assert(subtype(?t( {t, a|b, 1|2} ), + ?t( {t, a, 1} | {t, a, 2} | {t, b, 1} | {t, b, 2} ))), + ?_assert(subtype(?t( {t, a, 1} | {t, a, 2} | {t, b, 1} | {t, b, 2} ), + ?t( {t, a|b, 1|2} ))), %% Lists ?_assert(subtype(?t( [a] ), ?t( list() ))), @@ -164,6 +171,13 @@ not_subtype_test_() -> ?_assertNot(subtype(?t( {} ), ?t( {any()} ))), ?_assertNot(subtype(?t( {1..2, 3..4} ), ?t( {1, 3} ))), + ?_assertNot(subtype(?t( {t, a|b} ), ?t( {t, a} ))), + ?_assertNot(subtype(?t( {t, a} | {t, b} ), ?t( {t, a} ))), + ?_assertNot(subtype(?t( {t, a|b, 1|2} ), + ?t( {t, a, 1} | {t, b, 1} ))), + ?_assertNot(subtype(?t( {t, a, 1} | {t, a, 2} | {t, b, 1} | {t, b, 2} ), + ?t( {t, a|b, 1} ))), + %% Maps ?_assertNot(subtype(?t( #{} ), ?t( #{a := b} ))), ?_assertNot(subtype(?t( #{a => b} ), ?t( #{a := b} ))),