more path-dependent GADT examples

Author: Linyxus

tests/pos/pdgadt-asmember.scala

@@ -0,0 +1,14 @@
+// Taken from https://github.com/lampepfl/dotty/pull/14754#issuecomment-1157427912.
+trait T[X]
+case object Foo extends T[Unit]
+
+trait AsMember {
+  type L
+  val tl: T[L]
+}
+
+def testMember(am: AsMember): Unit =
+  am.tl match {
+    case Foo => println(summon[am.L =:= Unit])
+    case _ => ()
+  }

tests/pos/pdgadt-nat-simpleadd.scala

@@ -0,0 +1,40 @@
+trait Z
+trait S[N]
+
+type of[A, B] = A & { type T = B }
+
+trait Nat { type T }
+case class Zero() extends Nat { type T = Z }
+case class Succ[P](prec: Nat of P) extends Nat { type T = S[P] }
+
+
+type :=:[T, X] = T & { type R = X }
+
+trait :+:[A, B] {
+  type R
+}
+
+object Addition {
+  given AddZero[N]: :+:[Z, N] with {
+    type R = N
+  }
+
+  given AddSucc[M, N, X](using e: (M :+: N) :=: X): :+:[S[M], N] with {
+    val e0: (M :+: N) :=: X = e
+    type R = S[X]
+  }
+}
+
+object Proof {
+  import Addition.given
+
+  def zeroAddN[N]: (Z :+: N) :=: N = summon
+
+  def nAddZero[N](n: Nat of N): (N :+: Z) :=: N = n match {
+    case Zero() => zeroAddN[Z]
+    case p: Succ[pn] =>
+      val e0: (pn :+: Z) :=: pn = nAddZero[pn](p.prec)
+      AddSucc(using e0)
+  }
+}
+

tests/pos/pdgadt-tupof.scala

@@ -0,0 +1,37 @@
+import scala.compiletime.ops.int.S
+
+type sized[T, N <: Int] = T & { type Size = N }
+
+abstract class TupOf[T, +A] {
+  type Size <: Int
+}
+
+object TupOf {
+  given Empty[A]: TupOf[EmptyTuple, A] with {
+    type Size = 0
+  }
+
+  final given Cons[A, T <: Tuple, N <: Int](using p: T TupOf A sized N): TupOf[A *: T, A] with {
+    val p0: T TupOf A sized N = p
+    type Size = S[N]
+  }
+}
+
+enum Vec[N <: Int, +A]:
+  case VecNil extends Vec[0, Nothing]
+  case VecCons[N0 <: Int, A](head: A, tail: Vec[N0, A]) extends Vec[S[N0], A]
+
+object Vec {
+  import TupOf._
+  def apply[A, T <: Tuple](xs: T)(using p: T TupOf A): Vec[p.Size, A] = p match {
+    case _: TupOf.Empty[A] => VecNil
+    case p1: TupOf.Cons[a, t, n] =>
+      VecCons(xs.head, apply(xs.tail)(using p1.p0))
+  }
+
+  def main(): Unit = {
+    val vec1: Vec[3, Int] = VecCons(1, VecCons(2, VecCons(3, VecNil)))
+    val vec2: Vec[3, Int] = Vec(1, 2, 3)
+  }
+}
+