Dialyzer not detecting obvious type error in parametrized type

Question

I'm trying to understand how the dialyzer works with polymorphic/parametrized types. I understand that it is optimistic and will succeed if there is any path through the code that does not cause a crash; what I don't understand is how to use type variables, given this fact.

I have a simple recursive binary search tree type specification that is intended to produce a BST with values of only one type. I know that (for instance) atoms and integers are comparable in Erlang, but I don't want my BST to allow those comparisons. I wrote and exported a function b/0 that builds a BST with an integer and an atom, and the dialyzer isn't compaining.

-module(bst).

-export([add/2, b/0, new/1]).

-type bst(T) :: {T, bst(T), bst(T)} | nil.

-spec new(T) -> bst(T).

-spec add(T, bst(T)) -> bst(T).

new(Root) -> {Root, nil, nil}.

add(Val, nil) -> {Val, nil, nil};
add(Val, {Root, Left, Right}) ->
    case Val =< Root of
      true -> {Root, add(Val, Left), Right};
      false -> {Root, Left, add(Val, Right)}
    end.

% Why no type error here? Adding atom to bst(integer()),
% but type spec allows only same type.
b() -> N = new(8), add(why_no_type_error, N).

Running the dialyzer gives the following success result:

dialyzer-tests ❯ dialyzer bst.erl
  Checking whether the PLT /home/.../.dialyzer_plt is up-to-date... yes
  Proceeding with analysis... done in 0m0.12s
done (passed successfully)

I was able to make this example fail by editing my add/2 spec as below:

-spec new(integer()) -> bst(integer());
     (atom()) -> bst(atom()).

-spec add(integer(), bst(integer())) -> bst(integer());
     (atom(), bst(atom())) -> bst(atom()).

Is this in any way idiomatic, or is there a better way to do this? I would not necessarily want to elaborate each possible type for each possible operation on my tree.

Answer 1

The reason you get no warning is the fact that unconstrained type variables in specs (i.e. those that have no when clause) are generalized and treated as term().

Notice that in your example, even without maximal generalization, there is the possibility of the type atom() | integer() for instances of T in your code which would give no warnings.

I can't think of an example where use of a type variable leads to an error, as I don't fully understand what you are looking for.

Answer 2

Restricting the first element of the tuple to an integer works

-module(bst).

-export([add/2, b/0, new/1]).

-type bst() :: {integer(), bst(), bst()} | nil.

-spec new(integer()) -> bst().

-spec add(integer(), bst()) -> bst().

new(Root) -> {Root, nil, nil}.

add(Val, nil) -> {Val, nil, nil};
add(Val, {Root, Left, Right}) ->
    case Val =< Root of
      true -> {Root, add(Val, Left), Right};
      false -> {Root, Left, add(Val, Right)}
    end.

% this will generate a warning with dialyzer,
% but compile and execute without error.
b() -> 
    N = new(8), 
    add(why_no_type_error, N).

Then you get the error you expect (plus a strange "Function b/0 has no local return" which is apparently a consequence of the contract break):

C:\git\XXXXX\src>dialyzer bst.erl
  Checking whether the PLT c:/Users/YYYYY/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
bst.erl:22: Function b/0 has no local return
bst.erl:24: The call bst:add
         ('why_no_type_error',
          N :: {integer(), 'nil', 'nil'}) breaks the contract
          (integer(), bst()) -> bst()
 done in 0m0.20s
done (warnings were emitted)

at run time:

1> c(bst).                
{ok,bst}
2> bst:b().
{8,nil,{why_no_type_error,nil,nil}}

Note the fact that dializer issues a warning does not prevent the code to compile and execute without error. You need to add guard in the code if you want to generate errors at run time

-module(bst).

-export([add/2, b/0, new/1]).

% this version of code has the same warning with dialyzer
% and issues an exception at run time

-type bst() :: {integer(), bst(), bst()} | nil.

-spec new(integer()) -> bst().

-spec add(integer(), bst()) -> bst().

new(Root) when is_integer(Root) -> {Root, nil, nil}.

add(Val, nil) when is_integer(Val) -> {Val, nil, nil};
add(Val, {Root, Left, Right}) when is_integer(Val) ->
    case Val =< Root of
      true -> {Root, add(Val, Left), Right};
      false -> {Root, Left, add(Val, Right)}
    end.

b() -> 
    N = new(8), 
    add(why_no_type_error, N).

at run time:

3> c(bst).                
{ok,bst}
4> bst:b().               
** exception error: no function clause matching 
                    bst:add(why_no_type_error,{8,nil,nil}) (bst.erl, line 13)