Open expected and actual existentials (draft)

Author: odersky

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

@@ -696,6 +696,13 @@ class CheckCaptures extends Recheck, SymTransformer:
             interpolateVarsIn(tree.tpt)
           curEnv = saved
 
+    override def recheckRHS(rhs: Tree, pt: Type)(using Context): Type =
+      def avoidMap = new TypeOps.AvoidMap:
+        def toAvoid(tp: NamedType) =
+          tp.isTerm && tp.symbol.owner == ctx.owner && !tp.symbol.is(Param)
+      val tp = recheck(rhs, pt)
+      if ctx.owner.is(Method) then avoidMap(tp) else tp
+
     /** If val or def definition with inferred (result) type is visible
      *  in other compilation units, check that the actual inferred type
      *  conforms to the expected type where all inferred capture sets are dropped.
@@ -812,7 +819,8 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  Otherwise, if the result type is boxed, simulate an unboxing by
      *  adding all references in the boxed capture set to the current environment.
      */
-    override def recheck(tree: Tree, pt: Type = WildcardType)(using Context): Type =
+    override def recheck(tree: Tree, pt0: Type = WildcardType)(using Context): Type =
+      val pt = Existential.openExpected(pt0)
       val saved = curEnv
       tree match
         case _: RefTree | closureDef(_) if pt.isBoxedCapturing =>
@@ -878,23 +886,24 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  where local capture roots are instantiated to root variables.
      */
     override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Type =
-      var expected1 = alignDependentFunction(expected, actual.stripCapturing)
-      val actualBoxed = adaptBoxed(actual, expected1, tree.srcPos)
+      val actualUnpacked = Existential.skolemize(actual)
+      var expected1 = alignDependentFunction(expected, actualUnpacked.stripCapturing)
+      val actualBoxed = adaptBoxed(actualUnpacked, expected1, tree.srcPos)
       //println(i"check conforms $actualBoxed <<< $expected1")
 
-      if actualBoxed eq actual then
+      if actualBoxed eq actualUnpacked then
         // Only `addOuterRefs` when there is no box adaptation
-        expected1 = addOuterRefs(expected1, actual)
+        expected1 = addOuterRefs(expected1, actualUnpacked)
       if isCompatible(actualBoxed, expected1) then
         if debugSuccesses then tree match
             case Ident(_) =>
-              println(i"SUCCESS $tree:\n${TypeComparer.explained(_.isSubType(actual, expected))}")
+              println(i"SUCCESS $tree:\n${TypeComparer.explained(_.isSubType(actualUnpacked, expected))}")
             case _ =>
         actualBoxed
       else
         capt.println(i"conforms failed for ${tree}: $actual vs $expected")
         err.typeMismatch(tree.withType(actualBoxed), expected1, addenda ++ CaptureSet.levelErrors)
-        actual
+        actualUnpacked
     end checkConformsExpr
 
     /** Turn `expected` into a dependent function when `actual` is dependent. */
@@ -1121,7 +1130,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       /** If result derives from caps.Capability, yet is not a capturing type itself,
        *  make its capture set explicit.
        */
-      def makeCaptureSetExplicit(result: Type) = result match
+      def makeCaptureSetExplicit(actual: Type, result: Type) = result match
         case CapturingType(_, _) => result
         case _ =>
           if result.derivesFromCapability then
@@ -1147,16 +1156,17 @@ class CheckCaptures extends Recheck, SymTransformer:
               case _ =>
           case _ =>
         val adapted = adapt(actualw.withReachCaptures(actual), expected, covariant = true)
-        makeCaptureSetExplicit:
+        makeCaptureSetExplicit(actual,
           if adapted ne actualw then
             capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
             adapted
           else
-            actual
+            actual)
     end adaptBoxed
 
     /** Check overrides again, taking capture sets into account.
     *  TODO: Can we avoid doing overrides checks twice?
+    *
     *  We need to do them here since only at this phase CaptureTypes are relevant
     *  But maybe we can then elide the check during the RefChecks phase under captureChecking?
     */
@@ -1167,12 +1177,12 @@ class CheckCaptures extends Recheck, SymTransformer:
         *  @param sym  symbol of the field definition that is being checked
         */
         override def checkSubType(actual: Type, expected: Type)(using Context): Boolean =
-          val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing)
+          val expected1 = alignDependentFunction(addOuterRefs(Existential.strip(expected), actual), actual.stripCapturing)
           val actual1 =
             val saved = curEnv
             try
               curEnv = Env(clazz, EnvKind.NestedInOwner, capturedVars(clazz), outer0 = curEnv)
