<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Feb 28, 2021 at 3:49 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/28/21 11:39 AM, Josef Svenningsson wrote:<br>
> FWIW, here's what Gradualizer returns for your program:<br>
> <br>
>     dialyzer_issue.erl: The clause on line 11 at column 1 cannot be reached<br>
>     dialyzer_issue.erl: The clause on line 16 at column 1 cannot be reached<br>
>     dialyzer_issue.erl: The variable on line 20 at column 11 is expected<br>
>     to have type t1() but it has type a | b | x | y<br>
>     -spec foo(t1() | t2()) -> integer().<br>
>     foo(V) -><br>
>        case f1(V) of<br>
>                ^<br>
>     nok<br>
<br>
And the rationale for Gradualizer "expecting" foo/1 to have type t1() as <br>
argument is what exactly?  Simply that it calls f1/1 ?<br>
<br></blockquote><div>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. </div><div>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.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Note that expecting/insisting the above is inconsistent both with<br>
<br>
  - what the programmer has explicitly declared (i.e., that it has type <br>
t1() | t2())<br>
<br>
and<br>
<br>
  - the (erroneous) "expectation" on how the code should work (i.e. that <br>
[foo(N) || N <- [a, b, c, x, y, z]] evaluates to [1,2,0,3,4,0]) as <br>
explicitly mentioned below.<br>
<br>
Just curious on how one decides that the error is in foo's type spec and <br>
not in f1/1's or f2/1 (or in both/all, as it is clearly the case here).<br>
<br></blockquote><div>Gradualizer does complain about all functions but in different ways.</div><div><br></div><div>Josef</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">
<br>
Kostis<br>
<br>
> <br>
> On Sat, Feb 27, 2021 at 9:50 AM Nicolas Martyanoff <<a href="mailto:khaelin@gmail.com" target="_blank">khaelin@gmail.com</a> <br>
> <mailto:<a href="mailto:khaelin@gmail.com" target="_blank">khaelin@gmail.com</a>>> wrote:<br>
> <br>
> <br>
>     Hi,<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<br>
>     [1,2,0,3,4,0].<br>
<br>
</blockquote></div></div>