[erlang-questions] dialyzer issue with opaque types

[Kostis Sagonas]

On 09/19/2013 09:35 AM, Samuel wrote:
> Hi,
>
> I have next two (trimmed down) modules I want to dialyze (attached as well) :
>
> -module(foo).
>
> -export([foo/0]).
>
> -spec foo() -> bar:id().
> foo() -> bar:id_undef().
>
> --------------------------------------------------
>
> -module(bar).
>
> -export([id_undef/0]).
>
> -opaque undef() :: -1.
> -opaque id() :: undef().
>
> -export_type([id/0, undef/0]).
>
> -spec id_undef() -> id().
> id_undef() -> -1.
>
> -----------------------------------------------
>
> Running dialyzer on those fails like this:
>
> $ erlc +debug_info *.erl && dialyzer *.beam
>    Checking whether the PLT
> /home/samuel/local/var/dialyzer/plts/R16B02-src/otp.plt is
> up-to-date...
>   yes
>    Proceeding with analysis...
> foo.erl:5: Invalid type specification for function foo:foo/0. The
> success typing is () -> bar:id()
>   done in 0m3.02s
> done (warnings were emitted)
>
> That is, dialyzer thinks that bar:id() is the bad result type and that
> I should be using bar:id() instead :)

I can very well see why some would classify this as a dialyzer bug (I 
see that you were careful to use the word "issue" in the subject header) 
but I am afraid that it is more of a limitation (or is 
"misunderstanding" a better term here?) of how opaques work.

Dialyzer expects that the opaque declaration is something of the form:

  -opaque <type name> :: <type structure>.

where <type structure> describes the structure of terms that belong to 
the opaque type.  Ideally, the structure of these terms should be 
clearly distinguishable from that of all other type names that the 
module contains, hence we are prohibiting declarations of the form:

  -opaque <type name> :: term().

As a convenience to the programmer, we have so far allowed that type 
declarations can contain names of other type names where term structures 
are expected, i.e. declarations of the form

   <type_name> :: <type_name>

as in your program.

I am afraid this is problematic in the case of opaques, because the 
analysis is unable to classify on which opaque sort terms belong in this 
case. Is a -1 term an id() or an undef() in your example? OK, you have 
the spec declaration, but should dialyzer trust it? What I am trying to 
write is that general confusion can arise in these cases.
This is what happens here, hence the confusing warning.

To make the long story short, you can fix the immediate problem of this 
example at least by changing the declarations to:

-opaque undef() :: -1.
-opaque id() :: -1.

but whether this "solution" extends to the untrimmed program or not, I 
do not know. As I explained, it's problematic to have terms of the same 
structure belonging to different sorts of opaque types.

I'll look into this issue more closely.  Thanks for the report!

Kostis