If expressions typed with GADT constraints cause failure with `-Ycheck:all`

[Linyxus]

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.

[Linyxus]

And this could be triggered with the match expression too:

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() =>
    flag match
      case true => new T2 {}
      case false => e.data
}

Compilation of this snippet fails with -Ycheck:all.

[Linyxus]

I tried a fix like this. It does fix this issue, but will break a large bunch of tests.

[abgruszecki]

Note to self: why do we even insert a cast to (e.data : T) & T1 instead of T1? It seems that might be the real source of the problem.

[dwijnand]

Because e.data.type is stable: https://github.com/lampepfl/dotty/pull/12159/files

[Linyxus]

It turns out that this issue is not necessarily related to GADT casts. The following code reproduces the same problem without direct relationship to the GADT cast.

trait Expr[T]
case class IntExpr() extends Expr[Int]

def flag: Boolean = ???

def foo[T](ev: Expr[T]) = ev match
  case IntExpr() =>
    if flag then
      val i: T = 0
      i
    else
      0