Erlang: Why Dialyzer does not notice this error?

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.

Solution

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.