Scala 3 tuples - compile time check of members types fails with function parameter

I am testing if a tuple’s members have all the same type. Below the code shows how Tuple.Union can be used when we test against an instance. However, when I attempt to use this in a function’s parameter I get a compilation error (see the end of this post). I am using Scala 3.1.0. What am I doing wrong?

EDIT: same result with 3.1.1

Code can be found in scastie


    val t1          = ( 1,   2L,  3.0f,   4.0,    "five",    '6'   )
    val csv         = ("1", "2", "3.0",  "4.0", "\"five\"",  "'6'" )

                    summon[Tuple.Union[csv.type]  =:= String]

    def toCSVString[T<: Tuple](separator: String)(t:T): String = 
      summon[Tuple.Union[t.type] =:= String]

Compilation error:

error] -- Error: /home/hmf/VSCodeProjects/aiops/utils/test/src/TimeSeriesSpec.scala:622:44 
[error] 622 |      summon[Tuple.Union[t.type] =:= String]
[error]     |                                            ^
[error]     |Cannot prove that Tuple.Union[(t : T)]
[error]     |
[error]     |where:    T is a type in method toCSVString with bounds <: Tuple
[error]     | =:= String.
[error]     |
[error]     |Note: a match type could not be fully reduced:
[error]     |
[error]     |  trying to reduce  Tuple.Union[(t : T)]
[error]     |  trying to reduce  scala.Tuple.Fold[(t : T), Nothing, [x, y] =>> x | y]
[error]     |  failed since selector  (t : T)
[error]     |  does not match  case EmptyTuple => Nothing
[error]     |  and cannot be shown to be disjoint from it either.
[error]     |  Therefore, reduction cannot advance to the remaining case
[error]     |
[error]     |    case h *: t => h | scala.Tuple.Fold[t, Nothing, [x, y] =>> x | y]
[error] one error found
[error] one error found

Use summonInline instead of summon. (You’ll then also have to use inline def on the method.)


Works. Tested here. Thank you.

I understand that inline and summonInline should be used together, however I don’t understand why I cannot use summon in a standard method. In particular I finally used an explicit using clause in a standard def (not inlined), and that worked. So why can’t I substitute with an equivalent summon?

Can anyone shed light on this?


Let’s simplify the example a bit. Suppose we have:

def foo[T](x: T) = summon[T =:= String]

In the scope in which foo is defined, T is not known - it could be anything. Therefore there is no way to prove whether it is a String or not, and we get the compiler error Cannot prove that T =:= String.

(On the other hand, def foo[T <: String](x: T) = summon[T <:< String] would succeed since T is bound to be a subtype of String.)

Now we might ask: why can’t the proving, that is the summoning of T =:= String, happen in the scope where foo is invoked (i.e. where we write e.g. foo("bar")), instead of where it is defined?

Well, it can, and that is what summonInline does. And as such, when we write:

inline def foo[T](x: T) = summonInline[T =:= String]

and in another scope invoke e.g. foo(3) we get Cannot prove that Int =:= String, because in that scope T is known to be an Int.

The terminology used in the documentation is that for summonInline the summoning (i.e. implicit search) is “delayed until the call is inlined”. Compile-time operations | Scala 3 Language Reference | Scala Documentation

1 Like

@kavedaa That first sentence explains it all. Thank you.