Why does Dialyzer not catch this simple error?

Question

Dialyzer does not signal the inconsistency in the return type of this function:

-spec myfun(integer()) -> zero | one.
myfun(0) -> zero;
myfun(1) -> one;
myfun(2) -> other_number.

but it detects in the case of the last line being

myfun(_) -> other_number.

Why is this so? I believe the above should be a very simple case.

Thanks

Answer 1

The easy answer to questions of type "why Dialyzer doesn't..." is "because it has been designed to be always correct" or "because it never promises that it will catch everything or anything specific".

---

For the more complex answer, you need to specify your question further. If I write your example in a module:

-module(bar).

-export([myfun1/1, myfun2/1]).

-spec myfun1(integer()) -> zero | one.

myfun1(0) -> zero;
myfun1(1) -> one;
myfun1(2) -> other_number.

-spec myfun2(integer()) -> zero | one.

myfun2(0) -> zero;
myfun2(1) -> one;
myfun2(_) -> other_number.

And Dialyze it:

$ dialyzer bar.erl 
  Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis... done in 0m0.64s
done (passed successfully)

... neither discrepancy is 'detected', cause neither is an "error". It's just the case that the code is in some ways more generic (can return extra values) and in some ways more restrictive (cannot handle every integer, for version 1) than the spec.

The second version's problem can be found with -Woverspecs:

$ dialyzer -Woverspecs bar.erl 
  Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
bar.erl:11: Type specification bar:myfun2(integer()) -> 'zero' | 'one' is a subtype of the success typing: bar:myfun2(_) -> 'one' | 'other_number' | 'zero'
 done in 0m0.58s
done (warnings were emitted)

The warning explains exactly that the spec is more restrictive than the code.

Both problems can also be detected by the extremely unusual -Wspecdiffs:

$ dialyzer -Wspecdiffs bar.erl 
  Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
bar.erl:5: Type specification bar:myfun1(integer()) -> 'zero' | 'one' is not equal to the success typing: bar:myfun1(0 | 1 | 2) -> 'one' | 'other_number' | 'zero'
bar.erl:11: Type specification bar:myfun2(integer()) -> 'zero' | 'one' is a subtype of the success typing: bar:myfun2(_) -> 'one' | 'other_number' | 'zero'
 done in 0m0.61s
done (warnings were emitted)

Neither -Woverspecs nor -Wspecdiffs mode of operation is encouraged, as Dialyzer's type analysis can and will generalize types, so "something being specified in a more restrictive way" can be the result of generalization.

It can also be the case that you intend these functions to be called only with 0 and 1 as arguments, in which case the spec is 'ok'.