Unsettling dialyzer errors

[Nicolas Martyanoff]

Hi,

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 ?

Thank you in advance.

Regards,

-- 
Nicolas Martyanoff
http://snowsyn.net
khaelin@REDACTED