lrytz/efftp

Change Syntax for effect casts

Closed this issue · 0 comments

Currently, simple ascriptions are interpreted as effect casts:

  println(): @noIo

This is inconsistent with the behavior for normal types, where ascription triggers a type check. Also there is no way to trigger an effect check at a specific location, which would often be useful.

So we will change this:

  • Simple ascription will trigger an effect check, so println(): @noIo will trigger an error message
  • Effect casts will require an additional @unchecked annnotation, i.e. @println() @unchecked @noIo is an effect cast