dialyzer: Introduce nominal types

[lucioleKi]

Co-authored-by: John Högberg [email protected]

This PR implements EEP-69: Nominal Types
in Dialyzer. As a side effect, nominal types can encode opaque types. We
changed all opaque-handling logic and improved opaque warnings in
Dialyzer.

All existing Erlang type systems are structural: two types are seen as
equivalent if their structures are the same. Type comparison are based
on the structures of the types, not on how the user explicitly defines
them. For example, in the following example, meter() and foot() are
equivalent. The two types can be used interchangeably. Neither of them
differ from the basic type integer().

-type meter() :: integer().
-type foot() :: integer().

Nominal typing is an alternative type system, where two types are
equivalent if and only if they are declared with the same type name.
The EEP proposes one new syntax -nominal for declaring nominal types.
Under nominal typing, meter() and foot() are no longer compatible.
Whenever a function expects type meter(), passing in type foot()
would result in a Dialyzer error.

-nominal meter() :: integer().
-nominal foot() :: integer().

More nominal type-checking rules can be found in the EEP. It is worth
noting that most work for adding nominal types and type-checking
is in erl_types.erl. The rest are changes that removed the previous
opaque type-checking, and added an improved version of it using nominal
type-checking with reworked warnings.

Backwards compatibility for opaque type-checking is not preserved
by this PR. Previous opaque warnings can appear with slightly different
wordings. A new kind of opaque warning opaque_union is added, together
with a Dialyzer option no_opaque_union to turn this kind of warnings
off.

This PR is likely not bug-free, but not having it in master is blocking
other changes to Dialyzer. Once nominal type-checking and the new opaque
type-checking are applied to more codebases, we will fix the bugs as
they appear.

[github-actions]

CT Test Results

    18 files     854 suites   6h 31m 46s ⏱️
 8 589 tests  8 022 ✅   566 💤 1 ❌
19 360 runs  17 816 ✅ 1 543 💤 1 ❌

For more details on these failures, see this check.

Results for commit 5dab31e.

♻️ This comment has been updated with latest results.

To speed up review, make sure that you have read Contributing to Erlang/OTP and that all checks pass.

See the TESTING and DEVELOPMENT HowTo guides for details about how to run test locally.

Artifacts

• Complete CT logs (Download Logs)
• HTML Documentation (Download HTML Docs)
• Windows Installer

// Erlang/OTP Github Action Bot

[bjorng]

Is it really necessary to update the primary bootstrap as part of this pull request?

[TD5]

Looks like this this FIXME is done?

[jhogberg]

Is it really necessary to update the primary bootstrap as part of this pull request?

Yes, erl_lint actually checks that -dialyzer( ... ) directives don't contain any unknown options, which broke the build when we added -dialyzer(no_opaque_union, ...) directives to suppress certain warnings in OTP itself (which would otherwise have broken CI, because dialyzer has to run clean).

[TD5]

I suppose this can be cleaned up now?

[TD5]

How do we expect this logic to handle complex types which Dialyzer "simplifies", in terms of genuine issues not being raised due to type simplification vs. issues falsely raised due type simplification?

[jhogberg]

We'll only see such simplifications where we have unions of opaques and non-opaques, which is iffy enough that we're adding a warning for that in this PR, so I don't expect this to become a huge problem.

[lucioleKi]

By simplifying, do you mean mostly what erl_types:t_limit/2 produces? We wrote nominal clauses in that function to not count the nominal or opaque wrappers when counting depth of a term. Nominal and opaque wrappers are never removed by t_limit, yet their inner structures could be simplified.

[lucioleKi]

An opaque with inner type any is still an opaque. erl_types:t_opacity_conflict/3 will detect the opaque violation regardless of whether the opaque was simplified by t_limit/2. During testing, we had false positives due to our incorrect treatment for nominals in t_limit/2. We'll see if new ones pop up.

[TD5]

Ah, yes, that's exactly what I was getting at! Sounds like you've considered those cases I was wondering about :)

[TD5]

This is the most exciting change I've seen to Dialyzer's semantics... ever? Very cool stuff! 😎 I am definitely keen to try it out for myself.

What is your expectation regarding performance vs. previous logic for opaques? Should we expect an appreciable speed up / slow down of a Dialyzer analysis as a result of this change? The EEP mentioned a theoretical benefit, so I wanted to get a sense of what you've actually seen in practice.

[TD5]

With the introduction of nominal types, perhaps we should revisit any existing docs or other material which still claim that Dialyzer only reports "genuine" type errors in order to clarify that a Dialyzer complaint doesn't necessarily mean code will crash for any input at runtime, but rather there's a discrepancy between definition and use (e.g. due to record definitions, specs & nominal types). I am not sure whether any "official" docs still say something to that effect, but my impression is that it is a notion still circulating in the community.

[jhogberg]

What is your expectation regarding performance vs. previous logic for opaques? Should we expect an appreciable speed up / slow down of a Dialyzer analysis as a result of this change?

For most code there shouldn't be much of a difference, but the insane corner cases with quartic runtime are gone. I'd expect #7835 to be resolved with this PR.

With the introduction of nominal types, perhaps we should revisit any existing docs or other material which still claim that Dialyzer only reports "genuine" type errors in order to clarify that a Dialyzer complaint doesn't necessarily mean code will crash for any input at runtime, but rather there's a discrepancy between definition and use (e.g. due to record definitions, specs & nominal types). I am not sure whether any "official" docs still say something to that effect, but my impression is that it is a notion still circulating in the community.

That was never true for opaques to begin with, but yes, we should correct any documentation that makes those claims.

[TD5]

Not that I am a maintainer, but I have spent some time poking around inside Dialyzer, and I think this change makes sense, certainly given the linked EEP, and it is surprisingly uninvasive, all things considered.

I buy into the idea of landing this PR and fixing forward, since keeping this sort of change out of master just means stacking up more potential conflicts.