Error: No singleton value available for scala.compiletime.S[scala.compiletime.S[(0 : Int)]].

[Atry]

minimized code

import scala.compiletime._

final case class Coproduct[+Set, +Value, Index <: Int](value: Value & Set, index: Index)

object Coproduct {
  opaque type +:[+A, +B] = A | B

  trait At[+Set, -Value, Index <: Int] {
    def cast: Value <:< Set
  }

  object At {

    given atHead[Head, Tail]: At[Head +: Tail, Head, 0] {
      def cast: Head <:< Head +: Tail = summon[Head <:< Head +: Tail]
    }

    given atTail[Head, Tail, Value, NextIndex <: Int](given atNext: At[Tail, Value, NextIndex]): At[Head +: Tail, Value, S[NextIndex]] {
      val cast: Value <:< Head +: Tail = atNext.cast
    }

    given [A](given A): (() => A)= { () => summon[A]}
  }

  def upCast[A, B](a: A)(given erased evidence: (A <:< B)): B = a.asInstanceOf[B]

  def from[Set, Value, Index <: Int](value: Value)(given erased at: At[Set, Value, Index])(given ValueOf[Index]): Coproduct[Set, Value, Index] = {
    Coproduct[Set, Value, Index](upCast(value: Value)(given at.cast.liftCo[[+X] =>> Value & X]), valueOf[Index])
  }

}

object Test extends App {
  import Coproduct._

  // Error: No singleton value available for scala.compiletime.S[scala.compiletime.S[(0 : Int)]].
  val c = from[Set = Int +: String +: Seq[Double] +: Nothing](Nil)
}

expectation

It should compile

[MaximeKjaer]

Further minimized code:

import scala.compiletime.S

object Test {    
    def plusOne[I <: Int](given x: ValueOf[S[I]]): S[I] = x.value
    plusOne[0]
}

Error message

-- Error: tests/pos/singleton-ops-implicits.scala:5:14 -------------------------
5 |    plusOne[0]
  |              ^
  |          No singleton value available for scala.compiletime.S[(0 : Int)].

[nicolasstucki]

scala.compiletime.S[Int] is intended to not reduce.

Not sure where the ascription comes from in (0 : Int). That seems to be the source of the issue.

[nicolasstucki]

I could fix it but it required a small change in the first example https://github.com/lampepfl/dotty/pull/7905/files#r363396245

[Atry]

Interesting. What's the difference between (given ValueOf[Index]): Coproduct[Set, Value, Index] and (given ValueOf[Index]) => Coproduct[Set, Value, Index]?

[nicolasstucki]

In the first one, the search for the ValueOf is part of type inference of Index. While in the second one the result type uses the inferred type for Index.