[kachnuv_ocasek]

It's the size of the term. See this paper which proves the result for details: https://link.springer.com/chapter/10.1007/3-540-52590-4_50

[mmoskal]

More specifically, time is almost linear with the size of the type, which can be doubly exponential compared to the program but people don't write such programs.