Skip to content

Freeze GADTs more when comparing type member infos #15869

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 10 additions & 6 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -1931,7 +1932,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
|| symInfo.isInstanceOf[MethodType]
&& symInfo.signature.consistentParams(info2.signature)

def tp1IsSingleton: Boolean = tp1.isInstanceOf[SingletonType]
def allowGadt = mbr match
case _ if tp1.isInstanceOf[SingletonType] => false
case d: UniqueRefDenotation if d.prefix == NoPrefix && d.symbol != NoSymbol => false
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@odersky this is what I found works. Can you think of another way to identify when we have a member that required widening tp1 to a non-class info and thus we can't safely infer gadt constraints?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can't make sense of this condition and don't understand the logic behind this. This would at least need a fat comment explaining the issue and the attempted solution.

case _ => true

// A relaxed version of isSubType, which compares method types
// under the standard arrow rule which is contravarient in the parameter types,
Expand All @@ -1947,15 +1951,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
}
Expand Down
21 changes: 21 additions & 0 deletions tests/neg/i15485.scala
Original file line number Diff line number Diff line change
@@ -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
21 changes: 21 additions & 0 deletions tests/neg/i15485b.scala
Original file line number Diff line number Diff line change
@@ -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
23 changes: 23 additions & 0 deletions tests/neg/i15485c.scala
Original file line number Diff line number Diff line change
@@ -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
10 changes: 10 additions & 0 deletions tests/pos-macros/i15485.fallout2-monocle/Derivation_1.scala
Original file line number Diff line number Diff line change
@@ -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] }
3 changes: 3 additions & 0 deletions tests/pos-macros/i15485.fallout2-monocle/Lib_2.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
class Test:
def test =
Can.derived[EmptyTuple]
7 changes: 7 additions & 0 deletions tests/pos-macros/i15485.fallout3-monocle/Derivation_1.scala
Original file line number Diff line number Diff line change
@@ -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 }
4 changes: 4 additions & 0 deletions tests/pos-macros/i15485.fallout3-monocle/Lib_2.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
class Test:
def test =
case object Foo
val iso = Iso.fields[Foo.type]
11 changes: 11 additions & 0 deletions tests/run-macros/i15485.fallout-monocle/Derivation_1.scala
Original file line number Diff line number Diff line change
@@ -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]
1 change: 1 addition & 0 deletions tests/run-macros/i15485.fallout-monocle/Lib_2.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
final case class Box(value: Int) derives Foo
3 changes: 3 additions & 0 deletions tests/run-macros/i15485.fallout-monocle/Test_3.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
@main def Test =
val foo = summon[Foo[Box]].foo
assert(foo == 1, foo)