Skip to content

Match type fails to reduce in a simple case #23159

Open
@keynmol

Description

@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?

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions