[erlang-questions] Dialyzer confused by several clauses?

[Tobias Lindahl]

Paul,

Paul Guyot wrote:
> Hello,
> 
> Updating some code, I realized that dialyzer did not complain about an 
> incorrect specification.
> 
> Here is a simple code that it accepts:
> 
> -type(dict() :: any()).
> 
> -spec(clause/2::(integer(), dict()) -> tuple()).
> clause(0, Dict) ->
>     case orddict:find(0, Dict) of
>         {ok, Value} -> Value;
>         error -> 0.0
>     end;
> clause(Integer, Dict) ->
>     case orddict:find(Integer, Dict) of
>         {ok, Value} -> Value / Integer;
>         error -> 0.0
>     end.
> 
> The real contract is:
> -spec(clause/2::(integer(), dict()) -> float()).
> 
> An implied contact would be:
> -spec(clause/2::(integer(), dict()) -> float() | any()).
> 
> But this contract is certainly incompatible with the code:
> -spec(clause/2::(integer(), dict()) -> tuple()).
> 
> Am I doing something wrong or is it a known limitation?

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