Open marzipankaiser opened 2 months ago
The following program gives the annotated error:
interface Done { def done(): Nothing } def main() = { try { do done() } with Done { def done() = () // Error: Expected Nothing but got Unit. } }
Is this the behaviour we want?
Note that this also disallows, e.g., a hole instead of do done().
do done()
What would you expect, otherwise? The answer type of the handler is Nothing unless you upcast it there.
Nothing
We could of course compute the join of the different handlers and the answer type.
The following program gives the annotated error:
Is this the behaviour we want?
Note that this also disallows, e.g., a hole instead of
do done()
.