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

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) ?

Thanks for the input.

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

I did. No success.

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.

…and I already slapped my forehead. Thank you.

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

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.

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

• 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.

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

@prook curious did you track this down?

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.