Unsettling dialyzer errors

[Josef Svenningsson]

On Sun, Feb 28, 2021 at 3:49 PM Kostis Sagonas <kostis@REDACTED> wrote:

> 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 ?
>
> No, Gradualizer is not saying that foo/1 should take arguments of type
t1(). It's saying that the program calls f1/1 with a variable of type
t1()|t2() but the declared type of f1/1 only accepts arguments of t1().
Hence the error.
Gradualizer looks at the declared types of functions and will report an
error if there is an incompatibility, but it doesn't "expect" the types to
be anything.


> 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).
>
> Gradualizer does complain about all functions but in different ways.

Josef


>
> Kostis
>
> >
> > On Sat, Feb 27, 2021 at 9:50 AM Nicolas Martyanoff <khaelin@REDACTED
> > <mailto:khaelin@REDACTED>> 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].
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20210228/1f444b9c/attachment.htm>