Always freeze GADTs when comparing type member infos

Author: dwijnand

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

@@ -1923,8 +1923,6 @@ 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)
@@ -1939,8 +1937,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(!info2.isTypeAlias) { isSubType(info1, info2) }
+          case _ => inFrozenGadtIf(!info2.isTypeAlias) { isSubType(info1, info2) }
 
       def qualifies(m: SingleDenotation): Boolean =
         val info1 = m.info.widenExpr

tests/neg/i15485.scala

@@ -0,0 +1,20 @@
+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() =>
+    // unsound GADT constr because of approx state resetting:
+    // 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/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)