Fix a case of MT reduction using abstract types

[dwijnand]

The original motivation wasn't with a test case. And reproducing it
is not convincing. So I'd rather revert and fix this issue.

[sjrd]

The new match type spec refuses to reduce here, like main.

I think this is actually unsound, but I'm having a hard time actually causing a crash. My best attempt so far is

final class Box[T](var value: T)

type TupleIndex[T <: Tuple, A, I <: Int] <: (Any, Int) = T match
  case A *: _ => (A, I)
  case _ *: t => TupleIndex[t, A, S[I]]

def tupleIndex[T <: Tuple, A](box: Box[Tuple.Elem[TupleIndex[T, A, 0], 1]]): Unit = box.value = 5

def test(): Unit =
  summon[TupleIndex[(String, String), String, 0] =:= (String, 0)]
  summon[Tuple.Elem[TupleIndex[(String, String), String, 0], 1] =:= 0] // proof that it reduces to 0
  val box: Box[0] = new Box(0)
  tupleIndex[(String, String), String](box) // error here
  val zero: 0 = box.value
  println(zero)

but I still get

-- [E007] Type Mismatch Error: tests/pos/i18202.scala:35:39 --------------------
35 |  tupleIndex[(String, String), String](box)
   |                                       ^^^
   |                                       Found:    (box : Box[(0 : Int)])
   |                                       Required: Box[Int]
   |
   | longer explanation available when compiling with `-explain`
1 error found

However, at this point T is known to be (String, String) and A is String, so the type Tuple.Elem[TupleIndex[T, A, 0], 1] should reduce to 0. We even prove it at "proof that it reduces to 0".

So it's only by chance that this snippet does not compile, once this commit is applied.

[sjrd]

To better illustrate the "random"/"by chance" aspect of the above consider this variant:

import compiletime.ops.int.*

final class Box[T](var value: T)

type TupleIndex[T <: Tuple, A, I <: Int] <: (Any, Int) = T match
  case A *: _ => (A, I)
  case _ *: t => TupleIndex[t, A, S[I]]

class Container:
  type A
  type T <: Tuple
  type TheIndex = TupleIndex[T, A, 0]
  def tupleIndex(box: Box[Tuple.Elem[TheIndex, 1]]): Unit = box.value = 5 // LINE 13

class Child extends Container:
  type A = String
  type T = (String, String)
  type TheIndex = (String, 0)

def test(): Unit =
  val box: Box[0] = new Box(0)
  val child = new Child
  child.tupleIndex(box) // LINE 23
  val zero: 0 = box.value
  println(zero)

which gives the following error:

-- [E007] Type Mismatch Error: tests/pos/i18202.scala:13:72 --------------------
13 |  def tupleIndex(box: Box[Tuple.Elem[TheIndex, 1]]): Unit = box.value = 5
   |                                                                        ^
   |      Found:    (5 : Int)
   |      Required: Tuple.Elem[Container.this.TheIndex, (1 : Int)]
   |
   |      Note: a match type could not be fully reduced:
   |
   |        trying to reduce  Tuple.Elem[Container.this.TheIndex, (1 : Int)]
   |        failed since selector Container.this.TheIndex
   |        does not uniquely determine parameters x, xs in
   |          case x *: xs => (1 : Int) match {
   |        case (0 : Int) => x
   |        case scala.compiletime.ops.int.S[n1] => Tuple.Elem[xs, n1]
   |      }
   |        The computed bounds for the parameters are:
   |          x >: Any
   |          xs >: Int *: EmptyTuple.type <: Tuple
   |
   | longer explanation available when compiling with `-explain`
1 error found

but if we replace, on LINE 13, TheIndex by its right-hand-side, TupleIndex[T, A, 0], then we don't have any error on line 13 anymore, but we get one on line 23:

-- [E007] Type Mismatch Error: tests/pos/i18202.scala:23:19 --------------------
23 |  child.tupleIndex(box)
   |                   ^^^
   |                   Found:    (box : Box[(0 : Int)])
   |                   Required: Box[Int]
   |
   | longer explanation available when compiling with `-explain`
1 error found

On main, both variants get an error on line 13, and not on line 23.

[mrdziuban]

@sjrd thanks for your thoughts! I'd like the understand better why/how this could be unsound, though it's a bit out of my wheelhouse so please excuse my ignorance 😄

I'm having a hard time actually causing a crash

Even if you don't have a code sample for it, what kind of crash do you think might be possible?

