dialyzer: false positive

[ilya-klyuchnikov]

Describe the bug

-module(dial).

-export([test1/01]).
-record(in, {
  f1 :: binary() | undefined
}).

-spec test1(In :: #in{}) -> binary().
test1(#in{f1 = F1}) when F1 =/= undefined ->
  to_binary(F1).

-spec to_binary(string() | binary()) -> binary().
to_binary(Data) when is_binary(Data) ->
  Data;
to_binary(Data) ->
  list_to_binary(Data).

dialyzer dial.erl
dial.erl:17:18: The call erlang:list_to_binary
         (Data :: 'undefined') breaks the contract 
          (IoList) -> binary() when IoList :: iolist()

dialyzer considers Data == undefined, though it can never be undefined - since the only code path from (exported) test1/1 checks that F1 =/= undefined.

Expected behavior No report about Data :: undefined.

Affected versions Reproducible with OTP 26.0.2

Additional information

Changing the type of the record field from f1 :: binary() | undefined to f1 :: binary() | string() | undefined make the error gone.

[elbrujohalcon]

Well… the error is pretty confusing (as usual), but the second clause for to_binary/1 is actually unneeded, right? It would be good if dialyzer can tell you that it will never be used, but it instead assumes that it will called with undefined. So, it's not exactly a "false positive", it's an "incorrectly labeled true positive" I would say :)

[jhogberg]

This is unfortunate. dialyzer doesn't handle negation at the moment, and only handles simple cases of subtraction from unions opportunistically whenever the representation happens to allow it.

Here, we have excluded binary() in the first clause because it happened to be convenient to do so, but failed to do the same in test1/1 because it wasn't. We won't be able to fix this in the near future. :-(

[ilya-klyuchnikov]

@jhogberg - is it somehow connected to records?

changing the example to not use records make the error gone:

-module(dial).

-export([test1/01]).

-spec test1(binary() | undefined) -> binary().
test1(In) when In =/= undefined ->
  to_binary(In).

-spec to_binary(string() | binary()) -> binary().
to_binary(Data) when is_binary(Data) ->
  Data;
to_binary(Data) ->
  list_to_binary(Data).

[jhogberg]

The error disappears as specs describe arguments upon successful return, not as they enter the function (see point 4 in the EEP draft). This means that In, and therefore Data, can be anything in those functions.

#in{f1 = F1} in the clause head constrains the input to that record type, making F1 binary() | undefined.