dialyzer: add global variable binding

[kikofernandez]

Make typed argument names and type variables global in their declaration.

Before this PR, the following example would make the linter to complain about singleton variable used:

-foo(X :: integer()) -> X.
foo(X) ->
    X.

So the linter would complain with the following message:

type variable 'X' is only used once (is unbound)

With this pull request, an argument name given to a type becomes bound globally and usable anywhere in the type specification.

Furthermore, bound type annotations cannot receive different types, which was something that we never took care of, and duplicate annotation names are also disallowed.

Example:

-spec id(X) -> X when
    X :: string(),
    X :: integer().   # notice that this was allowed

-spec id(X :: term()) -> X :: term(). # throws error since annotation X is bound multiple times.

This code throws a linter error if such declaration of duplicate names with different types appear.

[github-actions]

CT Test Results

No tests were run for this PR. This is either because the build failed, or the PR is based on a branch without GH actions tests configured.

Results for commit c0275b4

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)
• No HTML docs found
• No Windows Installer found

// Erlang/OTP Github Action Bot

[kikofernandez]

Stalled until a new tag for getopt is created
jcomellas/getopt#54

[kikofernandez]

Stalled until the following PR is merged
deadtrickster/ssl_verify_fun.erl#30

[ilya-klyuchnikov]

I have a concern that this PR changes the semantics how type specs are interpreted:

Right now - as documentation says - such syntax is used for documentation purposes. - It's not the same as type variables.

https://www.erlang.org/doc/reference_manual/typespec.html#specifications-for-functions

Also, for documentation purposes, argument names can be given:
-spec Function(ArgName1 :: Type1, ..., ArgNameN :: TypeN) -> ReturnType.

And currently for dialyzer (and for eqWAlizer, and I believe for Gradualizer as well) -spec Function(ArgName1 :: Type1, ..., ArgNameN :: TypeN) -> ReturnType. is equivalent to just -spec Function(Type1, ..., TypeN) -> ReturnType.

---

To me, as a documentation reader, argument names and type variables are different concepts. This PR makes documentation confusing - as the addition to documentation (see below) implies that "argument names" and "type variables" are the same concepts.

Since OTP-27, argument names become global in the type specification. That is, the following examples are all equivalent

[kikofernandez]

I am not sure that this PR will go through, due to breaking existing 3rd party code.

That said:

To me, as a documentation reader, argument names and type variables are different concepts. This PR makes documentation confusing - as the addition to documentation (see below) implies that "argument names" and "type variables" are the same concepts.

Type variables and argument names are different. This PR only binds argument names to types, so that one can reuse the name.

Example:

-spec foo(X :: integer(), Y) -> {X, Y}.

Argument X is bound to integer(), so one can assume that the following is its equivalent:

-spec foo(X :: integer(), Y) -> {X :: integer(), Y}.

The type variable Y is still a type variable. Any type variable without a type is a type variable (as always). Argument names are bounded to a type and can be reused just by using their name, without having to duplicate its type. AFAIK this is fixing code where clients assumed that:

-spec foo(X :: integer(), Y) -> {X, Y}.

The first X was bound to integer() and the second X was also bound to integer(), when in reality, the second X is a free type variable (unbound). If you will, this is the same as re-writing the following:

-spec foo(X, Y) -> {X, Y} when X :: integer().

The only difference is that you do not need to use the when to do the binding of X "global" on the scope of the type declaration.

[kikofernandez]

This example below has tripped some customers thinking that X :: integer() in any place they used X.

-spec foo(X :: integer(), Y) -> {X, Y}.

which is not true. Here the second Y is a free (type) variable.
Since it does not appear as an input argument, it is illegal code from a standard type system perspective (AFAIK) since it is a singleton type variable happening at the return side.

Does this make sense?

[kikofernandez]

I will continue stalling this until we know this is correct and dependencies to which I submitted PRs have been merged.