Freeze GADTs more when comparing type member infos

Author: dwijnand

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

@@ -1923,7 +1923,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         || symInfo.isInstanceOf[MethodType]
             && symInfo.signature.consistentParams(info2.signature)
 
-      def tp1IsSingleton: Boolean = tp1.isInstanceOf[SingletonType]
+      def allowGadt: Boolean =
+        def rec(tp: Type): Boolean = tp match
+          case RefinedType(parent, name1, _) => name == name1 || rec(parent)
+          case tp: TypeRef                   => tp.symbol.isClass
+          case _                             => false
+        !approx.low && rec(tp1)
 
       // A relaxed version of isSubType, which compares method types
       // under the standard arrow rule which is contravarient in the parameter types,
@@ -1939,8 +1944,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 _ => inFrozenGadtIf(tp1IsSingleton) { isSubType(info1, info2) }
-          case _ => inFrozenGadtIf(tp1IsSingleton) { isSubType(info1, info2) }
+              case _ => inFrozenGadtIf(!allowGadt) { isSubType(info1, info2) }
+          case _ => inFrozenGadtIf(!allowGadt) { isSubType(info1, info2) }
 
       def qualifies(m: SingleDenotation): Boolean =
         val info1 = m.info.widenExpr

compiler/src/scala/quoted/runtime/impl/QuoteMatcher.scala

