Unify existentials when matching function types

Author: odersky

compiler/src/dotty/tools/dotc/cc/CaptureRef.scala

@@ -258,10 +258,12 @@ trait CaptureRef extends TypeProxy, ValueType:
         vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
         || !y.stripReadOnly.isCap && !yIsExistential && canAddHidden && vs.addHidden(hidden, y)
       case x @ root.Result(binder) =>
-        if y.derivesFromSharedCapability then true
-        else
+        val result = y match
+          case y @ root.Result(_) => vs.unify(x, y)
+          case _ => y.derivesFromSharedCapability
+        if !result then
           ccState.addNote(CaptureSet.ExistentialSubsumesFailure(x, y))
-          false
+        result
       case _ =>
         y match
           case ReadOnlyCapability(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden)

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

@@ -1102,6 +1102,14 @@ object CaptureSet:
     /** A map from captureset variables to their dependent sets at the time of the snapshot. */
     private val depsMap: util.EqHashMap[Var, Deps] = new util.EqHashMap
 
+    /** A map from root.Result values to other such values. If two result values
+     *  `a` and `b` are unified, then `eqResultMap(a) = b` and `eqResultMap(b) = a`.
+     */
+    private var eqResultMap: util.SimpleIdentityMap[root.Result, root.Result] = util.SimpleIdentityMap.empty
+
+    /** A snapshot of the `eqResultMap` value at the start of a VarState transaction */
+    private var eqResultSnapshot: util.SimpleIdentityMap[root.Result, root.Result] | Null = null
+
     /** The recorded elements of `v` (it's required that a recording was made) */
     def elems(v: Var): Refs = elemsMap(v)
 
@@ -1141,10 +1149,31 @@ object CaptureSet:
       hidden.add(elem)(using ctx, this)
       true
 
+    /** If root1 and root2 belong to the same binder but have different originalBinders
+     *  it means that one of the roots was mapped to the binder of the other by a
+     *  substBinder when comparing two method types. In that case we can unify
+     *  the two roots1, provided none of the two roots have already been unified
+     *  themselves. So unification must be 1-1.
+     */
+    def unify(root1: root.Result, root2: root.Result)(using Context): Boolean =
+      (root1, root2) match
+        case (root1 @ root.Result(binder1), root2 @ root.Result(binder2))
+        if (binder1 eq binder2)
+          && (root1.rootAnnot.originalBinder ne root2.rootAnnot.originalBinder)
+          && eqResultMap(root1) == null
+          && eqResultMap(root2) == null
+        =>
+          if eqResultSnapshot == null then eqResultSnapshot = eqResultMap
+          eqResultMap = eqResultMap.updated(root1, root2).updated(root2, root1)
+          true
+        case _ =>
+          false
+
     /** Roll back global state to what was recorded in this VarState */
     def rollBack(): Unit =
       elemsMap.keysIterator.foreach(_.resetElems()(using this))
       depsMap.keysIterator.foreach(_.resetDeps()(using this))
+      if eqResultSnapshot != null then eqResultMap = eqResultSnapshot.nn
 
     private var seen: util.EqHashSet[CaptureRef] = new util.EqHashSet
 

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -1255,8 +1255,11 @@ class CheckCaptures extends Recheck, SymTransformer:
                 i"""reference ${ref}$levelStr
                   |cannot be included in outer capture set $cs"""
             case ExistentialSubsumesFailure(ex, other) =>
+              def since =
+                if other.isRootCapability then ""
+                else " since that capability is not a SharedCapability"
               i"""the existential capture root in ${ex.rootAnnot.originalBinder.resType}
-                |cannot subsume the capability $other"""
+                |cannot subsume the capability $other$since"""
           i"""
              |
              |Note that ${msg.toString}"""

tests/neg-custom-args/captures/erased-methods2.check

@@ -5,7 +5,7 @@
    |    Required: (erased x$1: CT[Ex3]^) ?->{fresh} (erased x$2: CT[Ex2]^) ?->{localcap} Unit
    |
    |    Note that the existential capture root in (erased x$2: CT[Ex2]^) ?=> Unit
-   |    cannot subsume the capability x$1.type
+   |    cannot subsume the capability x$1.type since that capability is not a SharedCapability
 21 |     ?=> (x$2: CT[Ex2]^)
 22 |     ?=>
 23 |      //given (CT[Ex3]^) = x$1
@@ -19,7 +19,7 @@
    |Required: (erased x$1: CT[Ex3]^) ?->{fresh} (erased x$1: CT[Ex2]^) ?->{localcap} (erased x$2: CT[Ex1]^) ?->{localcap} Unit
    |
    |Note that the existential capture root in (erased x$1: CT[Ex2]^) ?=> (erased x$2: CT[Ex1]^) ?->{localcap} Unit
-   |cannot subsume the capability x$1.type
+   |cannot subsume the capability x$1.type since that capability is not a SharedCapability
 32 |     ?=> (erased x$2: CT[Ex2]^)
 33 |     ?=> (erased x$3: CT[Ex1]^)
 34 |     ?=> Throw(new Ex3)

tests/neg-custom-args/captures/reaches.check

@@ -56,11 +56,11 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:67:32 --------------------------------------
 67 |  val id: (x: File^) -> File^ = x => x // error
    |                                ^^^^^^
-   |                                Found:    (x: File^) ->? File^{x}
-   |                                Required: (x: File^) -> File^{localcap}
+   |                            Found:    (x: File^) ->? File^{x}
+   |                            Required: (x: File^) -> File^{localcap}
    |
-   |                                Note that the existential capture root in File^
-   |                                cannot subsume the capability x.type
+   |                            Note that the existential capture root in File^
+   |                            cannot subsume the capability x.type since that capability is not a SharedCapability
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:70:38 --------------------------------------

tests/neg-custom-args/captures/scoped-caps.scala

@@ -0,0 +1,28 @@
+class A
+class B
+class S extends caps.SharedCapability
+
+def test(io: Object^): Unit =
+  val f: (x: A^) -> B^ = ???
+  val g: A^ -> B^ = f // error
+  val _: (y: A^) -> B^ = f
+  val _: (x: A^) -> B^ = g // error
+  val _: A^ -> B^ = f // error
+  val _: A^ -> B^ = g
+  val _: A^ -> B^ = x => g(x)      // should be error, since g is pure, g(x): B^{x} , which does not match B^{fresh}
+  val _: (x: A^) -> B^ = x => f(x) // error: existential in B cannot subsume `x` since `x` is not shared
+
+  val h: S -> B^ = ???
+  val _: (x: S) -> B^ = h          // error: direct conversion fails
+  val _: (x: S) -> B^ = x => h(x)  // but eta expansion succeeds (for SharedCapabilities)
+
+  val j: (x: S) -> B^ = ???
+  val _: (x: S) -> B^ = j
+  val _: (x: S) -> B^ = x => j(x)
+  val _: S -> B^ = j               // error
+  val _: S -> B^ = x => j(x)       // should be error
+
+  val g2: A^ => B^ = ???
+  val _: A^ => B^ = x => g2(x)  // should be error: g2(x): B^{g2, x}, and the `x` cannot be subsumed by fresh
+  val g3: A^ => B^ = ???
+  val _: A^{io} => B^ = x => g3(x)  // ok, now g3(x): B^{g3, x}, which is widened to B^{g3, io}