Freeze GADTs more when comparing type member infos

Author: dwijnand

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

@@ -2,7 +2,7 @@ package dotty.tools
 package dotc
 package core
 
-import Types._, Contexts._, Symbols._, Flags._, Names._, NameOps._, Denotations._
+import Types._, Contexts._, Symbols._, Flags._, Names._, NameOps._, Denotations._, SymDenotations.*
 import Decorators._
 import Phases.{gettersPhase, elimByNamePhase}
 import StdNames.nme
@@ -1888,7 +1888,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
    *  rebase both itself and the member info of `tp` on a freshly created skolem type.
    */
   def hasMatchingMember(name: Name, tp1: Type, tp2: RefinedType): Boolean =
-    trace(i"hasMatchingMember($tp1 . $name :? ${tp2.refinedInfo}), mbr: ${tp1.member(name).info}", subtyping) {
+    val mbr = tp1.member(name)
+    trace(i"hasMatchingMember($tp1 . $name :? ${tp2.refinedInfo}), mbr: ${mbr.info}", subtyping) {
 
       // If the member is an abstract type and the prefix is a path, compare the member itself
       // instead of its bounds. This case is needed situations like:
@@ -1931,7 +1932,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         || symInfo.isInstanceOf[MethodType]
             && symInfo.signature.consistentParams(info2.signature)
 
-      def tp1IsSingleton: Boolean = tp1.isInstanceOf[SingletonType]
+      def allowGadt = tp1.member(name) match
+        case d: UniqueRefDenotation if d.prefix == NoPrefix && d.symbol != NoSymbol => false
+        case _ => true
 
       // A relaxed version of isSubType, which compares method types
       // under the standard arrow rule which is contravarient in the parameter types,
@@ -1947,15 +1950,15 @@ 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
         isSubInfo(info1, tp2.refinedInfo.widenExpr, m.symbol.info.orElse(info1))
         || matchAbstractTypeMember(m.info)
 
-      tp1.member(name) match // inlined hasAltWith for performance
+      mbr match // inlined hasAltWith for performance
         case mbr: SingleDenotation => qualifies(mbr)
         case mbr => mbr hasAltWith qualifies
     }

tests/neg/i15485.scala

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

tests/neg/i15485b.scala

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

tests/neg/i15485c.scala

@@ -0,0 +1,23 @@
+enum SUB[-L, +R]:
+  case Refl[C]() extends SUB[C, C]
+
+trait Tag { type T }
+
+def foo[B](g: Tag { type T >: B <: Int })(
+    e: SUB[g.type, Tag { type T = Int }], i: Int,
+): B = e match
+  case SUB.Refl() =>
+    // B = Nothing
+    // g = Tag { T = Int..Int } <: Tag { T = B..Int }
+    // SUB[g,                  Tag { T = Int..Int }]
+    // SUB[Tag { T = B..Int }, Tag { T = Int..Int }] approxLHS
+    // Int <: B
+    i // error: Found: (i: Int) Required: B
+
+def bad(i: Int): String =
+  val g = new Tag { type T = Int }
+  val e: SUB[g.type, Tag { type T = Int }] = SUB.Refl[g.type]()
+  foo[Nothing](g)(e, i) // cast Int to String!
+
+object Test:
+  def main(args: Array[String]): Unit = bad(1) // was: ClassCastException: Integer cannot be cast to String

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

@@ -0,0 +1,10 @@
+// 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] = ${ impl('m) }
+  private def impl[T](m: Expr[Mirror.Of[T]])(using Quotes, Type[T]): Expr[Can[T]] = m match
+    case '{ $_ : Mirror.Sum     { type MirroredElemTypes = met } } => '{ new Can[T] }
+    case '{ $_ : Mirror.Product { type MirroredElemTypes = met } } => '{ new Can[T] }

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

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

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

@@ -0,0 +1,7 @@
+object Iso:
+  import scala.deriving.*, scala.quoted.*
+  transparent inline def fields[S <: Product](using m: Mirror.ProductOf[S]): Int = ${ impl[S]('m) }
+  private def impl[S <: Product](m: Expr[Mirror.ProductOf[S]])(using Quotes, Type[S]): Expr[Int] =
+    import quotes.reflect.*
+    m match
+      case '{ type a <: Tuple; $m: Mirror.ProductOf[S] { type MirroredElemTypes = `a` } } => '{ 1 }

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

@@ -0,0 +1,4 @@
+class Test:
+  def test =
+    case object Foo
+    val iso = Iso.fields[Foo.type]

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

@@ -0,0 +1,11 @@
+// A minimisation of monocle's GenIsoSpec.scala
+// which broke when fixing soundness in infering GADT constraints on refined types
+trait Foo[T] { def foo: Int }
+object Foo:
+  import scala.deriving.*, scala.quoted.*
+  inline given derived[T](using inline m: Mirror.Of[T]): Foo[T] = ${ impl('m) }
+  private def impl[T](m: Expr[Mirror.Of[T]])(using Quotes, 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)