Difference in inference between [F <: List[A], A] and [F[_] <: List[A], A]

Question

Consider the difference in inference of type argument A to type constructors in the following two type parameter clauses

$ scala3-repl
scala> def f[F <: List[A], A](as: F) = as
def f[F <: List[A], A](as: F): F

scala> f(List(42))
val res0: List[Int] = List(42)

scala> def f[F[_] <: List[A], A](as: F[A]) = as
def f[F[_$1] <: List[A], A](as: F[A]): F[A]

scala> f(List(42))
val res1: List[Any] = List(42)

Why is type argument A to type constructor F inferred as Any in second case?

Answer 1

Not a full-fledged answer, just some food for thought: I've attempted to construct a counter-example, but couldn't quite come up with anything that would actually result in unsoundness under the assumption that A would be inferred as the narrowest type. Still, maybe you find it interesting.

Here is a function h with similar constraints, but instead of List, we take slightly different type constructors.

The main idea is that Cc has two separate type parameters:

• The first is what is meant by _ in F[_]
• The second one is the one that interacts with A in the <: Lst[A]-constraint

Note that this would not compile if the A was inferred to be the narrowest type (Nothing):

(run in 3.0.0-RC2)

scala> trait Lst[+X]
// defined trait Lst

scala> case class Cc[+I, +X](i: I) extends Lst[X]
// defined case class Cc

scala> type T[+I] = Cc[I, Nothing]
// defined alias type T[+I] = Cc[I, Nothing]

scala> def h[F[_] <: Lst[A], A](as: F[A]) = as
def h[F[_$1] <: Lst[A], A](as: F[A]): F[A]

scala> val xs: T[Int] = Cc(42)
val xs: T[Int] = Cc(42)

scala> h(xs)                                                                                             
val res9: Cc[Int, Nothing] = Cc(42)

Had A been inferred as the narrowest possible type satisfying the constraint of <: Lst[A], then A would be Nothing, and the argument would have to be of type T[Nothing] = Cc[Nothing, Nothing], which is uninhabited.

I think it's interesting, but I don't see why it would actually be bad if it didn't compile.