Skip to content

Commit fa06287

Browse files
committed
WIP: Fix aforementioned issue
1 parent bb52aa8 commit fa06287

File tree

5 files changed

+110
-26
lines changed

5 files changed

+110
-26
lines changed

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

Lines changed: 22 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -146,12 +146,13 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
146146
*/
147147
private [this] var leftRoot: Type = _
148148

149-
/** Are we forbidden from recording GADT constraints?
150-
*
151-
* This flag is set when we're already in [[Mode.GadtConstraintInference]],
152-
* to signify that we temporarily cannot record any GADT constraints.
153-
*/
149+
/** Are we forbidden from recording GADT constraints? */
154150
private var frozenGadt = false
151+
private inline def inFrozenGadt[T](op: => T): T = {
152+
val savedFrozenGadt = frozenGadt
153+
frozenGadt = true
154+
try op finally frozenGadt = savedFrozenGadt
155+
}
155156

156157
protected def isSubType(tp1: Type, tp2: Type, a: ApproxState): Boolean = {
157158
val savedApprox = approx
@@ -852,30 +853,31 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
852853
val tycon2sym = tycon2.symbol
853854

854855
var touchedGADTs = false
855-
def gadtBoundsContain(sym: Symbol, tp: Type): Boolean = {
856+
var gadtIsInstantiated = false
857+
def gadtBoundsContain(sym: Symbol, tp: Type, tpConSym: Symbol): Boolean = {
856858
touchedGADTs = true
857859
val b = gadtBounds(sym)
858-
b != null && inFrozenConstraint {
859-
(b.lo =:= tp) && (b.hi =:= tp)
860+
def boundsDescr = if b == null then "null" else b.show
861+
b != null && inFrozenGadt { isSubType(b.hi, tp) } && {
862+
gadtIsInstantiated = b.isInstanceOf[TypeAlias]
863+
true
860864
}
861865
}
862866

863867
val res = (
864-
tycon1sym == tycon2sym ||
865-
gadtBoundsContain(tycon1sym, tycon2) ||
866-
gadtBoundsContain(tycon2sym, tycon1)
867-
) &&
868-
isSubType(tycon1.prefix, tycon2.prefix) && {
868+
tycon1sym == tycon2sym
869+
&& isSubType(tycon1.prefix, tycon2.prefix)
870+
|| gadtBoundsContain(tycon1sym, tycon2, tycon2sym)
871+
|| gadtBoundsContain(tycon2sym, tycon1, tycon1sym)
872+
) && {
869873
// check both tycons to deal with the case when they are equal b/c of GADT constraint
870-
val tyconIsInjective = tycon1sym.isClass || tycon2sym.isClass
874+
val tyconIsInjective =
875+
(tycon1sym.isClass || tycon2sym.isClass)
876+
&& (if touchedGADTs then gadtIsInstantiated else true)
871877
def checkSubArgs() = isSubArgs(args1, args2, tp1, tparams)
872-
// we only record GADT constraints if tycon is guaranteed to be injective
878+
// we only record GADT constraints if *both* tycons are effectively injective
873879
if (tyconIsInjective) checkSubArgs()
874-
else {
875-
val savedFrozenGadt = frozenGadt
876-
frozenGadt = true
877-
try checkSubArgs() finally frozenGadt = savedFrozenGadt
878-
}
880+
else inFrozenGadt { checkSubArgs() }
879881
}
880882
if (res && touchedGADTs) GADTused = true
881883
res

tests/neg/gadt-uninjectivity.scala

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,18 +7,16 @@ object uninjectivity {
77
x // error
88
}
99

10-
def absurd2[F[_], G[_]](eq: EQ[F[Int], G[Int]], fi: F[Int], fs: F[String]): G[Int] = eq match {
10+
def absurd2[F[_], G[_]](eq: EQ[F[Int], G[Int]], fs: F[String]) = eq match {
1111
case Refl() =>
1212
val gs: G[String] = fs // error
13-
// fi
14-
???
13+
()
1514
}
1615

17-
def absurd3[F[_], G[_], X, Y](eq: EQ[F[X], G[Y]], fx: F[X]): G[Y] = eq match {
16+
def absurd3[F[_], G[_], X, Y](eq: EQ[F[X], G[Y]], fx: F[X]) = eq match {
1817
case Refl() =>
1918
val gx: G[X] = fx // error
2019
val fy: F[Y] = fx // error
21-
// fx
22-
???
20+
()
2321
}
2422
}

tests/neg/gadt-variant-hkt.scala

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
object test {
2+
3+
enum SUB[T, U] {
4+
case Refl[S]() extends SUB[S, S]
5+
}
6+
7+
// injective(G) & f[S] <: G[S] =X=> \forall t. f[t] <: Option[t]
8+
def foo[F[_]](fi: F[Int], sub: F[String] SUB Option[String]): Option[Int] =
9+
sub match {
10+
case SUB.Refl() =>
11+
fi // error
12+
}
13+
14+
// injective(G) & f[x] <: G[S] =X=> x <: S
15+
def bar[F[_], X](x: X, fi: F[Int], sub: F[X] SUB Option[Int]): Option[Int] =
16+
sub match {
17+
case SUB.Refl() =>
18+
val i: Int = x // error
19+
val y: X = (0: Int) // error
20+
fi // error
21+
}
22+
23+
enum KSUB[-F[_], +G[_]] {
24+
case Refl[S[_]]() extends KSUB[S, S]
25+
}
26+
27+
// injective(G) & f <: G & f[x] <: G[T] =X=> x <: T
28+
def baz[F[_], X](x: X, ksub: F KSUB Option, sub: F[X] SUB Option[Int]) =
29+
ksub match {
30+
case KSUB.Refl() =>
31+
sub match {
32+
case SUB.Refl() =>
33+
val i: Int = x // error
34+
val y: X = (0: Int) // error
35+
()
36+
}
37+
}
38+
39+
}

tests/pos/gadt-hkt-usage.scala

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
object test {
2+
class Foo[A]
3+
class Inv[M[_]]
4+
class InvFoo extends Inv[Foo]
5+
6+
object Test {
7+
def foo[F[_]](x: Inv[F]) = x match {
8+
case x: InvFoo =>
9+
val z: F[Int] = ??? : Foo[Int]
10+
case _ =>
11+
}
12+
}
13+
}

tests/pos/gadt-variant-hkt.scala

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
object test {
2+
3+
enum KSUB[-F[_], +G[_]] {
4+
case Refl[S[_]]() extends KSUB[S, S]
5+
}
6+
7+
trait Mkr[F[_]] {
8+
def mk[T](t: T): F[T]
9+
}
10+
11+
def foo[F[_]](mkr: Mkr[F], sub: F KSUB Option): Option[Int] =
12+
sub match {
13+
case KSUB.Refl() =>
14+
mkr.mk(0)
15+
}
16+
17+
enum SUB[T, U] {
18+
case Refl[S]() extends SUB[S, S]
19+
}
20+
21+
// f <: g & x <: T ==> f[x] <: g[T]
22+
def bar[F[_], G[_], X](fx: F[X], ksub: F KSUB G, sub: X SUB Int) =
23+
ksub match {
24+
case _: KSUB.Refl[s] =>
25+
sub match {
26+
case SUB.Refl() =>
27+
val gi: G[Int] = fx : s[X]
28+
()
29+
}
30+
}
31+
32+
}

0 commit comments

Comments
 (0)