[erlang-questions] Recent OTP dev branch dialyzer changes (when-constraints)

[Jesper Louis Andersen]

PRELIMINARIES

In the commit,

git show 76ca320fd37cecdcf225ddcc094bc72a607b0453 queue.erl

commit 76ca320fd37cecdcf225ddcc094bc72a607b0453
Author: Hans Bolinder <hasse@REDACTED>
Date:   Fri May 6 15:11:15 2011 +0200

    Types and specifications have been modified and added

we have the following hunk change:

@@ -133,7 +146,10 @@ in_r(X, Q) ->
 %% Take from head/front
 %%
 %% O(1) amortized, O(len(Q)) worst case
--spec out(queue()) -> {'empty' | {'value',term()}, queue()}.
+-spec out(Q1) -> Result when
+      Q1 :: queue(),
+      Q2 :: queue(),
+      Result :: {{value, Item :: term()}, Q2} | {empty, Q1}.
 out({[],[]}=Q) ->
     {empty,Q};
 out({[V],[]}) ->

QUESTION:

I have not seen this style before, and EEP-008 / The Reference
documentation makes little reason as to why one would want to change
the "polarity" from positive to negative in the spec constraint.

* What is the reason for the change? I think the change better
reflects the style of other user documentation which is a nice
welcome.

* I am asking because I don't know why the dialyzer complains in my
code. I have a recent branch with the following code:

-record(proc_info, {
	  receiver_q :: queue(),
	  sender_q   :: queue()
}).
-opaque t() :: #proc_info{}.
-export_type([t/0]).
...
-spec dequeue_receiver(t()) -> {ok, term(), t()} | empty.
dequeue_receiver(#proc_info { receiver_q = RQ } = PI) ->
    case queue:out(RQ) of
        {{value, Item}, NQ} ->
            {ok, Item, PI#proc_info { receiver_q = NQ }};
        {empty, _Q} ->
            empty
    end.

which uses the queue:out/2 call. And the dialyzer complains:

utp_process.erl:49: The specification for
utp_process:dequeue_receiver/1 states that the function might also
return {'ok',_,utp_process:t()} but the inferred return is 'empty'

This puzzles me! Clearly queue:out/2 may return '{empty, queue()}'. Is
the dialyzer so strong it guesses RQ is *never* anything but empty?
This is odd because if I look at coverage from my test runs, both
cases are covered (cue bad formatting if you have a non-monospaced
font):

        |  dequeue_receiver(#proc_info { receiver_q = RQ } = PI) ->
124304..|      case queue:out(RQ) of
        |          {{value, Item}, NQ} ->
   151..|              {ok, Item, PI#proc_info { receiver_q = NQ }};
        |          {empty, _Q} ->
124153..|              empty
        |      end.

also note that there is only one call-site of dequeue_receiver/1,
which leads me to think the dialyzer is wrong here, even though I know
the dialyzer is *always right*(tm) :)

VERSION OF ERLANG/OTP: Very recent:

jlouis@REDACTED:~/Projects/otp$ git describe
OTP_R14B02-625-g5f7fa62

Also, ask if more source in my project is needed. If there is any
interest I'll try to boil it down to a minimal example.


-- 
J.