Skip to content

Commit

Permalink
Fix #661 by improving type inference (#662)
Browse files Browse the repository at this point in the history
We now order block arguments to first type check those that do not
subtract effects. This hopefully gives enough info about type arguments
to uniquely determine effects of other block arguments.
  • Loading branch information
b-studios authored Nov 3, 2024
1 parent 6e71bcd commit 19b36bf
Show file tree
Hide file tree
Showing 3 changed files with 36 additions and 3 deletions.
15 changes: 12 additions & 3 deletions effekt/shared/src/main/scala/effekt/Typer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1198,10 +1198,10 @@ object Typer extends Phase[NameResolved, Typechecked] {
Context.abort(s"Wrong number of type arguments, given ${targs.size}, but ${name} expects ${funTpe.tparams.size}.")

if (vargs.size != funTpe.vparams.size)
Context.error(s"Wrong number of value arguments, given ${vargs.size}, but ${name} expects ${funTpe.vparams.size}.")
Context.abort(s"Wrong number of value arguments, given ${vargs.size}, but ${name} expects ${funTpe.vparams.size}.")

if (bargs.size != funTpe.bparams.size)
Context.error(s"Wrong number of block arguments, given ${bargs.size}, but ${name} expects ${funTpe.bparams.size}.")
Context.abort(s"Wrong number of block arguments, given ${bargs.size}, but ${name} expects ${funTpe.bparams.size}.")

val callsite = currentCapture

Expand All @@ -1222,7 +1222,16 @@ object Typer extends Phase[NameResolved, Typechecked] {
effs = effs ++ eff
}

(bps zip bargs zip captArgs) foreach { case ((tpe, expr), capt) =>
// To improve inference, we first type check block arguments that DO NOT subtract effects,
// since those need to be fully known.

val (withoutEffects, withEffects) = (bps zip (bargs zip captArgs)).partitionMap {
// TODO refine and check that eff.args refers to (inferred) type arguments of this application (`typeArgs`)
case (tpe : FunctionType, rest) if tpe.effects.exists { eff => eff.args.nonEmpty } => Right((tpe, rest))
case (tpe, rest) => Left((tpe, rest))
}

(withoutEffects ++ withEffects) foreach { case (tpe, (expr, capt)) =>
flowsInto(capt, callsite)
// capture of block <: ?C
flowingInto(capt) {
Expand Down
3 changes: 3 additions & 0 deletions examples/pos/issue661.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
2
3
4
21 changes: 21 additions & 0 deletions examples/pos/issue661.effekt
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
interface Iter[T] {
def yield(value: T): Unit
}

def iter[T](self: List[T]): Unit / {Iter[T]} =
self match {
case Cons(head, tail) => do yield(head); iter(tail)
case Nil() => ()
}

def my_map[T, U] {action: () => Unit / {Iter[T]}} {f: T => U}: Unit / {Iter[U]} =
try action()
with Iter[T] {
def yield(value) = { do yield(f(value)); resume(()) }
}

def main() =
try my_map { iter([1, 2, 3]) } { x => x+1 }
with Iter[Int] {
def yield(x) = { println(x); resume(()) }
}

0 comments on commit 19b36bf

Please sign in to comment.