Re: Unsettling dialyzer errors

Sorry to have missed one crucial point. Commenting out "case" on L24 and
removing exports, makes "f2" unused leading to a warning, Further to which,
commenting f2 makes the dialyzer happy, but putting a dummy call to f2(V),
in order to by-pass the warning, leads back to square 1.

Something fishy about f2. Got to get the head around it.

Thanks and Regards
Nalin Ranjan

On Sat, Feb 27, 2021 at 7:23 PM Nalin Ranjan <[email protected]> wrote:

> 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 <[email protected]> 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
>>
>