[erlang-questions] Dialyzer confused by several clauses?

[Paul Guyot]

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.
>
> Tobias
>
> (*) As you say, the type could be written as float() | any(), but  
> unions must be disjoint so this is collapsed to any().

Dear Tobias,

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()]?

Paul