[erlang-questions] dialyzer apparently-erroneously thinking a spec is underspecified

[Stavros Aronis]

Hi Felix!

The type system that Dialyzer is based on (success types) allows for the
return value of a function to be over-approximated (i.e. include more
values). An unfortunate side effect of that characteristic is that, in
general, Dialyzer cannot be sure whether a particular value can really be
returned from a function or not neither can it discern whether a particular
value is an overapproximation or not.

Assume e.g. that instead of random:uniform/0 you had a call to another
function foo:bar(X) (using boop's argument) with the following code:

-module(foo).
-export([bar/1]).
bar(X) when is_atom(X) -> 1;
bar(_) -> 0.

With no spec provided, the inferred type for foo:bar/1 one will be "any()
-> 0 | 1". Notice however that for every call from your module (with an
argument of type glory/0, or specifically 'hello') the result will be 1,
thus safe. Unfortunately Dialyzer cannot be sure about this and the
inferred type of boop/1 will be "hello -> hello | micronauts", an
overapproximation of the accurate "hello -> hello".

Now in either example, since there can be some overlap, Dialyzer makes the
'safe' assumption that any extra values in the inferred type are just due
to overapproximation and stays silent. It only complains about the
impossible *extra* value in the spec (glory) which can never be returned.

Hope this helps,

Stavros


On Thu, Dec 10, 2015 at 10:52 PM Felix Gallo <felixgallo@REDACTED> wrote:

> consider:
>
> https://gist.github.com/anonymous/e5165c443f6bdf0f0780
>
> by inspection, the spec on the boop function is "wrong", but this code
> passes dialyzer, unless you run it with -Wunderspecs or -Wspecdiffs, at
> which point it complains:
>
> tt.erl:10: The specification for tt:boop/1 states that the function might
> also return 'glory' but the inferred return is 'hello' | 'micronauts'
>
> So dialyzer does notice that 'micronauts' might be returned, and does know
> that the glory() type does not include that as a choice, but believes that
> the spec is just underspecified, rather than violated.  Why is that?
>
> F.
> _______________________________________________
> erlang-questions mailing list
> erlang-questions@REDACTED
> http://erlang.org/mailman/listinfo/erlang-questions
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20151210/0249b4c9/attachment.htm>