system.FFI effect doesn't "subsume" other effects

[Darya-]

In the text-editor application, annotate the logger type and module in the following way:

logger.wyv:

module def logger(logFile: fileSystem.File): Logger
effect Update = {}
def updateLog(msg: String): Unit
...

Logger.wyt:

resource type Logger
  effect Update
  def updateLog(msg: String): {this.Update} Unit

Then annotate textEditor's run and runPluginOnSetup methods in the following way:

In both textEditor.wyv and TextEditor.wyt:

def runPluginOnSetup(plugin: Plugin): {system.FFI} Unit
def run(): {system.FFI} Unit

Run the text-editor application.

Expected behavior: No error is thrown.

Actual behavior: The following error is thrown:
Effect annotation {system.FFI} on method run is not a subtype of effects that method produces, which are [system.FFI, logger.Update]; at location file wyvern/examples/text-editor/textEditor.wyv on line 134 column 5

[JonathanAldrich]

You don't show the implementation of run and runPluginOnSetup, so I can't tell for sure what the issue is.

But if you were expecting system.FFI to be the universal effect (i.e. top in the lattice of effect sets), that is not how I envisioned it. Rather, I see it as a primitive out of which other effects can be built. If you have a strong reason to treat it as Top, we should discuss. Perhaps there should be some other thing that is Top.

[Darya-]

The full implementations can be seen in the linked file: https://github.com/wyvernlang/wyvern/blob/master/examples/text-editor/textEditor.wyv.

Let's discuss this at our next meeting.