[erlang-questions] dialyzer issue with opaque types
Fri Sep 20 11:29:58 CEST 2013
On 09/19/2013 09:35 AM, Samuel wrote:
> I have next two (trimmed down) modules I want to dialyze (attached as well) :
> -spec foo() -> bar:id().
> foo() -> bar:id_undef().
> -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
> 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!
More information about the erlang-questions