Type inference for existentials

 - Add existentials to inferred types
 - Map existentials in one compared type to existentials in the other
 - Also: Don't re-analyze existentials in mapCap.

Author: odersky

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

@@ -14,7 +14,7 @@ import printing.{Showable, Printer}
 import printing.Texts.*
 import util.{SimpleIdentitySet, Property}
 import typer.ErrorReporting.Addenda
-import TypeComparer.canSubsumeExistentially
+import TypeComparer.subsumesExistentially
 import util.common.alwaysTrue
 import scala.collection.mutable
 import CCState.*
@@ -173,7 +173,7 @@ sealed abstract class CaptureSet extends Showable:
             x.info match
               case x1: SingletonCaptureRef => x1.subsumes(y)
               case _ => false
-          case x: TermParamRef => canSubsumeExistentially(x, y)
+          case x: TermParamRef => subsumesExistentially(x, y)
           case _ => false
 
   /** {x} <:< this   where <:< is subcapturing, but treating all variables
@@ -498,10 +498,13 @@ object CaptureSet:
       deps = state.deps(this)
 
     final def addThisElem(elem: CaptureRef)(using Context, VarState): CompareResult =
-      if isConst || !recordElemsState() then
-        CompareResult.Fail(this :: Nil) // fail if variable is solved or given VarState is frozen
+      if isConst                                // Fail if variable is solved,
+          || !recordElemsState()                // or given VarState is frozen,
+          || Existential.isBadExistential(elem) // or `elem` is an out-of-scope existential,
+      then
+        CompareResult.Fail(this :: Nil)
       else if !levelOK(elem) then
-        CompareResult.LevelError(this, elem)
+        CompareResult.LevelError(this, elem)    // or `elem` is not visible at the level of the set.
       else
         //if id == 34 then assert(!elem.isUniversalRootCapability)
         assert(elem.isTrackableRef, elem)
@@ -694,19 +697,10 @@ object CaptureSet:
         if cond then propagate else CompareResult.OK
 
       val mapped = extrapolateCaptureRef(elem, tm, variance)
+
       def isFixpoint =
         mapped.isConst && mapped.elems.size == 1 && mapped.elems.contains(elem)
 
-      def addMapped =
-        val added = mapped.elems.filter(!accountsFor(_))
-        addNewElems(added)
-          .andAlso:
-            if mapped.isConst then CompareResult.OK
-            else if mapped.asVar.recordDepsState() then { addAsDependentTo(mapped); CompareResult.OK }
-            else CompareResult.Fail(this :: Nil)
-          .andAlso:
-            propagateIf(!added.isEmpty)
-
       def failNoFixpoint =
         val reason =
           if variance <= 0 then i"the set's variance is $variance"
@@ -716,11 +710,14 @@ object CaptureSet:
         CompareResult.Fail(this :: Nil)
 
       if origin eq source then // elements have to be mapped
-        addMapped
+        val added = mapped.elems.filter(!accountsFor(_))
+        addNewElems(added)
           .andAlso:
             if mapped.isConst then CompareResult.OK
             else if mapped.asVar.recordDepsState() then { addAsDependentTo(mapped); CompareResult.OK }
             else CompareResult.Fail(this :: Nil)
+          .andAlso:
+            propagateIf(!added.isEmpty)
       else if accountsFor(elem) then
         CompareResult.OK
       else if variance > 0 then

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

@@ -9,6 +9,7 @@ import StdNames.nme
 import ast.tpd.*
 import Decorators.*
 import typer.ErrorReporting.errorType
+import Names.TermName
 import NameKinds.ExistentialBinderName
 import NameOps.isImpureFunction
 import reporting.Message
@@ -204,8 +205,10 @@ object Existential:
       case _ => None
 
   /** Create method type in the refinement of an existential type */
-  private def exMethodType(mk: TermParamRef => Type)(using Context): MethodType =
-    val boundName = ExistentialBinderName.fresh()
+  private def exMethodType(using Context)(
+      mk: TermParamRef => Type,
+      boundName: TermName = ExistentialBinderName.fresh()
+    ): MethodType =
     MethodType(boundName :: Nil)(
       mt => defn.Caps_Exists.typeRef :: Nil,
       mt => mk(mt.paramRefs.head))
