================================================================================ P9606 E. Visser "Solving type equations in multi-level specifications" (preliminary version) In first-order algebraic specification functions have types of the form s_1 x ... x s_n -> s_0, where the s_i are type constants. Such types exclude higher-order and polymorphic functions. In multi-level algebraic specification the structure of types used in function declarations is specified as an algebraic data type. If only free constructors are used in the types used in function declarations, type assignment is an extension of the Hindley/Milner algorithm to multiple levels of types. By means of equations over types, sophisticated type systems can be modeled in a simple and uniform language. The type assignment for arbitrary multi-level specifications requires E-unification. Although this is undecidable in general, it is decidable for restricted sets of equations. In an earlier paper, the modular applicative multi-level equational specification formalism MLS is defined. The typechecker supports only free type constructors. In this paper we introduce multi-level specification by means of a series of MLS examples and discuss the extension with an E-unification procedure instead of syntactic unification of the type assignment function for MLS such that it supports type definitions, defined type operators and recursive types.