ERL-687: Dialyzer map-based types inference

[OTP-Maintainer]

Original reporter: tim2cf
Affected version: OTP-21.0
Component: dialyzer
Migrated from: https://bugs.erlang.org/browse/ERL-687

---

Let's consider we have Elixir module


{code:ruby}
defmodule Car do

  defstruct [
    :year,
    :price,
    :model
  ]

  @type t :: %Car{
    year:  integer(),
    price: integer(),
    model: binary()
  }

  @spec can_buy?(Car.t, integer()) :: boolean()
  def can_buy?(%Car{year: year, price: price, model: model}, money)
          when
            is_integer(year) and
            is_integer(price) and
            is_binary(model) and
            is_integer(money) and
            (price <= money)
          do
    true
  end
  def can_buy?(%Car{year: year, price: price, model: model}, money)
          when
            is_integer(year) and
            is_integer(price) and
            is_binary(model) and
            is_integer(money)
          do
    false
  end

end
{code}

That compiles to Erlang AST equivalent to Erlang code


{code:erlang}
-file("/Users/timcf/HTprojects/crystal/lib/crystal.ex",
      46).

-module('Elixir.Car').

-compile(no_auto_import).

-spec 'can_buy?'('Elixir.Car':t(),
		 integer()) -> boolean().

-export_type([t/0]).

-type t() :: #{'__struct__' := 'Elixir.Car',
	       model := binary(), price := integer(),
	       year := integer()}.

-export(['__info__'/1, '__struct__'/0, '__struct__'/1,
	 'can_buy?'/2]).

-spec '__info__'(attributes | compile | functions |
		 macros | md5 | module | deprecated) -> any().

'__info__'(module) -> 'Elixir.Car';
'__info__'(functions) ->
    [{'__struct__', 0}, {'__struct__', 1}, {'can_buy?', 2}];
'__info__'(macros) -> [];
'__info__'(attributes) ->
    erlang:get_module_info('Elixir.Car', attributes);
'__info__'(compile) ->
    erlang:get_module_info('Elixir.Car', compile);
'__info__'(md5) ->
    erlang:get_module_info('Elixir.Car', md5);
'__info__'(deprecated) -> [].

'__struct__'() ->
    #{'__struct__' => 'Elixir.Car', model => nil,
      price => nil, year => nil}.

'__struct__'(_@1) ->
    'Elixir.Enum':reduce(_@1,
			 #{'__struct__' => 'Elixir.Car', model => nil,
			   price => nil, year => nil},
			 fun ({_@2, _@3}, _@4) -> maps:update(_@2, _@3, _@4)
			 end).

'can_buy?'(#{year := Vyear@1, price := Vprice@1,
	     model := Vmodel@1, '__struct__' := 'Elixir.Car'},
	   Vmoney@1)
    when (((erlang:is_integer(Vyear@1) andalso
	      erlang:is_integer(Vprice@1))
	     andalso erlang:is_binary(Vmodel@1))
	    andalso erlang:is_integer(Vmoney@1))
	   andalso Vprice@1 =< Vmoney@1 ->
    true;
'can_buy?'(#{year := Vyear@1, price := Vprice@1,
	     model := Vmodel@1, '__struct__' := 'Elixir.Car'},
	   Vmoney@1)
    when ((erlang:is_integer(Vyear@1) andalso
	     erlang:is_integer(Vprice@1))
	    andalso erlang:is_binary(Vmodel@1))
	   andalso erlang:is_integer(Vmoney@1) ->
    false.
{code}

And if I'm trying to apply Dialyzer (with overspcs flag) to this code, it gives me warning


{code}
lib/crystal.ex:60: Type specification 'Elixir.Car':'can_buy?'('Elixir.Car':t(),integer()) -> boolean() is a subtype of the success typing: 'Elixir.Car':'can_buy?'(#{'__struct__':='Elixir.Car', 'model':=binary(), 'price':=integer(), 'year':=integer(), _=>_},integer()) -> boolean()
{code}

Which is not correct. The interesting thing is if I will comment first or second clause of `can_buy?` function - warning will not be emitted at all.

[OTP-Maintainer]

ferd said:

Which options are you using for Dialyzer? This subtype error is usually something you would get when turning on some of these options:

* -Woverspecs : Warn about overspecified functions (the specification is strictly less allowing than the success typing).
* -Wspecdiffs: Warn when the specification is different than the success typing.

Specifically the error seems to care about the overspec: the function as defined only looks for the presence of the keys in `t()`:

'can_buy?'(#{ year := _, price := _, model := _, '__struct__' := 'Elixir.Car'}, ...)

This pattern means that if I pass in the map  #{year => 0, price => 0, model => <<"beep beep">>, '__struct__' => 'Elixir.Car', fake_key => screw_your_check}, the function will still pass.

Dialyzer warns that the actual inferred typing for the map is #{'__struct__':='Elixir.Car', 'model':=binary(), 'price':=integer(), 'year':=integer(), _=>_} and the critical part here is the  _ => _ , which is correctly inferred: the code accepts it, but the typespec does not allow it. Therefore the typespec is overspecified and you get the warning.

[OTP-Maintainer]

tim2cf said:

Thanks. It is like this, but it seems there is still other bug, because if I remove one function clause - it not emits warning, looks like inconsistent behaviour

[OTP-Maintainer]

tim2cf said:

If I specify type like this, Dialyzer gives no warnings

{code:ruby}
  @type t :: %{
    :__struct__ => Car,
    :year =>  integer(),
    :price => integer(),
    :model => binary(),
    any() => any()
  }
{code}

But. Other strange thing can be figured out from this example - if I specify for example *year* field like integer or nil (sorry for Elixir code)

{code:ruby}
  @type t :: %{
    :__struct__ => Car,
    :year =>  nil | integer(),
    :price => integer(),
    :model => binary(),
    any() => any()
  }

  @spec can_buy?(Car.t, integer()) :: boolean()
  def can_buy?(%Car{year: year, price: price, model: model}, money)
          when
            (is_nil(year) or is_integer(year)) and
            is_integer(price) and
            is_binary(model) and
            is_integer(money) and
            (price <= money)
          do
    true
  end
  def can_buy?(%Car{year: year, price: price, model: model}, money)
          when
            (is_nil(year) or is_integer(year)) and
            is_integer(price) and
            is_binary(model) and
            is_integer(money)
          do
    false
  end
{code}

Than Dialyzer emits other warning

{code}
lib/crystal.ex:62: Type specification 'Elixir.Car':'can_buy?'('Elixir.Car':t(),integer()) -> boolean() is a subtype of the success typing: 'Elixir.Car':'can_buy?'(#{'__struct__':='Elixir.Car', 'model':=binary(), 'price':=integer(), 'year':=_, _=>_},integer()) -> boolean()
{code}

Interested thing here is *any* type of *year* field:

{code}
'year':=_
{code}

Which is not correct. According specs and guards year is integer or nil, but not any

[OTP-Maintainer]

hasse said:

It seems you've hit the limit DISJ_NORM_FORM_LIMIT in lib/dialyzer/src/dialyzer_typesig.erl. More complex guards are handled with less precision by Dialyzer.