One way to ascertain the quality of the generated code – its
performance, hygiene, memory safety, deadlock freedom, etc. – is to
decorate it with annotations that explicate some aspect of the code:
e.g., the count of particular operations, its free variables, the
sequence of IO or memory allocation operations, correctness proof
obligations. The annotations are built along with generating
the code, and may be used to detect problems like scope
extrusion or deadlock – well before the whole program is
generated, let alone executed. Annotations are a worthy
alternative to fancy types.

Generating code along with annotations is almost straightforward. The
challenge comes from generating functions or other variable-binding
forms, with the often used so-called higher-order abstract syntax
(HOAS). That was the challenge posed by Olivier Danvy.

The present paper describes a new, simpler and general solution of the
challenge – actually, of its general form: pairing of
HOAS generators, or direct product of algebra-like structures with HOAS
operations. The solution also overcomes the hitherto unsolved HOAS problem:
latent effects.