WhatsApp / eqwalizer

A type-checker for Erlang
Apache License 2.0
506 stars 27 forks source link

eqwalizer warns about subtypes that can't be possible at the error line #20

Closed gonzalobf closed 1 year ago

gonzalobf commented 1 year ago

Sorry, if the title is not the best one but I tried to condense everything in a few words.

I was playing with eqwalizer in a project where I have a module similar to the example below. The module is a gen_server with socket in the #state{}. The socket can be undefined when there is no connection or gen_tcp:socket() when there is one. I have simulated the socket with two atoms: undefined | connected

-module(example).

-behaviour(gen_server).

-export([
    start_link/0,
    init/1,
    handle_cast/2,
    handle_call/3
]).

-record(state, {socket = undefined :: connected | undefined}).

start_link() ->
    gen_server:start_link(?MODULE, [], []).

init([]) ->
    {ok, #state{}}.

handle_call(_Msg, _From, State) ->
    {reply, ok, State}.

handle_cast(_Msg, #state{socket=undefined}) ->
    {noreply, #state{socket=connected}};
handle_cast(_Msg, State=#state{socket=Socket}) ->
  % At this point Socket can only be connected
    send(Socket),
    {noreply, State}.

-spec send(connected) -> ok.
send(connected) ->
    ok. 

Output:

error: expected_subtype
   ┌─ apps/example/src/example.erl:28:10
   │
28 │     send(Socket),
   │          ^^^^^^
   │          │
   │          Socket.
Expected: 'connected'
Got     : 'connected' | 'undefined'

   │

  'connected' | 'undefined' is not a subtype of 'connected'
  because
  'undefined' is not a subtype of 'connected'

I was expecting eqwalizer not to raise an error in send(Socket) since at this point Socket can't be undefined. If it was, the first handle_cast would have match and run the code inside. I can avoid the eqwalizer error by adding when Socket =/= undefined -> in the second handle_cast, but I was wondering if there are plans of supporting this in the future.

Than you

ilya-klyuchnikov commented 1 year ago

By default eqWAlizer may not refine record fields in general (as it may result in performance issues on average - especially with gigantic records). However, it is possible to force eqWAlizer to be smarter about it in two steps:

  1. Mark the field as refinable by using eqwalizer:refinable(X) marker: (https://github.com/WhatsApp/eqwalizer/blob/9935940d71ef65c7bf7a9dfad77d89c0006c288e/eqwalizer/test_projects/eqwalizer/src/eqwalizer.erl#L47-L54
  2. Add an explicit spec for handle_cast

This works:

...

-record(state, {
  socket = undefined :: eqwalizer:refinable(connected | undefined)
}).

...

-spec handle_cast(term(), #state{}) -> {noreply, #state{}}.
handle_cast(_Msg, #state{socket=undefined}) ->
    {noreply, #state{socket=connected}};
handle_cast(_Msg, State=#state{socket=Socket}) ->
    send(Socket),
    {noreply, State}.
gonzalobf commented 1 year ago

Cool! thank you :)

Closing it since there is a workaround.