Practical Tuple type errors

[Adam-Vandervorst]

Compiler version

3.0.2

Minimized code

val a = Tuple1(3)
val b = Tuple2(3, 4)
val ab = a ++ b

val a_new = ab.take(a.size) // fails
summon[Tuple.Take[ab.type, Tuple.Size[a.type]] =:= a.type] // fails
summon[Tuple.Take[Tuple.Concat[Tuple1[Int], Tuple2[Int, Int]], Tuple.Size[Tuple1[Int]]] =:= Tuple1[Int]] // inlined succeeds

Output

For the runtime version:

Found:    Tuple.Take[Int *: (b : (Int, Int)), (?3 : Tuple.Size[Tuple1[Int]])]
Required: Int *: EmptyTuple

where:    ?3 is an unknown value of type Tuple.Size[Tuple1[Int]]

  val a_new = ab.take(a.size)

For the first proof:

Cannot prove that Int *: EmptyTuple =:= (a : Tuple1[Int]).
  summon[Tuple.Take[ab.type, Tuple.Size[a.type]] =:= a.type]

Expectation

Not sure if I faithfully reduced the problem, but I expected all three to succeed.

In context

I want to drop the .asInstanceOf in the following example:

class SFunction[D <: Tuple, CD](f: Function1[D, CD]):
  type Dom = D
  type CoDom = CD

  inline def arity: Tuple.Size[D] = valueOf[Tuple.Size[D]]
  inline def apply(d: D): CD = f(d)

  inline infix def parallel[G <: Tuple, CG](other: SFunction[G, CG]) =
    SFunction[Tuple.Concat[D, G], (CD, CG)]((dg: Tuple.Concat[D, G]) =>
      (this(dg.take(arity).asInstanceOf[D]), other(dg.drop(arity).asInstanceOf[G])))

but doing this for the left yields:

Found:    Tuple.Take[Tuple.Concat[D, G], (?1 : Tuple.Size[D])]
Required: D

where:    ?1 is an unknown value of type Tuple.Size[D]
          G  is a type in method parallel with bounds <: Tuple

      (this(dg.take(arity)), other(dg.drop(arity))))

even though Tuple.Take[Tuple.Concat[D, G], (?1 : Tuple.Size[D])] logically reduces to D.

[nicolasstucki]

ab.take(a.size) works on master.

summon[Tuple.Take[ab.type, Tuple.Size[a.type]] =:= a.type] should fail as it is only true that summon[a.type <:< Tuple.Take[ab.type, Tuple.Size[a.type]]] but not the other way around. a.type is more precise than Tuple1[Int].

[nicolasstucki]

Though this fails with -Ycheck:all

val a: Int *: EmptyTuple = ???
val ab: (Int, Int, Int) = ???

val a_new = ab.take(a.size)

[Adam-Vandervorst]

Thanks for that update, that indeed works on 3.1.2-RC1-bin-20211025-968dd1b-NIGHTLY.

The second part (Tuple.Take[Tuple.Concat[D, G], (?1 : Tuple.Size[D])] not reducing to D) behaves the same though. I don't think this is caused by the specificity here (and yes, it makes a ton of sense that Tuple1[Int] <:< a.type doesn't hold). Running it from the console revealed:

    SFunction[Tuple.Concat[D, G], (CD, CG)](dg => (this(dg.take(arity)), other(dg.drop(arity))))
                                                        ^^^^^^^^^^^^^^
Found:    Tuple.Take[Tuple.Concat[D, G], (?1 : Tuple.Size[D])]
Required: D

where:    ?1 is an unknown value of type Tuple.Size[D]
          G  is a type in method parallel with bounds <: Tuple

Note: a match type could not be fully reduced:

  trying to reduce  Tuple.Take[Tuple.Concat[D, G], (?1 : Tuple.Size[D])]
  failed since selector  D
  does not match  case EmptyTuple => (0 : Int)
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining case

    case x *: xs => scala.compiletime.ops.int.S[scala.Tuple.Size[xs]]

though I can not bring this compiler note back to my code. Note this may be of similar nature to https://github.com/lampepfl/dotty/issues/13800.