[erlang-questions] Dialyzer: Why do I get a 'will never return success typing error' with this recursive function?

[Jesper Louis Andersen]

On 2/24/12 1:36 PM, Jeremy Raymond wrote:
> test(noloop) ->
>      ok;
> test(loop) ->
>      test(loop). % dialyzer warns about this call
It is usually worth it to give the version of Erlang/OTP you are using 
since the dialyzer often changes from version to version. But I can tell 
you why the dialyzer warns you:

We are looking a success typings. A success type says: "f : A -> B under 
the *assumption* of termination. That is, we look for ways to make the 
function terminate normally and then we annotate the function with an 
input type A and an output type B which makes this termination happen. 
If we pass 'noloop' then we get ok, hence we have the success type as 
'noloop' -> 'ok'.. making the function terminate. Now, the recursive 
call test(loop) will never terminate and we have figured this out. Hence 
'loop' as input cannot be in the success type of this function. In other 
words, the dialyzer just worked as a termination checker on your code.
> test(noloop) ->
>      ok;
> test(loop) ->
>      do_loop(loop).
>
> do_loop(loop) ->
>      do_loop(loop).
>
My guess is that the dialyzer does not in this case look for the 
discrepancy in the context of a recursive call to loop so it is 
conservative and finds the success type to be 'noloop' -> 'ok' as well. 
But unless it knows by some other means that you make a call test(loop) 
somewhere in your code, this limited success type is not a problem.

-- 
Jesper Louis Andersen
   Erlang Solutions Ltd., Copenhagen, DK