How to do type-level addition in Scala 3?

How can I impletement type-level operations (addition in this case) in Scala 3 ?

Here is what I would like to do (this does not compile) :

case class foo[S <: Int & Singleton](value: Double) {
    def bar[T <: Int & Singleton](that: foo[T]): foo[S + T] = new foo[S + T](this.value * that.value)
}

val t1 = foo[1](1.5)
val t2 = foo[1](2.0)

val t3 = t1 bar t2 //foo[2](3.0)

PS : the SIP-23 proposal talks about libraries that implement such behaviour in Scala 2 but I am interested in Scala 3.

You need to import scala.compiletime.ops.int.+

https://docs.scala-lang.org/scala3/reference/metaprogramming/compiletime-ops.html#the-scalacompiletimeops-package

But then you have to remove upper bound & Singleton for S

case class foo[S <: Int /*& Singleton*/](value: Double):
  def bar[T <: Int & Singleton](that: foo[T]): foo[S + T] =
    new foo[S + T](this.value * that.value)

The thing is that the + is defined as

type +[X <: Int, Y <: Int] <: Int

This addition is executed at compile time by the compiler but technically there is no upper bound <: Singleton for S + T.

If you really want to restore the upper bound for S you can replace the upper bound with generalized type constraint <:<

case class foo[S <: Int](value: Double)(using S <:< Singleton):
  def bar[T <: Int & Singleton](that: foo[T])(using (S + T) <:< Singleton): foo[S + T] =
    new foo[S + T](this.value * that.value)

More about the difference <: vs <:< :

In scala 3, is it possible to make covariant/contravariant type constructor to honour coercive subtyping?

https://blog.bruchez.name/posts/generalized-type-constraints-in-scala/