为什么Erlang Dialyzer在以下代码中找不到类型错误？

Question

free_vars_in_dterm({var, V}) -> {var, V};显然不能打字检查，但是，透析器说一切都好。

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

代码如下：

-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).