@@ -332,6 +335,8 @@ object Existential:
         mapFunOrMethod(t, args, res)
       case CapturingType(parent, refs) =>
         t.derivedCapturingType(this(parent), refs)
+      case Existential(_, _) =>
+        t
       case t: (LazyRef | TypeVar) =>
         mapConserveSuper(t)
       case _ =>
@@ -348,4 +353,11 @@ object Existential:
     case ref: TermParamRef => isExistentialMethod(ref.binder)
     case _ => false
 
+  def isBadExistential(ref: CaptureRef) = ref match
+    case ref: TermParamRef => ref.paramName == nme.OOS_EXISTENTIAL
+    case _ => false
+
+  def badExistential(using Context): TermParamRef =
+    exMethodType(identity, nme.OOS_EXISTENTIAL).paramRefs.head
+
 end Existential

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

@@ -262,7 +262,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
       end apply
     end mapInferred
 
-    try mapInferred(refine = true)(tp)
+    try
+      val tp1 = mapInferred(refine = true)(tp)
+      val tp2 = Existential.mapCapInResults(_ => assert(false))(tp1)
+      if tp2 ne tp then capt.println(i"expanded implicit in ${ctx.owner}: $tp  -->  $tp1  -->  $tp2")
+      tp2
     catch case ex: AssertionError =>
       println(i"error while mapping inferred $tp")
       throw ex
@@ -323,7 +327,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
     val tp1 = toCapturing(tp)
     val tp2 = Existential.mapCapInResults(fail)(tp1)
-    if tp2 ne tp then capt.println(i"expanded in ${ctx.owner}: $tp  -->  $tp1  -->  $tp2")
+    if tp2 ne tp then capt.println(i"expanded explicit in ${ctx.owner}: $tp  -->  $tp1  -->  $tp2")
     tp2
   end transformExplicitType
 

compiler/src/dotty/tools/dotc/core/StdNames.scala

@@ -294,6 +294,7 @@ object StdNames {
     val EVT2U: N                    = "evt2u$"
     val EQEQ_LOCAL_VAR: N           = "eqEqTemp$"
     val LAZY_FIELD_OFFSET: N        = "OFFSET$"
+    val OOS_EXISTENTIAL: N          = "<out-of-scope-existential>"
     val OUTER: N                    = "$outer"
     val REFINE_CLASS: N             = "<refinement>"
     val ROOTPKG: N                  = "_root_"

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -11,7 +11,7 @@ import collection.mutable
 import util.{Stats, NoSourcePosition, EqHashMap}
 import config.Config
 import config.Feature.{betterMatchTypeExtractorsEnabled, migrateTo3, sourceVersion}
-import config.Printers.{subtyping, gadts, matchTypes, noPrinter}
+import config.Printers.{subtyping, gadts, matchTypes, capt, noPrinter}
 import config.SourceVersion
 import TypeErasure.{erasedLub, erasedGlb}
 import TypeApplications.*
@@ -47,7 +47,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     GADTused = false
     opaquesUsed = false
     openedExistentials = Nil
-    assocExistentials = Map.empty
+    assocExistentials = Nil
     recCount = 0
     needsGc = false
     if Config.checkTypeComparerReset then checkReset()
@@ -76,7 +76,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
    *  Each existential gets mapped to the opened existentials to which it
    *  may resolve at this point.
    */
-  private var assocExistentials: Map[TermParamRef, List[TermParamRef]] = Map.empty
+  private var assocExistentials: ExAssoc = Nil
 
   private var myInstance: TypeComparer = this
   def currentInstance: TypeComparer = myInstance
@@ -358,7 +358,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         isMatchedByProto(tp2, tp1)
       case tp2: BoundType =>
         tp2 == tp1
-        || existentialVarsConform(tp1, tp2)
         || secondTry
       case tp2: TypeVar =>
         recur(tp1, typeVarInstance(tp2))
@@ -2787,6 +2786,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       false
   }
 
+  // ----------- Capture checking -----------------------------------------------
+
+  /** A type associating instantiatable existentials on the right of a comparison
+   *  with the existentials they can be instantiated with.
+   */
+  type ExAssoc = List[(TermParamRef, List[TermParamRef])]
+
   private def compareExistentialLeft(boundVar: TermParamRef, tp1unpacked: Type, tp2: Type)(using Context): Boolean =
     val saved = openedExistentials
     try
