[erlang-questions] Strange Dialyzer behavior when matching record fields with opaque types

[Kostis Sagonas]

On 01/17/2017 11:18 PM, Nick Marino wrote:
>
> I recently encountered a rather strange, unexpected Dialyzer error. I'm
> unsure if this might be considered a Dialyzer bug, or if I'm just
> missing some key piece of knowledge that would help me understand what's
> going on here.
>
> I took the code that generated the warning and pruned it down down to this:
>
> -module(opaque_weirdness).
> -export([public_func/0]).
>
> -record(a, {
>     d = dict:new() :: dict:dict()
> }).
>
> -record(b, {
>     q = queue:new() :: queue:queue()
> }).
>
> public_func() ->
>     add_element(#b{}, my_key, my_value).
>
> add_element(#a{d = Dict}, Key, Value) ->
>     dict:store(Key, Value, Dict);
> add_element(#b{q = Queue}, Key, Value) ->
>     queue:in({Key, Value}, Queue).
>
> Which yields the following warning when I run it through Dialyzer:
>
> opaque_weirdness.erl:16: The attempt to match a term of type
> #b{q::queue:queue(_)} against the pattern {'a', Dict} breaks the
> opaqueness of queue:queue(_)
>
> It seems like this warning is somehow being triggered by the presence of
> the unused function clause in add_element. If I modify the code and add
> a line to public_func so that we use both clauses, then Dialyzer passes
> with no warnings.

Your analysis is pretty correct.  The issue is related to dead code and 
the warning you get is indeed confusing and weird.  This should be fixed 
in dialyzer.  Till then, you can suppress it either by commenting the 
unused first clause, which is dead code in your module, or by exporting 
function add_element/3.


What roughly happens here is that Dialyzer gets confused by the fact 
that the first clause will not be used and marks its arguments as having 
the type none(), i.e. not contributing to the inferred success typing. 
Then the warning pass sees the none() in the first argument of the 
clause and thinks it has been produced due to the call to add_element 
being with a record with a different opaque subterm: these opacity 
violations are also denoted by/resulting in the none() type.  But the 
pattern matching failure is on the #a{} vs. #b{} level, not on their 
subterms (fields).

Dialyzer _should_ issue a warning for this line, but the correct warning 
to issue here is something along the lines of:

opaque_weirdness.erl:16: The attempt to match a term of type 
#b{q::queue:queue(_)} against the pattern {'a', Dict} will not succeed

or that this clause will not be used since the success typing arguments 
of this function are (#b{}, _, _)

Kostis