Dialyzer confusion over equal opaque and transparent types

[Fernando Benavides]

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 <elbrujohalcon@REDACTED>
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 <dszoboszlay@REDACTED>
> 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
>>
>
>
> --
>
> <https://about.me/elbrujohalcon?promo=email_sig&utm_source=product&utm_medium=email_sig&utm_campaign=gmail_api&utm_content=thumb>
> Brujo Benavides
> about.me/elbrujohalcon
> <https://about.me/elbrujohalcon?promo=email_sig&utm_source=product&utm_medium=email_sig&utm_campaign=gmail_api&utm_content=thumb>
>


-- 
<https://about.me/elbrujohalcon?promo=email_sig&utm_source=product&utm_medium=email_sig&utm_campaign=gmail_api&utm_content=thumb>
Brujo Benavides
about.me/elbrujohalcon
<https://about.me/elbrujohalcon?promo=email_sig&utm_source=product&utm_medium=email_sig&utm_campaign=gmail_api&utm_content=thumb>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20200225/a45a9b54/attachment.htm>