[Dialyzer] false positive, "pattern will never match" on interaction with :queue

[sgfn]

Describe the bug
Dialyzer does not complain when code uses Enum.reverse/1, but when it is replaced with Qex.reverse/1 (which AFAIK is an Elixir wrapper on :queue.reverse/1), it emits several warnings seemingly unrelated to the call, such as "pattern will never match" and "guard can never succeed".

To Reproduce

1. Clone https://github.com/membraneframework/membrane_http_adaptive_stream_plugin (related PR: Fix CAN-SKIP-UNTIL and delta generation membraneframework/membrane_http_adaptive_stream_plugin#88)
2. Delete or comment out the @dialyzer tags in lib/membrane_http_adaptive_stream/hls.ex
3. Run mix deps.get and mix dialyzer

Expected behavior
Task mix.dialyzer passes with no warnings emitted

Affected versions
Elixir 1.15.5-otp-26
Erlang 26.0.2

Additional context
The Qex.reverse/1 call happens in the following function (source):

  defp maybe_calculate_delta_params(track, target_duration) do
    #snip
    with true <- Track.supports_partial_segments?(track),
         latest_full_segments <-
           track.segments
           |> Qex.reverse()
           |> Enum.drop_while(&(&1.type == :partial)),
         # snip
         true <- skip_count > 0 do
      delta_ctx = %{ #snip
      }

      {:create_delta, delta_ctx}
    else
      _any -> :dont_create_delta
    end
  end

If |> Qex.reverse() is replaced with |> Enum.reverse(), the Dialyzer warnings disappear. Interestingly, the warnings also disappear if you insert either |> IO.inspect() or |> Function.identity() just before |> Qex.reverse()...

The emitted warnings are:

lib/membrane_http_adaptive_stream/hls.ex:133:pattern_match
The pattern can never match the type.

Pattern:
{:create_delta, _delta_ctx}

Type:
:dont_create_delta

________________________________________________________________________________
lib/membrane_http_adaptive_stream/hls.ex:187:pattern_match
The pattern can never match the type.

Pattern:
_track = %Membrane.HTTPAdaptiveStream.Manifest.Track{}, [{:delta?, true}]

Type:
atom() | map(), [{:delta?, false}, ...]

________________________________________________________________________________
lib/membrane_http_adaptive_stream/hls.ex:311:guard_fail
The guard clause:

when _segments_to_skip_count :: 0 > 0

can never succeed.

________________________________________________________________________________
lib/membrane_http_adaptive_stream/hls.ex:413:guard_fail
The guard clause:

when _duration :: 0 > 0

can never succeed.

________________________________________________________________________________
done (warnings were emitted)
Halting VM with exit status 2

I wasn't able to reproduce the bug in a minimal example, so the problem may be caused by interactions with something else. Apologies in advance if this turns out not to be a Dialyzer issue

[paulo-ferraz-oliveira]

If I'm reading Qex's code correctly, the reverse/1 function is not a "simple" wrapper over queue:reverse/1, but rather

  @spec reverse(t) :: t
  def reverse(%__MODULE__{data: q}) do
    %__MODULE__{data: :queue.reverse(q)}
  end

where

@opaque t() :: %__MODULE__{:data => :queue.queue()}

Enum.reverse/1 takes in an Enumerable.t().
Qex.reverse/1 takes in a %__MODULE__{:data => :queue.queue()}, which is a struct.

That could well justify the issue you're seeing.

What happens if instead of Qex.reverse you actually pipe to :queue.reverse?

[starbelly]

I think what @paulo-ferraz-oliveira said is possible, but I think more likely is that dialyzer doesn't see a path where skip_count will ever be anything other than zero. If you start with your the last dialyzer error vs the first and start sorting out those issues I do believe you'll find this is not a problem with dialyzer but a problem with the code.

Dialyzer in this sense is never wrong 😄

Edit : If you hack around you will find this is issues ranging from the skip_count to, empty lists, indexes, etc.) You can make those problems go away, but you'll end up with an entirely new dialyzer error, which is also probably not wrong.

I hope this helps

[paulo-ferraz-oliveira]

Yeah, you're most likely right, @starbelly. I got side-tracked by the fact that "Elixir wrapper" is mentioned, but now I cloned and checked the code and %__MODULE__{:data => :queue.queue()} is track.segments, so using :queue.reverse won't fix it (and the same issues are still present), which means something within

    with true <- Track.supports_partial_segments?(track),
         true <- track_supports_delta_creation?(track),
         latest_full_segments <- ...

