Confused about spec/dialyxir: "Invalid type specification for function"

Questions / Help
,
1

Hi,

I’m trying to get hang of specs, but I’ve hit a wall. I’m writing a thin facade over Nerves’ SystemRegistry, basically stuff like:

defmodule ConfigRegistry do
  @spec update(SystemRegistry.scope(), any) :: {:ok, {map, map}} | {:error, term}
  def update(scope, value) do
    SystemRegistry.update([:config | scope], value)
  end
end

Running mix dialyzer on that results in

lib/config_registry.ex:2:invalid_contract
Invalid type specification for function.

Function:
ConfigRegistry.update/2

Success typing:
@spec update([any()], _) :: %SystemRegistry.Transaction{
  :delete_nodes => MapSet.t(_),
  :deletes => MapSet.t(_),
  :key => _,
  :opts => Keyword.t(),
  :pid => pid(),
  :update_nodes => MapSet.t(_),
  :updates => map()
}

A quick look at

tells me there are two updates, one that can be used standalone (this is the one I’m interested in), and the other one for use with an open transaction.

The functions are specced like this:

@spec update(one, scope, value :: any) :: Transaction.t() when one: Transaction.t()
@spec update(one, value :: any, opts :: Keyword.t()) ::
          {:ok, {new :: map, old :: map}} | {:error, term}
        when one: scope

I can sort of understand dialyxir’s complaint, if I make an assumtion that it cannot recognize [:config | scope] as something that is not a SystemRegistry.Transaction.t(). But that assumption seems very wrong.

So… Either (and most likely) I’m missing some crucial and basic knowledge of spec, there is an error in SystemRegistry.update spec, or a bug in Dialixyr.

How can I persuade Dialyxir my code will always call the standalone update function?

2

A spec will not actually constrain the input to your update function. If someone calls your function with a Transaction.t for the first parameter, you will invoke the other clause in Nerves. Did you try adding a when clause to your update like when is_list(scope) ?

3

Thanks for the input.

I won’t; Note that [:config | scope] is passed to SystemRegistry.update.

I did. No success.

4

This is where your mental model breaks down: there is only and there can only be one update/3 function. That function may be implemented in terms of multiple function clauses - but they all belong to the same function.

The Erlang style of specs make that much clearer:

-spec foo(pos_integer()) -> pos_integer()
         ; (integer()) -> integer().

So strictly speaking the return type of SystemRegistry.update/3 is the sum type Transaction.t() | {:ok, {new :: map, old :: map}} | {:error, term}.

A more type-aware module API would have

  • SystemRegistry.update_with_scope/3
  • SystemRegistry.update_with_transaction/3
  • And a convenience function SystemRegistry.update/3 that delegates appropriately.

but given that Erlang/Elixir is dynamically typed you will run into functions that have only been typed after the fact rather than being designed with types in mind.

3 Likes
5

…and I already slapped my forehead. Thank you. :slight_smile:

6

Tried this approach?

  def update(scope, value) do
    case SystemRegistry.update([:config | scope], value) do
      %SystemRegistry.Transaction{} ->
        {:error, :undefined} # i.e. this will never happen
      result ->
        result
    end
  end

or even more explicitly, intention revealing

  @spec update(SystemRegistry.scope(), any) :: {:ok, {map, map}} | {:error, term}
  def update(scope, value),
    do: update_with_scope(scope, value)

  @spec update_with_scope(SystemRegistry.scope(), any) :: {:ok, {map, map}} | {:error, term}
  defp update_with_scope(scope, value) do
    case SystemRegistry.update([:config | scope], value) do
      %SystemRegistry.Transaction{} ->
        {:error, :undefined} # i.e. this will never happen
      result ->
        result
    end
  end
1 Like
7

Pondering the topic some more…

There is one SystemRegistry.update/3, but it actually does two very different things, or, better yet, it covers two completely different use cases; One is “do an update (and handle a transaction internally)”, the other is “add this update command to this transaction”.

These actually should be two functions, and that’s where my thoughts derailed.

8

That isn’t the success typing dialyzer is inferring, though.

9
  • I wasn’t sure whether the dialyzer error was completely quoted.
  • I wondered whether dialyzer was just complaining about the missing case.

… but I can see your point.

At least

