Refine GADT casts with GADT approximation of singleton types

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

@@ -209,7 +209,15 @@ final class ProperGadtConstraint private(
   def isNarrowing: Boolean = wasConstrained
 
   override def approximation(sym: Symbol, fromBelow: Boolean)(using Context): Type = {
-    val res = approximation(tvarOrError(sym).origin, fromBelow = fromBelow)
+    val res =
+      approximation(tvarOrError(sym).origin, fromBelow = fromBelow) match
+        case tpr: TypeParamRef =>
+          // Here we do externalization when the returned type is a TypeParamRef,
+          //  b/c ConstraintHandling.approximation may return internal types when
+          //  the type variable is instantiated. See #15531.
+          externalize(tpr)
+        case tp => tp
+
     gadts.println(i"approximating $sym ~> $res")
     res
   }

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

@@ -3767,7 +3767,13 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
             // up with a test case for this.
             val target =
               if tree.tpe.isSingleton then
-                val conj = AndType(tree.tpe, pt)
+                // In the target type, when the singleton type is intersected, we also intersect
+                //   the GADT-approximated type of the singleton to avoid the loss of 
+                //   information. See #14776.
+                val gadtApprox = Inferencing.approximateGADT(tree.tpe.widen)
+                gadts.println(i"gadt approx $wtp ~~~ $gadtApprox")
+                val conj =
+                  AndType(AndType(tree.tpe, gadtApprox), pt)
                 if tree.tpe.isStable && !conj.isStable then
                   // this is needed for -Ycheck. Without the annotation Ycheck will
                   // skolemize the result type which will lead to different types before

tests/pos/gadt-cast-singleton.scala

@@ -0,0 +1,13 @@
+enum SUB[-A, +B]:
+  case Refl[S]() extends SUB[S, S]
+
+trait R {
+  type Data
+}
+trait L extends R
+
+def f(x: L): x.Data = ???
+
+def g[T <: R](x: T, ev: T SUB L): x.Data = ev match
+  case SUB.Refl() =>
+    f(x)

tests/pos/i14776-patmat.scala

@@ -0,0 +1,15 @@
+trait T1
+trait T2 extends T1
+
+trait Expr[T] { val data: T = ??? }
+case class Tag2() extends Expr[T2]
+
+def flag: Boolean = ???
+
+def foo[T](e: Expr[T]): T1 = e match {
+  case Tag2() =>
+    flag match
+      case true => new T2 {}
+      case false => e.data
+}
+

tests/pos/i14776.scala

@@ -0,0 +1,16 @@
+trait T1
+trait T2 extends T1
+
+trait Expr[T] { val data: T = ??? }
+case class Tag2() extends Expr[T2]
+
+def flag: Boolean = ???
+
+def foo[T](e: Expr[T]): T1 = e match {
+  case Tag2() =>
+      if flag then
+        new T2 {}
+      else
+        e.data
+}
+

tests/pos/i15531.scala

@@ -0,0 +1,9 @@
+trait Tag { val data: Int }
+
+enum EQ[A, B]:
+  case Refl[C]() extends EQ[C, C]
+
+def foo[T, B <: Tag](ev: EQ[T, B], x: T) = ev match
+  case EQ.Refl() =>
+    val i: Int = x.data
+