Dialyzer confusion over equal opaque and transparent types

classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

Dialyzer confusion over equal opaque and transparent types

Dániel Szoboszlay
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:

-module(bar).
-export([f/1]).

-spec f(foo:f()) -> ok.
f(F) ->
  foo:f(F).

This would generate the below warning (with OTP 22.2.3):

bar.erl:4: Invalid type specification for function bar:f/1. The success typing is
          (foo:f()) -> 'ok'

This warning doesn't make any sense: the type specification for bar:f/1 is the same as the success typing found by Dialyzer. The problem is actually caused by foo:x/1's type specification: it uses the opaque ext() type instead of the transparent int(). The two types are declared equal, 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.

To give some context for the curious: the purpose of the equivalent ext() and int() types is that this type shall be transparent within the application (there are multiple modules using it), but opaque to the outside world. So internally the application uses the int() type, but all API functions that the outside world shall rely on use ext() instead (and they are all in the same module that declares the opaque type, so it can safely look into ext()-s and "convert" them into int()-s).

/Daniel
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer confusion over equal opaque and transparent types

Brujo Benavides-3
I think there is a bug somewhere, but as you probably know the warning also goes away if you change this…
-opaque f() :: #f{f :: int()}.
…to this…
-opaque f() :: #f{f :: ext()}.

