Dialyzer confusion over equal opaque and transparent types

[Dániel Szoboszlay]

On Wed, 26 Feb 2020 at 00:24, Kostis Sagonas <kostis@REDACTED> wrote:

> Right.  Since you have figured out what the problem is, why don't you
> use some solution along those lines?
>

I figured out a *workaround* for a bug in Dialyzer. That's lucky, but I
would strongly prefer the bug to be fixed. Or actually, multiple bugs:

   - The warning produced by Dialyzer is wrong. A tool simply cannot check
   my code and tell me "this line is incorrect, you should change it to X"
   where X is a verbatim copy of what I have there already. If a tool tells me
   this, it is a bug and should be fixed.
   - If there is any kind of problem Dialyzer should warn me about, it is
   within the foo module, and not in bar. If the type spec of foo:f/1 is
   correct, the type spec of bar:f/1 must be correct as well - I hope we can
   agree on this one at least. But it implies that Dialyzer shall give a
   warning on foo:f/1 too if it gives a warning on bar:f/1. It does not, so
   this is a bug that should be fixed.
   - And finally, there's a question about whether foo:f/1 does something
   wrong or not. Dialyzer believes it does, I believe it does not. I'm not
   sure who's right, that's what I wanted to ask in my first email. If I'm
   right, and foo:f/1 doesn't have any type errors, than that's the third a
   bug in Dialyzer.



> Note that x/1 is a module-local function, so there is really no good
> reason to declare a spec for it, let alone declare that it is called
> with some opaque term.
>

First of all, I think there's a good reason for declaring specs for
module-local functions too, namely that the developer can read them and
know how to use the functions.
But my real problem with this advise is this: what would happen if foo:x/1
would be an exported function?


> You are probably missing a very subtle difference between -type and
> -opaque declarations. (This is not your fault, because I think that the
> reference manual does not explain this very well.)  Opaque declarations
> are actually of the form TypeName :: TermStructure, i.e., the right hand
> side declares the structure of the opaque terms of that type name.
>
> They do not declare type aliases (as e.g., the -type int() :: atom().
> declaration does).
>

This doesn't seem to match the reference manual:
http://erlang.org/doc/reference_manual/typespec.html#type-declarations-of-user-defined-types

New types are declared using -type and -opaque attributes as in the
following:

  -type my_struct_type() :: Type.
  -opaque my_opaq_type() :: Type.

The right hand side is documented to be a Type in both cases, and both
attributes are documented to declare new types.

Also, I don't understand how opaque declaring a TermStructure would explain
the confusion of Dialyzer. Consider the below two functions (in module foo)
for example:

-spec g(x) -> ok.
g(X) ->
  x(X).

-spec h(x) -> ok.
h(X = x) ->
  x(X).

-spec i(x | integer()) -> ok.
i(X) when is_integer(X) ->
  ok;
i(X) ->
  x(X).


Calling g/1 from a different module triggers the warning, but calling h/1
or i/1 is OK. Why? The success typing of g/1 is ((ext()) -> ok), but why is
the caller checked against this type, when the spec clearly restricts the
argument to a single, transparent atom? The success typing of i/1 is
((integer() | ext()) -> ok) as well, but the caller is checked against the
declared type spec this time (even though the success typing of the caller
still contains ext() instead of the atom x).

Daniel
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20200227/5cc7af0b/attachment.htm>