Make subsitution performed by instantiate more eager

effekt-lang · Jan 20, 2024 · f7b0250 · f7b0250
1 parent f4d8688
commit f7b0250
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 7 deletions.
diff --git a/effekt/shared/src/main/scala/effekt/Namer.scala b/effekt/shared/src/main/scala/effekt/Namer.scala
@@ -288,18 +288,22 @@ object Namer extends Phase[Parsed, NameResolved] {
           val name = Context.nameFor(id)
 
           Context scoped {
-            // the parameters of the effect are in scope
+            // the parameters of the interface are in scope
             effectSym.tparams.foreach { p => Context.bind(p) }
 
             val tps = tparams map resolve
 
+            val resVparams = vparams map resolve
+            val resBparams = bparams map resolve
+
+            // bring capture names in scope that are introduced by blockparameters
+            resBparams.map { b => Context.bind(b.capture) }
+
             // The type parameters of an effect op are:
             //   1) all type parameters on the effect, followed by
             //   2) the annotated type parameters on the concrete operation
             val (result, effects) = resolve(ret)
-
-            val resVparams = vparams map resolve
-            val resBparams = bparams map resolve
+
             val op = Operation(name, effectSym.tparams ++ tps, resVparams, resBparams, result, effects, effectSym)
             Context.define(id, op)
             op

diff --git a/effekt/shared/src/main/scala/effekt/typer/Unification.scala b/effekt/shared/src/main/scala/effekt/typer/Unification.scala
@@ -256,7 +256,7 @@ class Unification(using C: ErrorReporter) extends TypeUnifier, TypeMerger, TypeI
     case (x: CaptUnificationVar, y: CaptUnificationVar, p) => mergeCaptures(Nil, List(x, y), ctx)
   }
 
-  def mergeCaptures(cs: List[Captures], ctx: ErrorContext): CaptUnificationVar =
+  def mergeCaptures(cs: List[Captures], ctx: ErrorContext): Captures =
     val (concrete, variables) = cs.partitionMap {
       case CaptureSet(xs) => Left(xs)
       case x: CaptUnificationVar => Right(x)
@@ -266,7 +266,10 @@ class Unification(using C: ErrorReporter) extends TypeUnifier, TypeMerger, TypeI
    /**
    * Should create a fresh unification variable bounded by the given captures
    */
-  def mergeCaptures(concreteBounds: List[Capture], variableBounds: List[CaptUnificationVar], ctx: ErrorContext): CaptUnificationVar =
+  def mergeCaptures(concreteBounds: List[Capture], variableBounds: List[CaptUnificationVar], ctx: ErrorContext): Captures =
+    // do not introduce a unification variable if there are ONLY concrete bounds
+    if (variableBounds.isEmpty) return CaptureSet(concreteBounds)
+
     val newVar = freshCaptVar(CaptUnificationVar.Substitution())
     ctx.polarity match {
       case Covariant =>
@@ -320,7 +323,7 @@ trait TypeInstantiator { self: Unification =>
           capt.captures
     }
     val contained = captureParams intersect concreteCapture // Should not contain CaptureOf
-    if (contained.isEmpty) return c;
+    if (contained.isEmpty) return CaptureSet(concreteCapture)
 
     val remaining = (concreteCapture -- captureParams).toList