Why does Dialyzer believe specs with too-specific return types?

Question

I expect adding specs to never make things less safe, but that's exactly what happens in the following case.

In the following code, Dialyzer (wrongly) trusts me that the return type of bar is 1. This leads it to saying that a pattern in foo() can never match–incorrect advice that, if heeded, would introduce a runtime error!

-module(sample).
-export([foo/0]).

foo() ->
    case bar() of
        1 -> ok;
        2 -> something
    end.

 -spec bar() -> 1.
bar() ->
  rand:uniform(2).

Deleting the spec for bar/0 fixes the problem–but why did Dialyzer trust me? Dialyzer is violating its "no false positives" promise here: it warns when there is no bug. And (even worse) Dialyzer nudges to introduce a new bug.

José M José M · Accepted Answer · 2020-12-16T22:05:56

Dialyzer calculates the success typing for each function before checking its spec, this action has several possible outcomes:

The spec type does not match the success type: Invalid type spec warning
The spec type is a strict supertype of the success type: Warning only with -Wunderspecs or -Wspecdiffs
The spec type is a strict subtype of the success type: Warning only with -Woverspecs or -Wspecdiffs.
The spec type and the success type match exactly: Everything's good
The spec type and the success type overlap but don't match exactly (like -1..1 and pos_integer()): Same as 2.

For 1, it continues with the success type, otherwise continues with the intersection between the success type and the spec type.

Your case is 3, which is usually not warned about because you, as the programmer, know better (as far as dialyzer is concerned, maybe rand:uniform(2) can only return 1). You can activate it with

{dialyzer, [{warnings, [underspecs,overspecs]}]}.

in the rebar.config file

Why does Dialyzer believe specs with too-specific return types?

2 Answers