@spec update([any()], _) :: %SystemRegistry.Transaction{

tells us that dialyzer is fully aware that the first argument will be a list and not a %Transaction{} - so there is no confusion there.

10

Yes my comment was so obviously wrong I didn’t bother to acknowledge it :slight_smile:

@prook curious did you track this down?

11

I’ve resolved Dialyxir’s complaints by replacing

SystemRegistry.update([@mount | scope], value)

with

    SystemRegistry.transaction()
    |> SystemRegistry.update([@mount | scope], value)
    |> SystemRegistry.commit()

This avoids ambiguous SR.update/3 with SR.commit/1, which is specced clearly, and matches my spec/requirements.

Although I understand @peerreynders’ approach, I just cannot stomach the if cannot_happen, then error "it did anyway!" pattern.

As for why Dialyxir does not see – or whether it should see – that my SR.update/3 call will never return SR.Transaction.t, I’m still as confused as when writing the OP.

12

Clearly the superior solution - but a solution that goes beyond the scope your original post was exploring :wink:

13

True.

I’ve learned, thanks to you, what the problem was, came up with a way to avoid it …and then let it slip out of my mind with “the API is kind of weird there”.

But, to reiterate, I still don’t understand why or whether Dialyxir should not be able to infer (that is, to exclude Transaction.t from) the return type from the call. I see the required information is all there; in the spec of SR.update/3 and in the call itself.

I guess that is the original scope of exploration, and I’d appreciate any insight on that.

14

I don’t have any special insight into how Dialyzer works beyond what LYSE has to say about it - and I don’t have access to your code to poke and prod it.

In any case I typically try to corral the problem into a fairly small code sample with which I can experiment fairly quickly and liberally and observe how Dialyzer reacts to any particular change. Once I figure out how it behaves it leads to stuff like this.

It’s one thing to assume to know how something works but with Dialyzer it’s usually instructive to test all assumptions.

15

(8 hours ago: Hmmm, I should probably do that…)

This has gotten interesting. First, I’ve reduced the warning-inducing code to this:

defmodule WhatTheSpec do
  @type key :: atom()
  @type transaction :: map()

  def put(_, _, _ \\ nil)

  @spec put(one, key(), any()) :: transaction() when one: transaction()
  def put(t, _, _) when is_map(t), do: t

  @spec put(one, any(), Keyword.t()) :: :ok when one: key()
  def put(_, _, _), do: :ok

  @spec put_foo(any()) :: :ok
  def put_foo(value) do
    put(:foo, value)
  end
end

Next, I realized that Keyword.t() does not include nil, yet the third parameter may be nil indeed. So the spec

@spec put(one, any(), Keyword.t()) :: :ok when one: key()

should actually be

@spec put(one, any(), Keyword.t() | nil) :: :ok when one: key()

And sure enough, Dialyxir goes green! So it was lack of understanding on my part after all! Also, this means there’s a similar problem in SystemRegistry @spec of update/3, which sent me on this trip! And furthermore, I point my finger at Dialyxir as well! *gasp!*

Dialyxir’s warning is misleading to say the least:

lib/spec.ex:13:invalid_contract
Invalid type specification for function.

Function:
WhatTheSpec.put_foo/1

Success typing:
@spec put_foo(_) :: map()

As I grok it, @spec put_foo(_) :: map() is not a success typing, as there is actually none. I reason this is a bug, as the complaint about map() being a return type goes away after the | nil fix. It should either stay there (no, it should not!), or never appear at all, right?

Also, changing update_foo from the original example (i. e., before the | nil fix) to

  @spec put_foo(any()) :: :ok
  def put_foo(value) do
    put(:foo, value, nil) # note the explicit nil here
  end

makes Dialyxir barf completely:

Please file a bug in Issues · jeremyjh/dialyxir · GitHub with this message.

Failed to format warning:
“@spec a(:one, any(), Keyword.t()) :: 'ok’whenone :: key()\ndef a() do\n :ok\nend\n”

Legacy warning:
lib/spec.ex:7: The contract ‘Elixir.WhatTheSpec’:put(one,key(),any()) → transaction() when one :: transaction();(one,any(),‘Elixir.Keyword’:t()) → ‘ok’ when one :: key() cannot be right because the inferred return for put(‘foo’,_value@1::any(),‘nil’) on line 15 is ‘ok’ | map()

lib/spec.ex:14:no_return
Function put_foo/1 has no local return.

@jeremyjh, It seems I’ve hit some murky parts of Dialyxir with this. :slight_smile:

16

Yeah. That success typing doesn’t make sense. I will dig into it in the morning, my brain is mush now. But definitely, we have a parser or formatter error in your last example. I think we may have a dialyzer bug in the first example, but I need to poke at it a bit and translate it to Erlang to be sure.

17

I think this maybe a bug in Erlang, but I will be honest, I’ve not used when clauses in specs before and I’m not sure I can expect this signature to work.

I decompiled this Elixir module to Erlang and cleaned it up, and can reproduce the issue with the following code:

-module(watspec).

-compile(no_auto_import).

-export([put/2, put/3, put_foo/1]).

put(One, Value) -> put(One, Value, nil).

-spec put(One, atom(), any()) -> map() when One :: map();
         (Two, any(), list()) -> ok when Two :: atom().
put(T, _, _) when erlang:is_map(T) -> T;
put(_, _, _) -> ok.

-spec put_foo(any()) -> ok.
put_foo(Value) -> put(foo, Value).

From shell you can run with:

$ dialyzer --build_plt --output_plt error.plt --apps erts kernel stdlib
$ dialyzer -n --plt error.plt --src *.erl

You will get:

watspec.erl:14: Invalid type specification for function watspec:put_foo/1. The success typing is (_) -> map()

If I comment out the spec for put/3 I get no errors. If I run typer without that signature, it gives me this:

-spec put(_,_) -> 'ok' | map().
-spec put(_,_,_) -> 'ok' | map().
-spec put_foo(any()) -> 'ok'.

The second issue you saw (the barfing) is definitely ours; I opened an issue to track it.

18

I just wanted to know how stuff works, not break half the universe. :slight_smile:

But yeah, Dialyzer reaction to that decompiled code is misleading in the same way.

I’ve slightly reduced the example (leaving the middle argument out, as it’s not part of the problem) to:

-module(watspec).

-compile(no_auto_import).

-export([put/1, put/2, put_foo/0]).

put(One) -> put(One, nil).

-spec put(One, any()) -> map() when One :: map();
         (Two, list()) -> ok when Two :: atom().
put(T, _) when erlang:is_map(T) -> T;
put(_, _) -> ok.

-spec put_foo() -> ok.
put_foo() -> put(foo).

But now I’m kinda clueless about what to do next… Should I ping someone here? File an issue on bugs.erlang.org? Is this even worth fixing?

19

Everything is worth fixing, and I’ve found the Erlang group to be very responsive and helpful on past Dialyzer bugs. My only hesitation again is that its possible the when spec doesn’t really intend to behave like we think it would. I’d probably post it on erlang-bugs before opening a Jira, but either way would be fine.

1 Like