[erlang-questions] Dialyzer confused by several clauses?
Tue Aug 19 11:32:20 CEST 2008
Le 18 août 08 à 10:44, Tobias Lindahl a écrit :
> The checking in Dialyzer whether a contract is valid is not as
> sophisticated as it could be. First it finds the success typing of
> a function and then it compares it with the contract. The default
> is to complain only if the two are contradicting.
> In your case the return type in the success typing is any() because
> of the Value in the first clause (*). Since this does not
> contradict the tuple() in the contract, Dialyzer is satisfied. The
> reason for this somewhat liberal reasoning is the principle of
> sound warnings; if there is a possibility that a contract is
> correct then Dialyzer gives no warning. However, we could of course
> lift this restriction by allowing the user to give some option, but
> this is not present today.
> There are options for getting more strict warnings about contracts.
> However, they would not have helped you in this case. The options
> are --Wunderspecs, --Woverspecs and --Wspecdiffs. Basically these
> options makes Dialyzer warn when the specs differ from the success
> typings of functions. They are not on by default since the
> resulting warnings are a bit confusing at times.
> (*) As you say, the type could be written as float() | any(), but
> unions must be disjoint so this is collapsed to any().
Thank you for your reply! And thanks for the hint about the options,
which actually detect the specification error.
I am somewhat confused by the type arithmetics used by dialyzer,
especially with unions. If code is of type any() | float() and
specification is of type tuple(), how can it match? In which case
would it be correct to match code[any() | x()] with spec[y()]?
More information about the erlang-questions