Insert GADT casts for needy match types

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

@@ -779,6 +779,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         && (!caseLambda.exists || canWidenAbstract || tp1.widen.underlyingClassRef(refinementOK = true).exists)
       then
         isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow)
+        && { GADTused ||= MatchType.thatReducesUsingGadt(tp1); true }
         || base.isInstanceOf[OrType] && fourthTry
           // if base is a disjunction, this might have come from a tp1 type that
           // expands to a match type. In this case, we should try to reduce the type

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

@@ -4705,6 +4705,13 @@ object Types {
       myReduced.nn
     }
 
+    /** True if the reduction uses GADT constraints. */
+    def reducesUsingGadt(using Context): Boolean =
+      (reductionContext ne null) && reductionContext.keysIterator.exists {
+        case tp: TypeRef => reductionContext(tp).exists
+        case _           => false
+      }
+
     override def computeHash(bs: Binders): Int = doHash(bs, scrutinee, bound :: cases)
 
     override def eql(that: Type): Boolean = that match {
@@ -4719,6 +4726,21 @@ object Types {
   object MatchType {
     def apply(bound: Type, scrutinee: Type, cases: List[Type])(using Context): MatchType =
       unique(new CachedMatchType(bound, scrutinee, cases))
+
+    def thatReducesUsingGadt(tp: Type)(using Context): Boolean = tp match
+      case MatchType.InDisguise(mt) => mt.reducesUsingGadt
+      case mt: MatchType            => mt.reducesUsingGadt
+      case _                        => false
+
+    /** Extractor for match types hidden behind an AppliedType/MatchAlias. */
+    object InDisguise:
+      def unapply(tp: AppliedType)(using Context): Option[MatchType] = tp match
+        case AppliedType(tycon: TypeRef, args) => tycon.info match
+          case MatchAlias(alias) => alias.applyIfParameterized(args) match
+            case mt: MatchType => Some(mt)
+            case _ => None
+          case _ => None
+        case _ => None
   }
 
   // ------ ClassInfo, Type Bounds --------------------------------------------------

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -1571,21 +1571,6 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
         val selType = rawSelectorTpe match
           case c: ConstantType if tree.isInline => c
           case otherTpe => otherTpe.widen
-        /** Extractor for match types hidden behind an AppliedType/MatchAlias */
-        object MatchTypeInDisguise {
-          def unapply(tp: AppliedType)(using Context): Option[MatchType] = tp match {
-            case AppliedType(tycon: TypeRef, args) =>
-              tycon.info match {
-                case MatchAlias(alias) =>
-                  alias.applyIfParameterized(args) match {
-                    case mt: MatchType => Some(mt)
-                    case _ => None
-                  }
-                case _ => None
-              }
-            case _ => None
-          }
-        }
 
         /** Does `tree` has the same shape as the given match type?
          *  We only support typed patterns with empty guards, but
@@ -1618,7 +1603,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
             }
 
         val result = pt match {
-          case MatchTypeInDisguise(mt) if isMatchTypeShaped(mt) =>
+          case MatchType.InDisguise(mt) if isMatchTypeShaped(mt) =>
             typedDependentMatchFinish(tree, sel1, selType, tree.cases, mt)
           case _ =>
             typedMatchFinish(tree, sel1, selType, tree.cases, pt)
@@ -3007,7 +2992,9 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
          || tree.isDef                              // ... unless tree is a definition
       then
         interpolateTypeVars(tree, pt, locked)
-        tree.overwriteType(tree.tpe.simplified)
+        val simplified = tree.tpe.simplified
+        if !MatchType.thatReducesUsingGadt(tree.tpe) then // needs a GADT cast. i15743
+          tree.overwriteType(simplified)
     tree
 
   protected def makeContextualFunction(tree: untpd.Tree, pt: Type)(using Context): Tree = {

tests/pos/i15743.gadt.scala

@@ -0,0 +1,12 @@
+abstract class C[Z] { def getZ: Z }
+final case class C1() extends C[Tuple] { def getZ = new Tuple1[String]("foo") }
+
+// Like pos/i15743 but definitely requires the constraint on T to be stored as a GADT constraint
+// where in pos/i15743 it may have been reasonable to think that the constraint could be stored
+// in the regular type inference constraints
+class Alt:
+  def test[T](e: C[T]) = e match
+    case c1 @ C1() => // GADT constr: T := Tuple
+      val t1: T        = c1.getZ
+      val t2: Int *: T = (1: Int) *: t1
+      val i1: Int      = (t2: Int *: T).head[Int *: T]

tests/pos/i15743.pass.scala

@@ -0,0 +1,4 @@
+// Like pos/i15743 but already passed, because the bounds are never lost so reduction never fails
+class Pass:
+  def pass[T >: Tuple <: Tuple](t2: Int *: T) =
+    val i1: Int = (t2: Int *: T).head[Int *: T]

tests/pos/i15743.scala

@@ -0,0 +1,5 @@
+case class Bar[T <: Tuple](val x: Int *: T)
+
+class Test:
+  def fail(e: Any): Int =
+    e match { case b: Bar[t] => b.x.head[Int *: t] }