Skip to content

Commit ea52ba8

Browse files
committed
Avoid direct Skolem types in GADT bounds
By constraining T s.t. T <: Sko(U) and T <: Sko(U), we end up with T <: Sko(U) & Sko(U), which is a singleton type intersection and is simplified to T <: U, which is just plain wrong for this case. To avoid this, we record only the _consequence_ of having a Skolem type in a bound. This is a temporary workaround while we cannot take unions and intersections of singleton types and should be removed in the future.
1 parent 6bfd47e commit ea52ba8

File tree

3 files changed

+36
-0
lines changed

3 files changed

+36
-0
lines changed

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

+15
Original file line numberDiff line numberDiff line change
@@ -779,6 +779,21 @@ object Contexts {
779779
}, gadts)
780780
}
781781

782+
// avoid recording skolems in bounds
783+
// recording two skolem bounds results in an union/intersection, which is then simplified
784+
// T <: Sko(U) & Sko(U) is simplified to T <: U, which is simply wrong
785+
// instead, we only ensure that new bounds would be satisfiable
786+
// TODO: this almost certainly causes unsoundess
787+
// TODO: it should be removed after we added support for singleton type unions/intersections
788+
bound match {
789+
case _: SkolemType =>
790+
val TypeBounds(lo, hi) = bounds(sym)
791+
val (newLo, newHi) = if (isUpper) (lo, hi & bound) else (lo | bound, hi)
792+
gadts.println(i"replacing skolem bound $sym <:< $bound with $newLo <:< $newHi")
793+
return newLo <:< newHi
794+
case _ => ;
795+
}
796+
782797
val symTvar: TypeVar = stripInternalTypeVar(tvar(sym)) match {
783798
case tv: TypeVar => tv
784799
case inst =>

tests/neg/int-extractor.scala

+14
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,24 @@ object Test {
88
0 // error
99
}
1010

11+
def foo2[T](t: T): T = t match {
12+
case EssaInt(_) => t match {
13+
case EssaInt(_) =>
14+
0 // error
15+
}
16+
}
17+
1118
case class Inv[T](t: T)
1219

1320
def bar1[T](t: T): T = Inv(t) match {
1421
case Inv(EssaInt(_)) =>
1522
0 // error
1623
}
24+
25+
def bar2[T](t: T): T = t match {
26+
case Inv(EssaInt(_)) => t match {
27+
case Inv(EssaInt(_)) =>
28+
0 // error
29+
}
30+
}
1731
}

tests/neg/invariant-gadt.scala

+7
Original file line numberDiff line numberDiff line change
@@ -17,4 +17,11 @@ object `invariant-gadt` {
1717
0 // error
1818
}
1919
}
20+
21+
def unsoundTwice[T](t: T): T = Invariant(t) match {
22+
case Invariant(_: Int) => Invariant(t) match {
23+
case Invariant(_: Int) =>
24+
0 // error
25+
}
26+
}
2027
}

0 commit comments

Comments
 (0)