Operations on NamedTuples do not work with singleton types due to match type refusing to reduce

[smarter]

Compiler version

7d559ad

Minimized code

import scala.language.experimental.namedTuples

object Test:
  val f: (name: String, age: Int) = ???
  val x: NamedTupleDecomposition.Names[f.type] = ("name", "age")

Output

5 |  val x: NamedTupleDecomposition.Names[f.type] = ("name", "age")
  |                                                 ^^^^^^^^^^^^^^^
  |Found:    (String, String)
  |Required: NamedTupleDecomposition.Names[(Test.f : (name : String, age : Int))]
  |
  |Note: a match type could not be fully reduced:
  |
  |  trying to reduce  NamedTupleDecomposition.Names[(Test.f : (name : String, age : Int))]
  |  failed since selector (Test.f : (name : String, age : Int))
  |  does not match  case NamedTuple.NamedTuple[n, _] => n
  |  and cannot be shown to be disjoint from it either.

Expectation

I'd expect this to reduce, otherwise all NamedTuple operations that use NamedTupleDecomposition like NamedTuple.Map will fail to reduce on singleton types. NamedTupleDecomposition is defined as:

/** Separate from NamedTuple object so that we can match on the opaque type NamedTuple. */
@experimental
object NamedTupleDecomposition:
  import NamedTuple.*

  /** The names of a named tuple, represented as a tuple of literal string values. */
  type Names[X <: AnyNamedTuple] <: Tuple = X match
    case NamedTuple[n, _] => n

So NamedTuple is treated as an abstract type constructor and we end up in

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

Lines 3506 to 3511 in 7d559ad

	case MatchTypeCasePattern.AbstractTypeConstructor(tycon, argPatterns) =>
	scrut.dealias match
	case scrutDealias @ AppliedType(scrutTycon, args) if scrutTycon =:= tycon =>
	matchArgs(argPatterns, args, tycon.typeParams, scrutIsWidenedAbstract)
	case _ =>
	false

Which fails since the scrutinee isn't widened. @sjrd : do you anticipate a soundness issue if we added a .widenSingleton on the scrutinee here? Or is the whole design of NamedTupleDecomposition doomed?

[sjrd]

Yes, widening singleton types of paths that can be substituted later creates established unsoundness issues. See #19746

[smarter]

Thanks for the reference. A possibly viable workaround is to use a wrapper type:

import scala.language.experimental.namedTuples

class Wrapper[T](x: T)
object Wrapper:
  type Extract[W <: Wrapper[?]] = W match
    case Wrapper[t] => t

object Test:
  val f: (name: String, age: Int) = ???
  val f2 = Wrapper(f)
  val x: NamedTupleDecomposition.Names[Wrapper.Extract[f2.type]] = ("name", "age")

Not sure if there's a better way or if that can help suggest some more systematic fix.

[soronpo]

@smarter what if we explicitly create a Widen type operation? So Names will be implemented as Widen[X] match ...

[smarter]

That would reopen the soundness hole of #19746 if Widen[this.type] can reduce to different types depending on the context.

[soronpo]

I'm not sure that will happen, because of the lazy nature of singleton ops operations.

[smarter]

Though note that the fix for #19746 (0a3497b) specifically target singleton types coming from parameters (since those can be substituted), so maybe something like a widenSingletonOfNonParamRef operation? It's not clear to me that this is enough if the underlying type of a non-param singleton is a GADT, in which case maybe the original hole isn't fixed.

[smarter]

in which case maybe the original hole isn't fixed.

Indeed: #20515.