Open
Description
I don't have a better title because I don't currently see the difference between failing and suceeding case.
Compiler version
3.3.6, 3.7.0
Minimized code
type TupleContains[X <: Tuple, Y] <: Boolean = X match
case Y *: _ => true
case _ *: xs => TupleContains[xs, Y]
case EmptyTuple => false
trait TC1[A]
trait TC2[A]
// this works
summon[
(TupleContains[(Int, String, Boolean), String]) =:= true
]
// this also works
summon[
(TupleContains[(Array[Int], Set[Int], List[Boolean]), Set[Int]]) =:= true
]
// how is this different from above?
summon[
(TupleContains[(TC1[Int], TC2[Int], Set[Boolean]), TC2[Int]]) =:= true
]
Output
https://scastie.scala-lang.org/BO4FKhFwRMSjhGaIQBKIlg
Cannot prove that Playground.TupleContains[
(Playground.TC1[Int], Playground.TC2[Int], Set[Boolean]), Playground.TC2[Int]] =:= (true : Boolean).
Note: a match type could not be fully reduced:
trying to reduce Playground.TupleContains[
(Playground.TC1[Int], Playground.TC2[Int], Set[Boolean]), Playground.TC2[Int]]
failed since selector (Playground.TC1[Int], Playground.TC2[Int], Set[Boolean])
does not match case Playground.TC2[Int] *: _ => (true : Boolean)
and cannot be shown to be disjoint from it either.
Therefore, reduction cannot advance to the remaining cases
case _ *: xs => Playground.TupleContains[xs, Playground.TC2[Int]]
case EmptyTuple => (false : Boolean)
Expectation
I'm not sure why the failing reduction is different from the one above it that succeeds?