Merge pull request #14728 from Linyxus/fix-gadt-sngl

Avoid unsound GADT constraints derived from subtyping relations between singletons and refined types

Author: abgruszecki

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

@@ -1813,6 +1813,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
           || symInfo.isInstanceOf[MethodType]
               && symInfo.signature.consistentParams(info2.signature)
 
+        def tp1IsSingleton: Boolean = tp1.isInstanceOf[SingletonType]
+
         // A relaxed version of isSubType, which compares method types
         // under the standard arrow rule which is contravarient in the parameter types,
         // but under the condition that signatures might have to match (see sigsOK)
@@ -1827,8 +1829,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                   matchingMethodParams(info1, info2, precise = false)
                   && isSubInfo(info1.resultType, info2.resultType.subst(info2, info1), symInfo1.resultType)
                   && sigsOK(symInfo1, info2)
-                case _ => isSubType(info1, info2)
-            case _ => isSubType(info1, info2)
+                case _ => inFrozenGadtIf(tp1IsSingleton) { isSubType(info1, info2) }
+            case _ => inFrozenGadtIf(tp1IsSingleton) { isSubType(info1, info2) }
 
         val info1 = m.info.widenExpr
         isSubInfo(info1, tp2.refinedInfo.widenExpr, m.symbol.info.orElse(info1))

tests/neg/gadt-sngl-refined.scala

@@ -0,0 +1,18 @@
+trait Foo {
+  type A >: Nothing <: Any
+}
+
+enum SUB[-A, +B]:
+  case Refl[X]() extends SUB[X, X]
+
+import SUB._
+
+def test[X](foo: Foo, e: SUB[foo.type, Foo {type A <: X}], x: Any): X = e match
+  case Refl() =>
+    // From foo.type <:< Foo{type A <: X} we should not infer GADT constraints.
+    x   // error
+
+val foo = new Foo { type A = Nothing }
+
+def unsound(x: Any): Nothing =
+  test[Nothing](foo, Refl(), x)