Support old-style 'catch' keyword

[erszcz]

The following code in rabbitmq/ra:

    case catch ra_server_sup_sup:restart_server(System, ServerId, #{}) of
        {ok, _} -> ok;
        {ok, _, _} -> ok;
        {error, _} = Err -> Err;
        {badrpc, Reason} -> {error, Reason};
        {'EXIT', Err} -> {error, Err}
    end.

fails with:

The pattern {'EXIT', Err} on line 179 at column 9 doesn't have the type {error, system_not_started} | {error, startchild_err()}

even though it's clear that the {'EXIT', Err} pattern is there to handle the result added by a call protected with catch.

[chiroptical]

@erszcz interested in trying to pick this up. Do you have any suggestions on where to start?

[chiroptical]

Why is this supposed to work?

https://github.com/rabbitmq/ra/blob/9be1971ccd6a55c8e030a903a82060ffc85dfe22/src/ra_server_sup_sup.erl#L49C9-L49C9

Wouldn't this need to describe the possibility of {'EXIT', _} as a return?

[chiroptical]

Ohh, I guess this is just how catch behaves. I am basically trying to make a smaller example,

-module(case_catch_expr_pass).

-export([bar/0]).

-spec foo() -> ok | no_return().
foo() -> throw({issue, "Issue"}).

-spec bar() -> ok | {error, term()}.
bar() ->
    case catch foo() of
        ok -> ok;
        {'EXIT', Err} -> {error, Err}
    end.

This yields

test/should_pass/case_catch_expr_pass.erl: The clause on line 12 at column 9 cannot be reached

[chiroptical]

If I read,

{error, system_not_started} | {error, startchild_err()}

How would it guarantee the x in {'EXIT', x} is that type? Can't you throw any type?

I am just trying to understand the issue.

[erszcz]

Hi, @chiroptical!

Firstly, sorry for a long lack of response. I'm volunteering on this project and sometimes I just don't have as much time to spend on it as I'd like to.

The point of this issue is that catch is not supported by Gradualizer yet. What is catch? It's a keyword predating the try ... catch ... mechanism which can be used to catch exceptions and handle them as first-class values, i.e. it's meant for value-based error handling.

So how does catch work? We can place it before an expression. If the expression evaluates to a value, catch just returns that value. If the expression throws an exception, catch catches that exception and converts to a tuple of the {'EXIT', _the_exception} form. It's described in more detail in the Reference Manual.

This means that in the example at the top when we do case catch ... of ... end:

    case catch ra_server_sup_sup:restart_server(System, ServerId, #{}) of
        {ok, _} -> ok;
        {ok, _, _} -> ok;
        {error, _} = Err -> Err;
        {badrpc, Reason} -> {error, Reason};
        {'EXIT', Err} -> {error, Err}
    end.

The case has to have clauses for each of ra_server_sup_sup:restart_server/3 return type's variants (that you correctly point at in one of your comments), but it also needs the special clause for the case when catch catches an exception and converts it - the {'EXIT', Err} clause.

Gradualizer should be aware of that, i.e. it should realise that given expression E of type T (also written as E :: T) the type of expression catch E is T | {'EXIT', any()}. If we made the typechecker understand that, then exhaustiveness checking would immediately remind us whether we're handling the {'EXIT', any()} clause when doing catch case ... of ....

Your attempt at minimising the initial example is a good one! However, we cannot expect the X in {'EXIT', X} to be of any particular type - we have to accept any() there.