Skip to content

Commit 2ebf2d0

Browse files
committed
Avoid direct Skolem types in lower 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 union and is simplified to T >: U, which is 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 c5286a6 commit 2ebf2d0

File tree

3 files changed

+36
-0
lines changed

3 files changed

+36
-0
lines changed

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -822,6 +822,21 @@ object Contexts {
822822
}, gadts)
823823
}
824824

825+
// avoid recording skolems in lower bounds
826+
// recording two skolem bounds results in an union, which is then simplified
827+
// T >: Sko(U) | Sko(U) is simplified to T >: U, which is simply wrong
828+
// instead, we only ensure that new bounds would be satisfiable
829+
// TODO: this likely causes unsoundness
830+
// TODO: it should be removed after we added support for singleton type unions
831+
if (!isUpper) bound match {
832+
case _: SkolemType =>
833+
val TypeBounds(lo, hi) = bounds(sym)
834+
val newLo = lo | bound
835+
gadts.println(i"replacing skolem bound $sym <:< $bound with $newLo <:< $hi")
836+
return newLo <:< hi
837+
case _ => ;
838+
}
839+
825840
val symTvar: TypeVar = stripInternalTypeVar(tvar(sym)) match {
826841
case tv: TypeVar => tv
827842
case inst =>

tests/neg/int-extractor.scala

Lines changed: 14 additions & 0 deletions
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

Lines changed: 7 additions & 0 deletions
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)