Dialyzer confusion over equal opaque and transparent types

[Kostis Sagonas]

On 2/25/20 11:12 AM, Dániel Szoboszlay wrote:
> Hi,
> 
> I have a small example where Dialyzer gives a very weird warning because 
> of some confusion over equal opaque and transparent types. Is this a bug 
> in Dialyzer or is there actually some type error here that my naked eyes 
> cannot see?
> 
>     -module(foo).
> 
>     -record(f, {f}).
>     -type   int() :: atom().
>     -opaque ext() :: int().
>     -opaque f() :: #f{f :: int()}.
> 
>     -export([f/1]).
>     -export_type([f/0, ext/0]).
> 
>     -spec f(f()) -> ok.
>     f(#f{f = F}) ->
>        x(F).
> 
>     -spec x(ext()) -> ok.
>     x(_) ->
>        ok.
> 
> 
> This module produces no Dialyzer warnings. However, a different module 
> using its API does: ... <SNIP>
> 
> The problem is actually caused by foo:x/1's type specification: it uses 
> the opaque ext() type instead of the transparent int().

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

I.e., either declare x/1 as taking an int(), because this is what the 
module-local x/1 function is called from the body of f/1, or, even 
simpler, simply remove the -spec for the x/1 function, so that you do 
not confuse dialyzer's type inferencer.

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.

Either of the above two actions will actually work and you will avoid 
the (admittedly confusing) warning.

> ... The two types [ext() and int()] are declared equal,

Not really; see below.

> so I'd assume they can be used interchangeably 
> within the foo module. The fact that ext() is opaque should only matter 
> in other modules. Yet, this construct somehow confuses Dialyzer.

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 is the reason why Brujo's suggestion

   >> Another way to make it work is to define your types like this…
   >>
   >> -opaque ext() :: atom().
   >> -type int() :: ext().
   >> -opaque f() :: #f{f :: int()}.

also stops confusing Dialyzer.  (By the way, this solution has nothing 
to do with "reversing any subtype" as written in that discussion.)


> To give some context for the curious: ... <SNIP> ...

<SNIP> because curiosity killed the cat :-)

Kostis