[remram]

That doesn't seem right to me. I can define a function returning "void", and it can terminate. I would expect that a function returning an uninhabited type can never complete.