-              val adapted = adaptBoxed(actual, expected1, srcPos, alwaysConst = true)
+              val adapted = adaptBoxed(Existential.strip(actual), expected1, srcPos, alwaysConst = true)
               actual match
                 case _: MethodType =>
                   // We remove the capture set resulted from box adaptation for method types,

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 NameKinds.exSkolemName
 
 /**
 
@@ -23,7 +24,7 @@ In adapt:
         method as owner, and use its termRef
     Then,
       + If the EX-bound variable appears only at toplevel, replace it with `x`
-      + Otherwise, replace it with a fresh reach capability `x*`.
+      + Otherwise, replace it with `x*`.
 
 In avoidance of a type T:
 
@@ -145,6 +146,21 @@ Existential source syntax:
     - The type of a type ascription in an expression or pattern
     - The argument and result types of a function.
 
+  Restrictions on Existential Types:
+
+    - An existential capture ref must be the only member of its set. This is
+      intended to model the idea that existential variables effectibely range
+      over capture sets, not capture references. But so far out calculus
+      and implementation does not yet acoommodate first-class capture sets.
+    - Existential capture refs must appear co-variantly in their bound type
+
+  So the following would all be illegal:
+
+      EX x.C^{x, io}            // error: multiple members
+      EX x.() => EX y.C^{x, y}  // error: multiple members
+      EX x.C^{x} ->{x} D        // error: contra-variant occurrence
+      EX x.Set[C^{x}]           // error: invariant occurrence
+
 Expansion of ^:
 
   We drop `cap` as a capture reference, but keep the unqualified `^` syntax.
@@ -188,6 +204,55 @@ Expansion of ^:
 */
 object Existential:
 
+  type Carrier = RefinedType
+
+  def openExpected(pt: Type)(using Context): Type = pt.dealias match
+    case Existential(boundVar, unpacked) =>
+      val tm = new IdempotentCaptRefMap:
+        val cvar = CaptureSet.Var(ctx.owner)
+        def apply(t: Type) = mapOver(t) match
+          case t @ CapturingType(parent, refs) if refs.elems.contains(boundVar) =>
+            assert(refs.isConst && refs.elems.size == 1, i"malformed existential $t")
+            t.derivedCapturingType(parent, cvar)
+          case t =>
+            t
+      openExpected(tm(unpacked))
+    case _ => pt
+
+  def strip(tp: Type)(using Context) = tp match
+    case Existential(_, tpunpacked) => tpunpacked
+    case _ => tp
+
+  def skolemize(tp: Type)(using Context) = tp.widenDealias match
+    case Existential(boundVar, unpacked) =>
+      val skolem = tp match
+        case tp: CaptureRef if tp.isTracked => tp
+        case _ => newSkolemSym(boundVar.underlying).termRef
+      val tm = new IdempotentCaptRefMap:
+        var deep = false
+        private inline def deepApply(t: Type): Type =
+          val saved = deep
+          deep = true
+          try apply(t) finally deep = saved
+        def apply(t: Type) =
+          if t eq boundVar then
+            if deep then skolem.reach else skolem
+          else t match
+            case defn.FunctionOf(args, res, contextual) =>
+              val res1 = deepApply(res)
+              if res1 ne res then defn.FunctionOf(args, res1, contextual)
+              else t
+            case defn.RefinedFunctionOf(mt) =>
+              mt.derivedLambdaType(resType = deepApply(mt.resType))
+            case _ =>
+              mapOver(t)
+      tm(unpacked)
+    case _ => tp
+  end skolemize
+
+  def newSkolemSym(tp: Type)(using Context): TermSymbol =
+    newSymbol(ctx.owner.enclosingMethodOrClass, exSkolemName.fresh(), Synthetic, tp)
+/*
   def fromDepFun(arg: Tree)(using Context): Type = arg.tpe match
     case RefinedType(parent, nme.apply, info: MethodType) if defn.isNonRefinedFunction(parent) =>
       info match
@@ -198,13 +263,7 @@ object Existential:
           errorType(em"Malformed existential: dependent function must have a singgle parameter of type caps.Capability", arg.srcPos)
     case _ =>
       errorType(em"Malformed existential: dependent function type expected", arg.srcPos)
-
-  def apply(fn: TermRef => Type)(using Context): RecType =
-    RecType(rt => fn(exBoundRef(rt)))
-
-  def exBoundRef(rt: RecType)(using Context): TermRef =
-    TermRef(rt.recThis, defn.captureRoot)
-
+*/
   private class PackMap(sym: Symbol, rt: RecType)(using Context) extends DeepTypeMap, IdempotentCaptRefMap:
     def apply(tp: Type): Type = tp match
       case ref: TermRef if ref.symbol == sym => TermRef(rt.recThis, defn.captureRoot)
@@ -235,7 +294,7 @@ object Existential:
     case (info: TypeRef) :: rest => info.symbol == defn.Caps_Exists && rest.isEmpty
     case _ => false
 
-  def unapply(tp: RefinedType)(using Context): Option[(TermParamRef, Type)] =
+  def unapply(tp: Carrier)(using Context): Option[(TermParamRef, Type)] =
     tp.refinedInfo match
       case mt: MethodType
       if isExistentialMethod(mt) && defn.isNonRefinedFunction(tp.parent) =>

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

@@ -237,6 +237,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
             val rinfo1 = apply(rinfo)
             if rinfo1 ne rinfo then rinfo1.toFunctionType(alwaysDependent = true)
             else tp
