[spacemanaki]

That's very interesting! This seems to me like it might be a different kind of edge case though, since the type of x is still t -> t, even if it takes a long time for the type checker to arrive at this. From the little I got out of Mairson's paper, it seems that the proof he uses depends on the exponential size of the type itself, but I could be mistaken... either way I wonder how they're related?

[throwaway_yy2Di]

    "I wonder how they're related?"

You could replace `id' with something that expands things, like \x -> (x,x):

    let f = \x -> (x,x) in (f.f.f.f.f.f) ()

Now it builds exponentially large tuple types. (?) And going back to the example in the blog:

    let f = \x -> (x,x) in (f.f.f.f.f.f) id

This is the same as the spacemanaki's example, without explicitly labeling the d1,d2,d3... intermediates.

[spacemanaki]

Actually, these examples are similar to the first example in my post (under the first "pathological case" heading) and don't quite exhibit the worst case behavior since the type can be represented in linear space as a dag.