Type variables are an often-used yet very misunderstood part of the type
language. As dialyzer has been lax in enforcing their defined semantics owing
to a few bugs, many users have been led to believe that they are simple generics
as in most other languages. As a significant amount of code has been written
with this in mind, OTP cannot fix the bugs that made dialyzer lax by accident
without breaking the analysis of a lot of code.
While that would be fine if dialyzer were the only tool out there, all the
other code analyzers we know of interpret type variables as generics which would
fragment the ecosystem should we elect to fix the bugs. One application might
have been written with eqWAlizer in mind and another with dialyzer,
preventing either tool from being applied to the whole release.
As dialyzer is simply broken in this regard, this EEP aims to solve the
problem by changing the definition of type variables from equality constraints
to generics (parametric polymorphism). We also propose several other changes
to make the type language more useful and less ambiguous.
Cool ! Value Variables with the same name stand for the Same Value, so Type Variables with the same name stand for the Same Type. (In dialyzer, Type Variables with the same name stand for the Same Value, which is painful)
I intensely dislike this solution. A clear-cut misunderstanding now formally enshrined. There is a case if we believe the mistaken semantics are better, but that is not stated here.
And is it bugs that make Dialyzer lax? My understanding is it’s intentionally conservative in what it reports, only complaining if it can prove there’s an error, so that existing correct but statically-ambiguous code doesn’t get a lot of false positives. eqWAlizer on the other hand is conservative in what it allows, to provide the strongest guarantees.
Yes, we are formally enshrining a misunderstanding because it is better. It has proven impossible to teach this stuff and even seasoned veterans make mistakes to this end, including past maintainers!
If type specs are so unintuitive that they cannot be used effectively by humans over time, that is a problem with the design. You should not have to actively maintain the tool in order to use specs correctly.
Furthermore, yes, dialyzer is lax when it comes to type variables because of a set of bugs (although funny enough, the documentation as written indirectly allows its current behavior, if you interpret it not to take type variables into account). It is not a case of dialyzer’s conservative nature causing it to be silent.