+          case Existential(_, unpacked) =>
+            apply(unpacked)
           case tp: MethodType =>
             tp.derivedLambdaType(
               paramInfos = mapNested(tp.paramInfos),
@@ -252,7 +254,10 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
       end apply
     end mapInferred
 
-    mapInferred(refine = true)(tp)
+    try mapInferred(refine = true)(tp)
+    catch case ex: AssertionError =>
+      println(i"error while maop inferred $tp")
+      throw ex
   end transformInferredType
 
   private def transformExplicitType(tp: Type, tptToCheck: Option[Tree] = None)(using Context): Type =

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

@@ -332,6 +332,7 @@ object NameKinds {
   val InlineScrutineeName: UniqueNameKind    = new UniqueNameKind("$scrutinee")
   val InlineBinderName: UniqueNameKind       = new UniqueNameKind("$proxy")
   val MacroNames: UniqueNameKind             = new UniqueNameKind("$macro$")
+  val exSkolemName: UniqueNameKind           = new UniqueNameKind("$exSkolem")
 
   val UniqueExtMethName: UniqueNameKind = new UniqueNameKindWithUnmangle("$extension")
 

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

@@ -3318,7 +3318,12 @@ object Types extends TypeUtils {
     private def badInst =
       throw new AssertionError(s"bad instantiation: $this")
 
-    def checkInst(using Context): this.type = this // debug hook
+    def checkInst(using Context): this.type =
+      if refinedName == nme.apply then
+        parent.dealias.stripAnnots match
+          case RefinedType(_, nme.apply, _) => assert(false, this) // debug hook
+          case _ =>
+      this
 
     final def derivedRefinedType
         (parent: Type = this.parent, refinedName: Name = this.refinedName, refinedInfo: Type = this.refinedInfo)

compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala

@@ -564,7 +564,9 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       case SingletonTypeTree(ref) =>
         toTextLocal(ref) ~ "." ~ keywordStr("type")
       case RefinedTypeTree(tpt, refines) =>
-        toTextLocal(tpt) ~ " " ~ blockText(refines)
+        if defn.isFunctionSymbol(tpt.symbol) && tree.hasType && !printDebug
+        then changePrec(GlobalPrec) { toText(tree.typeOpt) }
+        else toTextLocal(tpt) ~ blockText(refines)
       case AppliedTypeTree(tpt, args) =>
         if (tpt.symbol == defn.orType && args.length == 2)
           changePrec(OrTypePrec) { toText(args(0)) ~ " | " ~ atPrec(OrTypePrec + 1) { toText(args(1)) } }

compiler/src/dotty/tools/dotc/transform/Recheck.scala

@@ -249,14 +249,16 @@ abstract class Recheck extends Phase, SymTransformer:
     def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Type =
       val resType = recheck(tree.tpt)
       if tree.rhs.isEmpty then resType
-      else recheck(tree.rhs, resType)
+      else recheckRHS(tree.rhs, resType)
 
     def recheckDefDef(tree: DefDef, sym: Symbol)(using Context): Type =
       inContext(linkConstructorParams(sym).withOwner(sym)):
         val resType = recheck(tree.tpt)
         if tree.rhs.isEmpty || sym.isInlineMethod || sym.isEffectivelyErased
         then resType
-        else recheck(tree.rhs, resType)
+        else recheckRHS(tree.rhs, resType)
+
+    def recheckRHS(rhs: Tree, pt: Type)(using Context): Type = recheck(rhs, pt)
 
     def recheckTypeDef(tree: TypeDef, sym: Symbol)(using Context): Type =
       recheck(tree.rhs)

tests/neg/cc-existentials.scala renamed to tests/neg/cc-ex-conformance.scala

@@ -3,13 +3,13 @@ import caps.{Exists, Capability}
 
 class C
 
-type EX1 = (c: Exists) => (C^{c}, C^{c})
+type EX1 = () => (c: Exists) => (C^{c}, C^{c})
 
-type EX2 = (c1: Exists) => (c2: Exists) => (C^{c1}, C^{c2})
+type EX2 = () => (c1: Exists) => (c2: Exists) => (C^{c1}, C^{c2})
 
-type EX3 = (c: Exists) => () => C^{c}
+type EX3 = () => (c: Exists) => () => C^{c}
 
-type EX4 = () => (c: Exists) => C^{c}
+type EX4 = () => () => (c: Exists) => C^{c}
 
 def Test =
   val ex1: EX1 = ???

tests/pos/cc-ex-unpack.scala

@@ -0,0 +1,18 @@
+import language.experimental.captureChecking
+import caps.{Exists, Capability}
+
+class C
+
+type EX1 = (c: Exists) -> (C^{c}, C^{c})
+
+type EX2 = () -> (c1: Exists) -> (c2: Exists) -> (C^{c1}, C^{c2})
+
+type EX3 = () -> (c: Exists) -> () -> C^{c}
+
+type EX4 = () -> () -> (c: Exists) -> C^{c}
+
+def Test =
+  def f =
+    val ex1: EX1 = ???
+    val c1 = ex1
+    c1