Erlang: Why Dialyzer does not notice this error?

Question

Now, I try to use Dialyzer and use -spec, -type.

I give the below code to Dialyzer, and I expected Dialyzer to notice "hoge(a) + 1 is invalid", but Dialyzer does not notice.

-spec hoge (X) -> bad      when X :: a;
           (X) -> number() when X :: number().
hoge(X) when is_number(X) -> 1;
hoge(a) -> bad.

foo() ->
  _ = hoge(a) + 1.

But, in another setting,

-spec hoge (X) -> bad      when X :: a;
           (X) -> string() when X :: number().
hoge(X) when is_number(X) -> "1";
hoge(a) -> bad.


foo() ->
  _ = hoge(a) + 1.

Dialyzer tell me this error,

test.erl:12: The call erlang:'+'('bad' | [49,...],1) will never return since it differs in the 1st argument from the success typing arguments: (number(),number())

Why Dialyzer can't notice type-error in first setting.

-spec hoge (X) -> bad      when X :: a;
           (X) -> number() when X :: number().

This contract(specification) means not "hoge is typed of 'a' -> 'bad' | number() -> number()" but "'a' | number() -> 'bad' | number()"?

Here is a complete module for the first example.

-module(example).
-export([hoge/1, foo/0]).

-spec hoge (X) -> bad      when X :: a;
           (X) -> number() when X :: number().
hoge(X) when is_number(X) -> 1;
hoge(a) -> bad.

foo() ->
  _ = hoge(a) + 1.

I want to know how -spec information is used in type checking... — oky
What version of OTP are you running? I tried with 18, 19 and 20, and in all cases Dialyzer reported the error in the first version of the code. — RichardC
Ah, when the function hoge/1 is exported, you don't get the message. I think Dialyzer does not treat each call site separately. If hoge/1 is not exported, it knows that it will never return 1, because it's only called with a. If it is exported, it will be treated as returning either 1 or a, and one of those will make the addition work, so it's not deteted as an error. — RichardC
Don't worry too much about things not being reported. Dialyzer will only report things that are absolutely, definitely wrong, and will keep quiet whenever there is still a possibility for the code to work in some way. — RichardC

aronisstav aronisstav · Accepted Answer · 2018-04-03T16:21:32

The standard answer to "why Dialyzer doesn't catch this error" questions is always "because it is never wrong". Dialyzer never promises to find all errors.

In your problematic example, without the spec, Dialyzer's type inference algorithm indeed produces a union type for all the arguments and all the return values. With the spec, Dialyzer still infers the unions, but should have used the spec to narrow down the return value of the call and then produce an error. This looks like a case of "reduced sensitivity" (but not a bug, per se). You could, in any case, file a bug report.

In your working example, any possible value results in a bad result and Dialyzer's own type inference is enough, even without a spec.

Erlang: Why Dialyzer does not notice this error?

1 Answers