From 27f6370e5f334ad2bbb191b1071d7ac7c4e0d521 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 4 Apr 2021 22:29:00 +0200
Subject: [PATCH 1/2] Refine GADT casts on singletons

 - keep the singleton type in the cast target
 - assert cast target stability if original was stable
 - fix isStable test for TypeParamRefs
 - double check if GADT logic is really needed before inserting a cast

Fixes #11220
Fixes #11955
---
 .../tools/dotc/core/CheckRealizable.scala     |  1 +
 .../dotty/tools/dotc/core/Definitions.scala   |  1 +
 .../src/dotty/tools/dotc/core/Types.scala     |  2 +-
 .../src/dotty/tools/dotc/typer/Typer.scala    | 17 +++++++++++--
 .../test/dotc/pos-test-pickling.blacklist     |  4 +++
 .../scala/annotation/internal/Stable.scala    |  6 +++++
 tests/pos/i11220.scala                        |  8 ++++++
 tests/pos/i11955.scala                        | 25 +++++++++++++++++++
 8 files changed, 61 insertions(+), 3 deletions(-)
 create mode 100644 library/src/scala/annotation/internal/Stable.scala
 create mode 100644 tests/pos/i11220.scala
 create mode 100644 tests/pos/i11955.scala

diff --git a/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala b/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
index 7f15bd6271f1..dd188e54db29 100644
--- a/compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
+++ b/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)
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index 4ae31b2e05e8..6e43eec7d4f0 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/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")
diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 24537ac288cd..553976a85459 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/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
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 49b91a37c43f..e623ee5bc8c1 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -3530,12 +3530,25 @@ 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)) { tree.tpe.widenExpr frozen_<:< pt } =>
             // 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
     }
diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist
index e6fd9deb979d..e0810dd260bf 100644
--- a/compiler/test/dotc/pos-test-pickling.blacklist
+++ b/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
+
diff --git a/library/src/scala/annotation/internal/Stable.scala b/library/src/scala/annotation/internal/Stable.scala
new file mode 100644
index 000000000000..bb53701716b5
--- /dev/null
+++ b/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
diff --git a/tests/pos/i11220.scala b/tests/pos/i11220.scala
new file mode 100644
index 000000000000..f6d600280bf6
--- /dev/null
+++ b/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)
\ No newline at end of file
diff --git a/tests/pos/i11955.scala b/tests/pos/i11955.scala
new file mode 100644
index 000000000000..b4a9f3148ccf
--- /dev/null
+++ b/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
+  }
+}
\ No newline at end of file

From 5c987c25e8657ef4ff24413128565e7513ef2a04 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 5 Apr 2021 10:40:39 +0200
Subject: [PATCH 2/2] Better documentation for GADT casts

---
 compiler/src/dotty/tools/dotc/typer/Typer.scala | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index e623ee5bc8c1..20f15510cf7e 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -3532,7 +3532,12 @@ class Typer extends Namer
                 adaptToSubType(wtp)
           case CompareResult.OKwithGADTUsed
           if pt.isValueType
-             && !inContext(ctx.fresh.setGadt(EmptyGadtConstraint)) { tree.tpe.widenExpr frozen_<:< pt } =>
+             && !inContext(ctx.fresh.setGadt(EmptyGadtConstraint)) {
+               (tree.tpe.widenExpr frozen_<:< pt)
+                // we overshot; a cast is not needed, after all. (this happens a lot. We should
+                // find out whether we can make GADTused more precise)
+                .showing(i"false alarm for $tree: ${tree.tpe.widenExpr} vs $pt in ${ctx.source}", gadts)
+              } =>
             // 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