All type checkers for sophisticated dependent type theories (e.g. MLTT) will resist any bound on time or memory you try to place, let alone a quadratic or expon

All type checkers for sophisticated dependent type theories (e.g. MLTT) will resist any bound on time or memory you try to place, let alone a quadratic or exponential one. Somehow nobody seems to complain about how long they take to type-check. Both decidability and worst case time bounds are red herrings when it comes to a good type system (even for proof assistants).