Use of GADTs and Union/Intersection types cause compiler to fail -Ycheck:all

[pjmc-oliveira]

Compiler version

3.3.1
3.4.0-RC1

Minimized code

final abstract class PInt
final abstract class PLet
final abstract class PSeq

sealed trait Expr[+P]
final case class EInt(value: Int) extends Expr[PInt]
final case class ELet[+A](name: String, expr: Expr[A]) extends Expr[A | PLet]
final case class ESeq[+A, +B](left: Expr[A], right: Expr[B]) extends Expr[A | B | PSeq]

def go[P](e: Expr[P]): P = e match {
  case ESeq(left, right) =>
    val uname3: Expr[P] & (ELet[P] | ESeq[P,P]) = ???
    val uname4 = uname3
    val uname5: Expr[P] = uname4
    ???
}

Output

  exception while retyping val uname5: Playground.Expr[P] = uname4 of class ValDef # -1

  An unhandled exception was thrown in the compiler.
  Please file a crash report here:
  https://github.com/lampepfl/dotty/issues/new/choose

     while compiling: /tmp/scastie5517424655659426554/src/main/scala/main.scala
        during phase: MegaPhase{protectedAccessors, extmethods, uncacheGivenAliases, elimByName, hoistSuperArgs, forwardDepChecks, specializeApplyMethods, tryCatchPatterns, patternMatcher}
                mode: Mode(ImplicitsEnabled)
     library version: version 2.13.10
    compiler version: version 3.3.1
            settings: -Vprint List(all) -Ycheck List(all) -bootclasspath /home/sbtRunnerContainer/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala3-library_3/3.3.1/scala3-library_3-3.3.1.jar:/home/sbtRunnerContainer/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala-library/2.13.10/scala-library-2.13.10.jar -classpath /tmp/scastie5517424655659426554/target/scala-3.3.1/classes:/home/sbtRunnerContainer/.ivy2/local/org.scastie/runtime-scala_3/1.0.0-SNAPSHOT/jars/runtime-scala_3.jar:/home/sbtRunnerContainer/.ivy2/local/org.scastie/api_3/0.30.0-SNAPSHOT/jars/api_3.jar:/home/sbtRunnerContainer/.cache/coursier/v1/https/repo1.maven.org/maven2/com/typesafe/play/play-json_3/2.10.0-RC5/play-json_3-2.10.0-RC5.jar:/home/sbtRunnerContainer/.cache/coursier/v1/https/repo1.maven.org/maven2/com/typesafe/play/play-functional_3/2.10.0-RC5/play-functional_3-2.10.0-RC5.jar:/home/sbtRunnerContainer/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-core/2.11.4/jackson-core-2.11.4.jar:/home/sbtRunnerContainer/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-annotations/2.11.4/jackson-annotations-2.11.4.jar:/home/sbtRunnerContainer/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/datatype/jackson-datatype-jdk8/2.11.4/jackson-datatype-jdk8-2.11.4.jar:/home/sbtRunnerContainer/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/datatype/jackson-datatype-jsr310/2.11.4/jackson-datatype-jsr310-2.11.4.jar:/home/sbtRunnerContainer/.cache/coursier/v1/https/repo1.maven.org/maven2/com/fasterxml/jackson/core/jackson-databind/2.11.4/jackson-databind-2.11.4.jar -d /tmp/scastie5517424655659426554/target/scala-3.3.1/classes -deprecation true -feature true

                tree: go
       tree position: /tmp/scastie5517424655659426554/src/main/scala/main.scala:13:4
           tree type: (Playground.go : [P](e: Playground.Expr[P]): P)
              symbol: method go in object Playground
   symbol definition: def go[P](e: Playground.Expr[P]): P (a Symbol)
      symbol package: <empty>
       symbol owners:  in object Playground
           call site: method go in object Playground in module class <empty>

  == Source file context for tree position ==

-- Error: /tmp/scastie5517424655659426554/src/main/scala/main.scala:13:4 -------
13 |def go[P](e: Expr[P]): P = e match {
   |^

14 |  case ESeq(left, right) =>
15 |    val uname3: Expr[P] & (ELet[P] | ESeq[P,P]) = ???
16 |    val uname4 = uname3
17 |    val uname5: Expr[P] = uname4
18 |    ???
19 |}
*** error while checking /tmp/scastie5517424655659426554/src/main/scala/main.scala after phase MegaPhase{protectedAccessors, extmethods, uncacheGivenAliases, elimByName, hoistSuperArgs, forwardDepChecks, specializeApplyMethods, tryCatchPatterns, patternMatcher} ***

Expectation

Compiler should not fail -Ycheck:all if the code compiles

https://scastie.scala-lang.org/wuP0yMZ3TSmz3FBb8EEmcw

[EugeneFlesselle]

Here is little more minimised version:

final abstract class PLet

sealed trait Expr[+P]
case class ELet[+A](name: String, expr: Expr[A]) extends Expr[A | PLet]

def go[P](e: Expr[P]): P = e match
  case ELet(_, _) =>
    val x: Expr[P] | ELet[P] = ???
    val y: Expr[P] = x
    ???

It looks like this the cast for conformance from the GADT bounds is not being inserted in this case https://github.com/lampepfl/dotty/blob/1716bcd9dbefbef88def848c09768a698b6b9ed9/compiler/src/dotty/tools/dotc/typer/Typer.scala#L4075-L4084