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 ::
record(: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) :
SatSolver.run(
_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()}]},
0,
{: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)**
end
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
end
end
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?
