title: Dialyzer not detecting obvious type error in parametrized type
body: <p>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.</p>
  
  <p>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 <code>b/0</code> that builds a BST with an integer and an atom, and the dialyzer isn't compaining.</p>
  
  <pre class="lang-erlang prettyprint-override"><code>-module(bst).
  
  -export([add/2, b/0, new/1]).
  
  -type bst(T) :: {T, bst(T), bst(T)} | nil.
  
  -spec new(T) -&gt; bst(T).
  
  -spec add(T, bst(T)) -&gt; bst(T).
  
  new(Root) -&gt; {Root, nil, nil}.
  
  add(Val, nil) -&gt; {Val, nil, nil};
  add(Val, {Root, Left, Right}) -&gt;
      case Val =&lt; Root of
        true -&gt; {Root, add(Val, Left), Right};
        false -&gt; {Root, Left, add(Val, Right)}
      end.
  
  % Why no type error here? Adding atom to bst(integer()),
  % but type spec allows only same type.
  b() -&gt; N = new(8), add(why_no_type_error, N).
  </code></pre>
  
  <p>Running the dialyzer gives the following success result:</p>
  
  <pre><code>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)
  </code></pre>
  
  <p>I was able to make this example fail by editing my <code>add/2</code> spec as below: </p>
  
  <pre class="lang-erlang prettyprint-override"><code>-spec new(integer()) -&gt; bst(integer());
       (atom()) -&gt; bst(atom()).
  
  -spec add(integer(), bst(integer())) -&gt; bst(integer());
       (atom(), bst(atom())) -&gt; bst(atom()).
  </code></pre>
  
  <p>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.</p>