match? pattern seems to not affect the type

[LostKobrakai]

lib/a.ex:6: The variable is expected to have type nonempty_list(A) but it has type list(integer())
4     cond do
5       [] == list -> 0
6       match?([_a], list) -> list |> hd()
7       true -> Enum.max(list)
8     end

I'm not sure where the issue comes from or if it's supposed to be covered, but neither match? nor a normal function pattern matching on the list holding one item will make the type be refined to nonempty_list.

[erszcz]

Hi, @LostKobrakai!

Thanks for the report, that's appreciated. Both cond and match? are Elixir specific, which means there's no direct support for them in Gradualizer. We'll have to do some research to understand what's going on under the hood, but it seems that match? compiles down to something which doesn't allow for refinement of list's type.

[LostKobrakai]

match? compiles to a case, which is why I also tried a function doing that. That also caused the same error.

# match?([_a], list)
case list do
  [_a] -> true
  _ -> false
end

[erszcz]

Ok, here's some research. This Elixir:

  @spec g(list(integer())) :: integer()
  def g(list) do
    cond do
      [] == list ->
        0
      match?([_|_], list) ->
        list |> hd()
      true ->
        Enum.max(list)
    end
  end

Compiles to this Erlang:

-spec g([integer()]) -> integer().
g(_list@1) ->
    case [] == _list@1 of
        true -> 0;
        false ->
            case case _list@1 of
                     [_ | _] -> true;
                     _ -> false
                 end
                of
                true -> erlang:hd(_list@1);
                false ->
                    case true of
                        true -> 'Elixir.Enum':max(_list@1);
                        false -> erlang:error(cond_clause)
                    end
            end
    end.

Which means we would have to come up with a custom rule to refine the type of the Elixir list variable to a nonempty_list(). We might do it at some point, but it's probably a bit more distant future.

The best we could do now is a manual type assertion, like this:

  @spec g(list(integer())) :: integer()
  def g(list) do
    cond do
      [] == list ->
        0
      match?([_|_], list) ->
        list |> assert_type(nonempty_list(integer())) |> hd()
      true ->
        Enum.max(list)
    end
  end

Annotations and assertions are supported by Gradualizer, so we're good with that. There are some hurdles on the Elixir level, though:

1. integer() and nonempty_list() are interpreted as undefined local functions and lead to errors before the abstract syntax of the calls is passed to the assert_type macro. We can sidestep that by an auxiliary BuiltinType module (which ultimately could become a part of Gradient). BuiltingType.integer() is an external call, therefore does not have to be defined in the local module and gets processed assert_type as intended.
2. integer() and nonempty_list() are names of builtin types, so we cannot override them even in BuiltinType. This means we have to add the _ suffixes.

These lead to the following code:

  @spec g(list(integer())) :: integer()
  def g(list) do
    cond do
      [] == list ->
        0
      match?([_|_], list) ->
        list |> assert_type(BuiltinType.nonempty_list_(BuiltinType.integer_())) |> hd()
      true ->
        Enum.max(list)
    end
  end

Which results in the following warning:

$ cat lib/zxc.ex
defmodule BuiltinType do
  @type integer_() :: integer()
  @type nonempty_list_(e) :: nonempty_list(e)
end

defmodule ZXC do

  use Gradient.TypeAnnotation

  @spec f(list(integer())) :: boolean()
  def f(list) do
    case list do
      [_a] -> true
      _ -> false
    end
  end

  @spec g(list(integer())) :: integer()
  def g(list) do
    cond do
      [] == list ->
        0
      match?([_|_], list) ->
        list |> assert_type(BuiltinType.nonempty_list_(BuiltinType.integer_())) |> hd()
      true ->
        Enum.max(list)
    end
  end

end
$ mix gradient
Loading deps...
Compiling project...
Typechecking files...
lib/zxc.ex: Call to undefined function BuiltinType.nonempty_list_/1 on line 24

The returned warning seems to be caused by a bug in Gradient.TypeAnnotation.assert_type/2.

Thanks again for the report, @LostKobrakai. A lot of food for thought, but we should be able to pull it off with a manual annotation in the short term and therefore pave the way for a builtin rule in the long run.

[erszcz]

@LostKobrakai Could you check if https://github.com/esl/gradient/pull/101 works for you with an explicit type annotation like this:

  @spec g(list(integer())) :: integer()
  def g(list) do
    cond do
      [] == list ->
        0
      match?([_|_], list) ->
        list |> assert_type(nonempty_list(integer())) |> hd()
      true ->
        Enum.max(list)
    end
  end

If it does, then we're halfway there, i.e. there's no automatic type refinement yet, but at least we can let the typechecker know about the refined type ourselves.

[LostKobrakai]

Just saw I need use Gradient.TypeAnnotation and it seems to work with that.

[erszcz]

Thanks for the confirmation, @LostKobrakai!

I'm reclassifying this as an enhancement, as automagic refinement would be nice, but now it's at least possible to solve the problem with an explicit annotation.