Why doesn't dialyzer warn me?

classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Why doesn't dialyzer warn me?

Attila Rajmund Nohl
Hello!

I looked at a largish codebase with full of dialyzer warnings due to
record values created via multiple functions and the temporary values
does not satisfy the type spec. It's essentially the same problem as
mentioned in this thread:
https://erlang-questions.erlang.narkive.com/i74Hlqbm/temporarily-violating-record-type-constraints-annoys-dialyzer

I applied the solution recommended by Dániel and the warnings went
away - however, I'm a little afraid that if I end up creating a
"wrong" record, dialyzer still won't warn me. So I created a minimal
example:

-module(mylib).

-export([foo/1, t/0]).

-record(bar, {one, two}).
-type bar() :: #bar{one :: integer(), two :: list()}.

-spec foo(integer()) -> bar().
foo(12)  ->
  #bar{two = []};
foo(X) when is_integer(X) ->
  #bar{one = X, two = []}.

-spec t() -> bar().
t() ->
  foo(12).

Dialyzer does not warn me that the t/0 function returns a value that
does not satisfy the typespec (the field `one` will have `undefined`
value, not an integer). What am I doing wrong?
Reply | Threaded
Open this post in threaded view
|

Re: Why doesn't dialyzer warn me?

Dániel Szoboszlay
Hi,

I think it's not you doing something wrong, but these examples are probably stretching the boundaries of what errors success typing can detect.
I made a slight modification to your example to better illustrate my point:

-module(mylib).

-export([foo/1, t/0]).

-record(bar, {one, two}).
-type bar() :: #bar{one :: integer(), two :: list()}.

foo(A) when is_atom(A)  ->
  #bar{two = []};
foo(X) when is_integer(X) ->
  #bar{one = X, two = []}.

-spec t() -> bar().
t() ->
  foo(atom).

Then you can check the success types with typer:

%% File: "mylib.erl"
%% -----------------
-spec foo(atom() | integer()) -> #bar{one::'undefined' | integer(),two::[]}.
-spec t() -> bar().

The "problem" is that in your human mind foo's type spec is foo(atom()) -> #bar{one::undefined,two::[]}); (integer()) -> bar(), but Dialyzer "collapses" this overloaded type specification. And since bar() is a subtype of #bar{one::'undefined' | integer(),two::[]}, it won't complain about the type spec of t/0.

By the way, if foo/1 is not an exported function, you will get an error (even with your original example). I guess this is because Dialyzer does some dead code elimination before calculating the success type of foo/1 and realises the second clause will never apply, so there are no overloaded types left to collapse.

I also found a similar, very worrying example where Dialyzer cannot detect obvious violations of type specs:

-spec bars() -> [bar()].
bars() ->
  [#bar{two = []}, #bar{one = 1, two = []}].

This is the same problem, the success type of the function (when ignoring type specs) is bars() -> [#bar{one::'undefined' | 1,two::[]},...], and [bar()] is a subtype of this return type, so no error.

I honestly don't know any more how to write code that is Dialyzer-friendly. Looks like putting type specs within record definitions may help, because it forces type checking to happen right at the expression level, instead of using union types assembled from different bits of the code. But that technique has some serious drawbacks, and it isn't even applicable to non-record types. The same errors could go undetected when using a map instead of a record, for example.

/Dániel


On Fri, 13 Mar 2020 at 18:03, Attila Rajmund Nohl <[hidden email]> wrote:
Hello!

I looked at a largish codebase with full of dialyzer warnings due to
record values created via multiple functions and the temporary values
does not satisfy the type spec. It's essentially the same problem as
mentioned in this thread:
https://erlang-questions.erlang.narkive.com/i74Hlqbm/temporarily-violating-record-type-constraints-annoys-dialyzer

I applied the solution recommended by Dániel and the warnings went
away - however, I'm a little afraid that if I end up creating a
"wrong" record, dialyzer still won't warn me. So I created a minimal
example:

-module(mylib).

-export([foo/1, t/0]).

-record(bar, {one, two}).
-type bar() :: #bar{one :: integer(), two :: list()}.

-spec foo(integer()) -> bar().
foo(12)  ->
  #bar{two = []};
foo(X) when is_integer(X) ->
  #bar{one = X, two = []}.

-spec t() -> bar().
t() ->
  foo(12).

Dialyzer does not warn me that the t/0 function returns a value that
does not satisfy the typespec (the field `one` will have `undefined`
value, not an integer). What am I doing wrong?
Reply | Threaded
Open this post in threaded view
|

Re: Why doesn't dialyzer warn me?

Attila Rajmund Nohl
Dániel Szoboszlay <[hidden email]> ezt írta (időpont: 2020.
márc. 13., P, 23:26):
>
> Hi,
>
> I think it's not you doing something wrong, but these examples are probably stretching the boundaries of what errors success typing can detect.

Yes, thinking it actually through it makes sense that success typing
won't find this error.