Skip to content

Commit a324502

Browse files
smartersmarter
authored
Merge pull request #8522 from dotty-staging/fix-#8431
Fix #8431 (Make HKT GADT constraints actually work)
2 parents 1b70a14 + 146c453 commit a324502

File tree

8 files changed

+175
-30
lines changed

8 files changed

+175
-30
lines changed

‎compiler/src/dotty/tools/dotc/core/GadtConstraint.scala‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,7 @@ final class ProperGadtConstraint private(
124124

125125
// The replaced symbols are picked up here.
126126
addToConstraint(poly1, tvars)
127-
.reporting(i"added to constraint: $params%, %\n$debugBoundsDescription", gadts)
127+
.reporting(i"added to constraint: [$poly1] $params%, %\n$debugBoundsDescription", gadts)
128128
}
129129

130130
override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = {
@@ -237,8 +237,11 @@ final class ProperGadtConstraint private(
237237
}
238238

239239
override def fullUpperBound(param: TypeParamRef)(implicit ctx: Context): Type =
240-
constraint.minUpper(param).foldLeft(nonParamBounds(param).hi) {
241-
(t, u) => t & externalize(u)
240+
constraint.minUpper(param).foldLeft(nonParamBounds(param).hi) { (t, u) =>
241+
val eu = externalize(u)
242+
// Any as the upper bound means "no bound", but if F is higher-kinded,
243+
// Any & F = F[_]; this is wrong for us so we need to short-circuit
244+
if t.isAny then eu else t & eu
242245
}
243246

244247
// ---- Private ----------------------------------------------------------

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

Lines changed: 32 additions & 21 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
@@ -839,30 +840,40 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
839840
val tycon2sym = tycon2.symbol
840841

841842
var touchedGADTs = false
842-
def gadtBoundsContain(sym: Symbol, tp: Type): Boolean = {
843+
var gadtIsInstantiated = false
844+
def byGadtBounds(sym: Symbol, tp: Type, fromAbove: Boolean): Boolean = {
843845
touchedGADTs = true
844846
val b = gadtBounds(sym)
845-
b != null && inFrozenConstraint {
846-
(b.lo =:= tp) && (b.hi =:= tp)
847+
def boundsDescr = if b == null then "null" else b.show
848+
b != null && inFrozenGadt {
849+
if fromAbove then isSubType(b.hi, tp) else isSubType(tp, b.lo)
850+
} && {
851+
gadtIsInstantiated = b.isInstanceOf[TypeAlias]
852+
true
847853
}
848854
}
849855

850856
val res = (
851-
tycon1sym == tycon2sym ||
852-
gadtBoundsContain(tycon1sym, tycon2) ||
853-
gadtBoundsContain(tycon2sym, tycon1)
854-
) &&
855-
isSubType(tycon1.prefix, tycon2.prefix) && {
856-
// check both tycons to deal with the case when they are equal b/c of GADT constraint
857-
val tyconIsInjective = tycon1sym.isClass || tycon2sym.isClass
857+
tycon1sym == tycon2sym
858+
&& isSubType(tycon1.prefix, tycon2.prefix)
859+
|| byGadtBounds(tycon1sym, tycon2, fromAbove = true)
860+
|| byGadtBounds(tycon2sym, tycon1, fromAbove = false)
861+
) && {
862+
// There are two cases in which we can assume injectivity.
863+
// First we check if either sym is a class.
864+
// Then:
865+
// 1) if we didn't touch GADTs, then both symbols are the same
866+
// (b/c of an earlier condition) and both are the same class
867+
// 2) if we touched GADTs, then the _other_ symbol (class syms
868+
// cannot have GADT constraints), the one w/ GADT cstrs,
869+
// must be instantiated, making the two tycons equal
870+
val tyconIsInjective =
871+
(tycon1sym.isClass || tycon2sym.isClass)
872+
&& (if touchedGADTs then gadtIsInstantiated else true)
858873
def checkSubArgs() = isSubArgs(args1, args2, tp1, tparams)
859-
// we only record GADT constraints if tycon is guaranteed to be injective
874+
// we only record GADT constraints if *both* tycons are effectively injective
860875
if (tyconIsInjective) checkSubArgs()
861-
else {
862-
val savedFrozenGadt = frozenGadt
863-
frozenGadt = true
864-
try checkSubArgs() finally frozenGadt = savedFrozenGadt
865-
}
876+
else inFrozenGadt { checkSubArgs() }
866877
}
867878
if (res && touchedGADTs) GADTused = true
868879
res

‎tests/neg/gadt-injectivity-alt.scala‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
object test {
2+
3+
enum SUB[-F, +G] {
4+
case Refl[S]() extends SUB[S, S]
5+
}
6+
7+
enum KSUB[-F[_], +G[_]] {
8+
case Refl[S[_]]() extends KSUB[S, S]
9+
}
10+
11+
def foo[F[_], G[_], A](
12+
keq: (F KSUB Option, Option KSUB F),
13+
ksub: Option KSUB G,
14+
sub: F[A] SUB G[Int],
15+
a: A
16+
) =
17+
keq._1 match { case KSUB.Refl() =>
18+
keq._2 match { case KSUB.Refl() =>
19+
ksub match { case KSUB.Refl() =>
20+
sub match { case SUB.Refl() =>
21+
// f = Option
22+
// & g >: Option
23+
// & f[a] <: g[I]
24+
// =X=>
25+
// a <: I
26+
// counterexample: g = [t] => Any
27+
val i: Int = a // error
28+
()
29+
}
30+
}
31+
}
32+
}
33+
}

‎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-hk-ordering.scala‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
object test {
2+
3+
enum KSUB[-F[_], +G[_]] {
4+
case Refl[S[_]]() extends KSUB[S, S]
5+
}
6+
7+
def foo[F[_]](ksub: Option KSUB F) =
8+
ksub match {
9+
case KSUB.Refl() =>
10+
// we have (s is type parameter of KSUB.Refl):
11+
// f >: Option
12+
// s <: f
13+
val fi: F[Int] = Option(0)
14+
()
15+
}
16+
}

‎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)