NamedTuple.From reducing on abstract types and singleton types lead to soundness holes

[smarter]

Compiler version

3.5.1-RC1-bin-20240602-c6fbe6f-NIGHTLY

Minimized code

import scala.language.experimental.namedTuples
import NamedTuple.From

case class Foo[+T](elem: T)

trait Base[T]:
  def dep(foo: T): From[T]

class SubAny[T <: Foo[Any]] extends Base[T]:
  def dep(foo: T): From[T] = (elem = "")

object Test:
  @main def run =
    val f: Foo[Int] = Foo(elem = 1)
    val b: Base[Foo[Int]] = SubAny[Foo[Int]]()
    val nt: (elem: Int) = b.dep(f)
    val x: Int = nt.elem // ClassCastException

Output

Exception in thread "main" java.lang.ClassCastException: class java.lang.String cannot be cast to class java.lang.Integer (java.lang.String and java.lang.Integer are in module java.base of loader 'bootstrap')
        at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:99)
        at Test$.run(nt-from.scala:20)
        at run.main(nt-from.scala:16)

Expectation

If From behaved like a match type then:

  def dep(foo: T): From[T] = (elem = "")

would be a type error as From[T] would not reduce.

And just like with match types, we can also run into troubles because of singleton types (at least those coming from dependent methods parameters as in #19746, though I had to make the test case more complex to delay reduction because NamedTuple.From doesn't compose with asSeenFrom like match types do):

import scala.language.experimental.namedTuples
import NamedTuple.From

case class Foo[+T](elem: T)

trait Base[M[_]]:
  def dep(foo: Foo[Any]): M[foo.type]

class SubAny extends Base[From]:
  def dep(foo: Foo[Any]): From[foo.type] = (elem = "")

object Test:
  @main def run =
    val f: Foo[Int] = Foo(elem = 1)
    val b: Base[From] = SubAny()
    val nt: (elem: Int) = b.dep(f)
    val x: Int = nt.elem // ClassCastException

So it seems that in general, NamedTuple.From and match types should share a lot more logic to prevent unsoundness.

[smarter]

@sjrd do you see a way of adapting the match type machinery to NamedTuple.From ? It seems we should at least have its argument checked via îsConcrete before proceeding with reduction:

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

Lines 3397 to 3410 in 0a3497b

	/* Concreteness checking
	*
	* When following a baseType and reaching a non-wildcard, in-variant-pos type capture,
	* we have to make sure that the scrutinee is concrete enough to uniquely determine
	* the values of the captures. This comes down to checking that we do not follow any
	* upper bound of an abstract type.
	*
	* See notably neg/wildcard-match.scala for examples of this.
	*
	* See neg/i13780.scala, neg/i13780-1.scala and neg/i19746.scala for
	* ClassCastException reproducers if we disable this check.
	*/
	def isConcrete(tp: Type): Boolean =

[sjrd]

Yes, we could/should extract isConcrete and reuse it here. It makes sense to share the logic.