Refine GADT casts on singletons

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

@@ -118,6 +118,7 @@ class CheckRealizable(using Context) {
     case tp =>
       def isConcrete(tp: Type): Boolean = tp.dealias match {
         case tp: TypeRef => tp.symbol.isClass
+        case tp: TypeParamRef => false
         case tp: TypeProxy => isConcrete(tp.underlying)
         case tp: AndType => isConcrete(tp.tp1) && isConcrete(tp.tp2)
         case tp: OrType  => isConcrete(tp.tp1) && isConcrete(tp.tp2)

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

@@ -919,6 +919,7 @@ class Definitions {
   @tu lazy val ParamMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.param")
   @tu lazy val SetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.setter")
   @tu lazy val ShowAsInfixAnnot: ClassSymbol = requiredClass("scala.annotation.showAsInfix")
+  @tu lazy val StableAnnot: ClassSymbol = requiredClass("scala.annotation.internal.Stable")
   @tu lazy val FunctionalInterfaceAnnot: ClassSymbol = requiredClass("java.lang.FunctionalInterface")
   @tu lazy val TargetNameAnnot: ClassSymbol = requiredClass("scala.annotation.targetName")
   @tu lazy val VarargsAnnot: ClassSymbol = requiredClass("scala.annotation.varargs")

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

@@ -168,7 +168,7 @@ object Types {
       case _: SingletonType | NoPrefix => true
       case tp: RefinedOrRecType => tp.parent.isStable
       case tp: ExprType => tp.resultType.isStable
-      case tp: AnnotatedType => tp.parent.isStable
+      case tp: AnnotatedType => tp.annot.symbol == defn.StableAnnot || tp.parent.isStable
       case tp: AndType =>
         // TODO: fix And type check when tp contains type parames for explicit-nulls flow-typing
         // see: tests/explicit-nulls/pos/flow-stable.scala.disabled

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

@@ -3530,12 +3530,31 @@ class Typer extends Namer
                 typr.println(i"adapt to subtype ${tree.tpe} !<:< $pt")
                 //typr.println(TypeComparer.explained(tree.tpe <:< pt))
                 adaptToSubType(wtp)
-          case CompareResult.OKwithGADTUsed if pt.isValueType =>
+          case CompareResult.OKwithGADTUsed
+          if pt.isValueType
+             && !inContext(ctx.fresh.setGadt(EmptyGadtConstraint)) {
+               val res = (tree.tpe.widenExpr frozen_<:< pt)
+               if res then
+                 // we overshot; a cast is not needed, after all.
+                 gadts.println(i"unnecessary GADTused for $tree: ${tree.tpe.widenExpr} vs $pt in ${ctx.source}")
+               res
+              } =>
             // Insert an explicit cast, so that -Ycheck in later phases succeeds.
             // I suspect, but am not 100% sure that this might affect inferred types,
             // if the expected type is a supertype of the GADT bound. It would be good to come
             // up with a test case for this.
-            tree.cast(pt)
+            val target =
+              if tree.tpe.isSingleton then
+                val conj = AndType(tree.tpe, 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
+                  // and after checking. See i11955.scala.
+                  AnnotatedType(conj, Annotation(defn.StableAnnot))
+                else conj
+              else pt
+            gadts.println(i"insert GADT cast from $tree to $target")
+            tree.cast(target)
           case _ =>
             tree
     }

compiler/test/dotc/pos-test-pickling.blacklist

@@ -64,3 +64,7 @@ i8182.scala
 
 # local lifted value in annotation argument has different position after pickling
 i2797a
+
+# GADT cast applied to singleton type difference
+i4176-gadt.scala
+

library/src/scala/annotation/internal/Stable.scala

@@ -0,0 +1,6 @@
+package scala.annotation.internal
+
+import scala.annotation.Annotation
+
+/** An annotation asserting that the annotated type is stable */
+final class Stable() extends Annotation

tests/pos/i11220.scala

@@ -0,0 +1,8 @@
+import scala.annotation.tailrec
+class Context {
+  type Tree
+}
+
+final def loop3[C <: Context](): Unit =
+  @tailrec
+  def loop4[A <: C](c: A): c.Tree = loop4(c)

tests/pos/i11955.scala

@@ -0,0 +1,25 @@
+object Hello {
+
+  sealed abstract class X[+A] {
+    type This[+A] <: X[A]
+    def asThis: This[A]
+  }
+
+  class Y[+A] extends X[A] {
+    override type This[+AA] = Y[AA]
+    override def asThis: This[A] = this
+  }
+
+  def hackBackToSelf[F[+u] <: X[u], A](f: F[Any])(f2: f.This[A]): F[A] =
+    f2.asInstanceOf[F[A]]
+
+  case class G[F[+u] <: X[u], A](wrapped: F[A]) {
+
+    def mapF[F2[+u] <: X[u]](f: F[A] => F2[A]): G[F2, A] =
+      G[F2, A](f(wrapped))
+
+    def test_ko_1: G[F, A] = mapF(ct => hackBackToSelf(ct)(ct.asThis)) // error
+    def test_ko_2: G[F, A] = mapF[F](ct => hackBackToSelf(ct)(ct.asThis)) // error
+    def test_ok  : G[F, A] = mapF(ct => hackBackToSelf[F, A](ct)(ct.asThis)) // ok
+  }
+}