From #18202 (comment)

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)

I don't fully follow this, but I think my understanding might be off -- I thought that if TupleIndex[T, A] can't reduce, then reduction of Tuple.Elem wouldn't even be tried. In the case of an implicit search (like in the original issue), my thinking was that failure to reduce would cause the compiler to stop considering that instance as a candidate.

[sjrd]

@sjrd thanks for your thoughts! I'd like the understand better why/how this could be unsound, though it's a bit out of my wheelhouse so please excuse my ignorance 😄

I'm having a hard time actually causing a crash

Even if you don't have a code sample for it, what kind of crash do you think might be possible?

In this case I expect the println(zero) to print 5 although val zero: 0. In general if you use classes instead of literal types, you can cause ClassCastExceptions even though you never wrote any asInstanceOf. That's usually what we consider to be unsoundness.

From #18202 (comment)

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)

I don't fully follow this, but I think my understanding might be off -- I thought that if TupleIndex[T, A] can't reduce, then reduction of Tuple.Elem wouldn't even be tried. In the case of an implicit search (like in the original issue), my thinking was that failure to reduce would cause the compiler to stop considering that instance as a candidate.

Implicit resolution has nothing to do with this example. We're type-checking the body of the method, in which we already have the value at our disposal. It is only a matter of reduction.

The fact that your body previously typechecked shows that reduction of Tuple.Elem did happen, even though TupleIndex[T, A] did not. If the inner match type does not reduce, we can still use its upper bound, namely <: (Any, Int). However, as was demonstrated before and as shows up in the fix-that-broke-your-code, when we follow a bound, we have to relinquish some power about what we can reduce. In particular, we cannot capture in covariant type parameter position anymore.

[dwijnand]

In general if you use classes instead of literal types, you can cause ClassCastExceptions even though you never wrote any asInstanceOf. That's usually what we consider to be unsoundness.

Perhaps it's easier to get the exception with a class Foo and subclass Foo1, rather than Int and 0.

[dwijnand]

I think this is actually unsound, but I'm having a hard time actually causing a crash.

I don't think it's unsound, and the fact that it doesn't compile is because it's right not to. box.value = 5 only compiles if we reduced to Box[Int]. So you can't then want to pass a Box[0].

However, at this point T is known to be (String, String) and A is String, so the type Tuple.Elem[TupleIndex[T, A, 0], 1] should reduce to 0. We even prove it at "proof that it reduces to 0".

Sure, when T is more specific, it reduces to something more specific. But the method compiled without the specificity, so it reduced to Int, allowing 5 to be set.

but if we replace, on LINE 13, TheIndex by its right-hand-side, TupleIndex[T, A, 0], then we don't have any error on line 13 anymore, but we get one on line 23:

I don't understand why that changes, but the ultimate error on line 23 is still right.

[sjrd]

Sure, when T is more specific, it reduces to something more specific. But the method compiled without the specificity, so it reduced to Int, allowing 5 to be set.

That's not how match types work. Match types have to follow a stronger property:

• If S is more specific than T, and T match { ... } reduces to some X, then S match { ... } must also reduce to the same X (not something more specific than X).

Concretely, that means that type captures cannot be instantiated to some Y from T but some other X <: Y for S <: T. This is the critical bit behind the test cases in https://github.com/lampepfl/dotty/blob/main/tests/neg/wildcard-match.scala.

I don't think it's unsound, and the fact that it doesn't compile is because it's right not to. box.value = 5 only compiles if we reduced to Box[Int]. So you can't then want to pass a Box[0].

We reduced to Box[Int] given a more abstract type. But refining that scrutinee type makes it reduce to Box[0]. That's bad; it's a direct occurrence of the wildcard-match.scala problem.

but if we replace, on LINE 13, TheIndex by its right-hand-side, TupleIndex[T, A, 0], then we don't have any error on line 13 anymore, but we get one on line 23:

I don't understand why that changes, but the ultimate error on line 23 is still right.

Imagine that in version 1 of a library I define it with TheIndex and I don't write something in the box. I can then write client code that passes in a Box[0]. In version 2 of the library, I decide to "inline" the type alias, which should be equivalent so a valid/compatible rewrite, and that lets me write a 5 into the box. Then I relink everything and I get an incoherent result (or a CCE if we use classes).

That's the problem with the "it reduces by chance". The presence of type aliases in the middle of the path should never alter what a match type reduces to.