Open
Description
effect throw[A](x: A): Nothing
def f[A]() = {
def left(x: A): Unit / throw[A] = do throw(x)
def right { f: => Unit / throw[A] } =
try { f(); None() } with throw[A] { x => Some(x) }
(box left, box right)
}
def upcast[A](x: A): Any = x
def main(): Unit = {
def block(): Unit / throw[Any] = (unbox f[Any]().first)(42.upcast)
val r = (unbox f[Any].second) { () => block() }
// ^^^^^^^^^^^^^^^^^
// Effects need to be fully known, but effect throw[A]'s type parameter(s) A could not be inferred. Maybe try annotating them?
inspect(r)
}
When I try to be more specific:
def apply { g: => Unit / throw[Any] } = (unbox f[Any].second) {g}
// Cannot fully infer type for apply: {() => Unit / { throw[Any] }} => Option[A]
This error is especially weird, do we not propagate the result of the substitution somewhere?
I have to ascribe the Option[Any]
return type here for it to work...
Only then the program starts working (here's the playground link)