The current reducer is hacky and not sound. In order to be fast, we make certain assumptions of the term's structure and its reduction behavior (e.g. every substitution is shared, even if they're supposed to be structuredCloned; we cache very liberally and don't rehash the parents after substitutions).

(NOTE: there are certain lines of thought that repeatedly lead me to believe that the current implementation is (or could be, with slight modifications) in fact sound... It's quite complex! 🦆)

A Haskell backend could do the sharing automagically in a higher order fashion. Lambda screen would also be a perfect target for optimal reduction because of the huge amount of sharing in typical terms/renderings.