That would be a very restrictive programming environment, or type checking might fail or produce ridiculously large runtime bounds. It is not decidable whether a given Turing machine has runtime O(n^k) for a particular k, even if you're given the promise that such a k exists.