The TypeChoice is a kind of link, specifically, a kind of ChoiceLink, that allows a type to be polymorphic. It lists a set of types that a VariableNode may have, or that might occur in a SignatureLink. It is a type constructor.
Thus, for example,
TypedVariableLink VariableNode $G TypeChoice TypeNode "ConceptNode" TypeNode "PredicateNode"
The TypeChoice link is interpreted as an ChoiceLink, specifying that the variable $G can be either a ConceptNode or a PredicateNode.
A TypeChoice link can enclose a SignatureLink if more complex polymorphic types are needed. Thus, for example,
TypeChoice SignatureLink TypeNode "ListLink" TypeNode "ConceptNode" TypeNode "ConceptNode" SignatureLink TypeNode "ListLink" TypeNode "ConceptNode" TypeNode "ConceptNode" TypeNode "ConceptNode"
In type theory, the TypeChoice Link corresponds to the sum type, and thus is a form of disjoint union; it is the coproduct in the category of sets. The product, of course, corresponds the product type. The AtomSpace allows both of these, when working with types: use the TypeChoice link for sum types, and the SignatureLink for product types.
Note that by virtue of being a sum type, the empty TypeChoice corresponds to the bottom type. Thus can be used as such instead of an actually Bottom type construct (which might or not be introduced in the future).