Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Match types fail to infer correct type #19936

Closed
lbialy opened this issue Mar 13, 2024 · 7 comments
Closed

Match types fail to infer correct type #19936

lbialy opened this issue Mar 13, 2024 · 7 comments
Assignees
Labels
area:match-types itype:bug itype:soundness Soundness bug (it lets us compile code that crashes at runtime with a ClassCastException) regression This worked in a previous version but doesn't anymore

Comments

@lbialy
Copy link

lbialy commented Mar 13, 2024

Compiler version

This fails differently on 3.3.3 and 3.4.0.

Minimized code

//> using scala 3.3.3 // 3.4.0
import scala.compiletime.ops.int.S

trait Slider[N <: Int & Singleton, A]:
  type Out <: Tuple = N match
    case 0    => EmptyTuple
    case S[n] => Tuple.Append[A, Slider[n, A]#Out]

extension [A](v: Vector[A])
  def slidingN(n: Int & Singleton): Iterator[Slider[n.type, A]#Out] =
    v.sliding(n).map { block =>
      block.foldLeft[Tuple](EmptyTuple)((acc, a) => acc :* a).asInstanceOf[Slider[n.type, A]#Out]
    }

@main def test: Unit =
  val it: Iterator[(Int, Int)] = (1 to 20).toVector.slidingN(2) // this compiles on 3.4.0 but fails to compile on 3.3.3
  it.map(_._1.toString).foreach(println)

  val it2: Iterator[Int] = (1 to 20).toVector.slidingN(2).map(_._1) // this fails to compile on both

Output

For 3.3.3:

[error] ./test.scala:15:61
[error] Match type reduction failed since selector Int
[error] matches none of the cases
[error]
[error]     case EmptyTuple => Slider[(1 : Int), Int]#Out *: EmptyTuple
[error]     case x *: xs => x *: Tuple.Append[xs, Slider[(1 : Int), Int]#Out]
[error]   val it: Iterator[(Int, Int)] = (1 to 20).toVector.slidingN(2)
[error]                                                             ^
[error] ./test.scala:18:65
[error] Match type reduction failed since selector Int
[error] matches none of the cases
[error]
[error]     case EmptyTuple => Slider[(1 : Int), Int]#Out *: EmptyTuple
[error]     case x *: xs => x *: Tuple.Append[xs, Slider[(1 : Int), Int]#Out]
[error]   val it2: Iterator[Int] = (1 to 20).toVector.slidingN(2).map(_._1)
[error]                                                                 ^
Error compiling project (Scala 3.3.3, JVM (17))

For 3.4.0:

[error] ./test.scala:15:38
[error] Match type reduction failed since selector Int
[error] matches none of the cases
[error]
[error]     case EmptyTuple => Slider[(1 : Int), Int]#Out *: EmptyTuple
[error]     case x *: xs => x *: Tuple.Append[xs, Slider[(1 : Int), Int]#Out]
[error]   (1 to 20).toVector.slidingN(2).map(_._1)
[error]                                      ^^^^
Error compiling project (Scala 3.4.0, JVM (17))
Compilation failed

Expectation

I expect this code to infer return type as Iterator[(Int, Int)] correctly in both use cases.

@lbialy lbialy added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label labels Mar 13, 2024
@SethTisue
Copy link
Member

I wonder if this can be minimized further (though it's also valuable to have the original code, because it shows context and intent).

@SethTisue
Copy link
Member

SethTisue commented Mar 13, 2024

Note that on 3.4.0 (but not 3.3.3), compilation succeeds if you split the expression into two parts and add an explicit type:

val xs: Iterator[(Int, Int)] = (1 to 20).toVector.slidingN(2)
xs.map(_._1)

so something progressed, but not as far we'd like.

@Gedochao Gedochao added area:match-types and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Mar 13, 2024
@Gedochao
Copy link
Contributor

An interesting spin on the minimization, credit by @prolativ

//> using scala 3.4.0

import scala.compiletime.ops.int.S

trait Slider[N <: Int & Singleton, A]:
  type Out <: Tuple = N match
    case 0    => EmptyTuple
    case S[n] => Tuple.Append[A, Slider[n, A]#Out]

extension [A](v: Vector[A])
  def slidingN(n: Int & Singleton): Iterator[Slider[n.type, A]#Out] =
    v.sliding(n).map { block =>
      block.foldLeft[Tuple](EmptyTuple)((acc, a) => acc :* a).asInstanceOf[Slider[n.type, A]#Out]
    }

@main def test: Unit =
  val it2: Iterator[String] = (1 to 20).toVector.slidingN(2)
  it2.map(_.length).foreach(println)

This fails the compilation on 3.3.3

scala-cli compile . -S lts
# Compiling project (Scala 3.3.3, JVM (17))
# [error] ./repro.scala:17:58
# [error] Match type reduction failed since selector Int
# [error] matches none of the cases
# [error] 
# [error]     case EmptyTuple => Slider[(1 : Int), Int]#Out *: EmptyTuple
# [error]     case x *: xs => x *: Tuple.Append[xs, Slider[(1 : Int), Int]#Out]
# [error]   val it2: Iterator[String] = (1 to 20).toVector.slidingN(2)
# [error]                                                          ^
# Error compiling project (Scala 3.3.3, JVM (17))
# Compilation failed

But actually compiles on 3.4.0, and only fails in runtime 😐

scala-cli run . -S 3.4.0
# Exception in thread "main" java.lang.ClassCastException: class scala.Tuple2 cannot be cast to class java.lang.String (scala.Tuple2 is in unnamed module of loader 'app'; java.lang.String is in module java.base of loader 'bootstrap')
#         at scala.collection.Iterator$$anon$9.next(Iterator.scala:584)
#         at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
#         at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
#         at scala.collection.AbstractIterator.foreach(Iterator.scala:1300)
#         at repro$package$.test(repro.scala:18)
#         at test.main(repro.scala:16)

This means we definitely have a regression here, and this might also be a case of unsoundness.
Note that val it2: Iterator[String] compiles, even though it should most definitely be val it2: Iterator[(Int, Int)]

@Gedochao Gedochao added regression This worked in a previous version but doesn't anymore itype:soundness Soundness bug (it lets us compile code that crashes at runtime with a ClassCastException) labels Mar 14, 2024
@SethTisue
Copy link
Member

Note that val it2: Iterator[String] compiles, even though it should most definitely be val it2: Iterator[(Int, Int)]

🙀

@EugeneFlesselle
Copy link
Contributor

EugeneFlesselle commented Mar 14, 2024

The definition of Append

type Append[X <: Tuple, Y] <: NonEmptyTuple = X match {
  case EmptyTuple => Y *: EmptyTuple
  case x *: xs => x *: Append[xs, Y]
}

expects a subtype of Tuple as first argument.

So I assume Tuple.Append[A, Slider[n, A]#Out] was meant to be Tuple.Append[Slider[n, A]#Out, A]. The error

Match type reduction failed since selector Int matches none of the cases

looks legitimate otherwise.

However, the fact that either of

val it: Iterator[(Int, Int)] = (1 to 20).toVector.slidingN(2) // compiles
it.map(_._1 + 1).foreach(println) // no ClassCastException

val it2: Iterator[String] = (1 to 20).toVector.slidingN(2) // compiles
it2.map(_.length).foreach(println) // ClassCastException

compiles is definitely unsound. It is also surprising that it does not lead to a runtime an error.

If we swap the order of the Append arguments, we get a recursion limit exceeded error in all cases, which is definitely not great either.

@lbialy
Copy link
Author

lbialy commented Mar 15, 2024

Yeah, my bad, I did bork it and got into weird errors without checking types. I got it working just fine:

import scala.compiletime.ops.int.S

type Slider[N <: Int & Singleton, A] <: Tuple = N match
  case 0    => EmptyTuple
  case S[n] => Tuple.Append[Slider[n, A], A]

extension [A](v: Vector[A])
  inline def slidingN(n: Int & Singleton): Iterator[Slider[n.type, A]] =
    v.sliding(n).map { block =>
      block.foldLeft[Tuple](EmptyTuple)((acc, a) => acc :* a).asInstanceOf[Slider[n.type, A]]
    }

@main def test: Unit =
  def it: Iterator[(Int, Int, Int, Int, Int)] = (1 to 20).toVector.slidingN(5)
  it.foreach(println)

@dwijnand
Copy link
Member

With the user code fixed, let's close this in favour of the unsoundness part covered in #19949

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area:match-types itype:bug itype:soundness Soundness bug (it lets us compile code that crashes at runtime with a ClassCastException) regression This worked in a previous version but doesn't anymore
Projects
None yet
Development

No branches or pull requests

5 participants