provokes an issue, per Dialyzer analysis (even if no issue is actually revealed when running the code, since this might be just typing).

Edit: and I also failed to see that "Inspect, Collectable and Enumerable are implemented"...

[sgfn]

Thanks for your time @paulo-ferraz-oliveira @starbelly; while I'm certain there is no dead/unaccessible code, I can't really pinpoint the exact source of this issue either :/

You can run mix test test/membrane_http_adaptive_stream/integration_test/sink_bin_integration_test.exs:220 to verify that both of the :(dont_)create_delta paths are executed

[kikofernandez]

Without knowing much about Elixir, my simplistic analysis is the same as @paulo-ferraz-oliveira

Apart from that, I think the entry point of serialize_segments is via serialize_track, and serialize_track is only called from here:

A quick look tells that line 135 sets always skip_count to 0, and line 145 as well, given its following definition:

defp serialize_track(
         %Track{} = track,
         target_duration,
         delta_ctx \\ %{skip_count: 0, skip_duration: 0}
       ) do
    supports_ll_hls? = Track.supports_partial_segments?(track)

so there is only one case to handle, line 138 for which Dialyzer seems to infer that skip_count: 0.

[starbelly]

This one continued to bug me 😄

So the problem here is non-obvious. I believe dialyzer is getting confused per opaque types and how the code ends up as erlang, specifically with map access in elixir (i.e., track.segments).

If you bind track.segments to another var and use that in place of track.segments before piping into Qex.reverse/1, all of your problems should go away.

If we de-compile the elixir to erlang we can perhaps start to get an idea of why (sort of) :

                        'Elixir.Enum':drop_while('Elixir.Qex':reverse(case
                                                                          _track@1
                                                                      of
                                                                          #{segments :=
                                                                                _@1} ->
                                                                              _@1;
                                                                          _@1
                                                                              when
                                                                                  is_atom(_@1),
                                                                                  _@1
                                                                                  =/=
                                                                                  nil,
                                                                                  _@1
                                                                                  =/=
                                                                                  true,
                                                                                  _@1
                                                                                  =/=
                                                                                  false ->
                                                                              _@1:segments();
                                                                          _@1 ->
                                                                              error({badkey,
                                                                                     segments,
                                                                                     _@1})
                                                                      end),...

Now, of course, that's nothing new, just how that works. I haven't seen a case like this before (or that I can remember), but it may be that the match all clause at the bottom doesn't doesn't play well with an opaque type of Qex.t/1 which in turn defines a type that is another opaque type (queue:queue/1).

You could swap it out for MapSet.t(), as those should be similar in their type definitions.

Likewise, you can avoid this situation by also opting out of specifying your segments key as Qex.t(Segments.t() and just go with Qex.t().

I'd have to dig further to understand what's going on, while Qex's types are little funny (defined slightly differently from how I've seen with modules such as MapSet or queue itself), that doesn't seem to be an issue though (in general).

Anyway, it's an interesting find none the less. Look forward to hearing more (if I don't dig first!) 😄

[sgfn]

Thank you @starbelly, binding track.segments to another variable certainly did the trick. The investigative work is much appreciated 🥇

The "unfixed" version will be available at the tag v0.17.0 in the repo, should anyone else want to have a look :)

[starbelly]

Thank you @starbelly, binding track.segments to another variable certainly did the trick. The investigative work is much appreciated 🥇

The "unfixed" version will be available at the tag v0.17.0 in the repo, should anyone else want to have a look :)

Cool. A couple of call outs.

1. Fixing up the type in qex (it's typed strange as far as opaque types go, see MapSet or queue for an example of a beter way) did not resolve the issue.
2. Being more specific around functions in qex also did not fix the issue.
3. While it may be that how the map access . expands is part of the problem, it's definitely not all of it. Clearly dialyzer had trouble finding a success path per that, but as stated, if you remove the sub-type, that also fixes the issue too. It's possible that the second clause in the expanded elixir code is also part of the issue here.

My 2 cents and hunch, which may be wrong, is this is not a problem in dialyzer. That said, purely out of interest and when I can find some type, I will see if I can reproduce the problem in erlang (unless someone gets there first).

[kikofernandez]

Thanks for all the work.
We are going to leave this ticket open for a bit in case someone can reproduce the error in Erlang with a minimal example, so that we could study why it goes wrong more easily.

Thanks everyone!