introduce type unions in the handbook

docs/language/ql-handbook/types.rst

@@ -14,7 +14,8 @@ than one type.
 
 The kinds of types in QL are :ref:`primitive types <primitive-types>`, :ref:`classes <classes>`,
 :ref:`character types <character-types>`, :ref:`class domain types <domain-types>`, 
-:ref:`algebraic datatypes <algebraic-datatypes>`, and :ref:`database types <database-types>`.
+:ref:`algebraic datatypes <algebraic-datatypes>`, :ref:`type unions <type-unions>`,
+and :ref:`database types <database-types>`.
 
 .. index:: boolean, float, int, string, date
 .. _primitive-types:
@@ -479,6 +480,44 @@ program, so it's helpful to extend a new type (namely ``TTaintType``)::
     class Tainted extends TaintType, TTaintedValue {
     }
     
+.. _type-unions:
+
+Type Unions
+***********
+
+.. note:: The syntax for type unions is considered experimental and is subject to change.
+   However, they appear in the `standard QL libraries <https://github.com/github/codeql>`.
+   The following sections should help you understand those examples
+
+   Type unions are user-defined types that are declared with the keyword ``class``.
+   The syntax resembles type aliases, but with two or more type expressions on the right-hand side.
+
+   Type unions are used for creating restricted versions of existing algebraic datatypes, by explicitly
+   selecting a subset of the branches of said datatype and binding them to a new type.
+   In addition to this, type unions of database types are also supported.
+
+   Using a type union to explicitly restrict the permitted branches from an algebraic datatype
+   can resolve spurious recursion in predicates.
+   For example, the following construction is legal::
+
+       newtype T =
+          T1(T t) { not exists(T2orT3 s | t = s) } or
+          T2(int x) { x = 1 or x = 2 } or
+          T3(int x) { x = 3 or x = 4 or x = 5 }
+
+       class T2orT3 = T2 or T3;
+
+   However, a similar implementation that restricts ``T`` in a class extension is not valid.
+   The class ``T2orT3`` triggers a type test for ``T``, which results in an illegal recursion
+   ``T2orT3->T->T1->¬T2orT2`` due to the reliance of ``T1`` on ``T2orT3``::
+
+       class T2orT3 extends T {
+         T2orT3() {
+           this instanceof T2 or this instanceof T3
+         }
+         // ...
+       }
+
 .. _database-types:
 
 Database types