Dialyzer cannot recognize error in function using polymorphic types

[Fl4m3Ph03n1x]

@LostKobrakai

The thing to understand here is that success typing is not all all concerned with exhaustive checks (at least with the default flags). It doesn’t care if your typespec has parts, which are off, for as long as there’s some “correct” parts to it. Correct meaning matching to the inferred type of dialyzer. So thinking your typespec is a 100% match just because dialyzer doesn’t complain is an incorrect expectation.

So, if I understand correctly, as long as 1 path in my code leads to a successful execution that is compatible with the specs I provide, dialyzer will not complain.

There may be many paths that break, but as long as 1 works, dialzyer is happy.

In my specific case, because I have a branch that returns [{:some, String.t}] dialyzer does not complain, because I have 1 branch that succeeds.

Thanks!

@LostKobrakai

You can make dialyzer catch the issue by enabling the :underspecs (there’s also :overspecs) flag. This will make dialyzer complain if parts of its inferred type is not covered by the typespec in code.

I tried this and didn’t get the same result:

mix.exs

  def project do
    [
      app: :my_app,
      version: "0.1.0",
      elixir: "~> 1.13",
      start_permanent: Mix.env() == :prod,
      deps: deps(),
      dialyzer: [
        flags: ["-Wunmatched_returns", :error_handling, :race_conditions, :underspecs]
      ]
    ]
  end

test.ex

defmodule Test do

  @type option(t) :: some(t) | nothing
  @type some(t) :: [t]
  @type nothing :: []

  @spec validate_name(String.t()) :: option(String.t())
  def validate_name(name) do
    if String.length(name) > 0 do
      [name]
    else
      nil
    end
  end
end

dialyzer output

$ mix dialyzer
Compiling 1 file (.ex)
Finding suitable PLTs
Checking PLT...
[:compiler, :currying, :elixir, :gradient, :gradualizer, :kernel, :logger, :stdlib, :syntax_tools]
PLT is up to date!
No :ignore_warnings opt specified in mix.exs and default does not exist.

Starting Dialyzer
[
  check_plt: false,
  init_plt: '/home/user/Workplace/fl4m3/grokking_fp/_build/dev/dialyxir_erlang-24.2.1_elixir-1.13.2_deps-dev.plt',
  files: [...],
  warnings: [:unmatched_returns, :error_handling, :race_conditions, :underspecs,
   ...]
]
Total errors: 0, Skipped: 0, Unnecessary Skips: 0
done in 0m1.15s
done (passed successfully)

Given this example is slightly different (no more tuples inside the list) my understanding is that underspecs should still complain. I will however say that the only resource I could find on the matter was this mail:

• [erlang-questions] Dialyzer underspecs and overspecs options

From it:

Let SpecIn be a set of @spec inputs and RealIn be a set of inputs as inferred by Dialyzer from real code, then:

• The Input Contract is satisfied when SpecIn <= RealIn (where <= is a non-strict subset operation). See over_in in demo code below.

• The Input Contract violation is detected by -Wunderspecs option when SpecIn > RealIn. See under_in below.

It is easy to see in the code:

• It’s OK for over_in to declare that it only accepts :a and :b while it also happens to accept :c. Maybe suboptimal, but fine.

• It’s NOT OK for under_in to claim that it accepts :a, :b and :c and break if :c is passed. Rejecting :c would break the caller.

Let SpecOut be a set of @spec outputs and RealOut be a set of outputs as inferred by Dialyzer from real code, then:

• The Output Contract is satisfied when SpecOut >= RealOut (where >= is a non-strict superset operation). See under_out below.

• The Output Contract violation is detected by -Woverspecs option when SpecOut < RealOut. See over_out below.

It is easy to see in the code:

• It’s OK for under_out to declare that it returns :a, :b and :c, while currently it only returns :a and :b. Maybe future implementations will return :c as well.
• It’s NOT OK for over_out to declare that it returns :a and :b, but to also return :c sometimes. Returning :c would break the caller.

So, in my case, if I understand:

• SpecOut is [] | [Any]
• RealOut is [Any]

And in this case, my SpecOut >= RealOut. So :underspec will not complain ( it doesnt).

I may very well be reading this all wrong. Keep that in mind.
I am just trying to understand why underspec wont work in my sample.