<div dir="ltr">FWIW, here's what Gradualizer returns for your program:<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 face="monospace">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 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</font></blockquote><div><br></div><div>All the best,</div><div><br></div><div>Josef</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Feb 27, 2021 at 9:50 AM Nicolas Martyanoff <<a href="mailto:khaelin@gmail.com">khaelin@gmail.com</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"><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 [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>
Thank you in advance.<br>
<br>
Regards,<br>
<br>
-- <br>
Nicolas Martyanoff<br>
<a href="http://snowsyn.net" rel="noreferrer" target="_blank">http://snowsyn.net</a><br>
<a href="mailto:khaelin@gmail.com" target="_blank">khaelin@gmail.com</a><br>
</blockquote></div>