Nothing type should affect definite return

[CeylonMigrationBot]

[@lucaswerkmeister]

Nothing die(String? cause = null) {
    // log error
    // send mail to administrator
    throw Exception(cause);
}

String doWork() {
    if (true || false) {
        return "work";
    } else {
        die("Fatal logic error");
    }
}

We can reason that since die returns Nothing, it cannot ever return normally (it could throw, terminate the VM / thread, or never return). Therefore, doWork definitely returns even in the else branch, just like if we inserted a throw; statement there.

The typechecker currently doesn’t do this reasoning, though:

source/tmp/run.ceylon:7: error: does not definitely return: 'doWork' has branches which do not end in a return statement

String doWork() {
      ^

I think this reasoning should be possible, since the flow analysis phase happens after the type assignment phase (see also #3997).

And I suppose this could also be applied to definite initialization.

[Migrated from ceylon/ceylon-spec#1179]

[CeylonMigrationBot]

[@gavinking] Interesting. Good idea. I never thought of that.

[CeylonMigrationBot]

[@lucaswerkmeister] The downside with this is that if people do use this (a powerful die function is the only example I can think of), they’ll get “expression has type Nothing” warnings for perfectly reasonable code. But at least we can disable warnings now, so perhaps that’s not so bad.

[CeylonMigrationBot]

[@gavinking] Well if we did this we could eliminate that warning for the case of an invocation of a function with return type Nothing that is occurs as a statement. It's clear in this case that the function is being called for its side-effect.

[CeylonMigrationBot]

[@lucaswerkmeister] Oh, good point. This still discourages stuff like gcc --version > /dev/null || die "No GCC found", which I’ve seen in Bash scripts, but makes much less sense in Ceylon.

[CeylonMigrationBot]

[@jvasileff] I think this would be a great improvement, with many uses. But for the common case, I think #3757 would result in much more readable, maintainable, and well documented code.

Edit - ok, I see you're not suggesting this be used in expressions. But I don't see how this wouldn't be at least as confusing, as presented in the initial example, as a "buried" throw in an expression.

[CeylonMigrationBot]

[@gavinking] Just pushed an experimental implementation of this, but it's not for 1.2.

[CeylonMigrationBot]

[@lucaswerkmeister] Now that process.exit() has type Nothing, perhaps disabling the “expression has type Nothing” warning should be something for 1.2? At the moment we get warnings for that in the SDK.

[weakish]

Now that process.exit() has type Nothing, perhaps disabling the “expression has type Nothing” warning should be something for 1.2?

@lucaswerkmeister I think at least it should be suppressed for process.exit(); statement in shared void run().