Dialyzer - Shouldn't this fail?

Questions / Help
1

I’ve been reading Functional Web Development with Elixir, OTP, and Phoenix and following along with the code. I’ve decided early on to start adding tests and type specs, mainly for my own learning opportunity.

I’ve ran into a case where I feel like dialyzer should be finding a problem yet it doesn’t.

I’ve pushed up my code to a public repo and opened a PR that changes a typespec to what I would expect dialyzer to fail but it doesn’t.

Here’s the PR: https://github.com/tielur/islands_engine/pull/1

Am I missing something here?

Here’s the entire function:

@spec guess(%Island{}, %Coordinate{}) :: :miss | {:hit, %Island{}}
def guess(%Island{} = island, %Coordinate{} = coordinate) do
  case MapSet.member?(island.coordinates, coordinate) do
    true ->
      hit_coordinates = MapSet.put(island.hit_coordinates, coordinate)
      {:hit, %{island | hit_coordinates: hit_coordinates}}

    false ->
      :miss
  end
end

It’s using MapSet.member? to check if a Coordinate is in the MapSet. If it is then it returns a tuple with :hit and the updated Island. Otherwise it returns :miss.

If I change the type spec from:

@spec guess(%Island{}, %Coordinate{}) :: :miss | {:hit, %Island{}}

to:

@spec guess(%Island{}, %Coordinate{}) :: :miss | {:hit, %Coordinate{}}

I would expect dialyzer to realize that it doesn’t return a %Coordinate{} and fail.

Also if I change the type spec to completely remove the case where it returns :miss

@spec guess(%Island{}, %Coordinate{}) :: {:hit, %Island{}}

mix dialyzer is still successful…

Only when I change the type spec to this:

@spec guess(%Island{}, %Coordinate{}) :: {:hit, %Coordinate{}}

do I get a failure:

lib/islands_engine/island.ex:28:invalid_contract
Invalid type specification for function.

Function:
IslandsEngine.Island.guess/2

Success typing:
@spec guess(%IslandsEngine.Island{:coordinates => MapSet.t(_), _ => _}, %IslandsEngine.Coordinate{
  _ => _
}) ::
  :miss
  | {:hit,
     %IslandsEngine.Island{
       :coordinates => MapSet.t(_),
       :hit_coordinates => MapSet.t(_),
       _ => _
     }}
________________________________________________________________________________
done (warnings were emitted)
2

Have you tried clearing any cached PLT’s and running mix dialyzer again?

3

If any of the conditions are met, dyalizer will not complain… because it assumes You are right, until it can prove You are wrong :slight_smile:

See this post

3 Likes