let x = id id id id id id id id id id id id id id id id id id id id id id id id
See how long that takes (add ids if your machine can take it). To deduce a type for x, ghci will use 2^k type variables, if you have k ids. This is easily seen by induction:
If k = 1, then the type of x is a -> a. This takes 2 = 2^1 = 2^k variables.
If k > 1, it is of the form id f. Let t be the type of f. t has 2^{k - 1} variables, by induction. Thus the outermost id must take something of type t (this is 2^{k - 1} variables) and produce something of that same type t (this is another 2^{k - 1} variables), that is, it's of type t -> t. 2^{k - 1} + 2^{k - 1} = 2^k.
Note that this information is purely at compile time. Haskell isn't typed at runtime, this is all just to check types. At runtime, x is a no-op, as expected.
I used to be able to kill Scala compiler performance with just a a few identifiers. Well, Scala is trying to deal with nominal subtyping, which is well known to be quite hard (so the type inference algorithm isn't really H-M, and must rely on heuristics).
This was in 2006/7 when I was working on scalac, so the early 2.1/2.2 days. I seemed to often push the type system in places that were not well defined, mostly because my scala style was so different (very OO, but with heavy recursive use of type parameters). Unfortunately, I've forgotten what the cases were, but they were usually simple constructions.
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?
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.
If k = 1, then the type of x is a -> a. This takes 2 = 2^1 = 2^k variables. If k > 1, it is of the form id f. Let t be the type of f. t has 2^{k - 1} variables, by induction. Thus the outermost id must take something of type t (this is 2^{k - 1} variables) and produce something of that same type t (this is another 2^{k - 1} variables), that is, it's of type t -> t. 2^{k - 1} + 2^{k - 1} = 2^k.
Note that this information is purely at compile time. Haskell isn't typed at runtime, this is all just to check types. At runtime, x is a no-op, as expected.