no dialyzer error if function specification comes from a behaviour

[flaviogrossi]

Describe the bug
the same function specification regarding maps gives a dialyzer error when using -spec but gives no error when implementing a behaviour and inferring the type from a -callback specification

To Reproduce
given the following behaviour in bvr.erl:

-module(bvr).

-type t() :: #{ x => integer(), y => boolean() }.

-callback foo(t) -> t().

and the implementation impl.erl:

-module(impl).
-behaviour(bvr).

-export([foo/1, test/0]).

% -type t() :: #{ x => integer(), y => boolean() }.

% -spec foo(t) -> t().
foo(M) ->
  M.

test() ->
  foo(#{ x => 12, z => 12 }).

no dialyzer error is raised:

$ make dialyze
[...]
  Proceeding with analysis... done in 0m0.06s
done (passed successfully)

Hovewer, decommenting the two lines in impl.erl (or removing the behaviour at all and just using the given spec), it correctly gives an error:

$ make dialyze
[...]
  Proceeding with analysis...
impl.erl:12:1: Function test/0 has no local return
impl.erl:13:7: The call impl:foo
         (#{'x' => 12, 'z' => 12}) breaks the contract 
          ('t') -> t()
 done in 0m0.08s
done (warnings were emitted)
make: *** [erlang.mk:6784: dialyze] Error 2

Expected behavior
the error should be raised in both cases

Affected versions
Tested with master branch, version Erlang/OTP 26 [DEVELOPMENT] [erts-13.1.1] [source-aa922e1216]

Additional context

[TD5]

tl;dr I think this is somewhat expected, but I can see an argument for changing how this works.

Why does Dialyzer comes to this conclusion?

As I understand it, Dialyzer uses specs as follows:

• Dialyzer infers the success type by looking at the body of a function (i.e. without the spec!)
• Dialyzer compares each inferred success typing argument and return type with the spec arguments and returns types to see whether there are any values in common between them. If any of them have an empty (none()) overlap ("infimum"/t_inf/2), then Dialyzer generates a warning about a mismatch between the spec and the body.
• If the above succeeded, it refines the overall type of the function as the overlap between the spec and the inferred success type

Dialyzer uses behaviours as follows:

• Dialyzer compares each inferred success typing argument and return type with the behaviour's callback's arguments and returns types to see whether there are any values in common between them. If any of them have an empty overlap, then Dialyzer generates a warning about any mismatch between them.
• Dialyzer compares each spec'd argument and return type with the behaviour's callback's arguments and returns types to see whether there are any values in common between them. If any of them have an empty overlap, then Dialyzer generates a warning about any mismatch between them.

Notably, unlike specs, behaviours don't seem to be used to refine the success type during Dialyzer's dataflow analysis. Although, if a spec is present, the spec will be checked for an overlap with the behaviour, and the implementation will be checked for an overlap with the spec. This means the callback type can have a second-order affect via constraining the spec type, even though it doesn't directly refine the success typing.

Could Dialyzer use the behaviour to refine the dataflow analysis and catch the issue?

I don't see why not. Looking at the code I linked to above, the dataflow analysis could simply do another t_inf_list/2 using the callback type (or perhaps a more nuanced check that handles the combination of the presence or absence of spec and behaviour more intelligently).

Why don't more people complain about this?

My best guess is that most of users who would locate this issue would also have linting or similar around exporting and spec'ing callback implementations, so typically they wouldn't be in this state of comparing the effect of the behaviour's type with and without a spec.

I also suspect there's a historical effect here, perhaps due to specs and behaviours being introduced at different times, and behaviours having some special cases (such as allowing implementations of callbacks to return none() even when spec'd otherwise, meaning we've ended up in a unintuitive surprising place, but where each step made some sense in isolation - hence the "this is somewhat expected" in the tl;dr.

Next steps

@bjorng / @kikofernandez / @jhogberg: Is my reasoning along the right lines? Does it make sense to include the behaviour type in dataflow analysis like the spec is? Should we make that change?

[paulo-ferraz-oliveira]

include the behaviour type in dataflow analysis like the spec is

I upvote for this. I've lost count of the number of times I've spec'ed a behaviour to repeat the spec in the implementing function, and at the same time having to potentially tweak both when the spec changes 😢.

Also, if we're going with the potential change suggested by @TD5 we should also remember the erl_opt warn_missing_spec (it could even potentially be replaced with a new directive such as -impl(bvr). to indicate what we're implementing - this would also be useful for the language servers, I imagine - but maybe that's a separate subject.

[TD5]

How would -impl differ from -behaviour?

[TD5]

And in case the above wasn't convoluted enough, we recently also changed the logic for precisely how we validate a spec against a callback in #6243

[paulo-ferraz-oliveira]

How would -impl differ from -behaviour?

-impl would be an indication, next to the function, of what behaviour you're implementing. This would ease reading and prevent you from having to re-typespec the function (lest we want that to be implicit).

You'd have something like

-module(impl).
-behaviour(bvr).

-export([foo/1, test/0]).

% -type t() :: #{ x => integer(), y => boolean() }.

-impl(bvr).
foo(M) ->
  M.

test() ->
  foo(#{ x => 12, z => 12 }).

Edit: fwiw, this (-impl) is not a new idea, but something I've found handy in the past - reference.

Edit: and also, it'd have to be optional for backward compatibility (let the linters take care of warning about it not being present), but if present should be validated against an existing behaviour declaration (and true shouldn't be accepted, as is the case in the reference).

[TD5]

This would ease reading and prevent you from having to re-typespec the function (lest we want that to be implicit)

I think this motivation, but I wonder if it might better be served by an in-editor hint that would show the type of the corresponding callback definition?