Skip to content

Commit db38c33

Browse files
committed
Fix bias in ConstraintHandling#subsumes
1 parent 42b622c commit db38c33

9 files changed

+197
-3
lines changed

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -345,7 +345,7 @@ trait ConstraintHandling[AbstractContext] {
345345
else {
346346
val saved = constraint
347347
try
348-
c2.forallParams(p =>
348+
pre.forallParams(p =>
349349
c1.contains(p) &&
350350
c2.upper(p).forall(c1.isLess(p, _)) &&
351351
isSubTypeWhenFrozen(c1.nonParamBounds(p), c2.nonParamBounds(p)))

tests/buffer.scala

+38
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
object buffer {
2+
// def bar[T, TT >: T <: T, U](tt: TT): TT = {
3+
// val u: U = ???
4+
// (0 : Int) match {
5+
// case _: u.type =>
6+
// val i: Int = (??? : U) // error
7+
// // morally not an error
8+
// // val i2: Int = u
9+
// tt
10+
// }
11+
// }
12+
13+
enum SUB[A, +B] { case Refl[T]() extends SUB[T, T] }
14+
15+
def baz[T](t: T, sub1: 5 SUB T, sub2: 6 SUB T): T = {
16+
(sub1, sub2) match {
17+
case (SUB.Refl(), SUB.Refl()) =>
18+
val _t: T = (5 : 5)
19+
???
20+
}
21+
}
22+
23+
// def bazfoo[T](t: T, sub1: 5 SUB T, sub2: 6 SUB T, sub3: String SUB T): T = {
24+
// (sub1, sub2, sub3) match {
25+
// case (SUB.Refl(), SUB.Refl(), SUB.Refl()) =>
26+
// val _t: T = (5 : 5)
27+
// ???
28+
// }
29+
// }
30+
31+
// def bazbar[T](t: T, sub1: String SUB T, sub2: 5 SUB T, sub3: 6 SUB T): T = {
32+
// (sub1, sub2, sub3) match {
33+
// case (SUB.Refl(), SUB.Refl(), SUB.Refl()) =>
34+
// val _t: T = (5 : 5)
35+
// ???
36+
// }
37+
// }
38+
}

tests/buffer2.scala

+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
object buffer2 {
2+
class SubInt[T <: Int]
3+
type SubIntStruct = { type Z <: Int }
4+
5+
object Unapp {
6+
def unapply[T <: Int & String](t: SubInt[T]): Boolean = false
7+
}
8+
9+
def foo[A](a: A) = a match {
10+
case Unapp() => 0
11+
}
12+
13+
def bar = "abc" match {
14+
case (1, 2) => 0
15+
case _ => 1
16+
}
17+
18+
def baz(list: List[String] | List[Int]) = list match {
19+
case (x : String) :: xs =>
20+
val xs2: List[String] = xs
21+
()
22+
case (x : Int) :: xs =>
23+
val xs2: List[Int] = xs
24+
()
25+
case Nil =>
26+
()
27+
}
28+
}

tests/buffer3.scala

+41
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
/** Natural transformation. */
2+
trait ~>[F[_], G[_]] {
3+
def apply[A](fa: F[A]): G[A]
4+
}
5+
6+
/** Higher-kinded pattern functor typeclass. */
7+
trait HFunctor[H[f[_], i]] {
8+
def hmap[A[_], B[_]](nt: A ~> B): ([x] => H[A,x]) ~> ([x] => H[B,x])
9+
}
10+
11+
/** Some HK pattern functor. */
12+
// enum ExprF[R[_],I] {
13+
// case Const[R[_]](i: Int) extends ExprF[R,Int]
14+
// case Neg[R[_]](l: R[Int]) extends ExprF[R,Int]
15+
// case Eq[R[_]](l: R[Int], r: R[Int]) extends ExprF[R,Boolean]
16+
// }
17+
18+
sealed trait ExprF[R[_],I]
19+
final case class Const[R[_]](i: Int) extends ExprF[R,Int]
20+
final case class Foo[T](t: T) extends ExprF[Option, T]
21+
final case class Neg[R[_]](l: R[Int]) extends ExprF[R,Int]
22+
final case class Eq[R[_]](l: R[Int], r: R[Int]) extends ExprF[R,Boolean]
23+
24+
object X {
25+
val x = (??? : Neg[Option])._1
26+
}
27+
28+
/** Companion. */
29+
object ExprF {
30+
implied hfunctor for HFunctor[ExprF] {
31+
def hmap[A[_], B[_]](nt: A ~> B): ([x] => ExprF[A,x]) ~> ([x] => ExprF[B,x]) = {
32+
new ~>[[x] => ExprF[A,x], [x] => ExprF[B,x]] {
33+
def apply[I](fa: ExprF[A,I]): ExprF[B,I] = fa match {
34+
case Const(i) => Const(i)
35+
case Neg(l) => Neg(nt(l))
36+
case Eq(l, r) => Eq(nt(l), nt(r))
37+
}
38+
}
39+
}
40+
}
41+
}

tests/buffer4.scala

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
object Test {
2+
sealed trait Nat
3+
case class Zero() extends Nat
4+
case class Succ[N <: Nat](pred: N) extends Nat
5+
6+
sealed trait Vec[A, N <: Nat]
7+
case class Cons[A, N <: Nat](head: A, tail: Vec[A, N]) extends Vec[A, Succ[N]]
8+
case class Nil[A]() extends Vec[A, Zero]
9+
10+
def size[A, N <: Nat](xs: Vec[A, N]): N =
11+
xs match {
12+
case xs: Nil[A] => Zero()
13+
case xs: Cons[A, m] => Succ(size(xs.tail))
14+
}
15+
16+
def replicate[A, N <: Nat & Product](n: N, a: A): Vec[A, N] =
17+
n match {
18+
case n: Zero => Nil[A]()
19+
case n: Succ[m] => Cons[A, m](a, replicate(n.pred, a))
20+
}
21+
}

tests/bufferR.scala

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
object Regions {
2+
class Region
3+
4+
class Cell[A, R <: Region](init: A) {
5+
private[this] var store: A = init
6+
def update(a: A) given R: Unit = store = a
7+
def apply() given R: A = store
8+
}
9+
10+
def cell[A](init: A) given (r: Region): Cell[A, r.type] =
11+
new Cell[A, r.type](init)
12+
13+
def enter[T](thunk: given Region => T): T = {
14+
thunk given new Region
15+
}
16+
}

tests/candidate.scala

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
object Test {
2+
def bar[U](u: U): U =
3+
(0 : Int) match {
4+
case _: u.type =>
5+
val i: Int = (??? : U) // error
6+
// morally not an error
7+
// val i2: Int = u
8+
U
9+
}
10+
11+
enum SUB[A, +B] { case Refl[T]() extends SUB[T, T] }
12+
13+
def baz[T](t: T, sub1: 5 SUB T, sub2: 6 SUB T): T = {
14+
(sub1, sub2) match {
15+
case (SUB.Refl(), SUB.Refl()) =>
16+
val _t: T = (5 : 5)
17+
???
18+
}
19+
}
20+
21+
def bazfoo[T](t: T, sub1: 5 SUB T, sub2: 6 SUB T, sub3: String SUB T): T = {
22+
(sub1, sub2, sub3) match {
23+
case (SUB.Refl(), SUB.Refl(), SUB.Refl()) =>
24+
val _t: T = (5 : 5)
25+
???
26+
}
27+
}
28+
29+
def bazbar[T](t: T, sub1: String SUB T, sub2: 5 SUB T, sub3: 6 SUB T): T = {
30+
(sub1, sub2, sub3) match {
31+
case (SUB.Refl(), SUB.Refl(), SUB.Refl()) =>
32+
val _t: T = (5 : 5)
33+
???
34+
}
35+
}
36+
}

tests/destructuring-var.scala

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
object `destructuring-var` {
2+
var Some(z) = Some(0)
3+
var a :: b :: Nil = 1 :: 2 :: Nil
4+
}

tests/neg/overconstrained-type-variables-gadt.scala

+12-2
Original file line numberDiff line numberDiff line change
@@ -2,16 +2,26 @@ object Test {
22
trait T1[A] { def a: A }
33
trait T2[B] { def b: B }
44

5-
def foo[X, Y](u: T1[X] | T2[Y]): X = u match {
5+
def foo[X, Y](v: T1[X] | T2[Y]): X = v match {
66
case t1: T1[t] =>
77
// consider: foo[Int, String](new T1[String] with T2[String] { ... })
88
t1.a // error
99
}
1010

1111
class T1Int extends T1[Int] { def a = 0 }
12-
def bar[X, Y](u: T1[X] | T2[Y]): X = u match {
12+
def bar[X, Y](v: T1[X] | T2[Y]): X = v match {
1313
case t1: T1Int =>
1414
// similar reasoning to above applies
1515
t1.a // error
1616
}
17+
18+
class T1IntT2String extends T1[Int] with T2[String] {
19+
def a = 0
20+
def b = ""
21+
}
22+
def baz[X](v: T1[X] | T2[X]): Unit = v match {
23+
case _: T1IntT2String =>
24+
val x1: X = 0 // error
25+
val x2: X = "" // error
26+
}
1727
}

0 commit comments

Comments
 (0)