Here we are interested in finding a completion for a standard program .
We
will do so by deriving a constraint system from the type system shown above
where we combine the different rules for the two-level variants of a
construct. This combined type system must be syntax-directed (i.e., only
one rule is applicable to each construct) to be suitable for type
reconstruction. Therefore we have to incorporate applications of [WEAK] and
[LIFT] into the appropriate rules. For example, the different rules for
(fixed-arity) abstraction are combined with [WEAK] to (using FV (E) to denote
the
free variables of E) the rule [ABS-COMB] in Fig. 12.