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.

Answer 1

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

1. The spec type does not match the success type: Invalid type spec warning
2. The spec type is a strict supertype of the success type: Warning only with -Wunderspecs or -Wspecdiffs
3. The spec type is a strict subtype of the success type: Warning only with -Woverspecs or -Wspecdiffs.
4. The spec type and the success type match exactly: Everything's good
5. 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

Answer 2

Dialyzer's own analysis is (currently) based on over-approximations, of several kinds, so it cannot discern whether your stricter spec is due to you being definitely wrong or due to Dialyzer having over-approximated somewhere.

It therefore chooses to trust your spec, and goes for reporting a definitive error later based on that information.

In general, type-error-related info by other modern systems comes with "all parts reported and no blame explicitly assigned" for this reason. Here it is actually the case that the inference, the spec and the patterns being incompatible, but Dialyzer blames just the patterns. This is a quirk to have in mind when using it.