<div dir="ltr">I tried following up a little. Excuse me if there is any discrepancy as I am beginning to run dialyzer from now on.<div><br></div><div>I exported f1 and f2, and it resulted in the following:</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><font size="4"><i>Proceeding with analysis...<br></i></font><font size="4"><i>dialyzer_issue.erl:24: The call dialyzer_issue:f2<br></i></font><font size="4"><i>         (V :: 'a' | 'b') breaks the contract<br> </i></font><font size="4"><i>          (t2()) -> {'ok', integer()} | 'error'<br></i></font><font size="4"><i> done in 0m0.27s<br></i></font><font size="4"><i>done (warnings were emitted)</i></font></blockquote><div><br></div><div>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. </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Feb 27, 2021 at 4:18 PM Kostis Sagonas <<a href="mailto:kostis@cs.ntua.gr">kostis@cs.ntua.gr</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2/27/21 10:50 AM, Nicolas Martyanoff wrote:<br>
> <br>
> I have come across Dialyzer errors which feel incorrect to me. I<br>
> managed to reproduce the problem with a minimal example:<br>
> <br>
>      -module(dialyzer_issue).<br>
>      <br>
>      -export([foo/1]).<br>
>      <br>
>      -type t1() :: a | b.<br>
>      -type t2() :: x | y.<br>
>      <br>
>      -spec f1(t1()) -> {ok, integer()} | error.<br>
>      f1(a) -> {ok, 1};<br>
>      f1(b) -> {ok, 2};<br>
>      f1(_) -> error.<br>
>      <br>
>      -spec f2(t2()) -> {ok, integer()} | error.<br>
>      f2(x) -> {ok, 3};<br>
>      f2(y) -> {ok, 4};<br>
>      f2(_) -> error.<br>
>      <br>
>      -spec foo(t1() | t2()) -> integer().<br>
>      foo(V) -><br>
>        case f1(V) of<br>
>          {ok, N1} -><br>
>            N1;<br>
>          error -><br>
>            case f2(V) of<br>
>              {ok, N2} -><br>
>                N2;<br>
>              error -><br>
>                0<br>
>            end<br>
>        end.<br>
> <br>
> The code works as expected:<br>
> [dialyzer_issue:foo(N) || N <- [a, b, c, x, y, z]] evaluates to [1,2,0,3,4,0].<br>
> <br>
> Running Dialyzer (OTP 23.2.2) produces the following errors:<br>
> <br>
> dialyzer_issue.erl:13: Invalid type specification for function dialyzer_issue:f2/1. The success typing is<br>
>            ('a' | 'b') -> 'error'<br>
> dialyzer_issue.erl:14: The pattern<br>
>            'x' can never match the type<br>
>            'a' | 'b'<br>
> dialyzer_issue.erl:15: The pattern<br>
>            'y' can never match the type<br>
>            'a' | 'b'<br>
> dialyzer_issue.erl:24: The call dialyzer_issue:f2<br>
>           (V :: 'a' | 'b') breaks the contract<br>
>            (t2()) -> {'ok', integer()} | 'error'<br>
> <br>
> It feels wrong to me: foo/1 first calls f1/1 which will always return<br>
> a value of type {ok, integer()} for (V :: a | b), therefore f2/1 cannot<br>
> be called for a or b. Since the argument of foo/1 is of type<br>
> t1() | t2(), I would expect Dialyzer to correctly infer that f2/1 can<br>
> only be called with a value of type t2(), since it cannot be called with<br>
> a value of type t1().<br>
> <br>
> The other errors are even more nonsensical but I imagine they derive<br>
> from the apparently incorrect last inference.<br>
> <br>
> I am used to Dialyzer always turning out to be right, but I cannot wrap<br>
> my head around this one. Does anyone here see what the problem is ?<br>
<br>
Yes.<br>
<br>
The problem is that you have constrained the input arguments of f1/1 and <br>
f2/1 too much -- e.g., you have specified that f1/1 only accepts a | b, <br>
so dialyzer can disregard the third clause and also the 'error' atom as <br>
a return value; similarly for f2/1. Note that returning the atom 'error'<br>
on all terms other than a | b is not the same as not-returning, i.e., <br>
not succeeding.<br>
<br>
To fix the issue, simply change the specs of f1/1 and f2/2 to accept <br>
term() as the type of their argument.<br>
<br>
Better yet, since you are only exporting foo/1 from this module, do NOT <br>
write specs for f1/1 and f2/2 and simply let dialyzer do its magic.<br>
<br>
<br>
Kostis<br>
</blockquote></div>