Dialyzer and private function causing an error. What am I missing?

Here is another story & question about Dialyzer and it’s error messages. I managed to resolve the issue but I hope somebody is able to explain what was going on and this topic is included in the result when someone else has an Dialyzer issue which seems impossible to resolve (as I never saw the error/solution before)

Relevant Context

@type level :: integer | nil
@type state ::
            graph: graph,
            backtrack: backtrack,
            next_assignment: assignment | nil,
            conflict_counter: integer

@spec run(cnf, level, state) :: {:ok, state} | error_result
  def run(cnf, 0 = level, state(next_assignment: nil) = state) do [...]
  def run(cnf, level, state(next_assignment: nil) = state) do [...]
  def run(cnf, level, state) do [...]

The Dialyzer error (highlighting the discrepancy) :

  _cnf :: {:cnf, _},
  _level :: any(),
  _state :: {:state, _, _, ---> {:assignment**, atom(), boolean(), _, false, true} <---, _}

will never return since the 3rd arguments differ from the success typing arguments:

   {:cnf, [{:clause, [any()], atom()}]}, 
   {:state, pid(), atom() | :ets.tid(), ---> nil  <---, integer()}

Dialyzer reported the error for the function call to run in the second function definition:

  # second definition
  def run(cnf, level, state(next_assignment: nil) = state) do
    next_assignment = assignment(atom: atom, value: !negated, level: level)
    state = state(state, next_assignment: next_assignment)
    **run(cnf, level, state)**

Here I could not understand the problem. Dialyzer did expects the assignment to be nil and the level to be 0. My type spec did however allow assignment to be of type assignment | nil and level to be of type ‘integer | nil’. Furthermore, if I changed the state = state(state, next_assignment: next_assignment) to state = state the error went away.

I took me quite some time to rule out various possible issues, focusing on the second function definition (where I could ‘fix’ the issue by not altering the state) . I failed in pinning down the issue. Finally I looked at a video mentioning that Dialyzer goes from generic to more specific while inferring types (by doing tests) and your custom typespecs are used last, only if all tests before pass.

With that new knowledge I figured that Dialyzers’ checks failed using inferred types before using my custom types. This explained why it’s success typing in the error was different than what I had specified. But why did it ‘fail’ in inferring the correct success type?

It expected the level to be 0 and assignment to be nil. Those values matched with the first function head so I figured Dialyzer inferred the types from that function definition only. However that function could return a level > 0 and an assignment != nil. Those values were returned by a private function called handle_result.

# first definition
  def run(cnf, 0 = level, state(next_assignment: nil) = state) do
    check_clauses(cnf(cnf, :clauses), state(state, :backtrack))
    |> handle_result(cnf, level, state)
    |> case do
      {cnf, level, state} -> run(cnf, level, state)
      other -> other

Was it possible that Dialyzer did not see those possible success results? Just to see if handle_result being private was causing the error, I made it public. Immediately the error went away.

Now I wonder: why?! And how can I make sure I don’t run into the same problem again?

@hauleth You seem quite an allround expert at this forum. I hope mentioning you in this topic might trigger your interest as this is tough material and I doubt many people can shed light on it :slight_smile:

How are you running Dialyzer? Is it the ElixirLS integration? Did you see this issue on a clean compile? Did the issue come back if you made that handle_result function private again?

The reason I’m asking is ElixirLS integration with Dialyzer is not ideal, and only analyzes modules that changed since last analysis. Elixir compiler is smart so doesn’t unnecessarily recompile modules that didn’t change. But type specs dependencies are not tracked by it, and there may be non obvious dependencies with regards to computed dialyzer specs between modules. So some results can get “stale”, and it often happens that when trying to fix a dialyzer issue, I need to force the Elixir compiler to recompile a module (e.g. by adding an empty newline somewhere in that file) so that ElixirLS picks it up and runs Dialyzer analysis on it again.

If you think that was not the case, it would be useful if you could provide a miminal example of a few modules and functions that shows this issue. This might turn out to be a bug in Dialyzer.


Running Dialyzer thought LS. I already tried before to tackle the issue of stale files/references by adding little nonsense into the functions that were causing trouble (including the private function). That did not solve it.

For another issues I had to rebuild the dialyzer cache. That issue was reporting the previous name of the module so it was clear something was wrong with the cache. Since I cleared the cache I can not reproduce the issue anymore.

Lesson learned: even when you are sure the cache should be renewed and it actually uses new information for other functions (changed specs/changed function/changed file) it is not guaranteed this actually happens for everything in the file. Just remove the whole cache folder when encountering errors you can not explain.

Reminder to myself:

  • write spec for public function
  • make function private
  • change spec
  • check if the new spec is used.