This takes two pretypes and returns an old-to-new instn list for generated tyvars, calculated by comparing corresponding subcomponents of the pretypes. This instn list is not necessarily closed (i.e. it may need to be applied repeatedly until it makes no change) and may contain inconsistencies when when the two pretypes cannot be unified (instead of failing). These are dealt with by instantiation closure (see below).

Checks that the supplied pretype is well-formed, by checking that all compound types have the correct arity for the type constant involved. This gets used on stand-alone type quotations and on types embedded as type annotations in term quotations.

Replaces the generated tyvars in the supplied preterm with their most general valid pretypes, deduced from type inference. Note that the preterm input is assumed to have been detyped.

Takes an existing closed pretype instn list 'theta0' and a second (not necessarily closed or consistent) pretype instn list 'theta', and incorporates 'theta' into 'theta0', resulting in either a new closed instn list or failure (if inconsistencies exist in 'theta' wrt 'theta0').

Unifies all pretypes in the supplied list with each other, incorporating the result into existing closed instn list 'theta0'.

Unifies the left pretype with the right pretype of each pair in the supplied list, incorporating all the results into existing closed instn list 'theta0'.

Unifies any generated tyvars in input pretypes 'pty1' and 'pty2', to result in either a closed pretype instn list for making them equal, or failure (when the pretypes cannot be unified). In 'unify_pretypes0', the unification is carried out wrt input pretype instn list 'theta0', and the result incorporates 'theta0' (but with its range instantiated according to the unification). Note that 'theta0' is assumed to be closed.