Description
Compiler version
3.1.2-RC2
Minimized code
trait T1
trait T2 extends T1
trait Expr[T] { val data: T = ??? }
case class Tag2() extends Expr[T2]
def flag: Boolean = ???
def foo[T](e: Expr[T]): T1 = e match {
case Tag2() =>
if flag then
new T2 {}
else
e.data
}
It seems that the cause of the problem is that we did not insert GADT casting properly. The compiler complains that the type of the if
expression from the typer (T2
) differs from that derived by the checker (T2 | (e.data : T) & T1
).
The if
tree after the typer looks like:
if flag then
{
final class $anon() extends Object(), T2 {}
new $anon():T2
}
else e.data.$asInstanceOf[(e.data : T) & T1]
We insert the casting asInstanceOf[(e.data : T) & T1]
because we try to adapt e.data
to type T1
and find that we used GADT constraints to type this. However, when assigning the type of the if
expression, the type assigner will compute lub
of T2
and (e.data : T) & T1
to get the simplified type T2
, which also relies on the GADT constraint T <: T2
. Therefore, to assign type T2
to the if
expression, we also have to insert GADT casting somewhere, which is missing for now.
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 -Ycheck:all -Xprint:typer issues/gadt-adapt.scala
[[syntax trees at end of typer]] // issues/gadt-adapt.scala
package <empty> {
trait T1() extends Object {}
trait T2() extends Object, T1 {}
trait Expr[T >: Nothing <: Any]() extends Object {
T
val data: Expr.this.T = ???
}
case class Tag2() extends Object(), Expr[T2], _root_.scala.Product, _root_.scala.Serializable {
def copy(): Tag2 = new Tag2()
}
final lazy module val Tag2: Tag2 = new Tag2()
final module class Tag2() extends AnyRef() { this: Tag2.type =>
def apply(): Tag2 = new Tag2()
def unapply(x$1: Tag2): true.type = true
override def toString: String = "Tag2"
}
final lazy module val gadt-adapt$package: gadt-adapt$package = new gadt-adapt$package()
final module class gadt-adapt$package() extends Object() { this: gadt-adapt$package.type =>
def flag: Boolean = ???
def foo[T >: Nothing <: Any](e: Expr[T]): T1 =
e match
{
case Tag2():Tag2 =>
if flag then
{
final class $anon() extends Object(), T2 {}
new $anon():T2
}
else e.data.$asInstanceOf[(e.data : T) & T1]
}
}
}
checking issues/gadt-adapt.scala after phase typer
exception while typing {
if flag then
{
final class $anon() extends Object(), T2 {}
new $anon():T2
}
else e.data.$asInstanceOf[(e.data : T) & T1]
} of class class dotty.tools.dotc.ast.Trees$Block # -1
exception while typing e match
{
case Tag2():Tag2 =>
if flag then
{
final class $anon() extends Object(), T2 {}
new $anon():T2
}
else e.data.$asInstanceOf[(e.data : T) & T1]
} of class class dotty.tools.dotc.ast.Trees$Match # -1
exception while typing def foo[T >: Nothing <: Any](e: Expr[T]): T1 =
e match
{
case Tag2():Tag2 =>
if flag then
{
final class $anon() extends Object(), T2 {}
new $anon():T2
}
else e.data.$asInstanceOf[(e.data : T) & T1]
} of class class dotty.tools.dotc.ast.Trees$DefDef # -1
exception while typing final module class gadt-adapt$package() extends Object() { this: gadt-adapt$package.type =>
def flag: Boolean = ???
def foo[T >: Nothing <: Any](e: Expr[T]): T1 =
e match
{
case Tag2():Tag2 =>
if flag then
{
final class $anon() extends Object(), T2 {}
new $anon():T2
}
else e.data.$asInstanceOf[(e.data : T) & T1]
}
} of class class dotty.tools.dotc.ast.Trees$TypeDef # -1
exception occurred while compiling issues/gadt-adapt.scala
exception while typing package <empty> {
trait T1() extends Object {}
trait T2() extends Object, T1 {}
trait Expr[T >: Nothing <: Any]() extends Object {
T
val data: Expr.this.T = ???
}
case class Tag2() extends Object(), Expr[T2], _root_.scala.Product, _root_.scala.Serializable {
def copy(): Tag2 = new Tag2()
}
final lazy module val Tag2: Tag2 = new Tag2()
final module class Tag2() extends AnyRef() { this: Tag2.type =>
def apply(): Tag2 = new Tag2()
def unapply(x$1: Tag2): true.type = true
override def toString: String = "Tag2"
}
final lazy module val gadt-adapt$package: gadt-adapt$package = new gadt-adapt$package()
final module class gadt-adapt$package() extends Object() { this: gadt-adapt$package.type =>
def flag: Boolean = ???
def foo[T >: Nothing <: Any](e: Expr[T]): T1 =
e match
{
case Tag2():Tag2 =>
if flag then
{
final class $anon() extends Object(), T2 {}
new $anon():T2
}
else e.data.$asInstanceOf[(e.data : T) & T1]
}
}
} of class class dotty.tools.dotc.ast.Trees$PackageDef # -1
*** error while checking issues/gadt-adapt.scala after phase typer ***
Exception in thread "main" java.lang.AssertionError: assertion failed: Types differ
Original type : T2
After checking: T2 | (e.data : T) & T1
Original tree : if flag then
{
final class $anon() extends Object(), T2 {}
new $anon():T2
}
else e.data.$asInstanceOf[(e.data : T) & T1]
After checking: if flag then
{
final class $anon() extends Object(), T2 {}
new $anon():T2
}
else e.data.$asInstanceOf[(e.data : T) & T1]
Why different :
Subtype trace:
==> T2 | (e.data : T) & T1 <: T2
==> T2 | T & T1 <: T2 in frozen constraint
==> T2 <: T2 in frozen constraint
<== T2 <: T2 in frozen constraint = true
==> T & T1 <: T2 in frozen constraint
==> glb(<notype>, <notype>)
<== glb(<notype>, <notype>) = <notype>
==> T <: T2 in frozen constraint
==> Any <: T2 (left is approximated) in frozen constraint
<== Any <: T2 (left is approximated) in frozen constraint = false
==> Any <: T2 in frozen constraint
<== Any <: T2 in frozen constraint = false
<== T <: T2 in frozen constraint = false
==> T1 <: T2 in frozen constraint
<== T1 <: T2 in frozen constraint = false
<== T & T1 <: T2 in frozen constraint = false
==> T1 <: T2 in frozen constraint
<== T1 <: T2 in frozen constraint = false
<== T2 | T & T1 <: T2 in frozen constraint = false
==> T2 <: T2
<== T2 <: T2 = true
==> (e.data : T) & T1 <: T2
==> glb(<notype>, <notype>)
<== glb(<notype>, <notype>) = <notype>
==> (e.data : T) <: T2
==> T <: T2 (left is approximated)
==> Any <: T2 (left is approximated)
<== Any <: T2 (left is approximated) = false
==> Any <: T2 in frozen constraint
<== Any <: T2 in frozen constraint = false
<== T <: T2 (left is approximated) = false
<== (e.data : T) <: T2 = false
==> T1 <: T2
<== T1 <: T2 = false
<== (e.data : T) & T1 <: T2 = false
==> T1 <: T2
<== T1 <: T2 = false
<== T2 | (e.data : T) & T1 <: T2 = false while compiling issues/gadt-adapt.scala
java.lang.AssertionError: assertion failed: Types differ
Original type : T2
After checking: T2 | (e.data : T) & T1
Original tree : if flag then
{
final class $anon() extends Object(), T2 {}
new $anon():T2
}
else e.data.$asInstanceOf[(e.data : T) & T1]
After checking: if flag then
{
final class $anon() extends Object(), T2 {}
new $anon():T2
}
else e.data.$asInstanceOf[(e.data : T) & T1]
Why different :
Subtype trace:
==> T2 | (e.data : T) & T1 <: T2
==> T2 | T & T1 <: T2 in frozen constraint
==> T2 <: T2 in frozen constraint
<== T2 <: T2 in frozen constraint = true
==> T & T1 <: T2 in frozen constraint
==> glb(<notype>, <notype>)
<== glb(<notype>, <notype>) = <notype>
==> T <: T2 in frozen constraint
==> Any <: T2 (left is approximated) in frozen constraint
<== Any <: T2 (left is approximated) in frozen constraint = false
==> Any <: T2 in frozen constraint
<== Any <: T2 in frozen constraint = false
<== T <: T2 in frozen constraint = false
==> T1 <: T2 in frozen constraint
<== T1 <: T2 in frozen constraint = false
<== T & T1 <: T2 in frozen constraint = false
==> T1 <: T2 in frozen constraint
<== T1 <: T2 in frozen constraint = false
<== T2 | T & T1 <: T2 in frozen constraint = false
==> T2 <: T2
<== T2 <: T2 = true
==> (e.data : T) & T1 <: T2
==> glb(<notype>, <notype>)
<== glb(<notype>, <notype>) = <notype>
==> (e.data : T) <: T2
==> T <: T2 (left is approximated)
==> Any <: T2 (left is approximated)
<== Any <: T2 (left is approximated) = false
==> Any <: T2 in frozen constraint
<== Any <: T2 in frozen constraint = false
<== T <: T2 (left is approximated) = false
<== (e.data : T) <: T2 = false
==> T1 <: T2
<== T1 <: T2 = false
<== (e.data : T) & T1 <: T2 = false
==> T1 <: T2
<== T1 <: T2 = false
<== T2 | (e.data : T) & T1 <: T2 = false
at scala.runtime.Scala3RunTime$.assertFailed(Scala3RunTime.scala:8)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:338)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2960)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2964)
at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309)
at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3080)
at dotty.tools.dotc.typer.Typer.typedBlock(Typer.scala:1073)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedBlock$$anonfun$1$$anonfun$1(TreeChecker.scala:530)
at dotty.tools.dotc.transform.TreeChecker$Checker.withDefinedSyms(TreeChecker.scala:191)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedBlock$$anonfun$1(TreeChecker.scala:530)
at dotty.tools.dotc.transform.TreeChecker$Checker.withBlock(TreeChecker.scala:219)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedBlock(TreeChecker.scala:530)
at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2840)
at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2895)
at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:123)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:325)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2960)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2964)
at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309)
at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3080)
at dotty.tools.dotc.typer.Typer.caseRest$1(Typer.scala:1702)
at dotty.tools.dotc.typer.Typer.typedCase(Typer.scala:1718)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedCase$$anonfun$1(TreeChecker.scala:512)
at dotty.tools.dotc.transform.TreeChecker$Checker.withPatSyms(TreeChecker.scala:209)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedCase(TreeChecker.scala:513)
at dotty.tools.dotc.typer.Typer.typedCases$$anonfun$1(Typer.scala:1648)
at dotty.tools.dotc.core.Decorators$ListDecorator$.loop$1(Decorators.scala:89)
at dotty.tools.dotc.core.Decorators$ListDecorator$.mapconserve$extension(Decorators.scala:105)
at dotty.tools.dotc.typer.Typer.typedCases(Typer.scala:1650)
at dotty.tools.dotc.typer.Typer.$anonfun$26(Typer.scala:1640)
at dotty.tools.dotc.typer.Applications.harmonic(Applications.scala:2204)
at dotty.tools.dotc.typer.Applications.harmonic$(Applications.scala:327)
at dotty.tools.dotc.typer.Typer.harmonic(Typer.scala:117)
at dotty.tools.dotc.typer.Typer.typedMatchFinish(Typer.scala:1640)
at dotty.tools.dotc.typer.Typer.typedMatch(Typer.scala:1596)
at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2846)
at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2895)
at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:123)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:325)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2960)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2964)
at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309)
at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3080)
at dotty.tools.dotc.typer.Typer.$anonfun$47(Typer.scala:2278)
at dotty.tools.dotc.typer.PrepareInlineable$.dropInlineIfError(PrepareInlineable.scala:248)
at dotty.tools.dotc.typer.Typer.typedDefDef(Typer.scala:2278)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedDefDef$$anonfun$1(TreeChecker.scala:505)
at dotty.tools.dotc.transform.TreeChecker$Checker.withDefinedSyms(TreeChecker.scala:191)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedDefDef(TreeChecker.scala:508)
at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:2808)
at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2894)
at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:123)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:325)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2960)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2964)
at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309)
at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:2986)
at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:3036)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:548)
at dotty.tools.dotc.typer.Typer.typedClassDef(Typer.scala:2476)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedClassDef(TreeChecker.scala:483)
at dotty.tools.dotc.typer.Typer.typedTypeOrClassDef$1(Typer.scala:2820)
at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:2824)
at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2894)
at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:123)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:325)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2960)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2964)
at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309)
at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:2986)
at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:3036)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:548)
at dotty.tools.dotc.typer.Typer.typedPackageDef(Typer.scala:2603)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedPackageDef(TreeChecker.scala:574)
at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2865)
at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2895)
at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:123)
at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:325)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2960)
at dotty.tools.dotc.typer.Typer.typed(Typer.scala:2964)
at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309)
at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3080)
at dotty.tools.dotc.transform.TreeChecker.check(TreeChecker.scala:143)
at dotty.tools.dotc.transform.TreeChecker.run(TreeChecker.scala:110)
at dotty.tools.dotc.core.Phases$Phase.runOn$$anonfun$1(Phases.scala:311)
at scala.collection.immutable.List.map(List.scala:246)
at dotty.tools.dotc.core.Phases$Phase.runOn(Phases.scala:312)
at dotty.tools.dotc.Run.runPhases$1$$anonfun$1(Run.scala:225)
at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1328)
at dotty.tools.dotc.Run.runPhases$1(Run.scala:236)
at dotty.tools.dotc.Run.compileUnits$$anonfun$1(Run.scala:244)
at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
at dotty.tools.dotc.util.Stats$.maybeMonitored(Stats.scala:68)
at dotty.tools.dotc.Run.compileUnits(Run.scala:253)
at dotty.tools.dotc.Run.compileSources(Run.scala:186)
at dotty.tools.dotc.Run.compile(Run.scala:170)
at dotty.tools.dotc.Driver.doCompile(Driver.scala:35)
at dotty.tools.dotc.Driver.process(Driver.scala:195)
at dotty.tools.dotc.Driver.process(Driver.scala:163)
at dotty.tools.dotc.Driver.process(Driver.scala:175)
at dotty.tools.dotc.Driver.main(Driver.scala:205)
at dotty.tools.dotc.Main.main(Main.scala)
[error] Nonzero exit code returned from runner: 1
[error] (scala3-compiler / Compile / runMain) Nonzero exit code returned from runner: 1
[error] Total time: 1 s, completed Mar 25, 2022, 6:16:44 PM
Expectation
The code should pass the tree checker.