Match type fails to reduce in a simple case

[keynmol]

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?

[sjrd]

TC1 and TC2 are traits, so not probably disjoint. The others are classes.

[keynmol]

Gotcha, Aly on Discord educated me:

Yeah it's bcs you could have val x: TC2[Int] = new TC1 with TC2

Do you know if there's a way to implement this Contains check? As it only returns true or false (shortcircuiting), those conflicting cases are not a concern.

[sjrd]

I don't think so. Perhaps wrapping both sides in an invariant container, but I don't remember what we settled on for invariant type constructors.