[Dontrememberit]

Dependent types prevent infinite loops at compile time because if you have nonterminating terms, your types are unsound as a logic (you can derive true and false properties altogether)

That's because theorem proving with dependent types is based on the idea that you can prove something by providing a proof object that is a witness that what you want to prove is true. But a nonterminating function can fake it: you can write a function that promises a proof that something is true, while it never returns (so it never has to build a proof object). That way you can prove that false things are "true".

[kentonv]

Sorry, I don't understand.

Does this non-terminating function run at compile time or at runtime?

If it runs at compile time, and it doesn't terminate, then presumably no executable is generated? That's good enough for me.

Or are you describing a function that checks some property at runtime, which the type system then depends on afterwards? But if that function never returns, then the subsequent code that depends on the property it was checking won't ever execute. So a false thing is only proven true in code that never executes. That seems fine to me.

(Also note that as a practical matter I mostly don't care if it's possible for a developer to maliciously trick the type system. I only care about catching accidental errors. Relying on a complex type checker for sandboxing of malicious code seems too risky.)