Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 15 additions & 0 deletions commons/containsOnly.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
119 changes: 117 additions & 2 deletions test/ContainsOnlyTest.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -335,3 +335,118 @@ 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]
}