Dialyzer misses error with type specification

Question

The following Erlang code seems to have an obvious error in its type specification, but dialyzer says that everything is ok. Am I misunderstanding or is this a bug in dialyzer? Running on Erlang 19.3

-module(foobar).

-export([foo/1]).

-spec foo(atom()) -> ok | {error, atom()}.
foo(Arg) -> bar(Arg).

-spec bar(atom()) -> ok | error.
bar(baz) -> error;
bar(_) -> ok.

Beaumarchais

This is really a duplicate of #43070830 but I cannot flag it since it hasn't been accepted/upvoted. – Winn

That link is to a question that is completely incomprehensible, so I don't see how a clear question like this one is a duplicate of that one. – Seed

@Seed your observation is correct, my fault. – Winn

Does this answer your question? Why Erlang Dialyzer cannot find type error in the following code? – Glans

Answer 1

Regime 1:

If there is any path through your code that does not match your specified types, then dialyzer will report an error.

Regime 2:

If there is any path through your code that does match your specified types, then dialyzer will not report an error.

diaylyzer operates under Regime 2. In your case, if you call foo(hello):

1> c(foobar).
{ok,foobar}

2> foobar:foo(hello).
ok

3> 

...then foo() was called with the required argument type atom(), and foo() returned one of the required types, ok, so dialyzer doesn't report an error.

Remember, Dialyzer is optimistic. It has figurative faith in your code, and because there is the possibility that the function call to [foo] succeeds ..., Dialyzer will keep silent. No type error is reported in this case.

http://learnyousomeerlang.com/dialyzer

Dialyzer can be more confounding than in your example, for instance:

-module(my).
-export([test/0, myand/2]).
%-compile(export_all).
-include_lib("eunit/include/eunit.hrl").

test() ->
    myand({a,b}, [1,2]).

myand(true, true) -> true;
myand(false, _) -> false;
myand(_, false) -> false.

1. Can you spot the error in the code?
2. Will dialyzer find the error? Take a minute and try to determine what you can infer about the types of the arguments to myand().

Answer: The first argument to myand() has to be a boolean()...well that's not actually true--look at the last clause of myand(). The first argument can also be anything. The three function clauses tell us that all the possible values for the first argument are: true, false, or anything. A type that encompasses all three possibilities is any(). Then dialyzer looks at the second argument, and dialyzer comes to the same conclusion about the second argument's type. Therefore, dialyzer infers the type of myand() to be:

myand(any(), any()) -> boolean().

...which means that in dialyzer's opinion calling myand({a,b}, [1,2]) isn't an error. Huh?? Au contraire, my feathered friend:

1> c(my).  
{ok,my}

2> my:test().
** exception error: no function clause matching my:myand({a,b},[1,2]) (my.erl, line 9)

3> 

Obviously, the intent of the myand() code is that myand() should require at least one boolean() argument--but apparently dialyzer collects information on each variable in isolation:

+---------------------------------------+
|          1st arg info                 |
|                                       |               
|   info1     true                      |                          
|   info2     false                     |
|   info3     any                       |
|           ---------                   |
|             any() -- inferred type    |
|                                       |
+---------------------------------------+

+---------------------------------------+
|          2nd arg info                 |
|                                       |    
|   info1     true                      |
|   info2     any                       |
|   info3     false                     |
|            -------                    |
|             any() -- inferred type    |
|                                       |
+---------------------------------------+

As a consequence, the test()/myand() code is a case where dialyzer isn't able to report an actual error in your code.

There are ways to help dialyzer find errors:

1) Enumerate all possible arguments in the function clauses:

myand(true, true) -> true;
myand(false, true) -> false;
myand(true, false) -> false.

"Programming Erlang" p. 152 warns against using _ for arguments if you are using dialyzer.

2) Or, if there are too many cases to enumerate, you can use guards to specify argument types:

myand(true, true) -> true;
myand(false, _Y) when is_boolean(_Y) -> false;
myand(_X, false) when is_boolean(_X) -> false.

3) And of course, you can employ a type specification:

 -spec myand(boolean(), boolean()) -> boolean().

Seed

Answer 2

First a short answer, using Dialyzer's maxims:

1. Dialyzer is never wrong. (recited very often by Erlang programmers)
2. Dialyzer never promised to find all errors in your code. (not so famous)

Maxim number 2 is the (admittedly not very satisfying) "standard" answer to any "Why Dialyzer didn't catch this error" question.

---

More explanatory answer:

Dialyzer's analysis for return values of functions is frequently doing over-approximations. As a result, any value included in the types is considered to be a "maybe returned" value. This has the unfortunate side-effect that sometimes values that are certainly going to be returned (such as your error atom) are also considered "maybe returned". Dialyzer must guarantee maxim 1 (never be wrong), so in cases where an unexpected value "may be returned" it will not give a warning (in the spec of foo), unless none of the actually specified values can be returned. This last part is checked at the level of the entire function, and since in your example some of the clauses indeed return ok, no warnings are generated.

---

Finally, if you want Dialyzer to be very strict about specs, you can use -Wunderspecs or -Woverspecs or -Wspec_diffs (see the documentation about what each of these does)

Winn