In order to put the type system of the preceding section to work we need an efficient type reconstruction algorithm which--given the binding-times of the arguments of a goal function--automatically constructs a well-typed two-level program from a program. This two-level program should be minimal in a sense to be defined below.