-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Description
Compiler version
3.1.2-RC2
Minimized code
Under certain conditions involving parameter unification, the GADT bounds will not get fully propagated.
In the following example, we have three type parameters X
, A
and B
, with bound A: >: X <: X
and B: <: Int
.
In the snippet, we first add the ordering B <: A
, then the ordering A <: B
.
When we add the ordering A <: B
, the upper bound <: Int
should be propagated to X
, since we have X <: A <: B <: Int
.
However, that is not the case. The bound is not propagated in the GADT solver, and we have to explicitly cast X
to A
to make use of the bound X <: Int
.
def test[X, A >: X <: X, B <: Int] = {
enum Expr[+T]:
case TagA() extends Expr[A]
case TagB() extends Expr[B]
import Expr._
def foo(e1: Expr[A], e2: Expr[B]) = e1 match {
case TagB() => // add GADT constr: B <: A
e2 match {
case TagA() =>
// add GADT constr: A <: B
// should propagate bound X (<: A <: B) <: Int for X.
val t0: X = ???
val t1: Int = t0 // error
val t2: Int = t0 : A // cast explicitly, works
case _ =>
}
case _ =>
}
}
The problem happens during the unification of type parameters. When adding the constraint A <: B
, the constraint handler checks that B <: A
already holds, and it will unify A
into B
.
Ideally, the handler should propagate the upper bound of B
(<: Int
) to the parameters known to be the subtype of A
(X
in our case). To do this, the handler will first query all parameters less than A
(except for those already known to be less than B
, to avoid propgating bounds repeatedly) with the exclusiveLower
function, then propagate the upper bounds of B
to these parameters.
The problem is that, in the current implementation, we call exclusiveLower(A, B)
after we call addLess(A, B)
. addLess(A, B)
will order all lower parameters to be lower than B
, which means that the result of exclusiveLower(A, B)
will be List(B)
instead of List(X, B)
.
To fix the problem we could call exclusiveLower
before we call addLess
.
Output
[info] running (fork) dotty.tools.dotc.Main -classpath /Users/linyxus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala-library/2.13.8/scala-library-2.13.8.jar:/Users/linyxus/Workspace/dotty/library/../out/bootstrap/scala3-library-bootstrapped/scala-3.1.3-RC1-bin-SNAPSHOT-nonbootstrapped/scala3-library_3-3.1.3-RC1-bin-SNAPSHOT.jar -color:never issues/gadt-unify.scala
-- [E007] Type Mismatch Error: issues/gadt-unify.scala:15:24 --------------------------------------------------------------------------------------------------------------------------------------------------------
15 | val t1: Int = t0 // error
| ^^
| Found: (t0 : X)
| Required: Int
|
| where: X is a type in method test which is an alias of B
|
| longer explanation available when compiling with `-explain`
1 error found
[error] Nonzero exit code returned from runner: 1
[error] (scala3-compiler / Compile / runMain) Nonzero exit code returned from runner: 1
[error] Total time: 2 s, completed Mar 21, 2022, 4:56:21 PM
Expectation
The 15th line should also work, without casting explicitly.