@@ -2798,16 +2804,32 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   private def compareExistentialRight(tp1: Type, boundVar: TermParamRef, tp2unpacked: Type)(using Context): Boolean =
     val saved = assocExistentials
     try
-      assocExistentials = assocExistentials.updated(boundVar, openedExistentials)
+      assocExistentials = (boundVar, openedExistentials) :: assocExistentials
       recur(tp1, tp2unpacked)
     finally
       assocExistentials = saved
 
-  def canSubsumeExistentially(tp1: TermParamRef, tp2: CaptureRef)(using Context): Boolean =
-    Existential.isExistentialVar(tp1)
-      && assocExistentials.get(tp1).match
-        case Some(xs) => !Existential.isExistentialVar(tp2) || xs.contains(tp2)
-        case None => false
+  /** Is `tp1` an existential var that subsumes `tp2`? This is the case if `tp1` is
+   *  instantiatable (i.e. it's a key in `assocExistentials`) and one of the
+   *  following is true:
+   *    - `tp2` is not an existential var,
+   *    - `tp1` is associated via `assocExistentials` with `tp2`,
+   *    - `tp2` appears as key in `assocExistentials` further out than `tp1`.
+   *  The third condition allows to instantiate c2 to c1 in
+   *    EX c1: A -> Ex c2. B
+   */
+  def subsumesExistentially(tp1: TermParamRef, tp2: CaptureRef)(using Context): Boolean =
+    def canInstantiateWith(assoc: ExAssoc): Boolean = assoc match
+      case (bv, bvs) :: assoc1 =>
+        if bv == tp1 then
+          !Existential.isExistentialVar(tp2)
+          || bvs.contains(tp2)
+          || assoc1.exists(_._1 == tp2)
+        else
+          canInstantiateWith(assoc1)
+      case Nil =>
+        false
+    Existential.isExistentialVar(tp1) && canInstantiateWith(assocExistentials)
 
   /** Are tp1, tp2 termRefs that can be linked? This should never be called
    *  normally, since exietential variables appear only in capture sets
@@ -2817,16 +2839,70 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   private def existentialVarsConform(tp1: Type, tp2: Type) =
     tp2 match
       case tp2: TermParamRef => tp1 match
-        case tp1: CaptureRef => canSubsumeExistentially(tp2, tp1)
+        case tp1: CaptureRef => subsumesExistentially(tp2, tp1)
         case _ => false
       case _ => false
 
+  /** bi-map taking existentials to the left of a comparison to matching
+   *  existentials on the right. This is not a bijection. However
+   *  we have `forwards(backwards(bv)) == bv` for an existentially bound `bv`.
+   *  That's enough to qualify as a BiTypeMap.
+   */
+  private class MapExistentials(assoc: ExAssoc)(using Context) extends BiTypeMap:
+
+    private def bad(t: Type) =
+      Existential.badExistential
+        .showing(i"existential match not found for $t in $assoc", capt)
+
+    def apply(t: Type) = t match
+      case t: TermParamRef if Existential.isExistentialVar(t) =>
+        // Find outermost existential on the right that can be instantiated to `t`,
+        // or `badExistential` if none exists.
+        def findMapped(assoc: ExAssoc): CaptureRef = assoc match
+          case (bv, assocBvs) :: assoc1 =>
+            val outer = findMapped(assoc1)
+            if !Existential.isBadExistential(outer) then outer
+            else if assocBvs.contains(t) then bv
+            else bad(t)
+          case Nil =>
+            bad(t)
+        findMapped(assoc)
+      case _ =>
+        mapOver(t)
+
+    /** The inverse takes existentials on the right to the innermost existential
+     *  on the left to which they can be instantiated.
+     */
+    lazy val inverse = new BiTypeMap:
+      def apply(t: Type) = t match
+        case t: TermParamRef if Existential.isExistentialVar(t) =>
+          assoc.find(_._1 == t) match
+            case Some((_, bvs)) if bvs.nonEmpty => bvs.head
+            case _ => bad(t)
+        case _ =>
+          mapOver(t)
+
+        def inverse = MapExistentials.this
+        override def toString = "MapExistentials.inverse"
+    end inverse
+  end MapExistentials
+
   protected def subCaptures(refs1: CaptureSet, refs2: CaptureSet, frozen: Boolean)(using Context): CaptureSet.CompareResult =
