Re: Unsettling dialyzer errors

On 2/28/21 11:39 AM, Josef Svenningsson wrote:
> 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

And the rationale for Gradualizer "expecting" foo/1 to have type t1() as 
argument is what exactly?  Simply that it calls f1/1 ?

Note that expecting/insisting the above is inconsistent both with

  - what the programmer has explicitly declared (i.e., that it has type 
t1() | t2())

and

  - the (erroneous) "expectation" on how the code should work (i.e. that 
[foo(N) || N <- [a, b, c, x, y, z]] evaluates to [1,2,0,3,4,0]) as 
explicitly mentioned below.

Just curious on how one decides that the error is in foo's type spec and 
not in f1/1's or f2/1 (or in both/all, as it is clearly the case here).


Kostis

> 
> On Sat, Feb 27, 2021 at 9:50 AM Nicolas Martyanoff <[email protected] 
> <mailto:[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].