Unsettling dialyzer errors

[Nalin Ranjan]

I tried following up a little. Excuse me if there is any discrepancy as I
am beginning to run dialyzer from now on.

I exported f1 and f2, and it resulted in the following:


> *Proceeding with analysis...*
> *dialyzer_issue.erl:24: The call dialyzer_issue:f2*
> *         (V :: 'a' | 'b') breaks the contract *
> *          (t2()) -> {'ok', integer()} | 'error'*
> * done in 0m0.27s**done (warnings were emitted)*


Now I tried yet another thing. I commented out the nested "case" on L24
returning 'error' atom as the value, instead. This makes dialyzer happy.
But if I remove the exports, I am back to square 1.

On Sat, Feb 27, 2021 at 4:18 PM Kostis Sagonas <kostis@REDACTED> wrote:

> On 2/27/21 10:50 AM, Nicolas Martyanoff wrote:
> >
> > 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 ?
>
> Yes.
>
> The problem is that you have constrained the input arguments of f1/1 and
> f2/1 too much -- e.g., you have specified that f1/1 only accepts a | b,
> so dialyzer can disregard the third clause and also the 'error' atom as
> a return value; similarly for f2/1. Note that returning the atom 'error'
> on all terms other than a | b is not the same as not-returning, i.e.,
> not succeeding.
>
> To fix the issue, simply change the specs of f1/1 and f2/2 to accept
> term() as the type of their argument.
>
> Better yet, since you are only exporting foo/1 from this module, do NOT
> write specs for f1/1 and f2/2 and simply let dialyzer do its magic.
>
>
> Kostis
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20210227/42408556/attachment.htm>