Skip to content

Commit

Permalink
remove limitation errors in testcases
Browse files Browse the repository at this point in the history
Thanks to the path-dependent GADT reasoning logic, these limitation errors can
be dropped from the testcases. See scala#14754.
  • Loading branch information
Linyxus committed Jul 22, 2022
1 parent e81d8f2 commit 26367f5
Show file tree
Hide file tree
Showing 5 changed files with 18 additions and 22 deletions.
14 changes: 6 additions & 8 deletions tests/neg/structural-gadt.scala
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
// This file is part of tests for inferring GADT constraints from type members,
// which needed to be reverted because of soundness issues.
//
// Lines with "// limitation" are the ones that we could soundly allow.
// This file is part of tests for inferring GADT constraints from type members.
// They are now supported by path-dependent GADT reasoning. See #14754.
object Test {

trait Expr { type T }
Expand All @@ -11,19 +9,19 @@ object Test {
def foo[A](e: Expr { type T = A }) = e match {
case _: IntLit =>
val a: A = 0 // error
val i: Int = ??? : A // limitation // error
val i: Int = ??? : A

case _: Expr { type T <: Int } =>
val a: A = 0 // error
val i: Int = ??? : A // limitation // error
val i: Int = ??? : A

case _: IntExpr =>
val a: A = 0
val i: Int = ??? : A // limitation // error
val i: Int = ??? : A

case _: Expr { type T = Int } =>
val a: A = 0
val i: Int = ??? : A // limitation // error
val i: Int = ??? : A
}

def bar[A](e: Expr { type T <: A }) = e match {
Expand Down
4 changes: 2 additions & 2 deletions tests/neg/structural-recursive-both1-gadt.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// This file is part of tests for inferring GADT constraints from type members,
// which needed to be reverted because of soundness issues.
// This file is part of tests for inferring GADT constraints from type members.
// They are now supported by path-dependent GADT reasoning. See #14754.
//
// Lines with "// limitation" are the ones that we could soundly allow.
object Test {
Expand Down
4 changes: 2 additions & 2 deletions tests/neg/structural-recursive-both2-gadt.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// This file is part of tests for inferring GADT constraints from type members,
// which needed to be reverted because of soundness issues.
// This file is part of tests for inferring GADT constraints from type members.
// They are now supported by path-dependent GADT reasoning. See #14754.
//
// Lines with "// limitation" are the ones that we could soundly allow.
object Test {
Expand Down
14 changes: 6 additions & 8 deletions tests/neg/structural-recursive-pattern-gadt.scala
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
// This file is part of tests for inferring GADT constraints from type members,
// which needed to be reverted because of soundness issues.
//
// Lines with "// limitation" are the ones that we could soundly allow.
// This file is part of tests for inferring GADT constraints from type members.
// They are now supported by path-dependent GADT reasoning. See #14754.
object Test {

trait Expr { type T }
Expand All @@ -28,23 +26,23 @@ object Test {
def foo[A](e: ExprExact[A]) = e match {
case _: IndirectIntLit =>
val a: A = 0 // error
val i: Int = ??? : A // limitation // error
val i: Int = ??? : A

case _: IndirectExprSub[Int] =>
val a: A = 0 // error
val i: Int = ??? : A // limitation // error
val i: Int = ??? : A

case _: IndirectExprSub2[Int] =>
val a: A = 0 // error
val i: Int = ??? : A // limitation // error
val i: Int = ??? : A

case _: IndirectIntExpr =>
val a: A = 0
val i: Int = ??? : A

case _: IndirectExprExact[Int] =>
val a: A = 0
val i: Int = ??? : A // limitation // error
val i: Int = ??? : A
}

def bar[A](e: ExprSub[A]) = e match {
Expand Down
4 changes: 2 additions & 2 deletions tests/neg/structural-recursive-scrutinee-gadt.scala
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// This file is part of tests for inferring GADT constraints from type members,
// which needed to be reverted because of soundness issues.
// This file is part of tests for inferring GADT constraints from type members.
// They are now supported by path-dependent GADT reasoning. See #14754.
//
// Lines with "// limitation" are the ones that we could soundly allow.
object Test {
Expand Down

0 comments on commit 26367f5

Please sign in to comment.