# How do I compute type-level M + N?

This query got no love on Discord.

How do I use the sum of two singleton integer types? I am trying to make a ++ operator for concatenating a vector of length N with one of length M (both compile-time constants). The obvious thing

``````class Vec[N <: Int & Singleton](using n: ValueOf[N]) :
private val xs: Array[Double] = Array.ofDim[Double](n.value)
def ++[M <: Int & Singleton](other: Vec[M]) =
val result = Vec[N + M]
for i <- 0 until xs.length do
result.xs(i) = xs(i)
for i <- 0 until other.xs.length do
result.xs(i + xs.length) = other.xs(i)
result
``````

(complete code on Scastie - An interactive playground for Scala.) fails with

``````No singleton value available for N + M where:    M is a type in method ++ with bounds <: Int & Singleton.
``````

There is a related bug report at https://github.com/lampepfl/dotty/issues/8257 that was closed, apparently without action. So how am I supposed to do this?

You can move the responsibility to prove that `N + M` is a singleton value to the callsite of `++`.

``````class Vec[N <: Int](using n: ValueOf[N]) :
private val xs: Array[Double] = Array.ofDim[Double](n.value)
def ++[M <: Int](other: Vec[M])(using ValueOf[N + M]) =
val result = Vec[N + M]
for i <- 0 until xs.length do
result.xs(i) = xs(i)
for i <- 0 until other.xs.length do
result.xs(i + xs.length) = other.xs(i)
result
``````

That seems to work in this scastie:

1 Like

Thank you very much! That works.

I would love to understand why. My guess is the `using` clause of the class.

I tried removing the `using` clause, like this:

``````class Vec[N <: Int & Singleton] :
private val xs: Array[Double] = Array.ofDim[Double](summon[ValueOf[N]].value)
``````

Now I got

``````No singleton value available for N.
``````

With

``````class Vec[N <: Int & Singleton] :
private val xs: Array[Double] = Array.ofDim[Double](valueOf[N])
``````

the message becomes even less helpful:

``````cannot reduce summonFrom with patterns :  case given ev @ _:ValueOf[N]
``````

Obviously, I ascribe too much power to the `Singleton` bound, perhaps because of the wording in https://scala-lang.org/api/3.x/scala/Singleton.html: “When a type parameter has an explicit upper bound of Singleton, the compiler infers a singleton type.” Clearly here it did not.

Is that how it should be, or should I report a bug?

Thanks,

Cay

I think your analysis is pretty accurate. I’m not sure there’s a bug here though. But the error messages could definitely be better.

Thanks very much! I filed https://github.com/lampepfl/dotty/issues/15829, noting that either this is a bug or the error message needs work.

1 Like