-    try refs1.subCaptures(refs2, frozen)
+    try
+      if assocExistentials.isEmpty then
+        refs1.subCaptures(refs2, frozen)
+      else
+        val mapped = refs1.map(MapExistentials(assocExistentials))
+        if mapped.elems.exists(Existential.isBadExistential)
+        then CaptureSet.CompareResult.Fail(refs2 :: Nil)
+        else subCapturesMapped(mapped, refs2, frozen)
     catch case ex: AssertionError =>
       println(i"fail while subCaptures $refs1 <:< $refs2")
       throw ex
 
+  protected def subCapturesMapped(refs1: CaptureSet, refs2: CaptureSet, frozen: Boolean)(using Context): CaptureSet.CompareResult =
+    refs1.subCaptures(refs2, frozen)
+
   /** Is the boxing status of tp1 and tp2 the same, or alternatively, is
    *  the capture sets `refs1` of `tp1` a subcapture of the empty set?
    *  In the latter case, boxing status does not matter.
@@ -3291,9 +3367,6 @@ object TypeComparer {
   def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false, isSoft: Boolean = true)(using Context): Type =
     comparing(_.lub(tp1, tp2, canConstrain = canConstrain, isSoft = isSoft))
 
-  def canSubsumeExistentially(tp1: TermParamRef, tp2: CaptureRef)(using Context) =
-    comparing(_.canSubsumeExistentially(tp1, tp2))
-
   /** The least upper bound of a list of types */
   final def lub(tps: List[Type])(using Context): Type =
     tps.foldLeft(defn.NothingType: Type)(lub(_,_))
@@ -3366,6 +3439,9 @@ object TypeComparer {
 
   def subCaptures(refs1: CaptureSet, refs2: CaptureSet, frozen: Boolean)(using Context): CaptureSet.CompareResult =
     comparing(_.subCaptures(refs1, refs2, frozen))
+
+  def subsumesExistentially(tp1: TermParamRef, tp2: CaptureRef)(using Context) =
+    comparing(_.subsumesExistentially(tp1, tp2))
 }
 
 object MatchReducer:
@@ -3881,5 +3957,10 @@ class ExplainingTypeComparer(initctx: Context, short: Boolean) extends TypeCompa
       super.subCaptures(refs1, refs2, frozen)
     }
 
+  override def subCapturesMapped(refs1: CaptureSet, refs2: CaptureSet, frozen: Boolean)(using Context): CaptureSet.CompareResult =
+    traceIndented(i"subcaptures mapped $refs1 <:< $refs2 ${if frozen then "frozen" else ""}") {
+      super.subCapturesMapped(refs1, refs2, frozen)
+    }
+
   def lastTrace(header: String): String = header + { try b.toString finally b.clear() }
 }

tests/neg-custom-args/captures/heal-tparam-cs.scala

@@ -11,12 +11,12 @@ def main(io: Capp^, net: Capp^): Unit = {
   }
 
   val test2: (c: Capp^) -> () => Unit =
-    localCap { c =>  // should work
+    localCap { c =>  // error
       (c1: Capp^) => () => { c1.use() }
     }
 
   val test3: (c: Capp^{io}) -> () ->{io} Unit =
-    localCap { c =>  // should work
+    localCap { c =>  // error
       (c1: Capp^{io}) => () => { c1.use() }
     }
 

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

@@ -2,9 +2,9 @@
 8 |  ps.map((x, y) => compose1(x, y)) // error // error
   |          ^
   |reference (ps : List[(box A => A, box A => A)]) @reachCapability is not included in the allowed capture set {}
-  |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
+  |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? (ex$15: caps.Exists) -> A^?
 -- Error: tests/neg-custom-args/captures/reaches2.scala:8:13 -----------------------------------------------------------
 8 |  ps.map((x, y) => compose1(x, y)) // error // error
   |             ^
   |reference (ps : List[(box A => A, box A => A)]) @reachCapability is not included in the allowed capture set {}
-  |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
+  |of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? (ex$15: caps.Exists) -> A^?