`if` expression support and type refinement

[eksperimental]

I have

  @spec child_pid(term) :: pid | nil
  def child_pid(term) when not is_pid(term) do
    pid({:child, term})
  end

  def child_pid(pid) do
    case Supervisor.which_children(pid) do
      [{_id, child_pid, _type, _modules}] ->
        if is_pid(child_pid) do
          child_pid
        else
          nil
        end

      _ ->
        nil
    end
  end

I'm getting:

lib/checker/util.ex: The variable on line 59 is expected to have type pid() | nil but it has type :restarting | :undefined | pid()
57       [{_id, child_pid, _type, _modules}] ->
58         if is_pid(child_pid) do
59           child_pid
60         else
61           nil

I don't think it should get any error,

Rewritting the clause like this makes the error go away, and it is clearer, but I thought of sharing it here anyway.

  def child_pid(pid) do
    case Supervisor.which_children(pid) do
      [{_id, child_pid, _type, _modules}] when is_pid(child_pid) ->
        child_pid

      _ ->
        nil
    end
  end

[erszcz]

Thanks, @eksperimental, good catch! The Elixir if is compiled to an Erlang case and it seems something is too quirky in the resulting code to be type checked properly. Marking it as a bug.

[hworld]

Not sure if this belongs here or in a new issue. It seems to be potentially the same issue.

@spec handle(pos_integer() | nil) :: :ok
def handle(id) do
  if id != nil do
    # This has an error complaining about nil.
    do_something(id)
  end
  
  case id do
    id when id != nil ->
      # This is correctly narrowed to just pos_integer().
      do_something(id)
      
    _ ->
      nil
  end
  
  # This is how elixir seems to compile the above if expression.
  case id != nil do
    false ->
      nil
    
    true ->
      # This also fails like the above if.
      do_something(id)
  end
  
  :ok
end
  
@spec do_something(pos_integer()) :: :ok
def do_something(id), do: id

Does Gradualizer only work with guards for refining the type?

[erszcz]

Hi, @hworld!

Thanks for your interest and another example. Indeed, it seems to be another case of the same issue. We're aware that refinement is still somewhat limited and this seems to one of the cases where it's clearly visible.