Match types fail -Ycheck with GADT constraints #15743
Description
Compiler version
3.2.0-RC2 (main branch)
Minimized code
trait Foo case class Bar[A, T <: Tuple]() extends Foo object test { def bar[T <: Tuple](e: Foo) = e match { case _: Bar[a, t] => // this works val xs0: a *: T = ??? val t0: a = xs0.head // this breaks val xs1: a *: t = ??? val t1: a = xs1.head } }Output
checking issues/pdgadt-tupof-mini.scala after phase typer exception while typing val t1: a = xs1.head[(a *: t)] of class class dotty.tools.dotc.ast.Trees$ValDef # -1 exception while typing { val xs0: *:[a, T] = ??? val t0: a = xs0.head[(a *: T)] val xs1: *:[a, t] = ??? val t1: a = xs1.head[(a *: t)] () } of class class dotty.tools.dotc.ast.Trees$Block # -1 exception while typing e match { case _:Bar[a @ _, t @ _] => val xs0: *:[a, T] = ??? val t0: a = xs0.head[(a *: T)] val xs1: *:[a, t] = ??? val t1: a = xs1.head[(a *: t)] () } of class class dotty.tools.dotc.ast.Trees$Match # -1 exception while typing def bar[T >: Nothing <: Tuple](e: Foo): Unit = e match { case _:Bar[a @ _, t @ _] => val xs0: *:[a, T] = ??? val t0: a = xs0.head[(a *: T)] val xs1: *:[a, t] = ??? val t1: a = xs1.head[(a *: t)] () } of class class dotty.tools.dotc.ast.Trees$DefDef # -1 exception while typing final module class test() extends Object() { this: test.type => def bar[T >: Nothing <: Tuple](e: Foo): Unit = e match { case _:Bar[a @ _, t @ _] => val xs0: *:[a, T] = ??? val t0: a = xs0.head[(a *: T)] val xs1: *:[a, t] = ??? val t1: a = xs1.head[(a *: t)] () } } of class class dotty.tools.dotc.ast.Trees$TypeDef # -1 exception while typing package <empty> { trait Foo() extends Object {} case class Bar[A >: Nothing <: Any, T >: Nothing <: Tuple]() extends Object(), Foo, _root_.scala.Product, _root_.scala.Serializable { A T <: Tuple def copy[A, T <: Tuple](): Bar[A, T] = new Bar[A, T]() } final lazy module val Bar: Bar = new Bar() final module class Bar() extends AnyRef() { this: Bar.type => def apply[A, T <: Tuple](): Bar[A, T] = new Bar[A, T]() def unapply[A, T <: Tuple](x$1: Bar[A, T]): true.type = true override def toString: String = "Bar" } final lazy module val test: test = new test() final module class test() extends Object() { this: test.type => def bar[T >: Nothing <: Tuple](e: Foo): Unit = e match { case _:Bar[a @ _, t @ _] => val xs0: *:[a, T] = ??? val t0: a = xs0.head[(a *: T)] val xs1: *:[a, t] = ??? val t1: a = xs1.head[(a *: t)] () } } } of class class dotty.tools.dotc.ast.Trees$PackageDef # -1 exception occurred while compiling issues/pdgadt-tupof-mini.scala *** error while checking issues/pdgadt-tupof-mini.scala after phase typer *** java.lang.AssertionError: assertion failed: Found: Tuple.Head[a *: t] Required: a found: ?? expected: type a with type a, flags = case, underlying = a, , Any, {...} tree = xs1.head[(a *: t)] while compiling issues/pdgadt-tupof-mini.scala Exception in thread "main" java.lang.AssertionError: assertion failed: Found: Tuple.Head[a *: t] Required: a found: ?? expected: type a with type a, flags = case, underlying = a, , Any, {...} tree = xs1.head[(a *: t)] at scala.runtime.Scala3RunTime$.assertFailed(Scala3RunTime.scala:8) at dotty.tools.dotc.transform.TreeChecker$Checker.adapt(TreeChecker.scala:636) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3029) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3033) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309) at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3149) at dotty.tools.dotc.typer.Typer.typedValDef(Typer.scala:2271) at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:2874) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2963) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:325) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3029) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3033) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309) at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:3055) at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:3105) at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:555) at dotty.tools.dotc.typer.Typer.typedBlockStats(Typer.scala:1058) at dotty.tools.dotc.typer.Typer.typedBlock(Typer.scala:1062) at dotty.tools.dotc.transform.TreeChecker$Checker.typedBlock$$anonfun$1$$anonfun$1(TreeChecker.scala:537) at dotty.tools.dotc.transform.TreeChecker$Checker.withDefinedSyms(TreeChecker.scala:191) at dotty.tools.dotc.transform.TreeChecker$Checker.typedBlock$$anonfun$1(TreeChecker.scala:537) at dotty.tools.dotc.transform.TreeChecker$Checker.withBlock(TreeChecker.scala:219) at dotty.tools.dotc.transform.TreeChecker$Checker.typedBlock(TreeChecker.scala:537) at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2909) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2964) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:325) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3029) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3033) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309) at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3149) at dotty.tools.dotc.typer.Typer.caseRest$1(Typer.scala:1752) at dotty.tools.dotc.typer.Typer.typedCase(Typer.scala:1768) at dotty.tools.dotc.transform.TreeChecker$Checker.typedCase$$anonfun$1(TreeChecker.scala:519) at dotty.tools.dotc.transform.TreeChecker$Checker.withPatSyms(TreeChecker.scala:209) at dotty.tools.dotc.transform.TreeChecker$Checker.typedCase(TreeChecker.scala:520) at dotty.tools.dotc.typer.Typer.typedCases$$anonfun$1(Typer.scala:1698) at dotty.tools.dotc.core.Decorators$ListDecorator$.loop$1(Decorators.scala:87) at dotty.tools.dotc.core.Decorators$ListDecorator$.mapconserve$extension(Decorators.scala:103) at dotty.tools.dotc.typer.Typer.typedCases(Typer.scala:1700) at dotty.tools.dotc.typer.Typer.$anonfun$28(Typer.scala:1690) at dotty.tools.dotc.typer.Applications.harmonic(Applications.scala:2226) at dotty.tools.dotc.typer.Applications.harmonic$(Applications.scala:327) at dotty.tools.dotc.typer.Typer.harmonic(Typer.scala:119) at dotty.tools.dotc.typer.Typer.typedMatchFinish(Typer.scala:1690) at dotty.tools.dotc.typer.Typer.typedMatch(Typer.scala:1624) at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2915) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2964) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:325) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3029) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3033) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309) at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3149) at dotty.tools.dotc.typer.Typer.$anonfun$49(Typer.scala:2335) at dotty.tools.dotc.inlines.PrepareInlineable$.dropInlineIfError(PrepareInlineable.scala:249) at dotty.tools.dotc.typer.Typer.typedDefDef(Typer.scala:2335) at dotty.tools.dotc.transform.TreeChecker$Checker.typedDefDef$$anonfun$1(TreeChecker.scala:512) at dotty.tools.dotc.transform.TreeChecker$Checker.withDefinedSyms(TreeChecker.scala:191) at dotty.tools.dotc.transform.TreeChecker$Checker.typedDefDef(TreeChecker.scala:515) at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:2877) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2963) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:325) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3029) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3033) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309) at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:3055) at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:3105) at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:555) at dotty.tools.dotc.typer.Typer.typedClassDef(Typer.scala:2540) at dotty.tools.dotc.transform.TreeChecker$Checker.typedClassDef(TreeChecker.scala:490) at dotty.tools.dotc.typer.Typer.typedTypeOrClassDef$1(Typer.scala:2889) at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:2893) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2963) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:325) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3029) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3033) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309) at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:3055) at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:3105) at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:555) at dotty.tools.dotc.typer.Typer.typedPackageDef(Typer.scala:2671) at dotty.tools.dotc.transform.TreeChecker$Checker.typedPackageDef(TreeChecker.scala:581) at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2934) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2964) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:325) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3029) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3033) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:309) at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3149) 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:234) 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:245) at dotty.tools.dotc.Run.compileUnits$$anonfun$1(Run.scala:253) at dotty.tools.dotc.Run.compileUnits$$anonfun$adapted$1(Run.scala:262) at dotty.tools.dotc.util.Stats$.maybeMonitored(Stats.scala:68) at dotty.tools.dotc.Run.compileUnits(Run.scala:262) 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: 2 s, completed Jul 24, 2022, 5:28:35 PMExpectation
This code should pass the tree checker. As seen in the log, the tree checker fails at the expression xs1.head[(a *: t)], whose expected type is a but the found type is Tuple.Head[a *: t]. The Tuple.Head is a match type defined as:
type Head[X <: NonEmptyTuple] = X match { case x *: _ => x }The possible cause seems to be: to reduce Tuple.Head[a *: t] to a we need to show that t is a subtype of Tuple. However, the GADT bound t <: Tuple is not available when we run the checker phase. This is why the expression xs0.head[(a *: T)] whose type does not need GADT constraints to reduce works but xs1.head[(a *: t)] breaks.