Type variables in implicit result are narrowed too eagerly

[neko-kai]

Example:

trait Tc1[A]
trait Tc2[A] extends Tc1[A]

class PinTypeTo[K[_]]
object PinTypeTo {
  implicit val pinType: PinTypeTo[Tc2] = new PinTypeTo[Tc2]
}

class X
object X {
  implicit def Tc2Instance[F[x] >: Tc2[x]: PinTypeTo]: F[X] = new Tc2[X] {}
}

object app extends App {
  implicitly[Tc2[X]] // ok
  implicitly[Tc1[X]] // fails
}

Expected:
Search for Tc1 should succeed, since F[X] always matches Tc1[X] (Scala 2 behavior)

Actual:
Search fails with

//[error] 17 |  implicitly[Tc1[X]] // fails
//[error]    |                    ^
//[error]    |no implicit argument of type Tc1[X] was found for parameter ev of method implicitly in object DottyPredef.
//[error]    |I found:
//[error]    |
//[error]    |    X.Tc2Instance[F](/* missing */implicitly[PinTypeTo[Tc1]])
//[error]    |
//[error]    |But no implicit values were found that match type PinTypeTo[Tc1].

Seems like F is narrowed to target type Tc1 overeagerly, with all implicit summons then following that assumptions, although it should probably only be constrained to a subtype of Tc1 instead.

[odersky]

This is a tough one. Here's Dotty's algorithm for type checking

   F[A] <: C[B]

where F is an instantiatable type parameter:

• try to instantiate F to C.
• If this succeeds, continue with A <: B, A = B, or A >: B, depending on variance of C's type parameter.

This is indeed incomplete since it ignores the possibility that F might be a true subtype of C. But if we admit this possibility, and just decompose to F <: C, A <: B, we become unsound. Indeed, consider:

  class C[X]
  class D[X] extends C[Int]

  F[X] <: C[String]

If we decompose this to F <: C, X <: String and later instantiate F to D we violate the original constraint, i.e. after instantiation we get D[String] <: C[String] which is false. So this is a source of unsoundness. It would be great if somebody could make the effort to construct a test case along these lines. I don't have the time right now to do it.

I am not sure how else to decompose this subtyping judgment /cc @adriaanm.

EDIT: No, it's actually quite clear what should be done: Add the constraint F <:< [X] => C[X].
F cannot be instantiated to D after this, since D == [X] => D[X] !<: [X] => C[X] even though D[_] <: C[_].