Rules for turning type names into types.
Type names arise, in quoted constant form, from the abstract syntax that is symbolically executed. In some circumstance, these type names are turned into types, via tyname-to-type. If we just enabled the executable counterpart of this function we would end up with types in quoted constant form. Instead, we want to keep types as terms with constructors, particularly because some types include identifiers (e.g. structure types), and we want to keep identifiers as terms with constructors instead of in quoted constant form (see atc-identifier-rules.
Thus, here we collect rules to rewrite quoted type names to types that are terms with constructors.