[breatheoften]

A user configurable parameter for timeout would be a terrible language design mistake.

You would want as much as possible to make the timeout not based on runtime -- but on an abstract model of the computation which doesn't actually depend on any machine particular. "Hey your program didn't compile on my machine -- try a faster cpu" would be a nightmarish interaction.

You want constraints about how long these programs are allowed to execute to be tight enough for developers to learn a sense for what is reasonable to do with these features -- as opposed to waiting for runtime.

[dependenttypes]

So, the user should not have the option to say "hey, I want this done within 10 minutes because I have to leave soon" or "I want my auto-complete to be done within 1 second", got it. Instead we should care about the feelings of arm and atom cpus.