wyvernlang/wyvern

Method effect annotations may differ between type and module

Opened this issue · 1 comments

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 = {system.FFI}
def updateLog(msg: String): Unit
  val logAppender = logFile.makeAppender()
  logAppender.write(msg)
  logAppender.close()

Logger.wyt:

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

Run the text-editor application.

Expected behavior: Throws an error saying that the logger module doesn't match the Logger type because logger's method isn't annotated with the matching effect (i.e., logger's method should have the signature: def updateLog(msg: String): {Update} Unit).

Actual behavior: No error is thrown.

It's not surprising that no error would be given because logger.wyv does not have effect annotations. Putting an annotation {} on the module definition should force an annotation on updateLog. According to my conversation with @Darya- this is not the case, so that is the first thing we should fix.