Handle existential types in subtyping

An existential type is represented as

    <typelambda> [ wildcard-args ]

This commit makes subtyping between such types work as
intended.

Author: odersky

src/dotty/tools/dotc/core/ConstraintHandling.scala

@@ -32,7 +32,11 @@ trait ConstraintHandling {
 
   private var addConstraintInvocations = 0
 
-  private var needsCleanup = false
+  /** Does `constraint` contain parameters that are instantiated but
+   *  that have not yet been checked for removal? In that case we should
+   *  remove them when we are at a top-level subtype check.
+   */
+  private var hasInstantiations = false
 
   /** If the constraint is frozen we cannot add new bounds to the constraint. */
   protected var frozenConstraint = false
@@ -115,7 +119,7 @@ trait ConstraintHandling {
     constr.println(s"unifying $p1 $p2")
     val down = constraint.exclusiveLower(p2, p1)
     val up = constraint.exclusiveUpper(p1, p2)
-    needsCleanup = true
+    hasInstantiations = true
     constraint = constraint.unify(p1, p2)
     val bounds = constraint.nonParamBounds(p1)
     val lo = bounds.lo
@@ -176,6 +180,83 @@ trait ConstraintHandling {
     inst
   }
 
+  /** The instance type of `param` in the current constraint (which contains `param`).
+   *  `fromBelow` is true, the isntance type is the lub of the parameter's
+   *  lower bounds; otherwise it is the glb of its upper bounds. However,
+   *  a lower bound instantiation can be a singleton type only if the upper bound
+   *  is also a singleton type.
+   */
+  def instanceType(param: PolyParam, fromBelow: Boolean): Type = {
+    def upperBound = ctx.typerState.constraint.fullUpperBound(param)
+    def isSingleton(tp: Type): Boolean = tp match {
+      case tp: SingletonType => true
+      case AndType(tp1, tp2) => isSingleton(tp1) | isSingleton(tp2)
+      case OrType(tp1, tp2) => isSingleton(tp1) & isSingleton(tp2)
+      case _ => false
+    }
+    def isFullyDefined(tp: Type): Boolean = tp match {
+      case tp: TypeVar => tp.isInstantiated && isFullyDefined(tp.instanceOpt)
+      case tp: TypeProxy => isFullyDefined(tp.underlying)
+      case tp: AndOrType => isFullyDefined(tp.tp1) && isFullyDefined(tp.tp2)
+      case _ => true
+    }
+    def isOrType(tp: Type): Boolean = tp.stripTypeVar.dealias match {
+      case tp: OrType => true
+      case tp: RefinedOrRecType => isOrType(tp.parent)
+      case AndType(tp1, tp2) => isOrType(tp1) | isOrType(tp2)
+      case WildcardType(bounds: TypeBounds) => isOrType(bounds.hi)
+      case _ => false
+    }
+
+    // First, solve the constraint.
+    var inst = approximation(param, fromBelow)
+
+    // Then, approximate by (1.) - (3.) and simplify as follows.
+    // 1. If instance is from below and is a singleton type, yet
+    // upper bound is not a singleton type, widen the instance.
+    if (fromBelow && isSingleton(inst) && !isSingleton(upperBound))
+      inst = inst.widen
+
+    inst = inst.simplified
+
+    // 2. If instance is from below and is a fully-defined union type, yet upper bound
+    // is not a union type, approximate the union type from above by an intersection
+    // of all common base types.
+    if (fromBelow && isOrType(inst) && isFullyDefined(inst) && !isOrType(upperBound))
+      inst = inst.approximateUnion
+
+    // 3. If instance is from below, and upper bound has open named parameters
+    //    make sure the instance has all named parameters of the bound.
+    if (fromBelow) inst = inst.widenToNamedTypeParams(param.namedTypeParams)
+
+    if (ctx.typerState.isGlobalCommittable)
+      assert(!inst.isInstanceOf[PolyParam], i"bad inst $this := $inst, constr = ${ctx.typerState.constraint}")
+    // If this fails, you might want to turn on Config.debugCheckConstraintsClosed
+    // to help find the root of the problem.
+    inst
+  }
+
+  def instantiateLambdaParam(param: PolyParam, variance: Int): Type = {
+    val inst = instanceType(param, fromBelow = variance >= 0)
+    hk.println(i"remove type lambda param $param with inst = $inst in $constraint")
+    constraint = constraint.replace(param, inst, canRemove = true)
+    inst
+  }
+
+  /*
+  def dropConstrainedLambdas() =
+    if (hasConstrainedLambdas) {
+      constraint.domainPolys.foreach {
+        case tl: TypeLambda =>
+          tl.paramRefs.foreach { param =>
+            if (constraint.contains(param)) instantiateLambdaParam(param, 0)
+          }
+        case _ =>
+      }
+      hasConstrainedLambdas = false
+    }
+*/
+
   /** Constraint `c1` subsumes constraint `c2`, if under `c2` as constraint we have
    *  for all poly params `p` defined in `c2` as `p >: L2 <: U2`:
    *
@@ -320,13 +401,21 @@ trait ConstraintHandling {
     constraint =
       if (addConstraint(param, tp, fromBelow = true) &&
           addConstraint(param, tp, fromBelow = false)) {
-        needsCleanup = true
+        hasInstantiations = true
         constraint.replace(param, tp, canRemove = false)
       }
       else saved
     constraint ne saved
   }
 
+  /** A new constraint with all polytypes that only have instantiated parameters removed */
+  protected def cleanupConstraint() =
+    if (hasInstantiations) {
+      constraint =
+        (constraint /: constraint.domainPolys.filter(constraint.isRemovable(_)))(_.remove(_))
+      hasInstantiations = false
+    }
+
   /** Check that constraint is fully propagated. See comment in Config.checkConstraintsPropagated */
   def checkPropagated(msg: => String)(result: Boolean): Boolean = {
     if (Config.checkConstraintsPropagated && result && addConstraintInvocations == 0) {
@@ -346,12 +435,4 @@ trait ConstraintHandling {
     }
     result
   }
-
-  /** A new constraint with all polytypes that only have instantiated parameters removed */
-  protected def cleanup(): Unit =
-    if (needsCleanup) {
-      constraint =
-        (constraint /: constraint.domainPolys.filter(constraint.isRemovable(_)))(_.remove(_))
-      needsCleanup = false
-    }
 }

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

@@ -12,6 +12,7 @@ import config.Config
 import config.Printers._
 import TypeErasure.{erasedLub, erasedGlb}
 import TypeApplications._
+import typer.ProtoTypes.constrained
 import scala.util.control.NonFatal
 
 /** Provides methods to compare types.
@@ -102,7 +103,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
         recCount = recCount - 1
         if (!result) constraint = saved
         else if (recCount == 0)
-          cleanup()
+          cleanupConstraint()
           if (needsGc) {
             state.gc()
             needsGc = false
@@ -587,6 +588,8 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
             }
           case tycon1: TypeVar =>
             isMatchingApply(tycon1.underlying)
+          case tycon1: LazyRef =>
+            isMatchingApply(tycon1.underlying)
           case tycon1: AnnotatedType =>
             isMatchingApply(tycon1.underlying)
           case _ =>
@@ -656,8 +659,14 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
       case tycon2: TypeRef =>
         isMatchingApply(tp1) ||
         compareLower(tycon2.info.bounds)
+      case tycon2: TypeLambda =>
+        val combined = constrained(mergeLambdaAndArgs(tycon2, args2))
+        typr.println(i"new lambda: $combined")
+        isSubType(tp1, combined.resultType)
       case tycon2: TypeVar =>
         isSubType(tp1, tycon2.underlying.appliedTo(args2))
+      case tycon2: LazyRef =>
+        compareHkApply2(tp1, tp2, tycon2.underlying, args2)
       case tycon2: AnnotatedType =>
         compareHkApply2(tp1, tp2, tycon2.underlying, args2)
       case _ =>
@@ -678,12 +687,24 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
         }
         canConstrain(param1) && canInstantiate ||
           isSubType(bounds(param1).hi.applyIfParameterized(args1), tp2)
+      case tycon1: TypeLambda =>
+        val combined = mergeLambdaAndArgs(tycon1, args1)
+        isSubType(combined.resultType, tp2)
       case tycon1: TypeProxy =>
         isSubType(tycon1.superType.applyIfParameterized(args1), tp2)
       case _ =>
         false
     }
 
+  /** A fresh type lambda like `tl`, but with bounds coming from `args` added to
+   *  the bounds of its type parameters.
+   */
+  def mergeLambdaAndArgs(tl: TypeLambda, args: List[Type]): TypeLambda =
+    tl.duplicate( // important to use duplicate here, as we need a fresh lambda in the constraint set.
+      tl.paramNames,
+      tl.paramBounds.zipWithConserve(args)((bounds, arg) => bounds & arg.bounds),
+      tl.resType).asInstanceOf[TypeLambda]
+
   /** Subtype test for corresponding arguments in `args1`, `args2` according to
    *  variances in type parameters `tparams`.
    */

src/dotty/tools/dotc/core/TypeOps.scala

@@ -152,8 +152,11 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
           tp2
         case tp1 => tp1
       }
-    case tp: PolyParam =>
-      typerState.constraint.typeVarOfParam(tp) orElse tp
+    case param: PolyParam =>
+      if (param.binder.isInstanceOf[TypeLambda] && typerState.constraint.contains(param))
+        typeComparer.instantiateLambdaParam(param, if (theMap == null) 1 else theMap.currentVariance)
+      else
+        typerState.constraint.typeVarOfParam(param) orElse param
     case  _: ThisType | _: BoundType | NoPrefix =>
       tp
     case tp: RefinedType =>
@@ -169,6 +172,7 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
   }
 
   class SimplifyMap extends TypeMap {
+    def currentVariance: Int = variance
     def apply(tp: Type) = simplify(tp, this)
   }
 

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

