add GADT approximation of the stable type in GADT casting

Author: Linyxus

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

@@ -3779,7 +3779,13 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
             // The check "safeToInstantiate" in `maximizeType` works to prevent unsound GADT casts.
             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
+}
+