Parse return type annotation of operations

[jiribenes]

Motivation

When a user mistakenly specifies a type annotation of an operation handler, they get an unfriendly error message from the parser at the wrong place:

This also happens when specifying a return type of a object operation:

Solution

• Allow the OpHandler AST to include an optional return type.
• Modify the parser to optionally parse the return type of an operation.
• In the Typer phase -- if a return type is specified for an operation, throw an error.
• Add negative test for annotated object operation and another negative test for annotated handler operation

Alternative solution

We could also just somehow forbid a return type annotation in the parser, but I haven't been able to do it in a nice way. However, I believe that we want to write down this information from the user even if we decide to ignore it.

Discussion

Is Typer the best phase to report this error? We could also report it earlier while in a Namer or PreTyper phase, but it seems like this is a typing-related problem that we might want to improve in the future.

The solution is not optimal. Ideally, we should take the user-specified return type annotation and somehow take it into consideration for better error messages.
Effect does in fact allow the annotation of the arguments of the handler and even checks them:

Unfortunately, there is an ambiguity about what the return type of an operation handler actually is -- is it the resulting type of the body, or the type of the argument we put into the resume continuation?

We also don't support annotations on object operations where we should just check the type and compared to the previously defined type in the interface. There are some subtleties to get right -- see comments below for more details.

[b-studios]

Maybe you could add a neg-test to show the error message?

After adding the effekt file to examples/neg you can simply run

project effektJVM
test:console
scala> effekt.TestUtils.generateCheckFiles()

to generate the check files. Passing true to generateCheckFiles will regenerate ALL check files.

[jiribenes]

I've updated the PR text and added a few details about what we (plan to?) do with object operations.

[b-studios]

// TODO: what about the effects?

That's an interesting question, because it influences the capability passing transformation.

[b-studios]

It should be clear that you can only annotate effects, which form a subset of the declared effects. However, we still need to introduce capabilities corresponding to the declared effects, not the annotated one (since the call site cannot know).

[b-studios]

That's very subtle...

[b-studios]

Whatever we do, it should behave similarly to how we deal with annotated effects on functions:

effekt/effekt/shared/src/main/scala/effekt/Typer.scala

Lines 594 to 614 in 5fa89a2

	case Some(annotated) =>
	// the declared effects are considered as bound
	val bound: ConcreteEffects = annotated.effects
	val capabilities = bound.controlEffects.map { tpe => Context.freshCapabilityFor(tpe) }
	val captures = capabilities.map { _.capture }
	// block parameters and capabilities for effects are assumed bound
	given Captures = inferredCapture
	val Result(tpe, effs) = Context.bindingCapabilities(d, capabilities) {
	Context in { body checkAgainst annotated.result }
	}
	Context.annotateInferredType(d, tpe)
	Context.annotateInferredEffects(d, effs.toEffects)
	// TODO also annotate the capabilities
	flowsIntoWithout(inferredCapture, functionCapture) {
	annotated.cparams ++ captures ++ List(selfRegion)
	}
	Result(annotated, effs -- bound)

It is just, that there we do not have any declared effects -- and capability passing should be informed by declared effects, not annotated effects :)

[jiribenes]

I think it might be wise to change the scope of this PR.

Let's first merge this more-or-less as-is, specifically with parsing return type annotations on all operations and reporting them as errors.
Then afterwards, let us add proper support for (type checking) return type annotations on object operations.

[I've updated the body of this PR to reflect this]