This is the datatype for internal HOL types. It has 2 classes, corresponding to the 2 primitive syntactic categories of types:

 

Type Variable denotes an occurrence of a type variable. It has just a name attribute. Any two occurrences of type variables within a given object represent the same entity iff they have the same name.

 

Compound Type denotes an instance of a type constant. It has name and type parameter list attributes, where the name must be the name of a declared type constant, and the parameter list length must equal the declared type constant's arity.