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