Instantiate argument type vars before implicit search

[EugeneFlesselle]

No description provided.

[odersky]

This looks actually quite promising. The one failure in libretto is probably due to the fact that a type variable is not instantiated to a singleton type. So we might have had a constraint

A <: String

and proceeded to instantiate toString but implicit search would have added the stronger constraint A <: "ping".
Just guessing. We should try to minimize the failure to better judge it.

[EugeneFlesselle]

This looks actually quite promising. The one failure in libretto is probably due to the fact that a type variable is not instantiated to a singleton type. So we might have had a constraint A <: String and proceeded to instantiate toString but implicit search would have added the stronger constraint A <: "ping". Just guessing. We should try to minimize the failure to better judge it.

That is indeed exactly what happens !

Here is the minimisation I got to:

case class Val[T](t: T)

trait Ev[T]

given Ev[String] = ???
given Ev["ping"] = ???
given[T: Ev]: Ev[Val[T]] = ???

def f[T: Ev](v: T): Unit = ???

def g[U](u: U)(using U =:= Val["ping"]): Unit = ???

def main =

  val v /*: Val3[String] */ = Val("ping")

  f(v)           // before changes ✅; after changes ✅
  f(Val("ping")) // before changes ❌; after changes ✅

  g(v)           // before changes ❌; after changes ❌
  g(Val("ping")) // before changes ✅; after changes ❌

The instantiation of T in Val[T]("ping") is widened from ("ping" : String) to String
https://github.com/lampepfl/dotty/blob/c88c0fe4103ef8fc2e96e0d33368c92036467a61/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala#L705-L708

[EugeneFlesselle]

Instead of fully instantiating the type variables, an another possibility we considered is to add the approximation computed for the instantiation as an upper bound constraint. E.g. T >: "ping" ==> T >: "ping" <: String instead of T >: "ping" ==> T := String.

This does fix the issue with g(Val("ping")). However, we get the original problem back for f(Val("ping")): adding a constraint T >: "ping" <: String does not make the given instances any less ambiguous than with T >: "ping".

[smarter]

Otherwise LGTM. The breakage in Libretto is unfortunate (/cc @TomasMikula) but having played with that code I haven't found an alternative that avoided that. It's possible something akin to scala/improvement-proposals#48 will allow for APIs that can control inference better in the future.

[smarter]

I think the documentation comment of tvarsInParams needs to be updated to account for these changes.

[EugeneFlesselle]

Indeed !

[TomasMikula]

Thanks for the heads up, @smarter. The breakage from this change is rather minor. I have added a definition

  transparent inline def constVal[A]: Done -⚬ Val[A] =
    constVal(scala.compiletime.constValue[A])

so that the diff to fix the broken code is then just changing constVal("ping") to constVal["ping"].

Though before I even got this breakage, I had to resolve a couple of different breakages (one of them reported as #19570). The thing is, the community build is using an old version of Libretto. Last time I tried to update (#17044), the community build did not support Java 9 required by Libretto. Would be good to get it resolved so that both you and me get breakage notifications earlier.

[WojciechMazur]

There is one more failure in the Open CB found in @Ichoran /kse3 - build logs
I believe it is an actual improvement, so I'm not creating a dedicated issue.

class Anon[A](val value: A)
class Mu[A]
object Mu:
  final class MuAny[A](v: A) extends Mu[A]

trait Typed[A]
def typed[A]: Typed[A] = ???
class Labeled[A](v: A):
  def ====[B](t: Typed[B])(using B =:= A): Unit = {}

@main def Test =
  Labeled(Anon(new Mu.MuAny("foo"))) ==== typed[Anon[Mu[String]]]
  
  // After typer:
  // In 3.4.0
  // new Labeled[Anon[Mu[String]]](
  //   new Anon[Mu[String]](new Mu.MuAny[String]("cod"))).====[
  //   Anon[Mu[String]]](typed[Anon[Mu[String]]])(<:<.refl[Anon[Mu[String]]])
  // }

  // In 3.4.1-RC1 and 3.4.2-RC1-nightly
  // new Labeled[Anon[Mu.MuAny[String]]](
  //   new Anon[Mu.MuAny[String]](new Mu.MuAny[String]("cod"))).====[
  //   Anon[Mu[String]]](typed[Anon[Mu[String]]])(
  //   /* missing */summon[Anon[Mu[String]] =:= Anon[Mu.MuAny[String]]])

[soronpo]

This PR caused the regression #20053

[Ichoran]

Wait, you added kse3 to the CB?! That's lovely! Um! I'll be a little less cavalier about pushing nonsense into it then! 😆

I agree that kse3 is the one who is wrong here: the types are supposed to match exactly, but don't. So the new behavior is an improvement because it catches the bug in how the test is written! 👍

[Ichoran]

@WojciechMazur - Sorry for not noticing your message initially! You're correct that this was (from my perspective) a bug in my test suite that 3.4.1 correctly caught, and I've now fixed it in main.