How to make Dialyzer more strict?

Questions / Help
, ,
41

This is correct. dialyzer does not unify type variables. Type variables are only really useful for specifying constraints via a when clause, and do not provide most of what people expect generics to do for them.

This is mentioned in this answer by one of the developers of dialyzer.

4 Likes
42

I really like this, v nice!

  @type good_hello() :: map() 
  @type bad_hello() :: map() 
  @type any_hello() :: good_hello() | bad_hello()

  @spec hello(integer()) :: any_hello()
  def hello(1), do: good()
  def hello(_), do: bad()

  @spec good() :: good_hello()
  def good(), do: %{hello: "world"}

  @spec bad() :: bad_hello()
  def bad(), do: :wtf
2 Likes
43

Came across this discussion when searching for Elixir types / dialyzer stuff. I think it’s worth mentioning that with the latest dialyxir (1.0.0-rc7) and Erlang/OTP 22.2, and the overspecs flag that Jose mentioned, dialyzer does catch the error as expected with the example:

lib/test_types.ex:15: The success typing for 'Elixir.TestTypes':hello/1 implies that the function might also return 'wtf' but the specification return is map()

Unfortunately, overspecs is noisy and fails, for example this function and spec:

  @spec hi(integer()) :: :foo | :bar
  def hi(n) do
    if n < 5 do
      :foo
    else
      :bar
    end
  end

with:

Type specification is a subtype of the success typing.

Function:
TestTypes.hi/1

Type specification:
@spec hi(integer()) :: :foo | :bar

Success typing:
@spec hi(_) :: :bar | :foo

You can fix it by adding def hi(n) when is_integer(n) do.

So it seems like overspecs might be something you could add when you’re starting a project, but hard to enable after the fact.

5 Likes
44

Question about typespecs:

The analysis can be improved by inclusion of type hints (called specs) but it can be useful even without those.

This is stated in the dialyxir readme (GitHub - jeremyjh/dialyxir: Mix tasks to simplify use of Dialyzer in Elixir projects.) which implies that adding typespecs makes the analysis better, but when you say

The compiler always ignores type specs except for some basic syntax checks.

How can dialyxir/dialyzer be improved through typespecs if they are ignored? Am I not understanding what dialyxir docs mean vs what you mean?

45

The elixir compiler ignores them, except for validating their syntax. (Well it also includes them into the generated byte code).

But dialyzer analysis them, so the more typespecs are there, the more dialyzer knows about the thing its analyzes.

1 Like
46

Thanks for the follow up but I’m still not sure which is true. In the paragraph before that @rvirding says:

Also in some ways dialyzer basically ignores a function spec when type checking so you don’t really need one to get the type checking. If you give one it will check that it is consistent with what it can work out about the function and it will use it when reporting type errors,

I’m reading it as “dialyzer ignores elixir typespecs”. :thinking:

47

As I said it both ignores and doesn’t ignore the erlang/elixir typespecs.

When it does its type checking it will look the code definition of a function and the calls to that function and check if they are consistent. For example if a function expects its first argument to be a list is it will check whether it is called with list. This it does irrespective of whether there is an explicit typespec or not. This means you don’t need typespecs to get dialyzer to check your code.

If there is a typespec then it will check the typespec against the function definition to see whether they are consistent and report if they are not. It will also use the typespec when reporting errors.

Try reading the “Learn You Some Erlang” chapter on dialyzer and typing, https://learnyousomeerlang.com/dialyzer which explains what is going quite well. While it is in Erlang it should be quite easy to understand. I don’t know of something similar written for Elixir.

4 Likes
48

I’ll read it, thank you!

Per your reply, to me it means that typespecs do not help in analysis but rather in reporting (unless I don’t understand what analysis means). I wish I wasn’t so confused.

The analysis can be improved by inclusion of type hints (called specs) but it can be useful even without those.

But yes, will read that chapter.

49

Exactly. Dialyzer will ensure that the typespecs you’ve written down match what it inferred (a.k.a. that they’re not wrong). It helps you to find cases, where your codebase is consistent based on what dialyzer infers, but it’s not consistent with the developers intention.

defmodule A do
  # This is fine
  def calc(a, b), do: a + b
  def run, do: add(1.0, 1.0)
end

# v.s.

defmodule B do
  # This is not
  @spec calc(integer, integer) :: integer
  def calc(a, b), do: a + b
  # The call 'Elixir.B':calc(1.0,float()) breaks the contract (integer(),integer()) -> integer()
  def run, do: add(1.0, 1.0)
end

Edit: One could’ve added guard clauses with when is_integer(a) and is_integer(b) as well, but I guess for an example it should be fine.

3 Likes
50

:boom: :exploding_head: :clap: :raised_hands: :bowing_man: thank you!

51

This is what I do. Helps keeping me in check.

52

For as long as there is a guard to do so, for sure.