Why Erlang Dialyzer cannot find type error in the following code?

Question

free_vars_in_dterm({var, V}) -> {var, V}; obviously cannot type check, however, dialyzer says everything is OK.

$ dialyzer *erl
  Checking whether the PLT ~/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis... done in 0m0.66s
done (passed successfully)

Code is as below:

-module(formulas).

-type formulas() :: {predicate(), [dterm()]}
                  | {'~', formulas()}
                  | {'&', formulas(), formulas()}
                  | {'|', formulas(), formulas()}
                  | {'->', formulas(), formulas()}
                  | {'<->', formulas(), formulas()}
                  | {'exist', variable(), formulas()}
                  | {'any', variable(), formulas()}.

-type dterm() :: constant()
               | variable()
               | {func(), [dterm()]}.

-type constant() :: {const, atom()}
                  | {const, integer()}.

-type variable() :: {var, atom()}.

-type func() :: {function,
                 Function_name::atom(),
                 Arity::integer()}.

-type predicate() :: {predicate,
                      Predicate_name::atom(),
                      Arity::integer()}.


-include_lib("eunit/include/eunit.hrl").

-export([is_ground/1, free_vars/1, is_sentence/1]).

-spec is_ground(formulas()) -> boolean().
is_ground({_, {var, _}, _}) -> false;
is_ground({{predicate, _, _}, Terms}) ->
    lists:all(fun is_ground_term/1, Terms);
is_ground(Formulas) ->
    Ts = tuple_size(Formulas),
    lists:all(fun is_ground/1, [element(I, Formulas)
                                || I <- lists:seq(2, Ts)]).

-spec is_ground_term(dterm()) -> boolean().
is_ground_term({const, _}) -> true;
is_ground_term({var, _}) -> false;
is_ground_term({{function, _, _}, Terms}) ->
    lists:all(fun is_ground_term/1, Terms).


-spec is_sentence(formulas()) -> boolean().
is_sentence(Formulas) ->
    sets:size(free_vars(Formulas)) =:= 0.

-spec free_vars(formulas()) -> sets:set(variable()).
free_vars({{predicate, _, _}, Dterms}) ->
    join_sets([free_vars_in_dterm(Dterm)
               || Dterm <- Dterms]);
free_vars({_Qualify, {var, V}, Formulas}) ->
    sets:del_element({var, V}, free_vars(Formulas));
free_vars(Compound_formulas) ->
    Tp_size = tuple_size(Compound_formulas),
    join_sets([free_vars(element(I, Compound_formulas))
               || I <- lists:seq(2, Tp_size)]).

-spec free_vars_in_dterm(dterm()) -> sets:set(variable()).
free_vars_in_dterm({const, _}) -> sets:new();
free_vars_in_dterm({var, V}) -> {var, V};
free_vars_in_dterm({{function, _, _}, Dterms}) ->
    join_sets([free_vars_in_dterm(Dterm)
               || Dterm <- Dterms]).

-spec join_sets([sets:set(T)]) -> sets:set(T).
join_sets(Set_list) ->
    lists:foldl(fun (T, Acc) -> sets:union(T, Acc) end,
                sets:new(),
                Set_list).

Subadar

Do you mean that the value {var, V} is not a set? – Zaffer

@Zaffer Yes. This is a type inconsistent. However, dialyzer complained nothing. – Subadar

Answer 1

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 should be 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 {var, V} tuple) 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, 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 sets, no warnings are generated.

Zaffer