Correction:
We show how to merge two folds into another fold `elementwise'. ... We need recursive types -- but again, never value recursion.
There is no need for recursive types, actually. Higher-rank types are still present, which we need for fold anyway. Introducing recursive types wasn't a good idea anyway, because with recursive types "\x -> x x" becomes typeable and we can easily recover value recursion. The following is an implementation of szipWith (the zip function over two folds) that uses no recursion -- neither in value nor in types. All iterative processing is driven by the folds themselves. I'm afraid the code is a bit less perspicuous than before (although the general idea remained the same): We introduce another higher-rank type (the old FR would have sufficed, too). The bulk of the code is splitting the fold l2 into the head and the "rest of the fold".
newtype FR1 a b = FR1 (forall w. (a->b->w) -> w -> w) unFR1 (FR1 x) = x
szipWith :: (a->b->c) -> FR a -> FR b -> FR c szipWith t l1 l2 = FR(\f z -> let p str e r = unFR1 (unFR str ssk caseB) (sk e r) z sk e1 r1 e2 r2 = f (t e1 e2) (r1 r2) caseB = FR1(\a b -> b) ssk v fk = FR1(\a _ -> a v (FR (\s' f' -> unFR1 fk (\ v'' x -> s' v'' (unFR x s' f')) f'))) in unFR l1 (\e r x -> p x e r) (\r -> z) l2)
All the old tests pass.