Lack of type refinement for match case

[Bersier]

Compiler version

3.1.3

Minimized code

sealed trait NatT
case class Zero() extends NatT
case class Succ[N<: NatT](n: N) extends NatT

trait IsLessThan[M <: NatT, N <: NatT]
object IsLessThan:
  given base[M <: NatT]: IsLessThan[M, Succ[M]]()
  given weakening[N <: NatT, M <: NatT] (using IsLessThan[N, M]): IsLessThan[N, Succ[M]]()
  given reduction[N <: NatT, M <: NatT] (using IsLessThan[Succ[N], Succ[M]]): IsLessThan[N, M]()

sealed trait UniformTuple[Length <: NatT, T]:
  def apply[M <: NatT](m: M)(using IsLessThan[M, Length]): T

case class Empty[T]() extends UniformTuple[Zero, T]:
  def apply[M <: NatT](m: M)(using IsLessThan[M, Zero]): T = throw new AssertionError("Uncallable")

case class Cons[N <: NatT, T](head: T, tail: UniformTuple[N, T]) extends UniformTuple[Succ[N], T]:
  def apply[M <: NatT](m: M)(using proof: IsLessThan[M, Succ[N]]): T = m match
    case Zero() => head
    case Succ(predM): Succ[predM] => tail(predM)(using IsLessThan.reduction(using proof))

Output

Found:    (proof : IsLessThan[M, Succ[N]])
Required: IsLessThan[Succ[predM], Succ[N]]

Expectation

The code is expected to compile, as within that case branch, M is identified with Succ[predM].

I opened a discussion thread on contributors.scala-lang.org about this, but didn't get any answer. So I'm tentatively filing this as a bug.

[prolativ]

@abgruszecki could you confirm this should actually work?

[abgruszecki]

I don't see a good way of making this example work, unfortunately.

Pattern matching can't really reconstruct the bound M = Succ[predM] simply from m : M matching Succ(predM), since in general M could be NatT. In this specific case, we actually must have M = Succ[predM], because otherwise we can't construct the IsLessThan evidence. However, this sort of reasoning is too complex to implement in the compiler.

Perhaps we could make examples like this one work in the future, if we could somehow express that M needs to be a "precise" type.

[abgruszecki]

Alternatively, we will soon be merging a PR where we will reconstruct the bound m.type <: Succ[predM], which does hold in general. If the definitions could be changed so that we have proof : m.type IsLessThan Succ[N], the example should work with the PR. Do you think something like that would be possible, @Bersier?

[Bersier]

@abgruszecki Thank you for the kind explanation.

I'm not sure I fully follow it, unfortunately. In my example, the case pattern is actually Succ(predM): Succ[predM], with the type of the pattern explicitly given as Succ[predM]. Is that still insufficient to easily conclude that M = Succ[predM]?

For my own code, it would not be a problem to change the signature of Cons.apply to

def apply[M <: NatT](m: M)(using proof: IsLessThan[m.type, Succ[N]]): T

once the PR you mentioned is merged.

P.S.: Being able to force precise types would be nice.

[abgruszecki]

Even if the pattern is Succ(predM) : Succ[predM], we can't conclude that M = Succ[predM]. If not for the proof argument, we could have a call like this one:

cons.apply[NatT](Succ(Zero()))

If we did conclude that M = Succ[predM], we would run into unsoundness in cases like this one:

def foo[X](x: X): (X => Unit) =
  x match
    case _: String => 
      // returning `String => Unit` is OK, since we believe that `X = String`
      (str: String) => println(str.toLowerCase())
val fun : Any => Unit = foo[Any]("")
fun(0) // type error at runtime, 0 doesn't have .toLowerCase

[abgruszecki]

The PR I mentioned is #14754 .

[Bersier]

@abgruszecki Thank you! Interesting.

Can unsoundness happen even if the return type is not contravariant in X?

[abgruszecki]

The return type is just one way to use the reconstructed bound. In general it simply doesn't need to be the case that X = String, like the snippet shows. For instance, foo could have another parameter which uses X.

[Bersier]

@abgruszecki I still feel like there might be a condition related to contravariance which is required for unsoundness to happen. But fair enough. Should this issue be closed, then, since this is behaving as expected?

[abgruszecki]

@Bersier think about it this way: X = T is exactly the same as X <: T and T <: X. I think when you say "there is a condition which is required for unsoudness to happen", you basically mean "what if we don't use one of these bounds, can we then reconstruct both bounds?". In a sense, the answer to that is "yes", since the program is correct. We typically think in the reverse way: "is there any way to use this bound which is unsound?". Since the answer to that is "yes", we only reconstruct one of these bounds. Think about it this way: technically, if a program doesn't use a pointer, it's safe for the pointer to be null. This doesn't mean that null pointers are safe in general.

I'd keep this issue around. We should at least verify that the PR I mentioned does infer the bound on m.type. @Linyxus can you take a look at this issue? Would your PR infer that bound?

[Linyxus]

Currently in #14754 we only record equalities between singleton types. So we will not record a constraint like m.type <: Succ[predM]. However, by rewriting the example a bit:

def apply[M <: NatT](m: M)(using proof: IsLessThan[m.type, Succ[N]]): T = m match
  case Zero() => head
  case m1: Succ[predM] =>
    // ...

we will be able to record the equality m.type == m1.type. But this still cannot make the example work. The furthest i can go is:

case class Cons[N <: NatT, T](head: T, tail: UniformTuple[N, T]) extends UniformTuple[Succ[N], T]:
  def apply[M <: NatT](m: M)(using proof: IsLessThan[m.type, Succ[N]]): T = m match
    case Zero() => head
    case m1: Succ[predM] =>
      // ???
      val predM: predM = m1.n
      val proof1: IsLessThan[m1.type, Succ[N]] = proof
      val proof2: IsLessThan[Succ[predM], Succ[N]] = proof1

      tail(predM)(using IsLessThan.reduction(using proof2))

The last line still cannot typecheck because what we want here is a IsLessThan[Succ[predM.type], Succ[N]], but what we have is IsLessThan[Succ[predM], Succ[N]]. (note that to allow the val proof2 line typecheck we have to make the first type parameter of IsLessThan covariant, since the widen type of m1.type is M & Succ[predM]).