Dialyzer and function clauses

Questions / Help
,
1 
defmodule Foo do
  @spec inc(a :: integer() | nil) :: integer() | nil
  def inc(nil), do: nil
  def inc(a), do: {a + 1, a + 2}
end

The second clause of inc function in this example doesn’t match the spec. But dialyzer doesn’t output any error messages. Why?

2

That is how “success typing” works.

It simply assumes, that you will never call it in a way that will cause that branch to be evaluated.

3

Interesting. It looks like dialyzer will only check the clauses that are actually called from the code.

defmodule Foo do
  @spec foo(a :: integer()) :: integer()
  def foo(a), do: inc(a)

  @spec inc(a :: integer() | nil) :: integer() | nil
  def inc(nil), do: nil
  def inc(a), do: {a + 1, a + 2}
end

In this case, dialyzer reports an error.

4

No, I was wrong. It doesn’t check.

I believe this is a bug in dialyzer.

5

Dialyzer doesn’t really know how foo/1 is called so it can’t do a better check than before. Try adding some code which calls foo/1 or inc/1 with explicit values, some good and some bad. As @NobbZ was pointing out is that success typing checks both sides working together, so it checks whether the values in a call will match the values expected in the definition.

And, shh, in many ways dialyzer actually ignores the type specs when doing the checking. It will find the same errors wit or without them, though it can give better error messages if they are there.

3 Likes