@@ -2870,63 +2870,9 @@ object Types {
       tp
     }
 
-    /** Instantiate variable from the constraints over its `origin`.
-     *  If `fromBelow` is true, the variable is instantiated to the lub
-     *  of its lower bounds in the current constraint; otherwise it is
-     *  instantiated to the glb of its upper bounds. However, a lower bound
-     *  instantiation can be a singleton type only if the upper bound
-     *  is also a singleton type.
-     */
-    def instantiate(fromBelow: Boolean)(implicit ctx: Context): Type = {
-      def upperBound = ctx.typerState.constraint.fullUpperBound(origin)
-      def isSingleton(tp: Type): Boolean = tp match {
-        case tp: SingletonType => true
-        case AndType(tp1, tp2) => isSingleton(tp1) | isSingleton(tp2)
-        case OrType(tp1, tp2) => isSingleton(tp1) & isSingleton(tp2)
-        case _ => false
-      }
-      def isFullyDefined(tp: Type): Boolean = tp match {
-        case tp: TypeVar => tp.isInstantiated && isFullyDefined(tp.instanceOpt)
-        case tp: TypeProxy => isFullyDefined(tp.underlying)
-        case tp: AndOrType => isFullyDefined(tp.tp1) && isFullyDefined(tp.tp2)
-        case _ => true
-      }
-      def isOrType(tp: Type): Boolean = tp.stripTypeVar.dealias match {
-        case tp: OrType => true
-        case tp: RefinedOrRecType => isOrType(tp.parent)
-        case AndType(tp1, tp2) => isOrType(tp1) | isOrType(tp2)
-        case WildcardType(bounds: TypeBounds) => isOrType(bounds.hi)
-        case _ => false
-      }
-
-      // First, solve the constraint.
-      var inst = ctx.typeComparer.approximation(origin, fromBelow)
-
-      // Then, approximate by (1.) - (3.) and simplify as follows.
-      // 1. If instance is from below and is a singleton type, yet
-      // upper bound is not a singleton type, widen the instance.
-      if (fromBelow && isSingleton(inst) && !isSingleton(upperBound))
-        inst = inst.widen
-
-      inst = inst.simplified
-
-      // 2. If instance is from below and is a fully-defined union type, yet upper bound
-      // is not a union type, approximate the union type from above by an intersection
-      // of all common base types.
-      if (fromBelow && isOrType(inst) && isFullyDefined(inst) && !isOrType(upperBound))
-        inst = inst.approximateUnion
-
-      // 3. If instance is from below, and upper bound has open named parameters
-      //    make sure the instance has all named parameters of the bound.
-      if (fromBelow) inst = inst.widenToNamedTypeParams(this.namedTypeParams)
-
-      if (ctx.typerState.isGlobalCommittable)
-        assert(!inst.isInstanceOf[PolyParam], i"bad inst $this := $inst, constr = ${ctx.typerState.constraint}")
-          // If this fails, you might want to turn on Config.debugCheckConstraintsClosed
-          // to help find the root of the problem.
-
-      instantiateWith(inst)
-    }
+    /** Instantiate variable from the constraints over its `origin`. */
+    def instantiate(fromBelow: Boolean)(implicit ctx: Context): Type =
+      instantiateWith(ctx.typeComparer.instanceType(origin, fromBelow))
 
     /** Unwrap to instance (if instantiated) or origin (if not), until result
      *  is no longer a TypeVar

tests/pos/existentials.scala

@@ -0,0 +1,16 @@
+object TestList {
+
+  var x: ([X] -> List[List[X]])[_] = List(List(1))
+
+  var y: List[_] = x
+
+}
+object TestSet {
+
+  class Set[S](x: S)
+
+  var x: ([Y] -> Set[Set[Y]])[_] = new Set(new Set("a"))
+
+  var y: Set[_] = x
+
+}