 Solution

Suppose that a direct tree fold with result type [Tree a] implements proper, so proper = fold one two. Every leaf has result [], hence one x = [] for every label x. Consequently proper (Two (One x) (One y)) would always equal two [] [], independently of either label. Taking labels from Bool, the inputs Two (One False) (One False) and Two (One True) (One False) would therefore have equal results. Their correct results are [One False, One False] and [One True, One False], which differ. This is a contradiction.

There is no direct fold with only the proper-subtree list as its recursive summary. This is the direct tree-fold information obstruction: replacing both children by equal summaries prevents the parent operation from recovering their different labels. The claim must not be extended to every expression containing a tree fold. A fold retaining the original tree alongside its proper-subtree list, followed by projection, does work; alternatively tail . subs uses the richer fold from part (f).