Capability escapes from higher-order function

[b-studios]

@dvdvgt identified the following program

interface Time {
  def now(): Int
}

def withTime[A] { prog: { Time } => A }: A =
  try {
    prog {timeCap}
  } with timeCap: Time {
    def now() = resume(1)
  }

def main() = {
  def b { t: Time }: Time at {t} = box t;  // this is fine
  val cap = withTime {b} // ERROR escapes
  def t2: Time = unbox cap
  t2.now()
}

which type-checks but crashes at runtime. It appears, we forgot the wellformedness check on higher-order functions.

[b-studios]

We need to check that all inferred type arguments (and potentially return types) are well-formed. In this case both are not, for instance:

withTime[Time at {t}] {b}
//       ^^^^^^^^^^^
//      t not in scope

[b-studios]

Same wellformedness bug with higher rank types:

def hof[A] { prog: [B](B) => A }: A = prog[String]("hello")

def main() = {
  val res = hof { [C](x: C) => x };
  println(res.genericShow)
}

[dvdvgt]

https://github.com/effekt-lang/effekt/blob/68d40378fea59cb66074de3eb61df7048578a4e1/effekt/shared/src/main/scala/effekt/typer/Wellformedness.scala#L12

needs to be changed to class WFContext(var capsInScope: List[symbols.BlockParam]) and then updated at every binding instance while type checking. We still need to investigate whether we need to check the well-formedness in every "type judgement".

[b-studios]

We have a very similar case for existentials, where we also forgot to reintroduce the WF-check:

type Box { Wrap[X](x: X) }

def main() = {
  val res = Wrap[Int](5) match {
    case Wrap(y) =>
      val res = y;
      res
  };
  ()
}

Here it is a bit different in that we cannot talk about an "annotation" that goes wrong, but the "motif" (the return type of the match).