Implement safe widening of singleton types for abstract type constructors

Author: noti0na1

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

@@ -3716,7 +3716,7 @@ class MatchReducer(initctx: Context) extends TypeComparer(initctx) {
                 false
 
           case MatchTypeCasePattern.AbstractTypeConstructor(tycon, argPatterns) =>
-            scrut.dealias match
+            scrut.dealias.widenSingletonNonParamRefs match
               case scrutDealias @ AppliedType(scrutTycon, args) if scrutTycon =:= tycon =>
                 matchArgs(argPatterns, args, tycon.typeParams, scrutIsWidenedAbstract)
               case _ =>

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -1400,6 +1400,18 @@ object Types extends TypeUtils {
       case _ => this
     }
 
+    /** Widen singleton types that are safe to widen (not parameters)
+     *  to allow matching against abstract type constructors.
+     *  See issue #20453
+     */
+    final def widenSingletonNonParamRefs(using Context): Type = stripped match {
+      case tp: TermRef if !tp.symbol.is(TypeParam) =>
+        val denot = tp.denot
+        if denot.isOverloaded then this else denot.info.widenSingletonNonParamRefs
+      case tp: SingletonType => tp.underlying.widenSingletonNonParamRefs
+      case _ => this
+    }
+
     /** Widen from TermRef to its underlying non-termref
      *  base type, while also skipping Expr types.
      */

tests/neg/i20453.check

@@ -0,0 +1,14 @@
+-- [E007] Type Mismatch Error: tests/neg/i20453.scala:7:4 --------------------------------------------------------------
+7 |    ("name", "age") // error
+  |    ^^^^^^^^^^^^^^^
+  |    Found:    (String, String)
+  |    Required: NamedTupleDecomposition.Names[(f : (name : String, age : Int))]
+  |
+  |    Note: a match type could not be fully reduced:
+  |
+  |      trying to reduce  NamedTupleDecomposition.Names[(f : (name : String, age : Int))]
+  |      failed since selector (f : (name : String, age : Int))
+  |      does not match  case NamedTuple.NamedTuple[n, _] => n
+  |      and cannot be shown to be disjoint from it either.
+  |
+  | longer explanation available when compiling with `-explain`

tests/neg/i20453.scala

@@ -0,0 +1,7 @@
+import scala.language.experimental.namedTuples
+
+// Ensure we don't widen parameter singleton types
+// which would cause unsoundness similar to #19746
+object Test:
+  def foo[T](f: (name: String, age: Int)): NamedTupleDecomposition.Names[f.type] =
+    ("name", "age") // error

tests/pos/i20453.scala

@@ -0,0 +1,5 @@
+import scala.language.experimental.namedTuples
+
+object Test:
+  val f: (name: String, age: Int) = ???
+  val x: NamedTupleDecomposition.Names[f.type] = ("name", "age")