Match types fail `-Ycheck` with GADT constraints

[Linyxus]

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 PM

Expectation

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.

[SethTisue]

Minimized and scala-cli-ified:

//> using scala "3.2.0-RC3"
//> using option "-Ycheck:typer"
case class Bar[T <: Tuple]()
def bar(e: Any): Int = e match
  case _: Bar[t] =>
    (??? : Int *: t).head

(Foo is unnecessary, and Bar only needs a single type parameter.)

[SethTisue]

Dale's current working hypothesis is that patternSymbolBound is putting the bound in the GADT constraints but it should be going in the regular constraints. We'll dig into it more tomorrow.

[Linyxus]

Note that there are cases where we do have bounds as GADT constraints:

enum C[-T]:
  case C1() extends C[EmptyTuple]

def foo[A](e: C[A]) = e match {
  case C.C1() =>
    // GADT constr: A <: EmptyTuple
    val i: Int = (??? : Int *: A).head
}

Head[Int *: A] would also need A <: EmptyTuple to reduce (so this fails -Ycheck too), which is a GADT constraint.

[SethTisue]

It makes sense to tackle Linyxus's case first, since it's entirely in GADT-land, and then later consider the original case, which seems to involve crossing in and out of that land.

In both cases, the feature intersection involved is bounds and match types: we're using a bounded type as input to a match type.

[SethTisue]

This is an interesting one.

Dale is considering (and experimenting with) a couple possible solution paths. One is to try to solve it by inserting a GADT cast. The other I won't try to summarize but it involves thinking a bit more broadly about how and where GADT constraints are handled during typechecking.