From f5cf140a58f334fba0412463e71e73d0d5ea5fe7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bart=C5=82omiej=20Kozak?= Date: Fri, 4 Sep 2026 15:47:34 +0200 Subject: [PATCH 1/2] Support more Tuple shapes in containsOnly (Elem, Init, Take, Drop, Filter, Union, Append) Generalizes the Head/Last-style <:< evidence to Tuple.Elem[This, N] for an arbitrary index (given lower priority since it can collide with the Head evidence for a literal N=0), and adds containsOnly-preserving givens for Init, Take, Drop, Filter and Append, plus a Union[This] <:< T evidence for the union of all elements. Co-Authored-By: Claude Sonnet 5 --- commons/containsOnly.scala | 15 +++++ test/ContainsOnlyTest.scala | 117 +++++++++++++++++++++++++++++++++++- 2 files changed, 130 insertions(+), 2 deletions(-) diff --git a/commons/containsOnly.scala b/commons/containsOnly.scala index 00b7a45..0167261 100644 --- a/commons/containsOnly.scala +++ b/commons/containsOnly.scala @@ -25,6 +25,16 @@ object containsOnly extends containsOnlyLowPriority: given [Tup <: Tuple: Of[T], T] => (Tuple.Tail[Tup] containsOnly T) = refl + given [Tup <: Tuple: Of[T], T] => (Tuple.Init[Tup] containsOnly T) = refl + + given [Tup <: Tuple: Of[T], N <: Int, T] => (Tuple.Take[Tup, N] containsOnly T) = refl + + given [Tup <: Tuple: Of[T], N <: Int, T] => (Tuple.Drop[Tup, N] containsOnly T) = refl + + given [Tup <: Tuple: Of[T], P[_ <: Tuple.Union[Tup]] <: Boolean, T] => (Tuple.Filter[Tup, P] containsOnly T) = refl + + given [Tup <: Tuple: Of[T], Y <: T, T] => (Tuple.Append[Tup, Y] containsOnly T) = refl + given [Tup <: Tuple: Of[T], T] => (Tuple.Reverse[Tup] containsOnly T) = refl given [Tup1 <: Tuple: Of[T], Tup2 <: Tuple: Of[T], T] => (Tuple.Concat[Tup1, Tup2] containsOnly T) = refl @@ -37,5 +47,10 @@ object containsOnly extends containsOnlyLowPriority: given [Tup <: Tuple: Of[T], This >: Tup <: Tuple, T] => (Tuple.Last[This] <:< T) = <:<.refl.asInstanceOf[(Tuple.Last[This] <:< T)] + given [Tup <: Tuple: Of[T], This >: Tup <: Tuple, T] => (Tuple.Union[This] <:< T) = + <:<.refl.asInstanceOf[(Tuple.Union[This] <:< T)] + sealed trait containsOnlyLowPriority: + given [Tup <: Tuple: Of[T], This >: Tup <: Tuple, N <: Int, T] => (Tuple.Elem[This, N] <:< T) = + <:<.refl.asInstanceOf[(Tuple.Elem[This, N] <:< T)] given Tuple containsOnly Any = containsOnly.refl diff --git a/test/ContainsOnlyTest.scala b/test/ContainsOnlyTest.scala index 770985d..2765fdf 100644 --- a/test/ContainsOnlyTest.scala +++ b/test/ContainsOnlyTest.scala @@ -211,8 +211,8 @@ class ContainsOnlyTest extends munit.FunSuite: assertEquals(last, 3) } - // `containsOnly` only provides Head/Last → T conversions today. Operations like - // `apply(i)`, `drop`, `take`, `tail`, `init`, `reverse`, `mapAs`, `toList`, `++` + // `containsOnly` provides Head/Last/Elem → T conversions today. Operations like + // `drop`, `take`, `tail`, `init`, `reverse`, `mapAs`, `toList`, `++` // need the static tuple shape to reduce match types, which we don't carry on an // abstract `Tuple` value. Coverage for those would require a richer evidence type. @@ -335,3 +335,116 @@ class ContainsOnlyTest extends munit.FunSuite: summon[Tuple.Reverse[tuple.type] containsOnly String] } + + test("Tuple.Elem gives evidence at an arbitrary index") { + val tuple: Tuple = ("one", "two", "three") + given tuple.type containsOnly String = containsOnly.refl + + // N=0 is deliberately not tested here: it collides with the dedicated Head evidence + // (both reduce to the same type), which is exactly why Elem is given lower priority. + summon[Tuple.Elem[tuple.type, 1] <:< String] + summon[Tuple.Elem[tuple.type, 2] <:< String] + } + + test("Tuple.Init preserves containsOnly") { + val tuple = ("one", "two", "three") + + summon[Tuple.Init[tuple.type] containsOnly String] + } + + test("Tuple.Take preserves containsOnly") { + val tuple = ("one", "two", "three") + + summon[Tuple.Take[tuple.type, 0] containsOnly String] + summon[Tuple.Take[tuple.type, 2] containsOnly String] + summon[Tuple.Take[tuple.type, 3] containsOnly String] + } + + test("Tuple.Drop preserves containsOnly") { + val tuple = ("one", "two", "three") + + summon[Tuple.Drop[tuple.type, 0] containsOnly String] + summon[Tuple.Drop[tuple.type, 1] containsOnly String] + summon[Tuple.Drop[tuple.type, 3] containsOnly String] + } + + test("Tuple.Filter preserves containsOnly") { + val tuple = ("one", "two", "three") + + type IsString[X] <: Boolean = X match + case String => true + case _ => false + + summon[Tuple.Filter[tuple.type, IsString] containsOnly String] + } + + test("Tuple.Filter preserves containsOnly for an abstract Tuple") { + val tuple: Tuple = ("one", "two", "three") + given tuple.type containsOnly String = containsOnly.refl + + type IsString[X] <: Boolean = X match + case String => true + case _ => false + + summon[Tuple.Filter[tuple.type, IsString] containsOnly String] + } + + test("Tuple.Union gives evidence for the union of all elements") { + val tuple: Tuple = ("one", "two", "three") + given tuple.type containsOnly String = containsOnly.refl + + summon[Tuple.Union[tuple.type] <:< String] + } + + test("Tuple.Append preserves containsOnly") { + val tuple = ("one", "two", "three") + + summon[Tuple.Append[tuple.type, "four"] containsOnly String] + + import Tuple.:* + summon[(tuple.type :* "four") containsOnly String] + } + + test("Tuple.Append preserves containsOnly for an abstract Tuple") { + val tuple: Tuple = ("one", "two", "three") + given tuple.type containsOnly String = containsOnly.refl + + summon[Tuple.Append[tuple.type, "four"] containsOnly String] + } + + test("Tuple.Map with a constant function preserves containsOnly (already supported)") { + type Es = (Int, String, Boolean) + + summon[Tuple.Map[Es, [_] =>> List[Int]] containsOnly List[Int]] + } + + test("Tuple.Map with a covariant type constructor preserves containsOnly (already supported)") { + val tuple = (1, 2, 3) + + summon[Tuple.Map[tuple.type, Option] containsOnly Option[Any]] + } + + test("Tuple.Fold has no blanket containsOnly given: it depends entirely on F, so only Union (a specific Fold) is covered") { + val tuple: Tuple = (1, 2, 3) + given tuple.type containsOnly Int = containsOnly.refl + + // Union[Tup] = Fold[Tup, Nothing, [x, y] =>> x | y] — this specific instantiation is covered. + summon[Tuple.Union[tuple.type] <:< Int] + + // A generic Fold isn't: nothing constrains F to preserve "all elements are T" (F could + // produce a String out of Ints, e.g. `[x, y] =>> String`), so no sound blanket given can exist. + } + + test("Tuple.Split preserves containsOnly via the existing Take/Drop givens") { + val tuple = ("one", "two", "three", "four") + + summon[Tuple.Take[tuple.type, 2] containsOnly String] + summon[Tuple.Drop[tuple.type, 2] containsOnly String] + + // Tuple.Split[Tup, N] = (Take[Tup, N], Drop[Tup, N]) — a 2-tuple of tuples, not itself + // homogeneous in String, so it needs no dedicated given; each half is already covered. + val split: Tuple.Split[tuple.type, 2] = (("one", "two"), ("three", "four")) + val (taken, dropped) = split + summon[taken.type containsOnly String] + summon[dropped.type containsOnly String] + } From 56e26058f54476e7d9c3ca00812d48ef612e963a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bart=C5=82omiej=20Kozak?= Date: Fri, 4 Sep 2026 16:08:57 +0200 Subject: [PATCH 2/2] fmt --- test/ContainsOnlyTest.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/test/ContainsOnlyTest.scala b/test/ContainsOnlyTest.scala index 2765fdf..83c7385 100644 --- a/test/ContainsOnlyTest.scala +++ b/test/ContainsOnlyTest.scala @@ -424,7 +424,9 @@ class ContainsOnlyTest extends munit.FunSuite: summon[Tuple.Map[tuple.type, Option] containsOnly Option[Any]] } - test("Tuple.Fold has no blanket containsOnly given: it depends entirely on F, so only Union (a specific Fold) is covered") { + test( + "Tuple.Fold has no blanket containsOnly given: it depends entirely on F, so only Union (a specific Fold) is covered", + ) { val tuple: Tuple = (1, 2, 3) given tuple.type containsOnly Int = containsOnly.refl