dialyzer: Introduce nominal types

This PR implements [EEP-69: Nominal Types](https://www.erlang.org/eeps/eep-0069)
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.

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

bootstrap/lib/compiler/ebin/compiler.app

@@ -1,7 +1,7 @@
 % This is an -*- erlang -*- file.
 %% %CopyrightBegin%
 %%
-%% Copyright Ericsson AB 1997-2023. All Rights Reserved.
+%% Copyright Ericsson AB 1997-2024. All Rights Reserved.
 %%
 %% Licensed under the Apache License, Version 2.0 (the "License");
 %% you may not use this file except in compliance with the License.
@@ -19,7 +19,7 @@
 
 {application, compiler,
  [{description, "ERTS  CXC 138 10"},
-  {vsn, "8.3.2"},
+  {vsn, "8.5.2"},
   {modules, [
 	     beam_a,
 	     beam_asm,
@@ -31,6 +31,7 @@
 	     beam_dict,
 	     beam_digraph,
 	     beam_disasm,
+         beam_doc,
 	     beam_flatten,
 	     beam_jump,
 	     beam_listing,
@@ -43,11 +44,11 @@
              beam_ssa_check,
              beam_ssa_codegen,
              beam_ssa_dead,
+             beam_ssa_destructive_update,
              beam_ssa_lint,
              beam_ssa_opt,
              beam_ssa_pp,
              beam_ssa_pre_codegen,
-             beam_ssa_private_append,
              beam_ssa_recv,
              beam_ssa_share,
              beam_ssa_ss,
@@ -76,12 +77,13 @@
 	     sys_core_fold_lists,
 	     sys_core_inline,
 	     sys_core_prepare,
+             sys_coverage,
 	     sys_messages,
 	     sys_pre_attributes,
 	     v3_core
 	    ]},
   {registered, []},
   {applications, [kernel, stdlib]},
   {env, []},
-  {runtime_dependencies, ["stdlib-5.0","kernel-8.4","erts-13.0",
+  {runtime_dependencies, ["stdlib-6.0","kernel-8.4","erts-13.0",
 			  "crypto-5.1"]}]}.

bootstrap/lib/kernel/ebin/kernel.app

@@ -1,7 +1,7 @@
 %%
 %% %CopyrightBegin%
 %% 
-%% Copyright Ericsson AB 1996-2023. All Rights Reserved.
+%% Copyright Ericsson AB 1996-2024. All Rights Reserved.
 %% 
 %% Licensed under the Apache License, Version 2.0 (the "License");
 %% you may not use this file except in compliance with the License.
@@ -22,7 +22,7 @@
 {application, kernel,
  [
   {description, "ERTS  CXC 138 10"},
-  {vsn, "9.0.2"},
+  {vsn, "10.1.1"},
   {modules, [application,
 	     application_controller,
 	     application_master,
@@ -72,6 +72,7 @@
              logger_filters,
              logger_formatter,
              logger_h_common,
+             logger_handler,
              logger_handler_watcher,
              logger_olp,
              logger_proxy,
@@ -88,6 +89,7 @@
 	     user_drv,
 	     user_sup,
              prim_tty,
+             prim_tty_sighandler,
              disk_log,
              disk_log_1,
              disk_log_server,
@@ -121,6 +123,7 @@
 	     seq_trace,
              socket,
 	     standard_error,
+             trace,
 	     wrap_log_reader]},
   {registered, [application_controller,
 		erl_reply,
@@ -158,10 +161,11 @@
          {net_tickintensity, 4},
          {net_ticktime, 60},
          {prevent_overlapping_partitions, true},
-         {shell_docs_ansi,auto}
+         {shell_docs_ansi,auto},
+         {shell_history_drop,[]}
         ]},
   {mod, {kernel, []}},
-  {runtime_dependencies, ["erts-14.0", "stdlib-5.0",
+  {runtime_dependencies, ["erts-15.1", "stdlib-6.0",
                           "sasl-3.0", "crypto-5.0"]}
   ]
 }.

bootstrap/lib/stdlib/ebin/stdlib.app

@@ -2,7 +2,7 @@
 %% 
 %% %CopyrightBegin%
 %%
-%% Copyright Ericsson AB 1996-2023. All Rights Reserved.
+%% Copyright Ericsson AB 1996-2024. All Rights Reserved.
 %%
 %% Licensed under the Apache License, Version 2.0 (the "License");
 %% you may not use this file except in compliance with the License.
@@ -20,7 +20,7 @@
 %%
 {application, stdlib,
  [{description, "ERTS  CXC 138 10"},
-  {vsn, "5.0.2"},
+  {vsn, "6.1.2"},
   {modules, [argparse,
 	     array,
 	     base64,
@@ -37,6 +37,7 @@
 	     digraph,
 	     digraph_utils,
 	     edlin,
+	     edlin_key,
 	     edlin_context,
 	     edlin_expand,
 	     edlin_type_suggestion,
@@ -77,6 +78,7 @@
 	     io_lib_format,
 	     io_lib_fread,
 	     io_lib_pretty,
+             json,
 	     lists,
 	     log_mf_h,
 	     maps,
@@ -99,6 +101,7 @@
 	     shell,
 	     shell_default,
 	     shell_docs,
+         shell_docs_markdown,
 	     slave,
 	     sofs,
 	     string,
@@ -115,6 +118,6 @@
                dets]},
   {applications, [kernel]},
   {env, []},
-  {runtime_dependencies, ["sasl-3.0","kernel-9.0","erts-13.1","crypto-4.5",
+  {runtime_dependencies, ["sasl-3.0","kernel-10.0","erts-15.0","crypto-4.5",
 			  "compiler-5.0"]}
 ]}.

lib/common_test/src/ct_ssh.erl

@@ -1362,6 +1362,7 @@ init(KeyOrName, {ConnType,Addr,Port}, AllOpts) ->
 			      target=KeyOrName}}
     end.
 
+-dialyzer({no_opaque_union, [handle_msg/2]}).
 -doc false.
 handle_msg(sftp_connect, State) ->
     #state{ssh_ref=SSHRef, target=Target} = State,

lib/compiler/src/beam_core_to_ssa.erl

@@ -1566,7 +1566,7 @@ partition_intersection([U|_]=Us, [_,_|_]=Cs0, St0) ->
     case find_key_intersection(Ps) of
         none ->
             {Us,Cs0,St0};
-        Ks ->
+        {ok, Ks} ->
             Cs1 = map(fun(#iclause{pats=[Arg|Args]}=C) ->
                               {Arg1,Arg2} = partition_keys(Arg, Ks),
                               C#iclause{pats=[Arg1,Arg2|Args]}
@@ -1601,7 +1601,7 @@ find_key_intersection(Ps) ->
                     %% the keys could only make the code worse.
                     none;
                 false ->
-                    Intersection
+                    {ok, Intersection}
             end
     end.
 

lib/compiler/src/beam_disasm.erl

@@ -41,8 +41,8 @@
 %%-----------------------------------------------------------------------
 
 -type index()        :: non_neg_integer().
--type literals()     :: 'none' | gb_trees:tree(index(), term()).
--type types()        :: 'none' | gb_trees:tree(index(), term()).
+-type literals()     :: gb_trees:tree(index(), term()).
+-type types()        :: gb_trees:tree(index(), term()).
 -type symbolic_tag() :: 'a' | 'f' | 'h' | 'i' | 'u' | 'x' | 'y' | 'z'.
 -type disasm_tag()   :: symbolic_tag() | 'fr' | 'atom' | 'float' | 'literal'.
 -type disasm_term()  :: 'nil' | {disasm_tag(), _}.
@@ -254,7 +254,7 @@ disasm_lambdas(<<>>, _, _) -> [].
 -spec beam_disasm_types('none' | binary()) -> types().
 
 beam_disasm_types(none) ->
-    none;
+    gb_trees:empty();
 beam_disasm_types(<<Version:32,Count:32,Table0/binary>>) ->
     case beam_types:convert_ext(Version, Table0) of
         none ->
@@ -265,7 +265,7 @@ beam_disasm_types(<<Version:32,Count:32,Table0/binary>>) ->
             Res
     end;
 beam_disasm_types(<<_/binary>>) ->
-    none.
+    gb_trees:empty().
 
 disasm_types(Types0, Index) ->
     case beam_types:decode_ext(Types0) of

lib/compiler/src/beam_doc.erl

@@ -61,7 +61,7 @@
                deprecated = #{}    :: map(),
 
                docformat = ?DEFAULT_FORMAT :: binary(),
-               moduledoc = {?DEFAULT_MODULE_DOC_LOC, none} :: {integer() | erl_anno:anno(), none | map() | hidden},
+               moduledoc = {erl_anno:new(?DEFAULT_MODULE_DOC_LOC), none} :: {erl_anno:anno(), none | map() | hidden},
                moduledoc_meta = none :: none | #{ _ := _ },
 
                behaviours = []     :: list(module()),

lib/compiler/src/beam_ssa_dead.erl

@@ -240,7 +240,7 @@ shortcut_3(L, From, Bs0, UnsetVars0, St) ->
                             %% because it refers to a variable defined
                             %% in this block.
                             shortcut_unsafe_br(Br, L, Bs, UnsetVars0, St);
-                        UnsetVars ->
+                        {safe, UnsetVars} ->
                             %% Continue checking whether this br is
                             %% suitable.
                             shortcut_test_br(Br, L, Bs, UnsetVars, St)
@@ -381,16 +381,16 @@ update_unset_vars(L, Is, Br, UnsetVars, #st{skippable=Skippable}) ->
                             %% to the UnsetVars set would not change
                             %% the outcome of the tests in
                             %% is_br_safe/2.
-                            UnsetVars
+                            {safe, UnsetVars}
                     end;
                 #b_br{} ->
-                    UnsetVars
+                    {safe, UnsetVars}
             end;
         false ->
             %% Some variables defined in this block are used by
             %% successors. We must update the set of unset variables.
             SetInThisBlock = [V || #b_set{dst=V} <:- Is],
-            list_set_union(SetInThisBlock, UnsetVars)
+            {safe, list_set_union(SetInThisBlock, UnsetVars)}
     end.
 
 shortcut_two_way(#b_br{succ=Succ,fail=Fail}, From, Bs0, UnsetVars0, St0) ->

lib/dialyzer/src/dialyzer.erl

@@ -787,9 +787,10 @@ message_to_string({call, [M, F, Args, ArgNs, FailReason,
 message_to_string({call_to_missing, [M, F, A]}, _I, _E) ->
   io_lib:format("Call to missing or unexported function ~w:~tw/~w\n",
                 [M, F, A]);
-message_to_string({exact_eq, [Type1, Op, Type2]}, I, _E) ->
-  io_lib:format("The test ~ts ~s ~ts can never evaluate to 'true'\n",
-		[t(Type1, I), Op, t(Type2, I)]);
+message_to_string({exact_compare, [Type1, Op, Type2]}, I, _E) ->
+  io_lib:format("The test ~ts ~s ~ts can never evaluate to '~w'\n",
+                [t(Type1, I), Op, t(Type2, I),
+                 (Op =:= '=:=' orelse Op =:= '==')]);
 message_to_string({fun_app_args, [ArgNs, Args, Type]}, I, _E) ->
   PositionString = form_position_string(ArgNs),
   io_lib:format("Fun application with arguments ~ts will fail"
@@ -887,7 +888,8 @@ message_to_string({invalid_contract, [M, F, A, InvalidContractDetails, Contract,
 		" The success typing is ~ts\n"
 		" But the spec is ~ts\n"
 		"~ts",
-    [M, F, A, con(M, F, Sig, I), con(M, F, Contract, I), format_invalid_contract_details(InvalidContractDetails)]);
+    [M, F, A, con(M, F, Sig, I), con(M, F, Contract, I),
+     format_invalid_contract_details(InvalidContractDetails)]);
 message_to_string({contract_with_opaque, [M, F, A, OpaqueType, SigType]},
                  I, _E) ->
   io_lib:format("The specification for ~w:~tw/~w"
@@ -910,18 +912,25 @@ message_to_string({spec_missing_fun, [M, F, A]}, _I, _E) ->
   io_lib:format("Contract for function that does not exist: ~w:~tw/~w\n",
 		[M, F, A]);
 %%----- Warnings for opaque type violations -------------------
-message_to_string({call_with_opaque, [M, F, Args, ArgNs, ExpArgs]}, I, _E) ->
+message_to_string({call_with_opaque,
+                   [M, F, Args, Conflicts, ExpectedTypes]}, I, _E) ->
+  Positions = [N || {N, _T, _TStr} <- Conflicts],
   io_lib:format("The call ~w:~tw~ts contains ~ts when ~ts\n",
-		[M, F, a(Args, I), form_positions(ArgNs),
-                 form_expected(ExpArgs, I)]);
-message_to_string({call_without_opaque, [M, F, Args, ExpectedTriples]}, I, _E) ->
+                [M, F, a(Args, I), form_positions(Positions),
+                 form_expected(ExpectedTypes, I)]);
+message_to_string({call_without_opaque,
+                   [M, F, Args, Conflicts, _ExpectedTypes]}, I, _E) ->
   io_lib:format("The call ~w:~tw~ts does not have ~ts\n",
-		[M, F, a(Args, I),
-                 form_expected_without_opaque(ExpectedTriples, I)]);
-message_to_string({opaque_eq, [Type, _Op, OpaqueType]}, I, _E) ->
-  io_lib:format("Attempt to test for equality between a term of type ~ts"
-		" and a term of opaque type ~ts\n",
-                [t(Type, I), t(OpaqueType, I)]);
+                [M, F, a(Args, I),
+                 form_expected_without_opaque(Conflicts, I)]);
+message_to_string({opaque_compare, [Type, Op, OpaqueType]}, I, _E) ->
+  Kind = if
+            Op =:= '=:='; Op =:= '==' -> "equality";
+            Op =:= '=/='; Op =:= '/=' -> "inequality"
+         end,
+  io_lib:format("Attempt to test for ~ts between a term of type ~ts"
+                " and a term of opaque type ~ts\n",
+                [Kind, t(Type, I), t(OpaqueType, I)]);
 message_to_string({opaque_guard, [Arg1, Infix, Arg2, ArgNs]}, I, _E) ->
   io_lib:format("Guard test ~ts ~s ~ts contains ~s\n",
 		[a(Arg1, I), Infix, a(Arg2, I), form_positions(ArgNs)]);
@@ -930,15 +939,21 @@ message_to_string({opaque_guard, [Guard, Args]}, I, _E) ->
 		[Guard, a(Args, I)]);
 message_to_string({opaque_match, [Pat, OpaqueType, OpaqueTerm]}, I, _E) ->
   Term = if OpaqueType =:= OpaqueTerm -> "the term";
-	    true -> t(OpaqueTerm, I)
-	 end,
-  io_lib:format("The attempt to match a term of type ~ts against the ~ts"
-		" breaks the opacity of ~ts\n",
-                [t(OpaqueType, I), ps(Pat, I), Term]);
-message_to_string({opaque_neq, [Type, _Op, OpaqueType]}, I, _E) ->
-  io_lib:format("Attempt to test for inequality between a term of type ~ts"
-		" and a term of opaque type ~ts\n",
-                [t(Type, I), t(OpaqueType, I)]);
+            true -> "a term of type " ++ t(OpaqueTerm, I)
+         end,
+  io_lib:format("The attempt to match ~ts against the "
+                "~ts breaks the opacity of the term\n",
+                [Term, ps(Pat, I)]);
+message_to_string({opaque_union, [IsOpaque, Type]}, I, _E) ->
+  TypeString = t(Type, I),
+  case IsOpaque of
+    true ->
+      io_lib:format("Body yields the opaque type ~ts whose opacity is "
+                    "broken by the other clauses.\n", [TypeString]);
+    false ->
+      io_lib:format("Body yields the type ~ts which violates the "
+                    "opacity of the other clauses.\n", [TypeString])
+  end;
 message_to_string({opaque_type_test, [Fun, Args, Arg, ArgType]}, I, _E) ->
   io_lib:format("The type test ~ts~ts breaks the opacity of the term ~ts~ts\n",
                 [Fun, a(Args, I), Arg, t(ArgType, I)]);
@@ -1004,7 +1019,6 @@ format_invalid_contract_details({InvalidArgIdxs, IsRangeInvalid}) ->
       false -> ""
     end,
   case {ArgDesc, RangeDesc} of
-    {"", ""} -> "";
     {"", [_|_]} -> io_lib:format(" The ~ts\n", [RangeDesc]);
     {[_|_], ""} -> io_lib:format(" ~ts\n", [ArgDesc]);
     {[_|_], [_|_]} -> io_lib:format(" ~ts, and the ~ts\n", [ArgDesc, RangeDesc])
@@ -1045,24 +1059,25 @@ form_positions(ArgNs) ->
   case ArgNs of
     [_] -> "an opaque term as ";
     [_,_|_] -> "opaque terms as "
- end ++ form_position_string(ArgNs) ++
-  case ArgNs of
-    [_] -> " argument";
-    [_,_|_] -> " arguments"
-  end.
+  end
+    ++ form_position_string(ArgNs)
+    ++ case ArgNs of
+         [_] -> " argument";
+         [_,_|_] -> " arguments"
+       end.
 
 %% We know which positions N are to blame;
 %% the list of triples will never be empty.
 form_expected_without_opaque([{N, T, TStr}], I) ->
   case erl_types:t_is_opaque(T) of
-    true  ->
+    true ->
       io_lib:format("an opaque term of type ~ts as ", [t(TStr, I)]);
     false ->
       io_lib:format("a term of type ~ts (with opaque subterms) as ",
                     [t(TStr, I)])
   end ++ form_position_string([N]) ++ " argument";
-form_expected_without_opaque(ExpectedTriples, _I) -> %% TODO: can do much better here
-  {ArgNs, _Ts, _TStrs} = lists:unzip3(ExpectedTriples),
+form_expected_without_opaque(Conflicts, _I) -> %% TODO: can do much better here
+  ArgNs = [N || {N, _T, _TStr} <- Conflicts],
   "opaque terms as " ++ form_position_string(ArgNs) ++ " arguments".
 
 form_expected(ExpectedArgs, I) ->

lib/dialyzer/src/dialyzer.hrl

@@ -51,6 +51,7 @@
 -define(WARN_NON_PROPER_LIST, warn_non_proper_list).
 -define(WARN_NOT_CALLED, warn_not_called).
 -define(WARN_OPAQUE, warn_opaque).
+-define(WARN_OPAQUE_UNION, warn_opaque_union).
 -define(WARN_OVERLAPPING_CONTRACT, warn_overlapping_contract).
 -define(WARN_RETURN_NO_RETURN, warn_return_no_exit).
 -define(WARN_RETURN_ONLY_EXIT, warn_return_only_exit).