document module signature member defaults

docs/codeql/ql-language-reference/name-resolution.rst

@@ -223,7 +223,8 @@ For a module ``M``, it is useful to distinguish between its **privately declared
 - The **publically declared** namespaces of ``M`` contain all entities and aliases that are declared—that is, defined—in ``M`` and that are not annotated as ``private``.
 - The **exported** namespaces of ``M`` contain
     1. all entries from the **publically declared** namespaces of ``M``, and
-    2. for each module ``N`` that is imported into ``M`` with an import statement that is not annotated as ``private``: all entries from the **exported** namespaces of ``N`` that do not have the same name as any of the entries in the **publically declared** namespaces of ``M``.
+    2. for each module ``N`` that is imported into ``M`` with an import statement that is not annotated as ``private``: all entries from the **exported** namespaces of ``N`` that do not have the same name as any of the entries in the **publically declared** namespaces of ``M``, and
+    3. for each module signature ``S`` that is implemented by ``M``: an entry for each module signature default predicate in ``S`` that does not have the same name and arity as any of the entries in the **publically declared** predicate namespace of ``M``.
 - The **visible** namespaces of ``M`` contain
     1. all entries from the **exported** namespaces of ``M``, and
     2. all entries from the **global** namespaces, and

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

@@ -144,7 +144,9 @@ These are defined as follows (with X denoting the type of entity we are currentl
 
     1.  its *publically declared X environment*, and
 
-    2.  for each module which the current module directly imports (excluding ``private`` imports - see "`Import directives <#import-directives>`__"): all entries from the *exported X environment* that have a key not present in the *publically declared X environment* of the current module.
+    2.  for each module which the current module directly imports (excluding ``private`` imports - see "`Import directives <#import-directives>`__"): all entries from the *exported X environment* that have a key not present in the *publically declared X environment* of the current module, and
+
+    3.  if X is ``predicates``, then for each module signature ``S`` that is implemented by the current module: an entry for each module signature default predicate in ``S`` that does not have the same name and arity as any of the entries in the **publically declared predicate environment** of the current module.
 
 -  The *visible X environment* of a module is the union of
 

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

@@ -83,16 +83,24 @@ In detail, a type signature definition consists of:
 #. The name of the module signature. This is an `identifier <https://codeql.github.com/docs/ql-language-reference/ql-language-specification/#identifiers>`_
    starting with a uppercase letter.
 #. Optionally, a list of parameters for :ref:`parameterized module signatures <parameterized-module-signatures>`.
-#. The module signature body, consisting of type signatures and predicate signatures enclosed in braces.
+#. The module signature body, consisting of type signatures, predicate signatures, and default predicates enclosed in braces.
    The ``signature`` keyword is omitted for these contained signatures.
 
+Module signature default predicates are syntactically constructed like predicate signatures,
+but preceded by the ``default`` keyword, and with a predicate body instead of the concluding
+semicolon ``;``.
+Default predicate bodies are restricted in that they may not use entities that in any way
+depend on other module signature members or parameters of the module signature or any
+existing enclosing modules.
+
 For example:
 
 .. code-block:: ql
 
     signature module MSig {
       class T;
       predicate restriction(T t);
+      default string descr(T t) { result = "default" }
     }
 
     module Module implements MSig {