Regression around match type reduction in 3.3.2 nightly versions

[mrdziuban]

Compiler version

Nightly versions 3.3.2-RC1-bin-20230605-5d2812a-NIGHTLY through the latest 3.3.2-RC1-bin-20230710-ed319e8-NIGHTLY

By testing every nightly version I've narrowed it down to something in the commit range 348729e...5d2812a, and if git bisect is telling me the truth, then I believe the specific commit is 09f5e4c

Minimized code

type TupleIndex[T <: Tuple, A] = TupleIndex0[T, A, 0]

type TupleIndex0[T <: Tuple, A, I <: Int] <: (Any, Int) =
  T match {
    case A *: _ => (A, I)
    case _ *: t => TupleIndex0[t, A, compiletime.ops.int.S[I]]
  }

def tupleIndex[T <: Tuple, A](using i: ValueOf[Tuple.Elem[TupleIndex[T, A], 1]]): Int = i.value

Output

A type mismatch error is given at the RHS of def tupleIndex

-- [E007] Type Mismatch Error: /path/to/TupleIndex.scala:9:90
9 |def tupleIndex[T <: Tuple, A](using i: ValueOf[Tuple.Elem[TupleIndex[T, A], 1]]): Int = i.value
  |                                                                                        ^^^^^^^
  |Found:    Tuple.Elem[TupleIndex[T, A], (1 : Int)]
  |Required: Int
  |
  |where:    T is a type in method tupleIndex with bounds <: Tuple
  |
  |
  |Note: a match type could not be fully reduced:
  |
  |  trying to reduce  Tuple.Elem[TupleIndex[T, A], (1 : Int)]
  |  trying to reduce  TupleIndex[T, A]
  |  trying to reduce  TupleIndex0[T, A, (0 : Int)]
  |  failed since selector T
  |  does not match  case A *: _ => (A, (0 : Int))
  |  and cannot be shown to be disjoint from it either.
  |  Therefore, reduction cannot advance to the remaining case
  |
  |    case _ *: t => TupleIndex0[t, A, scala.compiletime.ops.int.S[(0 : Int)]]
  |  trying to reduce  TupleIndex[T, A]
  |  trying to reduce  TupleIndex0[T, A, (0 : Int)]
  |  failed since selector T
  |  does not match  case A *: _ => (A, (0 : Int))
  |  and cannot be shown to be disjoint from it either.
  |  Therefore, reduction cannot advance to the remaining case
  |
  |    case _ *: t => TupleIndex0[t, A, scala.compiletime.ops.int.S[(0 : Int)]]
  |  trying to reduce  TupleIndex0[T, A, (0 : Int)]
  |  failed since selector T
  |  does not match  case A *: _ => (A, (0 : Int))
  |  and cannot be shown to be disjoint from it either.
  |  Therefore, reduction cannot advance to the remaining case
  |
  |    case _ *: t => TupleIndex0[t, A, scala.compiletime.ops.int.S[(0 : Int)]]

Expectation

The compiler should recognize that Tuple.Elem[TupleIndex[T, A], 1] is an Int since TupleIndex0 specifies a bound of (Any, Int)

Things work properly if TupleIndex0 has a bound of <: Int and I don't use Tuple.Elem, so does this maybe have something to do with nested match types? i.e. this compiles

type TupleIndex[T <: Tuple, A] = TupleIndex0[T, A, 0]

type TupleIndex0[T <: Tuple, A, I <: Int] <: Int =
  T match {
    case A *: _ => I
    case _ *: t => TupleIndex0[t, A, compiletime.ops.int.S[I]]
  }

def tupleIndex[T <: Tuple, A](using i: ValueOf[TupleIndex[T, A]]): Int = i.value

[sjrd]

As I mention in the PR attempting to fix this, at #18243 (comment), I believe the new error is actually correct. In other words, not emitting an error would be unsound. (And fixing unsoundness issues is allowed in patch releases.)

Your "workaround" is the proper fix, IMO. By removing the indirection through Tuple.Elem, you do not force Tuple.Elem to widen the abstract type _ <: (Any, Int) which is what TupleIndex[T, A] resolves to (given that it cannot reduce because T is too abstract). Widening abstract types then capturing arguments to covariant type params is known to cause unsoundness. See existing test cases in https://github.com/lampepfl/dotty/blob/ca6a80e3c7aef6b16304df20544c41a96556c834/tests/neg/wildcard-match.scala

[dwijnand]

@sjrd happy to close this as invalid?