[erlang-questions] dialyzer is driving me nuts

[Jesper Louis Andersen]

On Tue, Oct 18, 2011 at 20:45, Joel Reymont <joelr1@REDACTED> wrote:

> Expanding the type spec to
>
> -spec barrier_start(#game{}, game_ctx(), barrier_event()) -> {continue, #game{}, game_ctx()};
>                   (#game{}, game_ctx(), {'EXIT', pid(), _}) -> {stop, #game{}, game_ctx()};
>                   (#game{}, game_ctx(), _) -> {skip, #game{}, game_ctx()}.
>
> results in an error
>
> barrier_start.erl:50: Overloaded contract has overlapping domains; such contracts are currently unsupported and are simply ignored

Yes, because now your 2nd and 3rd input is overlapping. Note that the
2nd is a specialized variant of the 3rd (technically, a subtype).
These are not yet used by Dialyzer. Basically, given an output, the
inputs must be discriminable from each other. You have to coalesce the
inputs and outputs. It is weaker, but few type systems actually
support the above notion.

>
> I tried to dialyze a simple module, e.g.
>
> -module(z).
>
> -compile([export_all]).
>
> -record(z, {
>    xref = gb_trees:empty()
>  }).
>
> -spec foo(#z{}) -> tuple().
>
> foo(Z = #z{}) -> Z#z.xref.
>
> Dialyzer did not warn me on the mismatch between tuple() and gb_tree(), though.
>
> After removing the foo spec, Typer told me that the return type is any().

Technically, the dialyzer doesn't see anything problematic here. If
foo/1 terminates, the output is a tuple() and the input is of type
#z{}. So the success typing is okay. If you kill the foo spec, then
clearly, due to erlang semantics, it doesn't matter what is in xref,
the function will terminate. So as long as the input has the structure
of an #z{} record, the function terminates, irrespective of the value
inside that #z{}.

Note that without the spec, the notion 'Z = #z{}' is just a match
against if Z has record structure, {'Z', ...}. Nothing more. #z.xref
is handled at compile time and expanded, so this is rougly equivalent
to:

foo({'Z', Xref}) -> Xref.

which clearly has a type in which Xref is any().

-- 
J.