Dyalizer warnings for too wide return type

[Alexey Romanov]

One problem I have with Dialyzer is that it complains about cases
where the return type specified is too wide.

E.g.

-type handle_cast_return() :: {noreply, tuple()} | {noreply, tuple(),
integer()} | {stop, any(), tuple()}.
-spec handle_cast(any(), tuple()) -> handle_cast_return().
handle_cast(_Msg, State) ->
    {noreply, State}.

The definition says that handle_cast returns what it is supposed to
return according to behaviour, but it gives this warning:

sqlite3.erl:520: The specification for sqlite3:handle_cast/2 states
that the function might also return {'noreply',tuple(),integer()} |
{'stop',_,tuple()} but the inferred return is {'noreply',_}

Given this definition of success typing (from "A Language for
Specifying Type Contracts in Erlang"):

"A success Typing of a function, f, is a type signature, (α) → β ,
such that whenever an application f(p) reduces to a value v, then p ∈
α and v ∈ β."

the given specification satisfies it, and shouldn't result in a
warning. Or at least, there should be an option to turn this set of
warnings off, and I don't see one in
`dialyzer -Whelp`.

Obviously, I can narrow the return type, but then if implementation
changes later, I have to review it. In some cases I _know_ that the
implementation will change, which makes this even more annoying:

-spec some_test() -> boolean().
some_test() -> false. %% TODO implement later

%% in a different module
foo() ->
  case m1:some_test() of
    true -> ...
    false -> ...
  end.

In addition to the warning about some_test() I get warnings about
foo(): "Pattern 'true' can never match type 'false' ", any functions
called only from the 'true' branch are reported to be unused, etc.
While these warnings are correct, they ignore my specification for
some_test(). Can Dialyzer be forced to prefer the return type given in
the spec over the` one it infers?

Yours, Alexey Romanov