Take actual arguments for dependent TypeVars into account

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

@@ -6,7 +6,6 @@ import Contexts._, Types._, Symbols._, Names._, Flags._
 import SymDenotations._
 import util.Spans._
 import util.Stats
-import NameKinds.DepParamName
 import Decorators._
 import StdNames._
 import collection.mutable

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

@@ -28,7 +28,7 @@ import config.Printers.{ transforms => debug }
 object TypeTestsCasts {
   import ast.tpd._
   import typer.Inferencing.maximizeType
-  import typer.ProtoTypes.{ constrained, newTypeVar }
+  import typer.ProtoTypes.constrained
 
   /** Whether `(x:X).isInstanceOf[P]` can be checked at runtime?
    *

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

@@ -529,7 +529,7 @@ class SpaceEngine(using Context) extends SpaceLogic {
       case mt: MethodType => mt
       case pt: PolyType   =>
         inContext(ctx.fresh.setExploreTyperState()) {
-          val tvars = pt.paramInfos.map(newTypeVar)
+          val tvars = pt.paramInfos.map(newTypeVar(_))
           val mt = pt.instantiate(tvars).asInstanceOf[MethodType]
           scrutineeTp <:< mt.paramInfos(0)
           // force type inference to infer a narrower type: could be singleton

compiler/src/dotty/tools/dotc/typer/Inferencing.scala

@@ -599,6 +599,8 @@ trait Inferencing { this: Typer =>
         val toInstantiate = new InstantiateQueue
         for (tvar <- qualifying)
           if (!tvar.isInstantiated && constraint.contains(tvar)) {
+            constrainIfDependentParamRef(tvar, tree)
+
             // Needs to be checked again, since previous interpolations could already have
             // instantiated `tvar` through unification.
             val v = vs(tvar)
@@ -663,6 +665,33 @@ trait Inferencing { this: Typer =>
     }
     tree
   }
+
+  /** If `tvar` represents a parameter of a dependent method type in the current `call`
+   *  approximate it from below with the type of the actual argument. Skolemize that
+   *  type if necessary to make it a Singleton.
+   */
+  private def constrainIfDependentParamRef(tvar: TypeVar, call: Tree)(using Context): Unit =
+    representedParamRef(tvar) match
+      case ref: TermParamRef =>
+
+        def findArg(tree: Tree)(using Context): Tree = tree match
+          case Apply(fn, args) =>
+            if fn.tpe.widen eq ref.binder then
+              if ref.paramNum < args.length then args(ref.paramNum)
+              else EmptyTree
+            else findArg(fn)
+          case TypeApply(fn, _) => findArg(fn)
+          case Block(_, expr) => findArg(expr)
+          case Inlined(_, _, expr) => findArg(expr)
+          case _ => EmptyTree
+
+        val arg = findArg(call)
+        if !arg.isEmpty then
+          var argType = arg.tpe
+          if !argType.isSingleton then argType = SkolemType(argType)
+          argType <:< tvar
+      case _ =>
+  end constrainIfDependentParamRef
 }
 
 /** An enumeration controlling the degree of forcing in "is-dully-defined" checks. */

compiler/src/dotty/tools/dotc/typer/ProtoTypes.scala

@@ -642,30 +642,49 @@ object ProtoTypes {
   def constrained(tl: TypeLambda)(using Context): TypeLambda =
     constrained(tl, EmptyTree)._1
 
-  def newTypeVar(bounds: TypeBounds)(using Context): TypeVar = {
+  /** A new type variable with given bounds for its origin.
+   *  @param  represents  If exists, the TermParamRef that the TypeVar represents
+   *                      in the substitution generated by `resultTypeApprox`
+   *  If `represents` exists, it is stored in the result type of the PolyType
+   *  that backs the TypeVar, to be retrieved by `representedParamRef`.
+   */
+  def newTypeVar(bounds: TypeBounds, represents: Type = NoType)(using Context): TypeVar = {
     val poly = PolyType(DepParamName.fresh().toTypeName :: Nil)(
         pt => bounds :: Nil,
-        pt => defn.AnyType)
+        pt => represents.orElse(defn.AnyType))
     constrained(poly, untpd.EmptyTree, alwaysAddTypeVars = true)
       ._2.head.tpe.asInstanceOf[TypeVar]
   }
 
-  /** Create a new TypeVar that represents a dependent method parameter singleton */
-  def newDepTypeVar(tp: Type)(using Context): TypeVar =
-    newTypeVar(TypeBounds.upper(AndType(tp.widenExpr, defn.SingletonClass.typeRef)))
+  /** If `tvar` represents a parameter of a dependent function generated
+   *  by `newDepVar` called from `resultTypeApprox, the term parameter reference
+   *  for which the variable was substituted. Otherwise, NoType.
+   */
+  def representedParamRef(tvar: TypeVar)(using Context): Type =
+    if tvar.origin.paramName.is(DepParamName) then
+      tvar.origin.binder.resultType match
+        case ref: TermParamRef => ref
+        case _ => NoType
+    else NoType
+
+  /** Create a new TypeVar that represents a dependent method parameter singleton `ref` */
+  def newDepTypeVar(ref: TermParamRef)(using Context): TypeVar =
+    newTypeVar(
+      TypeBounds.upper(AndType(ref.underlying.widenExpr, defn.SingletonClass.typeRef)),
+      ref)
 
   /** The result type of `mt`, where all references to parameters of `mt` are
    *  replaced by either wildcards or TypeParamRefs.
    */
   def resultTypeApprox(mt: MethodType, wildcardOnly: Boolean = false)(using Context): Type =
     if mt.isResultDependent then
-      def replacement(tp: Type) =
+      def replacement(ref: TermParamRef) =
         if wildcardOnly
            || ctx.mode.is(Mode.TypevarsMissContext)
-           || !tp.widenExpr.isValueTypeOrWildcard
+           || !ref.underlying.widenExpr.isValueTypeOrWildcard
         then WildcardType
-        else newDepTypeVar(tp)
-      mt.resultType.substParams(mt, mt.paramInfos.map(replacement))
+        else newDepTypeVar(ref)
+      mt.resultType.substParams(mt, mt.paramRefs.map(replacement))
     else mt.resultType
 
   /** The normalized form of a type

tests/pos/i8802a.scala

@@ -0,0 +1,18 @@
+trait Foo[A1, B1] {
+  type Out
+}
+
+object Test {
+
+  type Bar[A2]
+
+  def unit: Bar[Unit] = ???
+  def product[A3, B3](fst: Bar[A3], snd: Bar[B3])(implicit foo: Foo[A3, B3]): Bar[foo.Out] = ???
+
+  implicit def foo[A4]: Foo[A4, Unit] { type Out = A4 } = ???
+
+  def check[A5](bar: Bar[A5])(a: A5): Unit = {}
+
+  check(product(unit, unit)) // ok
+  check(product(unit, unit)(summon[Foo[Unit, Unit]]))(()) // error
+}