Skip to content

Fix i11545 #12087

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 2 commits into from
Closed
Show file tree
Hide file tree
Changes from 1 commit
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
23 changes: 15 additions & 8 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -736,14 +736,21 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
fourthTry
}

def tryBaseType(cls2: Symbol) = {
val base = nonExprBaseType(tp1, cls2)
if (base.exists && (base `ne` tp1))
isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow) ||
base.isInstanceOf[OrType] && fourthTry
// if base is a disjunction, this might have come from a tp1 type that
// expands to a match type. In this case, we should try to reduce the type
// and compare the redux. This is done in fourthTry
def tryBaseType(cls2: Symbol): Boolean = {
Copy link
Contributor

Choose a reason for hiding this comment

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

This looks like it will overshoot. tryBaseType is an essential element for comparisons. Simply ignoring this step under GADT constraint inference is too drastic. I would expect instead a necessaryEither somewhere in the logic.

Copy link
Contributor Author

@abgruszecki abgruszecki Apr 15, 2021

Choose a reason for hiding this comment

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

We only avoid tryBaseType if the LHS is an AndType. In that case, using the base type can end up performing a comparison that is too approximate to be useful for GADTs (see neg/i11545a.scala, added in this PR). I have ideas for other fixes, we can discuss them during today's lab meeting.

// nonExprBaseType approximates its result in ways that are unsound for GADTs
// when it handles intersections. See neg/i11545a.scala for a specific example.
// Note that we can't simply freeze GADTs at this point. PatternTypeConstrainer
// passes a Skolem here and we _need_ to calculate its base type. Only intersection
// types are a problem.
if !(ctx.mode.is(Mode.GadtConstraintInference) && tp1.isInstanceOf[AndType]) then
val base = nonExprBaseType(tp1, cls2)
if (base.exists && (base `ne` tp1))
isSubType(base, tp2, if (tp1.isRef(cls2)) approx else approx.addLow) ||
base.isInstanceOf[OrType] && fourthTry
// if base is a disjunction, this might have come from a tp1 type that
// expands to a match type. In this case, we should try to reduce the type
// and compare the redux. This is done in fourthTry
else fourthTry
else fourthTry
}

Expand Down
13 changes: 13 additions & 0 deletions tests/neg/i11545.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
@main def test: Unit = {
trait S[A]
trait Inv[A]

class P[X] extends S[Inv[X] & Inv[String]]

def patmat[A, Y](s: S[Inv[A] & Y]): A = s match {
case p: P[x] =>
"Hello" // error
}

val got: Int = patmat[Int, Inv[String]](new P) // ClassCastException: String cannot be cast to Integer
}
20 changes: 20 additions & 0 deletions tests/neg/i11545a.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
@main def test: Unit = {
trait Inv[A]

trait S[+A]
final class P[+X] extends S[Inv[String] & X]


def patmat[A](s: S[Inv[A]]): A = s match {
// When inferring the GADT cstr here, we need to infer cstr following from:
// Inv[String] & a <: Inv[A]
// We end up invoking nonExprBaseType(`Inv[String] & a`, `Inv`),
// which returns just `Inv[String]`. After that we approximate with:
// Inv[String] <: Inv[A]
// Which is simply wrong.
case p: P[a] => "Hello" // error
}

val i: Int = patmat[Int](P[Inv[Int]]())
i
}