add QL specification section on module instantiations

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

@@ -199,10 +199,21 @@ Kinds of modules
 
 A module may be:
 
+-  A *declared module*, if it is defined by the ``module`` or ``ql`` grammar rules.
+-  A *non-declared module*, if it is not a *declared module*.
+
+A *declared module* may be:
+
 -  A *file module*, if it is defined implicitly by a QL file or a QLL file.
 -  A *query module*, if it is defined implicitly by a QL file.
 -  A *library module*, if it is not a query module.
 
+A *non-declared module* may be:
+
+-  A *built-in module*.
+-  An *instantiated module* (see :ref:`Parameterized modules`).
+-  An *instantiation-nested module*  (see :ref:`Parameterized modules`).
+
 A query module must contain one or more queries.
 
 Import directives
@@ -249,6 +260,67 @@ For qualified identifiers (``a.b``):
 
 A qualified module identifier is only valid within an import.
 
+.. _Parameterized modules:
+
+Parameterized modules
+~~~~~~~~~~~~~~~~~~~~~
+
+Modules with parameters are called *parameterized modules*. A *declared module* has parameters if and only if it is a *library module* and its declaration uses the ``parameters`` syntax.
+
+*Parameterized modules* can be instantiated with arguments that match the signatures of the parameters:
+
+- Given a type signature, the corresponding argument must be a type that transitively extends the specified ``extends`` types and is a transitive subtype of the specified ``instanceof`` types.
+- Given a predicate signature, the corresponding argument must be a predicate with exactly matching relational types.
+- Given a module signature, the corresponding argument must be a module that exports all the specified type and predicate members. Furthermore, the module must be declared as matching the module signature via the ``implements`` syntax.
+
+The result of instantiating a *parameterized module* is an *instantiated module*. The parameterized module is called the *underlying module* of the *instantiated module*.
+
+Instantiation-relative and instantiation-nested entities
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Given an *instantiated module*, every entity has a corresponding entity called the *instantiation-relative* entity, which is determined as follows:
+
+- If the entity is the *underlying module*, its *instantiation-relative entity* is the *instantiated module*.
+- If the entity is a parameter of the *underlying module*, its *instantiation-relative entity* is the corresponding argument.
+- If the entity is declared inside the *underlying module* or its nested modules, its *instantiation-relative* entity is an *instantiation-nested* entity that is generated by the module instantiation. Parameters of any modules that are nested inside the *underlying module* are considered declared inside the module for this purpose.
+- Otherwise, the entity's *instantiation-relative* entity is the initial entity itself.
+
+When the *instantiation-relative* entity of an entity is an *instantiation-nested* entity, then the initial entity is called the *underlying nested* entity of the *instantiation-nested* entity*, the *instantiated module* is called the *instantiation root* of the *instantiation-nested* entity, and the *underlying module* is called the *underlying root* of the *instantiation-nested* entity.
+
+The components of an *instantiation-nested* entity are the *instantiation-relative* entities of the components of its *underlying nested* entity. Among other things, this applies to:
+
+- values in the exported environments of *instantiation-nested* modules,
+- relational types of *instantiation-nested* predicates and predicate signatures,
+- required signatures of *instantiation-nested* parameters,
+- parameters of an *instantiation-nested* *parameterized module*,
+- fields and member predicates of *instantiation-nested* dataclasses.
+
+Given an *instantiated module*, any alias in the program has a corresponding alias called the *instantiation-relative* alias, which targets the *instantiation-relative* entity.
+
+Applicative instantiation
+~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Every entity has an *underlying completely uninstantiated* entity that is determined as follows:
+
+- If the entity is an *instantiated module*, its *underlying completely uninstantiated* entity is the *underlying completely uninstantiated* entity of the *underlying module*.
+- If the entity is an *instantiation-nested* entity, its *underlying completely uninstantiated* entity is the *underlying completely uninstantiated* entity of the *underlying nested* entity.
+- Otherwise, its *underlying completely uninstantiated* entity is the entity itself.
+
+An entity is called *completely uninstantiated* entity if it is its own *underlying completely uninstantiated* entity.
+
+Every *completely uninstantiated* entity has a *relevant set of parameters*, which is the set of all parameters of all the modules that the entity is transitively nested inside. For entities that are not nested inside any modules, the *relevant set of parameters* is empty.
+
+Note that the *relevant set of parameters* by construction contains only *completely uninstantiated* parameters.
+
+For a *completely uninstantiated* parameter, the *bottom-up instantiation-resolved* parameter relative to an entity is defined as:
+
+- If the entity is an *instantiated module* or an *instantiation-nested* entity, the *bottom-up instantiation-resolved* parameter is the *instantiation-relative* parameter of the *bottom-up instantiation-resolved* parameter relative to the *underlying module*.
+- Otherwise, the *bottom-up instantiation-resolved* parameter is the parameter itself.
+
+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-resolved* parameter relative to either *instantiated module*.
+
+Module instantiation is applicative, meaning that *equivalent* *instantiated modules* and *equivalent* *instantiation-nested* entities are indistinguishable.
+
 Module references and active modules
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~