I don't think you can have such compiler, at least for a general case, without solving the halting problem first. After all, you can encode arbitrary computatio

I don't think you can have such compiler, at least for a general case, without solving the halting problem first. After all, you can encode arbitrary computations at the type level.