>Specs/contracts are cool but ultimately don't afford the same kind of descriptive and expressive power that a static type system does.

What exactly dialyzer type checking lacks compared to static type systems?