dialyzer: false positive "overlapping domains" error

[ilya-klyuchnikov]

Describe the bug

Dialyzer produces "overlapping domains" error for "obviously non-overlapping" domains.

To Reproduce

-module(domains).

-type constant() ::
  {const, integer()}.

-type tagged() ::
  {tag01, term()}
| {tag02, term()}
| {tag03, term()}
| {tag04, term()}
| {tag05, term()}
| {tag06, term()}
| {tag07, term()}
| {tag08, term()}
| {tag09, term()}
| {tag10, term()}
| {tag11, term()}
| {tag12, term()}
| {tag13, term()}
| {tag14, term()}.

-export([process/1]).

-spec process
    (tagged()) -> atom();
    (constant()) -> integer().
process({const, I}) -> I;
process({Tag, _}) -> Tag.

dialyzer domains.erl
domains.erl:24:2: Overloaded contract for domains:process/1 has overlapping domains; such contracts are currently unsupported and are simply ignored

Expected behavior

the types/sets constants are non-overlapping - they are tagged tuples with distinct tags.

Affected versions

25.0.2

[ilya-klyuchnikov]

It seems that there should be some magical threshold in dialyzer - the error is gone if any of element of the type tagged() is deleted. - But if this is the case when dialyzer performs under/over-approximation - I believe it should just stay silent and not output a false positive.

[kostis]

I think you should pay more attention to the detail(s). This is not an error (or false positive).

It's just a warning from Dialyzer simply informing its user that it will discard (i.e., not take into account in its analysis) the spec of this function because the underlying type representation (which indeed has constraints / magical thresholds) makes Dialyzer think that the domains are overlapping. So, read this as a prompt to write the spec differently (e.g., as a simple spec and not as an overloaded contract).

Of course, it's a matter of taste / preferences whether it's a good idea to print this information by default or for having an option to silence these kinds of messages.

[josevalim]

@kostis I would say the key information missing in the warning message is that the domains have been "collapsed" due to constraints / magical thresholds and that's why they are overlapping. Otherwise, without having internal knowledge of if/when/how it happens, most users will assume they have indeed made a mistake and declared overlapped domains themselves.

[ilya-klyuchnikov]

UPDATE: this is a wrong example, - there is a shared element - an empty list.

Some much simpler case - that we got in our codebase today.

A simplified version:

-module(over).

-export([example/1]).

-type data() :: string() | binary().

-spec example
    (data()) -> data();
    ([data()]) -> [data()].
example(X) -> X.

dialyzer over.erl
over.erl:8:2: Overloaded contract for over:example/1 has overlapping domains; such contracts are currently unsupported and are simply ignored

---

But "obviously" (for humans) the domains are disjoint here.

[bjorng]

@ilya-klyuchnikov, your example can be further simplified and still produce the same warning:

-module(over).

-export([example/1]).

-type data() :: [char()].

-spec example
    (data()) -> data();
    ([data()]) -> [data()].
example(X) -> X.

Written that way, it is somewhat easier to see that the domains indeed do overlap. The overlap is [] (the empty list), which is part of both domains. That can be seen by making one of the lists involved nonempty, for example:

-spec example
    (data()) -> data();
    (nonempty_list(data())) -> [data()].

With that spec, there is no warning.

[bjorng]

I have recategorized this issue as a feature request to implement support for overlapping domains.

It seems that in principle that can be done by using the union (a.k.a. supremum or meet) of the domains of the contracts, and similarly for the return types. It need to be determined whether that will cause unintended consequences or cause other problems.

[ilya-klyuchnikov]

Yes, - I was too harsh - the last example is about overlapped domains indeed. My bad.

[kikofernandez]

it seems like Dialyzer is already doing the union (supremum) of the domains.
So instead, what we should think is whether this warning is really relevant at all, and if the warning should instead be opt-in and not a default.