Re: Unsettling dialyzer errors

FWIW, here's what Gradualizer returns for your program:

dialyzer_issue.erl: The clause on line 11 at column 1 cannot be reached
> dialyzer_issue.erl: The clause on line 16 at column 1 cannot be reached
> dialyzer_issue.erl: The variable on line 20 at column 11 is expected to
> have type t1() but it has type a | b | x | y
> -spec foo(t1() | t2()) -> integer().
> foo(V) ->
>   case f1(V) of
>           ^
> nok


All the best,

Josef

On Sat, Feb 27, 2021 at 9:50 AM Nicolas Martyanoff <[email protected]>
wrote:

>
> Hi,
>
> I have come across Dialyzer errors which feel incorrect to me. I
> managed to reproduce the problem with a minimal example:
>
>     -module(dialyzer_issue).
>
>     -export([foo/1]).
>
>     -type t1() :: a | b.
>     -type t2() :: x | y.
>
>     -spec f1(t1()) -> {ok, integer()} | error.
>     f1(a) -> {ok, 1};
>     f1(b) -> {ok, 2};
>     f1(_) -> error.
>
>     -spec f2(t2()) -> {ok, integer()} | error.
>     f2(x) -> {ok, 3};
>     f2(y) -> {ok, 4};
>     f2(_) -> error.
>
>     -spec foo(t1() | t2()) -> integer().
>     foo(V) ->
>       case f1(V) of
>         {ok, N1} ->
>           N1;
>         error ->
>           case f2(V) of
>             {ok, N2} ->
>               N2;
>             error ->
>               0
>           end
>       end.
>
> The code works as expected:
> [dialyzer_issue:foo(N) || N <- [a, b, c, x, y, z]] evaluates to
> [1,2,0,3,4,0].
>
> Running Dialyzer (OTP 23.2.2) produces the following errors:
>
> dialyzer_issue.erl:13: Invalid type specification for function
> dialyzer_issue:f2/1. The success typing is
>           ('a' | 'b') -> 'error'
> dialyzer_issue.erl:14: The pattern
>           'x' can never match the type
>           'a' | 'b'
> dialyzer_issue.erl:15: The pattern
>           'y' can never match the type
>           'a' | 'b'
> dialyzer_issue.erl:24: The call dialyzer_issue:f2
>          (V :: 'a' | 'b') breaks the contract
>           (t2()) -> {'ok', integer()} | 'error'
>
> It feels wrong to me: foo/1 first calls f1/1 which will always return
> a value of type {ok, integer()} for (V :: a | b), therefore f2/1 cannot
> be called for a or b. Since the argument of foo/1 is of type
> t1() | t2(), I would expect Dialyzer to correctly infer that f2/1 can
> only be called with a value of type t2(), since it cannot be called with
> a value of type t1().
>
> The other errors are even more nonsensical but I imagine they derive
> from the apparently incorrect last inference.
>
> I am used to Dialyzer always turning out to be right, but I cannot wrap
> my head around this one. Does anyone here see what the problem is ?
>
> Thank you in advance.
>
> Regards,
>
> --
> Nicolas Martyanoff
> http://snowsyn.net
> [email protected]
>