Check exhaustiveness argument-wise

[erszcz]

This enables checking exhaustiveness of functions of arity > 1 when some of the arguments cannot be
checked for exhaustiveness.

Consider the following example (Elixir syntax, but the problem is NOT Elixir specfic):

  @spec handle(message(), any, any) :: state()
  ## Try breaking the pattern match, e.g. by changing 'echo_req'
  def handle({:echo_req, payload}, from, state) do
    GenServer.reply(from, {:echo_res, payload})
    state
  end

  ## Try commenting out the following clause
  def handle({:hello, name}, from, state) do
    IO.puts("Hello, #{name}!")
    GenServer.reply(from, :ok)
    state
  end

Without this PR this function cannot be checked for exhaustiveness because arguments of type any are not refinable. However, the 2nd and 3rd arguments are not used for control flow and are not pattern matched on, so it's not useful to check if the function clauses exhaust them.

With this PR the exhaustiveness check is more flexible - it's up to the programmer to specify only some of the arguments to a level precise enough for exhaustiveness checking. Other, underspecified args, won't prevent the check from running on the well-specified ones.

[zuiderkwast]

I didn't read the code, but it's good to keep in mind that the arguments of a function clause can be treated as a tuple.

I.e. f(X,Y) is refineable if and only if case ... of {X,Y} is refinable.

[erszcz]

it's good to keep in mind that the arguments of a function clause can be treated as a tuple.

They can, but should they always be?
I'm looking at it from the perspective of utility - this PR makes the exhaustiveness check more useful for reporting non-exhaustiveness of a single specifically typed argument even when we know upfront the function is not total. I don't see a downside to this change, but I might be missing something.

[zuiderkwast]

it's good to keep in mind that the arguments of a function clause can be treated as a tuple.

They can, but should they always be?

Yes, I think they're equivalent.

That said, a free variable or _ exhausts any type (refinable/3 or not) so I think we should go that way instead.

Your example should be equally exhanstiveness-checking-enabled if all the args are wrapped in a tuple, don't you agree?

-type message() :: {echo_rec, any()} | {hello, any()}.
-spec handle({message(), any(), any()}) -> state().
handle({{echo_req, Payload} = Req, From, State}) ->
    gen_server:reply(From, Req),
    State;
handle({{hello, Name}, From, State}) ->
    io:format("Hello ~s!~n", [Name]),
    gen_server:reply(From, ok),
    State.

[erszcz]

Your example should be equally exhanstiveness-checking-enabled if all the args are wrapped in a tuple, don't you agree?

No, that's the whole point. From and State are specced as any(), so they're not going to be checked for exhaustiveness. This propagates to the whole tuple if they're going to be part of a tuple, which therefore disables the exhaustiveness check on a precisely specced Message :: message(). I omitted it from the original example, which might've made it unclear, but:

-type message() :: {echo_rec, string()} | {hello, string()}.

string() isn't that important, the important part is that it's a refinable / exhaustiveness-checking-enabled type, so message() doesn't have any ambiguity, it's completely exhaustiveness-checking-enabled too.

The example is actually a snippet taken from a bigger demo which you can check out at https://github.com/esl/gradient/blob/14ea6a70bef46f5b7e5ecb26cbedd9c1d989fb9c/examples/typed_gen_server/lib/typed_gen_server/stage1.ex#L55-L67.

[zuiderkwast]

I suppose you're right. For refinement, the args are equivalent to a tuple but for exhaustiveness they're separate. Thanks for convincing me.