[erlang-bugs] dialyzer does not like queue:out

[Paul Guyot]

Hello,

Dialyzer seems to consider that the second element of the output of queue:out/1 is not a queue.

The following code reproduces the error:

--------------------------
-module(dialyzer_queue).
-export([f/1]).

-record(rec, {
    q :: queue()
    }).

-spec f(#rec{}) -> ok.
f(Rec) ->
    case g(Rec) of
        {ok, _Value, _NewRec} -> ok;
        {none, _NewRec} -> ok
    end.

g(#rec{q = Queue} = Rec) ->
    case queue:out(Queue) of
        {empty, _} -> {none, Rec};
        {{value, Elem}, NewQueue} -> {ok, Elem, #rec{q = NewQueue}}
    end.
--------------------------

Dialyzer will say:

dialyzer_queue.erl:11: The pattern {'ok', _Value, _NewRec} can never match the type {'none',#rec{q::queue()}}

The error disappears if g returns {ok, Elem, Rec} instead of {ok, Elem, #rec{q = NewQueue}}, or if rec.q is typed as any().

Paul
-- 
Semiocast            http://semiocast.com/
+33.183627948 - 20 rue Lacaze, 75014 Paris