Document & test GADT reasoning for pattern alternatives

Author: Linyxus

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -2056,7 +2056,31 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   end necessaryEither
 
   /** Finds the necessary (the weakest) GADT constraint among a list of them.
-   * It returns the one being subsumed by all others if exists, and `None` otherwise. */
+   * It returns the one being subsumed by all others if exists, and `None` otherwise.
+   *
+   * This is used when typechecking pattern alternatives, for instance:
+   *
+   *   enum Expr[+T]:
+   *     case I1(x: Int) extends Expr[Int]
+   *     case I2(x: Int) extends Expr[Int]
+   *     case B(x: Boolean) extends Expr[Boolean]
+   *   import Expr.*
+   *
+   * The following function should compile:
+   *
+   *   def foo[T](e: Expr[T]): T = e match
+   *     case I1(_) | I2(_) => 42
+   *
+   * since `T >: Int` is subsumed by both alternatives in the first match clause.
+   *
+   * However, the following should not:
+   * 
+   *   def foo[T](e: Expr[T]): T = e match
+   *     case I1(_) | B(_) => 42
+   *
+   * since the `I1(_)` case gives the constraint `T >: Int` while `B(_)` gives `T >: Boolean`.
+   * Neither of the constraints is subsumed by the other.
+   */
   def necessaryGadtConstraint(constrs: List[GadtConstraint], preGadt: GadtConstraint)(using Context): Option[GadtConstraint] = boundary:
     constrs match
       case Nil => break(None)

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -2834,6 +2834,9 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
         gadtConstrs += ctx.gadt
         res
       .mapconserve(ensureValueTypeOrWildcard)
+    // Look for the necessary constraint that is subsumed by all alternatives.
+    // Use that constraint as the outcome if possible, otherwise fallback to not using
+    // GADT reasoning for soundness.
     TypeComparer.necessaryGadtConstraint(gadtConstrs.toList, preGadt) match
       case Some(constr) => nestedCtx.gadtState.restore(constr)
       case None => nestedCtx.gadtState.restore(preGadt)

tests/neg/gadt-alt-expr1.scala

@@ -0,0 +1,13 @@
+enum Expr[+T]:
+  case I1() extends Expr[Int]
+  case I2() extends Expr[Int]
+  case B() extends Expr[Boolean]
+import Expr.*
+def foo[T](e: Expr[T]): T =
+  e match
+    case I1() | I2() => 42  // ok
+    case B() => true
+def bar[T](e: Expr[T]): T =
+  e match
+    case I1() | B() => 42  // error
+    case I2() => 0

tests/neg/gadt-alt-expr2.scala

@@ -0,0 +1,15 @@
+enum Expr[+T]:
+  case I1() extends Expr[Int]
+  case I2() extends Expr[Int]
+  case I3() extends Expr[Int]
+  case I4() extends Expr[Int]
+  case I5() extends Expr[Int]
+  case B() extends Expr[Boolean]
+import Expr.*
+def test1[T](e: Expr[T]): T =
+  e match
+    case I1() | I2() | I3() | I4() | I5() => 42  // ok
+    case B() => true
+def test2[T](e: Expr[T]): T =
+  e match
+    case I1() | I2() | I3() | I4() | I5() | B() => 42  // error

tests/neg/gadt-alt-expr3.scala

@@ -0,0 +1,34 @@
+trait A
+trait B extends A
+trait C extends B
+trait D
+enum Expr[+T]:
+  case IsA() extends Expr[A]
+  case IsB() extends Expr[B]
+  case IsC() extends Expr[C]
+  case IsD() extends Expr[D]
+import Expr.*
+def test1[T](e: Expr[T]): T = e match
+  case IsA() => new A {}
+  case IsB() => new B {}
+  case IsC() => new C {}
+def test2[T](e: Expr[T]): T = e match
+  case IsA() | IsB() =>
+    // IsA() implies T >: A
+    // IsB() implies T >: B
+    // So T >: B is chosen
+    new B {}
+  case IsC() => new C {}
+def test3[T](e: Expr[T]): T = e match
+  case IsA() | IsB() | IsC() =>
+    // T >: C is chosen
+    new C {}
+def test4[T](e: Expr[T]): T = e match
+  case IsA() | IsB() | IsC() =>
+    new B {}  // error
+def test5[T](e: Expr[T]): T = e match
+  case IsA() | IsB() =>
+    new A {}  // error
+def test6[T](e: Expr[T]): T = e match
+  case IsA() | IsC() | IsD() =>
+    new C {}  // error

tests/neg/gadt-alt-expr4.scala

@@ -0,0 +1,19 @@
+trait A
+trait B extends A
+trait C extends B
+enum Expr[T]:
+  case IsA() extends Expr[A]
+  case IsB() extends Expr[B]
+  case IsC() extends Expr[C]
+import Expr.*
+def test1[T](e: Expr[T]): T = e match
+  case IsA() => new A {}
+  case IsB() => new B {}
+  case IsC() => new C {}
+def test2[T](e: Expr[T]): T = e match
+  case IsA() | IsB() =>
+    // IsA() implies T =:= A
+    // IsB() implies T =:= B
+    // No necessary constraint can be found
+    new B {}  // error
+  case IsC() => new C {}

tests/neg/gadt-alt-expr5.scala

@@ -0,0 +1,14 @@
+trait A
+trait B extends A
+trait C extends B
+enum Expr[-T]:
+  case IsA() extends Expr[A]
+  case IsB() extends Expr[B]
+  case IsC() extends Expr[C]
+import Expr.*
+def test1[T](e: Expr[T]): Unit = e match
+  case IsA() | IsB() =>
+    val t1: T = ???
+    val t2: A = t1
+    val t3: B = t1  // error
+  case IsC() =>

tests/pos/gadt-alt-doc1.scala

@@ -0,0 +1,8 @@
+trait Document[Doc <: Document[Doc]]
+sealed trait Conversion[Doc, V]
+
+case class C[Doc <: Document[Doc]]() extends Conversion[Doc, Doc]
+
+def Test[Doc <: Document[Doc], V](conversion: Conversion[Doc, V]) =
+  conversion match
+    case C() | C() => ??? // error