Thanks, Ed. It hadn't occurred to me that defunctionalization might be useful for monomorphization. Do you know of a connection?
I'm using a perfect leaf tree type similar to the one you mentioned but indexed by depth:
> data Tree :: (* -> *) -> Nat -> * -> * where
> L :: a -> Tree k 0 a
> B :: Tree k n (k a) -> Tree k (1+n) a
Similarly for "top-down" perfect leaf trees:
> data Tree :: (* -> *) -> Nat -> * -> * where
> L :: a -> Tree k 0 a
> B :: k (Tree k n a) -> Tree k (1+n) a
This way, after monomorphization, there won't be any sums remaining.
-- Conal