Unfortunately, beta-eta reduction on Church-coded terms (as in Morte) is much weaker than what is commonly understood as supercompilation, and it is false that

Unfortunately, beta-eta reduction on Church-coded terms (as in Morte) is much weaker than what is commonly understood as supercompilation, and it is false that "no matter how many layers of indirection you might add the binary size and runtime performance would be unaffected". This kind of statement can only theoretically hold for something like simple type theory with strong finite products and coproducts, for which (quasi) normalization has been recently shown in https://arxiv.org/abs/1610.01213 https://arxiv.org/abs/1610.01213