scala3
scala3 copied to clipboard
Published
20 hours ago •
scala
scala
Match types fail `-Ycheck` with GADT constraints
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.
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.)
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.
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.
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.
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.
One is to try to solve it by inserting a GADT cast
That's the approach taken in the now-merged PR.