otp icon indicating copy to clipboard operation
otp copied to clipboard

dialyzer: false positive "overlapping domains" error

Open ilya-klyuchnikov opened this issue 2 years ago • 7 comments

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 avatar Jun 29 '22 23:06 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.

ilya-klyuchnikov avatar Jun 30 '22 08:06 ilya-klyuchnikov

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.

kostis avatar Jun 30 '22 15:06 kostis

@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.

josevalim avatar Jul 13 '22 09:07 josevalim

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.

ilya-klyuchnikov avatar Oct 05 '22 08:10 ilya-klyuchnikov

@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 avatar Oct 05 '22 11:10 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.

bjorng avatar Oct 05 '22 11:10 bjorng

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

ilya-klyuchnikov avatar Oct 05 '22 13:10 ilya-klyuchnikov

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.

kikofernandez avatar Dec 02 '22 13:12 kikofernandez