Merge pull request github#15261 from github/ginsbach/WeakAliasesInLanguageReference

document weak aliases in the language reference

Author: ginsbach

docs/codeql/ql-language-reference/aliases.rst

@@ -123,4 +123,20 @@ You could give the predicate a more descriptive name as follows:
 
 .. code-block:: ql
 
-    predicate lessThanTen = isSmall/1;
+    predicate lessThanTen = isSmall/1;
+
+.. _weak_strong_aliases:
+
+Strong and weak aliases
+=======================
+
+Every alias definition is either **strong** or **weak**.
+An alias definition is **strong** if and only if it is a :ref:`type alias <type-aliases>` definition with
+:ref:`annotation <annotations>` ``final``.
+During :ref:`name resolution <name-resolution>`, ambiguity between aliases from **weak** alias definitions
+for the same module/type/predicate is allowed, but ambiguity between between aliases from distinct **strong**
+alias definitions is invalid QL.
+Likewise, for the purpose of applicative instantiation of :ref:`parameterised modules <parameterized-modules>`
+and `:ref:`parameterised module signatures <parameterized-module-signatures>`, aliases from **weak** alias
+definitions for instantiation arguments do not result in separate instantiations, but aliases from **strong**
+alias definitions for instantiation arguments do.

docs/codeql/ql-language-reference/modules.rst

@@ -180,7 +180,8 @@ For example, in the previous two snippets, we relied on the predicate signature
     signature int transformer(int x);
 
 The instantiation of parameterized modules is applicative.
-That is, if you instantiate a parameterized module twice with identical arguments, the resulting object is the same.
+That is, if you instantiate a parameterized module twice with equivalent arguments, the resulting object is the same.
+Arguments are considered equivalent in this context if they differ only by :ref:`weak aliasing <weak_strong_aliases>`.
 This is particularly relevant for type definitions inside parameterized modules as :ref:`classes <classes>`
 or via :ref:`newtype <algebraic-datatypes>`, because the duplication of such type definitions would result in
 incompatible types.

docs/codeql/ql-language-reference/ql-language-specification.rst

@@ -115,7 +115,7 @@ Environments may be combined as follows:
 -  *Union*. This takes the union of the entry sets of the two environments.
 -  *Overriding union*. This takes the union of two environments, but if there are entries for a key in the first map, then no additional entries for that key are included from the second map.
 
-A *definite* environment has at most one entry for each key. Resolution is unique in a definite environment.
+A *definite* environment has only values that are *equal modulo weak aliasing* for each key.
 
 Global environments
 ~~~~~~~~~~~~~~~~~~~
@@ -334,7 +334,7 @@ For a *completely uninstantiated* parameter, the *bottom-up instantiation-resolu
 
 An entity is called *fully instantiated* if none of the *bottom-up instantiation-resolutions* of the parameters in the *relevant set of parameters* of the entity's *underlying completely uninstantiated* entity are parameters.
 
-Two *instantiated modules* or two *instantiation-nested* entities are considered *equivalent* if they have the same *underlying completely uninstantiated* entity and each parameter in its *relevant set of parameters* has the same *bottom-up instantiation-resolution* relative to either *instantiated module*.
+Two *instantiated modules* or two *instantiation-nested* entities are considered *equivalent* if they have the same *underlying completely uninstantiated* entity and each parameter in its *relevant set of parameters* has *bottom-up instantiation-resolution*s relative both *instantiated module*s that are *equivalent modulo weak aliases*.
 
 Module instantiation is applicative, meaning that *equivalent* *instantiated modules* and *equivalent* *instantiation-nested* entities are indistinguishable.
 
@@ -1763,7 +1763,7 @@ The grammar given in this section is disambiguated first by precedence, and seco
 Aliases
 -------
 
-Aliases define new names for existing QL entities.
+Aliases define new names for existing QL bindings.
 
 ::
 
@@ -1772,7 +1772,19 @@ Aliases define new names for existing QL entities.
          |   qldoc? annotations "module" modulename "=" moduleExpr ";"
 
 
-An alias introduces a binding from the new name to the entity referred to by the right-hand side in the current module's declared predicate, type, or module environment respectively.
+An alias introduces a binding from the new name to the binding referred to by the right-hand side in the current module's visible predicate, type, or module environment respectively.
+
+An alias is called a *strong alias* if and only if it has the ``final`` annotation. Otherwise, it is called a *weak alias*.
+
+Two bindings `A`, `B` are called *equal modulo weak aliasing* if and only if one of the following conditions are satisfied:
+
+- `A` and `B` are the same binding or
+
+- `A`` is introduced by a *weak alias* for `C`, where `B` and `C` are *equal modulo weak aliasing* (or vice versa) or
+
+- `A` and `B` are introduced by the same strong alias and they are aliases for bindings that are *equal modulo weak aliasing*.
+
+Note that the third condition is only relevant in :ref:`Parameterized modules`, where the binding introduced by the alias can depend on instantiation parameters.
 
 Built-ins
 ---------