Skip to content

Commit 93f24a0

Browse files
authored
Merge pull request #10221 from dotty-staging/fix-#10129
Fix #10129: Fix comparisons of applied type aliases
2 parents a4ba3bd + 88dbba4 commit 93f24a0

File tree

2 files changed

+71
-21
lines changed

2 files changed

+71
-21
lines changed

Diff for: compiler/src/dotty/tools/dotc/core/TypeComparer.scala

+57-21
Original file line numberDiff line numberDiff line change
@@ -157,9 +157,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
157157

158158
/** Are we forbidden from recording GADT constraints? */
159159
private var frozenGadt = false
160-
private inline def inFrozenGadt[T](op: => T): T = {
160+
private inline def inFrozenGadt[T](inline op: T): T =
161+
inFrozenGadtIf(true)(op)
162+
163+
private inline def inFrozenGadtIf[T](cond: Boolean)(inline op: T): T = {
161164
val savedFrozenGadt = frozenGadt
162-
frozenGadt = true
165+
frozenGadt = cond
163166
try op finally frozenGadt = savedFrozenGadt
164167
}
165168

@@ -967,8 +970,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
967970
* corresponding arguments are subtypes relative to their variance (see `isSubArgs`).
968971
*/
969972
def isMatchingApply(tp1: Type): Boolean = tp1 match {
970-
case AppliedType(tycon1, args1) =>
971-
// We intentionally do not dealias `tycon1` or `tycon2` here.
973+
case tp1 as AppliedType(tycon1, args1) =>
974+
// We intentionally do not automatically dealias `tycon1` or `tycon2` here.
972975
// `TypeApplications#appliedTo` already takes care of dealiasing type
973976
// constructors when this can be done without affecting type
974977
// inference, doing it here would not only prevent code from compiling
@@ -977,6 +980,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
977980
//
978981
// Foo[?F, ?T] <:< Foo[[X] =>> (X, String), Int]
979982
//
983+
// where
984+
//
985+
// type Foo[F[_], T] = ErasedFoo[F[T]]
986+
//
980987
// Naturally, we'd like to infer:
981988
//
982989
// ?F := [X] => (X, String)
@@ -990,6 +997,25 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
990997
// ?F := [X] =>> (Int, X)
991998
//
992999
// Which is not what we wanted!
1000+
// On the other hand, we are not allowed to always stop at the present arguments either.
1001+
// An example is i10129.scala. Here, we have the following situation:
1002+
//
1003+
// type Lifted[A] = Err | A
1004+
// def point[O](o: O): Lifted[O] = o
1005+
// extension [O, U](o: Lifted[O]) def map(f: O => U): Lifted[U] = ???
1006+
// point("a").map(_ => if true then 1 else error)
1007+
//
1008+
// This leads to the constraint Lifted[U] <: Lifted[Int]. If we just
1009+
// check the arguments this gives `U <: Int`. But this is wrong. Dealiasing
1010+
// `Lifted` gives `Err | U <: Err | Int`, hence it should be `U <: Err | Int`.
1011+
//
1012+
// So it's a conundrum. We need to check the immediate arguments for hk type inference,
1013+
// but this could narrow the constraint too much. The solution is to also
1014+
// check the constraint arising from the dealiased subtype test
1015+
// in the case where isSubArgs adds a constraint. If that second constraint
1016+
// is weaker than the first, we keep it in place of the first.
1017+
// Note that if the isSubArgs test fails, we will proceed anyway by
1018+
// dealising by doing a compareLower.
9931019
def loop(tycon1: Type, args1: List[Type]): Boolean = tycon1 match {
9941020
case tycon1: TypeParamRef =>
9951021
(tycon1 == tycon2 ||
@@ -1016,10 +1042,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
10161042
}
10171043

10181044
val res = (
1019-
tycon1sym == tycon2sym
1020-
&& isSubPrefix(tycon1.prefix, tycon2.prefix)
1021-
|| byGadtBounds(tycon1sym, tycon2, fromAbove = true)
1022-
|| byGadtBounds(tycon2sym, tycon1, fromAbove = false)
1045+
tycon1sym == tycon2sym && isSubPrefix(tycon1.prefix, tycon2.prefix)
1046+
|| byGadtBounds(tycon1sym, tycon2, fromAbove = true)
1047+
|| byGadtBounds(tycon2sym, tycon1, fromAbove = false)
10231048
) && {
10241049
// There are two cases in which we can assume injectivity.
10251050
// First we check if either sym is a class.
@@ -1031,11 +1056,16 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
10311056
// must be instantiated, making the two tycons equal
10321057
val tyconIsInjective =
10331058
(tycon1sym.isClass || tycon2sym.isClass)
1034-
&& (if touchedGADTs then gadtIsInstantiated else true)
1035-
def checkSubArgs() = isSubArgs(args1, args2, tp1, tparams)
1036-
// we only record GADT constraints if *both* tycons are effectively injective
1037-
if (tyconIsInjective) checkSubArgs()
1038-
else inFrozenGadt { checkSubArgs() }
1059+
&& (!touchedGADTs || gadtIsInstantiated)
1060+
1061+
inFrozenGadtIf(!tyconIsInjective) {
1062+
if tycon1sym == tycon2sym && tycon1sym.isAliasType then
1063+
val preConstraint = constraint
1064+
isSubArgs(args1, args2, tp1, tparams)
1065+
&& tryAlso(preConstraint, recur(tp1.superType, tp2.superType))
1066+
else
1067+
isSubArgs(args1, args2, tp1, tparams)
1068+
}
10391069
}
10401070
if (res && touchedGADTs) GADTused = true
10411071
res
@@ -1544,19 +1574,25 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
15441574
* Method name comes from the notion that we are keeping a constraint which is sufficient to satisfy
15451575
* one of subtyping relationships.
15461576
*/
1547-
private def sufficientEither(op1: => Boolean, op2: => Boolean): Boolean = {
1577+
private def sufficientEither(op1: => Boolean, op2: => Boolean): Boolean =
15481578
val preConstraint = constraint
1549-
op1 && {
1579+
if op1 then tryAlso(preConstraint, op2) else op2
1580+
1581+
/** Check whether `op` generates a weaker constraint than the
1582+
* current constraint if we run it starting with `preConstraint`.
1583+
* If that's the case, replace the current constraint with the
1584+
* constraint generated by `op`.
1585+
*/
1586+
private def tryAlso(preConstraint: Constraint, op: => Boolean): true =
1587+
if constraint ne preConstraint then
1588+
// check whether `op2` generates a weaker constraint than `op1`
15501589
val leftConstraint = constraint
15511590
constraint = preConstraint
1552-
if (!(op2 && subsumes(leftConstraint, constraint, preConstraint))) {
1553-
if (constr != noPrinter && !subsumes(constraint, leftConstraint, preConstraint))
1591+
if !(op && subsumes(leftConstraint, constraint, preConstraint)) then
1592+
if constr != noPrinter && !subsumes(constraint, leftConstraint, preConstraint) then
15541593
constr.println(i"CUT - prefer $leftConstraint over $constraint")
15551594
constraint = leftConstraint
1556-
}
1557-
true
1558-
} || op2
1559-
}
1595+
true
15601596

15611597
/** Returns true iff the result of evaluating either `op1` or `op2` is true, keeping the smaller constraint if any.
15621598
* E.g., if

Diff for: tests/pos/i10129.scala

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
class Err
2+
3+
type Lifted[A] = Err | A
4+
5+
def point[O](o: O): Lifted[O] = o
6+
extension [O, U](o: Lifted[O]) def map(f: O => U): Lifted[U] = ???
7+
8+
val error: Err = Err()
9+
10+
def ok: Int | Err =
11+
point("a").map(_ => if true then 1 else error)
12+
13+
def fail: Lifted[Int] =
14+
point("a").map(_ => if true then 1 else error) // error

0 commit comments

Comments
 (0)