@@ -186,14 +186,14 @@ object QuoteMatcher {
             if patternHole.symbol.eq(defn.QuotedRuntimePatterns_patternHole) &&
                tpt2.tpe.derivesFrom(defn.RepeatedParamClass) =>
           scrutinee match
-            case Typed(s, tpt1) if s.tpe <:< tpt.tpe => matched(scrutinee)
+            case Typed(s, tpt1) if s.tpe.widenSingleton <:< tpt.tpe => matched(scrutinee)
             case _ => notMatched
 
         /* Term hole */
         // Match a scala.internal.Quoted.patternHole and return the scrutinee tree
         case TypeApply(patternHole, tpt :: Nil)
             if patternHole.symbol.eq(defn.QuotedRuntimePatterns_patternHole) &&
-                scrutinee.tpe <:< tpt.tpe =>
+                scrutinee.tpe.widenSingleton <:< tpt.tpe =>
           scrutinee match
             case ClosedPatternTerm(scrutinee) => matched(scrutinee)
             case _ => notMatched

tests/neg/i15485.scala

@@ -0,0 +1,22 @@
+enum SUB[-A, +B]:
+  case Refl[C]() extends SUB[C, C]
+
+trait Tag { type T }
+
+def foo[A, B, X <: Tag { type T <: A } ](
+    e: SUB[X, Tag { type T <: B }],
+    x: A,
+): B = e match {
+  case SUB.Refl() =>
+    // X <: C  and  C <: Tag { T <: B }
+    // X              <: Tag { T <: B }
+    // Tag { T <: A } <: Tag { T <: B }
+    // A <: B
+    x // error: Found: (x: A) Required: B
+}
+
+def bad(x: Int): String =
+  foo[Int, String, Tag { type T = Nothing }](SUB.Refl(), x)  // cast Int to String
+
+object Test:
+  def main(args: Array[String]): Unit = bad(1) // was: ClassCastException: class java.lang.Integer cannot be cast to class java.lang.String

tests/neg/i15485b.scala

@@ -0,0 +1,22 @@
+enum SUB[-A, +B]:
+  case Refl[C]() extends SUB[C, C]
+
+trait Tag { type T }
+
+def foo[L, H, X <: Tag { type T >: L <: H }](
+    e: SUB[X, Tag { type T = Int }],
+    x: Int,
+): L = e match {
+  case SUB.Refl() =>
+    // X <: C     and    C <: Tag { T = Int }
+    // X                   <: Tag { T = Int }
+    // Tag { T >: L <: H } <: Tag { T = Int }
+    // Int <: L and H <: Int
+    x // error
+}
+
+def bad(x: Int): String =
+  foo[Nothing, Any, Tag { type T = Int }](SUB.Refl(), x)  // cast Int to String!
+
+object Test:
+  def main(args: Array[String]): Unit = bad(1) // was: ClassCastException: class java.lang.Integer cannot be cast to class java.lang.String

tests/neg/i15485c.scala

@@ -0,0 +1,31 @@
+enum SUB[-A, +B]:
+  case Refl[C]() extends SUB[C, C]
+
+trait Tag { type T }
+
+def foo[L](t: Tag { type T >: L <: Int })(
+    e: SUB[t.type, Tag { type T = Int }],
+    x: Int,
+): L = e match {
+  case SUB.Refl() =>
+    // L = Nothing
+    // C = t
+    // t := Tag { T = Int..Int     }
+    // t <: Tag { T = Nothing..Int }
+    // SUB[t,                               Tag { T = Int..Int }]
+    // SUB[Tag { T = Nothing..Int },        Tag { T = Int..Int }]
+    // SUB[Tag { T = L..Int       },        Tag { T = Int..Int }] <:< SUB[C, C]
+    //     Tag { T = L..Int       } <: C <: Tag { T = Int..Int }]
+    //     Tag { T = L..Int       }   <:    Tag { T = Int..Int }
+    // Int <: L
+    x // error
+}
+
+def bad(x: Int): String =
+  val s: Tag { type T = Int }                      = new Tag { type T = Int }
+  val t: Tag { type T >: Nothing <: Int } & s.type = s
+  val e: SUB[t.type, Tag { type T = Int }] = SUB.Refl[t.type]()
+  foo[Nothing](t)(e, x) // cast Int to String!
+
+object Test:
+  def main(args: Array[String]): Unit = bad(1) // was: ClassCastException: class java.lang.Integer cannot be cast to class java.lang.String

tests/pos-macros/i15485.fallout2-monocle/Derivation_1.scala

@@ -0,0 +1,12 @@
+// Another minimisation (after tests/run-macros/i15485.fallout-monocle)
+// of monocle's GenIsoSpec.scala
+// which broke when fixing soundness in infering GADT constraints on refined types
+class Can[T]
+object Can:
+  import scala.deriving.*, scala.quoted.*
+
+  inline given derived[T](using inline m: Mirror.Of[T]): Can[T] = ${ derivedExpr('m) }
+
+  private def derivedExpr[T](m: Expr[Mirror.Of[T]])(using Quotes, Type[T]): Expr[Can[T]] = m match
+    case '{ $_ : Mirror.Sum     { type MirroredElemTypes = mirroredElemTypes } } => '{ new Can[T] }
+    case '{ $_ : Mirror.Product { type MirroredElemTypes = mirroredElemTypes } } => '{ new Can[T] }

tests/pos-macros/i15485.fallout2-monocle/Lib_2.scala

@@ -0,0 +1,3 @@
+class Test:
+  def test =
+    Can.derived[EmptyTuple]

tests/run-macros/i15485.fallout-monocle/Derivation_1.scala

@@ -0,0 +1,16 @@
+import scala.deriving.*, scala.quoted.*
+
+trait Foo[T]:
+  def foo: Int
+
+// A minimisation of monocle's GenIsoSpec.scala
+// which broke when fixing soundness in infering GADT constraints on refined types
+object Foo:
+  inline given derived[T](using inline m: Mirror.Of[T]): Foo[T] = ${ impl('m) }
+
+  private def impl[T](m: Expr[Mirror.Of[T]])(using qctx: Quotes, tpe: Type[T]): Expr[Foo[T]] = m match
+    case '{ $m : Mirror.Product { type MirroredElemTypes =      EmptyTuple   } } => '{ FooN[T](0) }
+    case '{ $m : Mirror.Product { type MirroredElemTypes = a *: EmptyTuple   } } => '{ FooN[T](1) }
+    case '{ $m : Mirror.Product { type MirroredElemTypes = mirroredElemTypes } } => '{ FooN[T](9) }
+
+  class FooN[T](val foo: Int) extends Foo[T]

tests/run-macros/i15485.fallout-monocle/Lib_2.scala

@@ -0,0 +1 @@
+final case class Box(value: Int) derives Foo

tests/run-macros/i15485.fallout-monocle/Test_3.scala

@@ -0,0 +1,3 @@
+@main def Test =
+  val foo = summon[Foo[Box]].foo
+  assert(foo == 1, foo)