Re: Unsettling dialyzer errors

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