And the thing is that, according to what I think dialyzer believes, all ext()s are int()s but not all int()s are ext()s. You can't pass an expression of type int() to a function that expects something with type ext(), because you're breaking opacity (in dialyzer's mind).

On Tue, Feb 25, 2020 at 11:13 AM Dániel Szoboszlay <[hidden email]> 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:

-module(bar).
-export([f/1]).

-spec f(foo:f()) -> ok.
f(F) ->
  foo:f(F).

This would generate the below warning (with OTP 22.2.3):

bar.erl:4: Invalid type specification for function bar:f/1. The success typing is
          (foo:f()) -> 'ok'

This warning doesn't make any sense: the type specification for bar:f/1 is the same as the success typing found by Dialyzer. The problem is actually caused by foo:x/1's type specification: it uses the opaque ext() type instead of the transparent int(). The two types are declared equal, 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.

To give some context for the curious: the purpose of the equivalent ext() and int() types is that this type shall be transparent within the application (there are multiple modules using it), but opaque to the outside world. So internally the application uses the int() type, but all API functions that the outside world shall rely on use ext() instead (and they are all in the same module that declares the opaque type, so it can safely look into ext()-s and "convert" them into int()-s).

/Daniel


--
Brujo Benavides
about.me/elbrujohalcon
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer confusion over equal opaque and transparent types

Brujo Benavides-3
Another way to make it work is to define your types like this…

-opaque ext() :: atom().
-type int() :: ext().
-opaque f() :: #f{f :: int()}.

In other words, reversing the subtyping by making int/0 a subtype of ext/0. Remember: :: does not mean "is equal to" it means "is a subtype of".

On Tue, Feb 25, 2020 at 11:43 AM Fernando Benavides <[hidden email]> wrote:
I think there is a bug somewhere, but as you probably know the warning also goes away if you change this…
-opaque f() :: #f{f :: int()}.
…to this…
-opaque f() :: #f{f :: ext()}.

And the thing is that, according to what I think dialyzer believes, all ext()s are int()s but not all int()s are ext()s. You can't pass an expression of type int() to a function that expects something with type ext(), because you're breaking opacity (in dialyzer's mind).

On Tue, Feb 25, 2020 at 11:13 AM Dániel Szoboszlay <[hidden email]> 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:

-module(bar).
-export([f/1]).

-spec f(foo:f()) -> ok.
f(F) ->
  foo:f(F).

This would generate the below warning (with OTP 22.2.3):

bar.erl:4: Invalid type specification for function bar:f/1. The success typing is
          (foo:f()) -> 'ok'

This warning doesn't make any sense: the type specification for bar:f/1 is the same as the success typing found by Dialyzer. The problem is actually caused by foo:x/1's type specification: it uses the opaque ext() type instead of the transparent int(). The two types are declared equal, 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.

To give some context for the curious: the purpose of the equivalent ext() and int() types is that this type shall be transparent within the application (there are multiple modules using it), but opaque to the outside world. So internally the application uses the int() type, but all API functions that the outside world shall rely on use ext() instead (and they are all in the same module that declares the opaque type, so it can safely look into ext()-s and "convert" them into int()-s).

/Daniel


--
Brujo Benavides
about.me/elbrujohalcon


--
Brujo Benavides
about.me/elbrujohalcon
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer confusion over equal opaque and transparent types

Dániel Szoboszlay
In reply to this post by Brujo Benavides-3
all ext()s are int()s but not all int()s are ext()s.
 
This is true, ext() is declared to be a subtype of int(), so it refers to a subset of the terms that are int()-s.

You can't pass an expression of type int() to a function that expects something with type ext(), because you're breaking opacity (in dialyzer's mind).

That would be true in a different module, but within the module where you declare an opaque type you are allowed to break opacity. (Otherwise an opaque type would be completely useless.) 

Daniel
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer confusion over equal opaque and transparent types

Dániel Szoboszlay
In reply to this post by Brujo Benavides-3
Reversing the subtyping solves this problem, but makes int() unusable outside of the foo module. If the foo module would return an int() value from an exported function, bar couldn't look into it, because int() is just a subtype of the opaque type ext(), and Dialyzer would (rightfully) give you a warning about peeking into an opaque type.

/Daniel

On Tue, 25 Feb 2020 at 11:51, Fernando Benavides <[hidden email]> wrote:
Another way to make it work is to define your types like this…

-opaque ext() :: atom().
-type int() :: ext().
-opaque f() :: #f{f :: int()}.

In other words, reversing the subtyping by making int/0 a subtype of ext/0. Remember: :: does not mean "is equal to" it means "is a subtype of".

On Tue, Feb 25, 2020 at 11:43 AM Fernando Benavides <[hidden email]> wrote:
I think there is a bug somewhere, but as you probably know the warning also goes away if you change this…
-opaque f() :: #f{f :: int()}.
…to this…
-opaque f() :: #f{f :: ext()}.

And the thing is that, according to what I think dialyzer believes, all ext()s are int()s but not all int()s are ext()s. You can't pass an expression of type int() to a function that expects something with type ext(), because you're breaking opacity (in dialyzer's mind).

On Tue, Feb 25, 2020 at 11:13 AM Dániel Szoboszlay <[hidden email]> 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:

-module(bar).
-export([f/1]).

-spec f(foo:f()) -> ok.
f(F) ->
  foo:f(F).

This would generate the below warning (with OTP 22.2.3):

bar.erl:4: Invalid type specification for function bar:f/1. The success typing is
          (foo:f()) -> 'ok'

This warning doesn't make any sense: the type specification for bar:f/1 is the same as the success typing found by Dialyzer. The problem is actually caused by foo:x/1's type specification: it uses the opaque ext() type instead of the transparent int(). The two types are declared equal, 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.

To give some context for the curious: the purpose of the equivalent ext() and int() types is that this type shall be transparent within the application (there are multiple modules using it), but opaque to the outside world. So internally the application uses the int() type, but all API functions that the outside world shall rely on use ext() instead (and they are all in the same module that declares the opaque type, so it can safely look into ext()-s and "convert" them into int()-s).

/Daniel


--
Brujo Benavides
about.me/elbrujohalcon


--
Brujo Benavides
about.me/elbrujohalcon
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer confusion over equal opaque and transparent types

Kostis Sagonas-2
In reply to this post by Dániel Szoboszlay
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
Reply | Threaded
Open this post in threaded view
|

Re: Dialyzer confusion over equal opaque and transparent types

Dániel Szoboszlay
On Wed, 26 Feb 2020 at 00:24, Kostis Sagonas <[hidden email]> 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).

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