Expressions with exponentially large types

Consider Haskell expressions like <haskell> let f x = (x, x) in let g = f . f . f in let h = g . g . g in h . h . h </haskell> I'll call this expression E(3, 3) because there are three layers using f, g and h, and in each layer three copies of a function are composed, as in f . f . f. In this expression, the type of g is <haskell> 'a -> ((('a, 'a), ('a, 'a)), (('a, 'a), ('a, 'a))) </haskell> which has the shape of a complete binary tree of depth three; I'll call it T(3). The type of h is obtained by substituting this type into itself to depth three, and is therefore T(9); and the type of the whole expression is correspondingly T(27). When printed out, it contains 2²⁷+1 occurrences of α.

Generalizing, the expression E(k, n) builds up functions whose types are T(n), T(n²), ..., T(n^k) and has a type containing 2^nk+1 occurrences of α. If the type of E(3, 3) isn't big enough, then E(4, 4) still fits on one line: <haskell> let f x = (x, x) in let g = f . f . f . f in let h = g . g . g . g in let p = h . h . h . h in p . p . p . p </haskell> and has a type containing 2²⁵⁶+1 occurrences of α – that's about 10⁷⁷.

It's still more satisfying to avoid the pair constructor and use a Church encoding instead. In the expression <haskell> let f x p = p x x in let g = f . f . f in let h = g . g . g in h . h . h </haskell> the type of g is <haskell> 'a -> ((((('a -> 'a -> 'b) -> 'b) -> (('a -> 'a -> 'b) -> 'b) -> 'c) -> 'c) ->

    (((('a -> 'a -> 'b) -> 'b) -> (('a -> 'a -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd

</haskell> which contains the expected eight occurrences of α, but also eight β's, four γ's and two δ's. And so on.