<div dir="ltr"><div dir="ltr">On Wed, 26 Feb 2020 at 00:24, Kostis Sagonas <<a href="mailto:kostis@cs.ntua.gr">kostis@cs.ntua.gr</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Right.  Since you have figured out what the problem is, why don't you <br>
use some solution along those lines?<br></blockquote><div><br></div><div>I figured out a <i>workaround</i> for a bug in Dialyzer. That's lucky, but I would strongly prefer the bug to be fixed. Or actually, multiple bugs:</div><div><ul><li>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.</li><li>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.</li><li>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.</li></ul></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Note that x/1 is a module-local function, so there is really no good <br>
reason to declare a spec for it, let alone declare that it is called <br>
with some opaque term.<br></blockquote><div><br></div><div>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.</div><div>But my real problem with this advise is this: what would happen if foo:x/1 would be an exported function?</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">You are probably missing a very subtle difference between -type and <br>
-opaque declarations. (This is not your fault, because I think that the <br>
reference manual does not explain this very well.)  Opaque declarations <br>
are actually of the form TypeName :: TermStructure, i.e., the right hand <br>
side declares the structure of the opaque terms of that type name.<br>
<br>
They do not declare type aliases (as e.g., the -type int() :: atom(). <br>
declaration does).<br></blockquote><div><br></div><div>This doesn't seem to match the reference manual: <a href="http://erlang.org/doc/reference_manual/typespec.html#type-declarations-of-user-defined-types">http://erlang.org/doc/reference_manual/typespec.html#type-declarations-of-user-defined-types</a></div></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div class="gmail_quote"><div><p style="max-width:42em;color:rgb(26,26,26);font-family:sans-serif;font-size:16px;background-color:rgb(254,254,254)">New types are declared using <span class="gmail-code" style="font-family:mono,Courier,monospace;background-color:rgb(243,243,243)">-type</span> and <span class="gmail-code" style="font-family:mono,Courier,monospace;background-color:rgb(243,243,243)">-opaque</span> attributes as in the following:</p></div></div><div class="gmail_quote"><div><div class="example" style="background-color:rgb(241,243,245);border:1px solid rgb(222,226,230);padding:0.5em 1em;margin:1em 0px;font-size:0.7em;color:rgb(26,26,26);font-family:sans-serif"><pre style="font-family:mono,Courier,monospace;margin-top:0px;margin-bottom:0px">  -type my_struct_type() :: Type.
  -opaque my_opaq_type() :: Type.</pre></div></div></div></blockquote><div class="gmail_quote"><div>The right hand side is documented to be a Type in both cases, and both attributes are documented to declare new types.</div><div><br></div><div>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:</div><div><br></div></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div class="gmail_quote"><div><font face="monospace">-spec g(x) -> ok.</font></div></div><div class="gmail_quote"><div><font face="monospace">g(X) -></font></div></div><div class="gmail_quote"><div><font face="monospace">  x(X).</font></div></div><div class="gmail_quote"><div><font face="monospace"><br></font></div></div><div class="gmail_quote"><div><font face="monospace">-spec h(x) -> ok.</font></div></div><div class="gmail_quote"><div><font face="monospace">h(X = x) -></font></div></div><div class="gmail_quote"><div><font face="monospace">  x(X).</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">-spec i(x | integer()) -> ok.<br>i(X) when is_integer(X) -><br>  ok;<br>i(X) -><br>  x(X).</font><br></div></div></blockquote><div class="gmail_quote"><div><br></div><div>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).</div><div><br></div><div>Daniel</div></div></div>