[apatil]

That's very interesting. In which variable is type inference EXPTIME complete?

Whichever variable it is, I suppose in practice humans can't create programs that are big enough in that way for type inference to become impractical. However, I wonder whether someone could comment on what this means about the utility of HM-like type systems in future AI generated software.

[disjunction181]

It's not that humans don't write such large programs, it's that the kind of pattern that causes the exponential behavior doesn't naturally occur in long chains in any kind of written code. You can provide the pathological inputs yourself and quickly freeze e.g. OCaml's typechecker, they just don't ever naturally occur to the point of becoming a problem.

Here's an example of the pathological pattern in OCaml: https://cs.stackexchange.com/questions/6617/concise-example-...

[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.