Dialyzer erroneously processes callback and spec types differently

[TD5]

Describe the bug

tl;dr Callback and spec types are "simplified" differently, which can break behaviour subtype checking since it is not commutative, unlike normal overlap checking of specs and implementations

Dialyzer sometimes simplifies types (e.g. types such as 1 | 2 | 3 | 4 | 5 | ... can be simplified to integer(), or [a] | [b] to [a | b], Dialyzer also limits how far it'll recurse into types, and has other mechanisms to keep it's analysis time quicker than it would otherwise be by making approximations.

Usually, these approximations are fine because Dialyzer checks types for compatibility by essentially taking the intersection of two types, and seeing whether it's empty (i.e. do the types "overlap"), and this sort of simplification taking place doesn't change whether a later intersection is empty or not, and nor does it matter whether one of the two types is simplified more than the other.

However, checking of specifications against a behaviour's callbacks are done via a different mechanism which Dialyzer considers "subtyping", which works a bit more like classical subtyping in object oriented systems and isn't commutative. Typically, this works fine, but types with the same structure can end up being "simplified" differently in specs vs. callbacks, resulting in a callback and spec with the same type not being considered subtypes of one another. This results in Dialyzer rejecting valid code (i.e. code where the callback, spec and implementation all agree).

To Reproduce

Given a behaviour in i.erl:

-module(i).

-callback foo() -> #{ {{{f,f}, f}, f} => x }.

And an implementation of it in j.erl:

-module(j).
-behaviour(i).

-export([foo/0]).

-type pair(A,B) :: {A,B}.

-type nested() :: pair(pair(pair(f,f),f),f).

-spec foo() -> #{ nested() => x }.
foo() ->
  Ret = #{ {{{f,f}, f}, f} => x },
  Ret.

We get a callback_spec_type_mismatch error like:

The return type #{{{_,'f'},'f'}=>'x'} in the specification of foo/0 is not a subtype of #{{{{'f','f'},'f'},'f'}=>'x'}, which is the expected return type for the callback of i behaviour

Note the _ in the spec's return type in the error message, despite both the spec and the callback both, once expanded, declaring to return a #{ {{{f,f}, f}, f} => x }.

Also note that if the declarations of the spec and callback were swapped, the _ would be in the callback's type, and so the spec would be considered a subtype, despite them not being simplified in the same way.

Expected behavior

I would expect this case to be accepted, because both spec and callback return the same type (and both should be simplified in the same way).

Affected versions

Recent HEAD of OTP, but also older official releases.

Additional context

In the above example, I showed this issue occurring with nested tuples where one element became _, breaking subtyping. However, with much bigger examples (as you might see in a production codebase, but much harder to put into a bug report), you can end up with breaking it more egregiously, making two identical types in spec and callback become an error like:

The return type {ok, map()} in the specification of foo/0 is not a subtype of {ok, #{ ... some huge map here ...}}, which is the expected return type for the callback of i behaviour

In fact, in sufficiently big examples with types defined across multiple files, and with header files including records and other types, this can happen even when the spec and callbacks are defined in precisely the same way, i.e. they don't need to just expand to the same thing, but they're literally syntactically the same type in the source files of both.

Notes

I've not validated my explanation of what's going on here by stepping through Dialyzer during a debugging session, so I could be wrong about the precise mechanism at play, but whatever the explanation, I think this must be a bug since Dialyzer seems to be rejecting a callback, spec and implementation which express the same structure, which goes against the philosophy that "if Dialyzer complains, there's something wrong in your specs or implementation".

[TD5]

Seems related to #6117 in the sense that this is Dialyzer collapsing types together to cause an unexpected warning/error

[TD5]

My gut says the most robust solution is to make dialyzer_behaviours:check_callback/6 not use subtyping (because that seemingly inherently breaks the invariant that Dialyzer "simplification" is always safe to apply), and use the logic applied to checking specs vs. implementations in dialyzer_contracts:check_contract/3 (logically something like erl_types:t_is_none(erl_types:t_inf(Behaviour, Spec))).

It may be the case that this is unnecessarily conservative, so I am keen to hear alternative suggestions that resolve the above soundness problem but continues to allow Dialyzer to pick up as many "genuine" discrepancies as possible.

[aronisstav]

I agree that this looks like a bug, and the proposed fix is exactly on the right track.

[TD5]

I agree that this looks like a bug, and the proposed fix is exactly on the right track.

Great, thanks. I'll take a look at implementing that and putting up a PR.

[TD5]

I've put up #6243, where I implemented my proposal above to switch from subtype checking to overlap checking (and also special casing specs that return none(), as per a test case I found when implementing this).