[erlang-questions] Dialyzer failing to find simple type error

[Stavros Aronis]

Well, this was what I ended up trying to improve in my master thesis back
in 2010...

(Mainly for Tobias:) The attempted solution was to take all the type
constraints that Dialyzer generates, convert them to disjunctive normal
form and then carefully assemble an 'intersection type', able to infer
things like bar(1) -> 'foo';(2) -> 'bar'. Still far from things like
<anything but 1> though.

For the provided examples, intersection types together with standard call
refinement would produce the desired warnings (I had a brief moment of
nostalgia trying it out with just erts in the PLT on:
https://github.com/aronisstav/otp/tree/intersection):

$ dialyzer test2.erl
[...]
test2.erl:5: Function main/0 has no local return
test2.erl:7: The call test2:foo('bar') will never return since it differs
in the 1st argument from the success typing arguments: ('foo')
[...]
 done in 0m0.11s
done (warnings were emitted)

$ typer test2.erl

%% File: "test2.erl"
%% -----------------
-spec main() -> none().
-spec foo('foo') -> 'ok'.
-spec bar(1) -> 'foo'; (2) -> 'bar'.

Unfortunately, this extension made the analysis too slow (my dead-stupid
conversion to disjunctive normal form leads to a lot of duplication of
work), so it never went into OTP and as the code has been evolving
significantly I would need to redo everything from scratch...

Other than that, I fully agree with Tobias.

Stavros

On Thu, Jan 1, 2015 at 11:57 PM, Tobias Lindahl <tobias.lindahl@REDACTED>
wrote:

> Hi Philip,
>
> You are confusing Dialyzer with a static type checker (which it isn't [1]).
>
> In one of your examples, there is no problem, and in the other one, the
> analysis would have to be pretty strong (and have a different type domain)
> to find the problem.
>
> In test.erl, you have the success typings (written as specs)
>
> -spec bar() -> 1 | 0.
> -spec foo(1) -> 'ok'
>
> So applying foo(bar()) _can_ succeed, which makes it perfectly fine in
> Dialyzer's eyes.
>
> Similarly, in test2.erl you have the success typings
>
> -spec bar(any()) -> 'foo' | 'bar'.
> -spec foo('foo') -> 'ok'.
>
> So applying
>
>     ok = foo(bar(1)),
>     ok = foo(bar(2)).
>
> once again _can_ succeed (based on the success typings) so Dialyzer
> remains quiet.
>
> Arguably, if Dialyzer's analysis was strong enough to infer the type
>
> -spec bar (1) -> 'foo';
>                 (<Anything but 1>) -> 'bar',
>
> it could warn, but the above typing is way beyond Dialyzer.
>
> Tobias
>
> [1]
> http://www.it.uu.se/research/group/hipe/dialyzer/publications/succ_types.pdf
>
>
> 2015-01-01 17:24 GMT+01:00 Philip Müller <mail@REDACTED>:
>
>> Hi there,
>>
>> a few days ago I wanted to demonstrate the dialyzer to a friend who is
>> unfamiliar with erlang/otp.
>>
>> Unfortunately, my simplest demo case did not work. I made a github
>> project for it at [1] which documents the steps taken.
>>
>> For me, the first case (test.erl) looks like dialyzer is ignoring
>> -Wunmatched_returns completely. The second case (test2.erl) I don't
>> understand at all.
>>
>> Can someone explain what's going on there? Or should I file a bug report?
>>
>> Best regards
>>  Philip
>>
>> [1]: https://github.com/exterm/dialyzer-fail-example
>> _______________________________________________
>> erlang-questions mailing list
>> erlang-questions@REDACTED
>> http://erlang.org/mailman/listinfo/erlang-questions
>>
>
>
> _______________________________________________
> erlang-questions mailing list
> erlang-questions@REDACTED
> http://erlang.org/mailman/listinfo/erlang-questions
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20150121/68e661db/attachment.htm>