> incorrect even in the face of the simplest examples

I haven't found this in my experience. Most issues arise from a lack of typespeccing. If one were to rely on type inference, then, yes, it's not going to catch much. Specifying types is a requirement of a strictly-typed language, so to make a claim of deficiency with Dialyzer's type checking, you'd be comparing code that's fully specced with that of a strictly typed language.

The unavoidable problem is when using libraries that aren't properly typespecced, but that the same story as any gradually typed language (e.g., Typescript). The only solution here is to make a PR or a feature request to the product owners.

I've used dialyzer since 2015, it's not a question of "holding it wrong". I have an example of this that I literally demonstrated live in a talk online. It's very likely you haven't used dialyzer enough if you think it's actually correct 100% of the time even with type specs. Dialyzer is an exceedingly poor implementation of static type checking and not sufficient with any level of use.

I thought Dialyzer never raised false positives at the expense of false negatives, though perhaps your example is a false negative? I’ve only used it in the last 4 years. Is it possible the bugs have been fixed by now? Or is this just an inherent to this kind of type checking?

I don't think the implementation itself is at fault (I phrased that poorly in my previous post), but yes, I do think that the design of dialyzer makes it an (at times) faulty type checker. The unfortunate reality of a type checker that fails sometimes is that it makes it mostly useless because you can never trust that it'll do the job.

To be clear, I've had it fail in a function where I've literally specced that very function to return a `binary` but I'm returning an `integer` in one of the cases. This is a very shallow context but it can still fail. Now add more functions, maybe one more `case`. Dialyzer will just never keep up over a long enough time frame.

I think an entire rethink of type checking on the BEAM had to be done and that's why eqWalizer[0] was created and why Elixir is looking to add an actual sound, well-developed type checker. Gleam[1] I would assume is just a Hindley-Milner system so that's completely solid. `purerl`[2] is just PureScript for the BEAM so that's also Hindley-Milner, meaning it's solid. `purerl` has some performance issues caused by it compiling down to closures everywhere but if you can pay that cost it's actually pretty fantastic. With that said my bet for the best statically typed experience right now on the BEAM would be `gleam`.

0 - https://github.com/WhatsApp/eqwalizer

1 - https://gleam.run

2 - https://github.com/purerl/purerl