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.