[erlang-questions] Dialyzer confused by several clauses?

[Tobias Lindahl]

Paul Guyot wrote:
> Le 18 août 08 à 10:44, Tobias Lindahl a écrit :
> 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()]?

Perhaps I was a bit unclear about the union type. The type float() | 
any() is not a valid union. The separate parts of the union must be 
disjoint, and since float() is a subtype of any() the union is collapsed 
to any().

Valid unions are for example tuple()|integer(), or 'ok'|{'error',any()}. 
Invalid unions would be something like byte()|integer(), 'ok'|atom(). Of 
course, there is nothing wrong with forming these unions, but they will 
be collapsed to integer() and atom() respectively.

When you specify that your function should return tuple(), and dialyzer 
finds that the function can return any() (because of the collapsed 
union), dialyzer simply assumes that you know better and accepts the 
annotation. Note that any() do not contradict tuple(), since tuple() is 
included in any().

Hope this made things a bit more clear.

Best,
Tobias


> 
> Paul
>