For languages with Hindley-Milner typing, like SML and OCaml, it has long been known that type-checking is even worse in the worst case (DEXPTIME hard) [1]. But the programs where this matters aren't what one would write by hand, typically.
OCaml:
let x1 = fun y -> (y, y) in
let x2 = fun y -> x1 (x1 y) in
let x3 = fun y -> x2 (x2 y) in
let x4 = fun y -> x3 (x3 y) in
let x5 = fun y -> x4 (x4 y) in
let x6 = fun y -> x5 (x5 y) in
x6 (fun z -> z)
test = let
x1 = \y -> (y, y)
x2 = \y -> x1 (x1 y)
x3 = \y -> x2 (x2 y)
x4 = \y -> x3 (x3 y)
x5 = \y -> x4 (x4 y)
x6 = \y -> x5 (x5 y)
in x6 (\z -> z)
So, while id id has type ('a -> 'a) -> ('a -> 'a), this is stored in memory by a pointer structure that amounts to let 'b = ('a -> 'a) in ('b -> 'b). The type of id id id would become let 'b = ('a -> 'a) in let 'c = ('b -> 'b) in ('c -> 'c). This grows linearly. If one were to write out the types without sharing then their size would grow exponentially.
Apparently that's been fixed. I can't confirm because that's not something I ever check the type of.
That is to say, pathological expressions don't stay small but induce horrendous searching, but rather merely get a log bigger (and that can cause more trouble for the rest of the program).
That means a heuristic to bail out when something grows a lot probably not violate the users intent and get it back into polynomial time.