Match type not working unless ascribed or inlined (2)

[nicolasstucki]

Minimized code

import annotation.showAsInfix
import scala.compiletime._

class TupleKOps {


  def tupleMerge(tuple1: TupleK, tuple2: TupleK): TupleK = ???

  def tupleMergeSort(tuple: TupleK): TupleK =
    if (tuple.size <= 1) tuple
    else {
      val (tuple1, tuple2) = tuple.splitAt(tuple.size / 2)
      // val (tuple1: TupleK, tuple2: TupleK) = tuple.splitAt(tuple.size / 2) // ok
      val (sorted1, sorted2) = (tupleMergeSort(tuple1), tupleMergeSort(tuple2))
      tupleMerge(sorted1, sorted2)
    }

}

sealed trait TupleK {
  import TupleK._
  /*inline*/ def size[This >: this.type <: TupleK]: Size[This] = ???
  /*inline*/ def splitAt[This >: this.type <: TupleK](n: Int): Split[This, n.type] = ???
}

object TupleK {
  type Size[X <: TupleK] <: Int = X match {
    case EmptyTupleK => 0
    case x #: xs => S[Size[xs]]
  }
  type Take[T <: TupleK, N <: Int] <: TupleK = N match {
    case 0 => EmptyTupleK
    case S[n1] => T match {
      case EmptyTupleK => EmptyTupleK
      case x #: xs => x #: Take[xs, n1]
    }
  }
  type Drop[T <: TupleK, N <: Int] <: TupleK = N match {
    case 0 => T
    case S[n1] => T match {
      case EmptyTupleK => EmptyTupleK
      case x #: xs => Drop[xs, n1]
    }
  }
  type Split[T <: TupleK, N <: Int] = (Take[T, N], Drop[T, N])
}

type EmptyTupleK = EmptyTupleK.type

object EmptyTupleK extends TupleK

sealed trait NonEmptyTupleK extends TupleK
sealed abstract class #:[+H, +T <: TupleK] extends NonEmptyTupleK

Output

-- [E043] Type Error: tests/pos/tuples1c.scala:12:6 ----------------------------
12 |      val (tuple1, tuple2) = tuple.splitAt(tuple.size / 2)
   |      ^
   |unreducible application of higher-kinded type TupleK.Take to wildcard arguments in inferred type TupleK.Take[TupleK, ? <: Int]

Expectation

They compile with the inline, they should also compile without it.

[nicolasstucki]

Related to #11236

[odersky]

It seems here the problem is that tuple.size is not constant unless the inline is presented? The workaround dotty-staging@ef72a88 sidesteps the problem by widening the type. We could do the same automatically, maybe, but in most cases it would simply render the error more obscure.

[odersky]

On second thought, I think it's OK to make an exception for match types here. It's expected that some match types don't reduce because the arguments are not sufficiently well known. In that case we should widen to the bound instead of failing with an error.