# How to prove type is a Singleton in match type?

I have this perfectly working match type along with its function:

``````    type Find[Columns <: Tuple, Label] =
Columns match
case TypedColumn[Label] *: ? => TypedColumn[Label]
case TypedColumn[?] *: t => Find[t, Label]

inline def findT[C <: Tuple, Label <: Singleton]: Find[C, Label] =
erasedValue[C] match
case _: (TypedColumn[Label] *: ?) =>
TypedColumn[Label](constValue[Label], None)
case _: (TypedColumn[?] *: tail) =>
findT[tail, Label]
``````

Which basically exists to reify an object from a homogeneous tuple. The type itself has signature like `TypedColumn[L <: Singleton](smth: Option[Something])` (the type has many compile-time labels, but I’m omitting them for sake of brevity) and this function works fine, but when I try to implement the same for multiple labels:

``````    // Match type is fine
type Pick[Columns <: NonEmptyTuple, Labels <: Tuple] <: Tuple =
Labels match
case l *: t => Find[Columns, l] *: Pick[Columns, t]

// I can't prove that my `h` is a Singleton
inline def pickT[C <: NonEmptyTuple, Labels <: Tuple]: Pick[C, Labels] =
erasedValue[Labels] match
case _: (h *: t) =>
findT[C, h] *: pickT[C, t]
``````

Tried to create ad-hoc type classes with `Out` singleton, `IsConst` type, `Mirror.Singleton` etc, but all of them break the function.

The end-goal would be to have something like:

``````type In = (TypedColumn["one"], TypedColumn["two"], TypedColumn["three"])
pickT[In, ("two", "one")]

// evaluating to runtime value of:
(TypedColumn(None), TypedColumn(None)): (TypedColumn["two"], TypedColumn["one"])
``````

The error is:

``````[error] 233 |          findT[C, h] *: pickT[C, t]
[error]     |                   ^
[error]     |             Type argument h does not conform to upper bound Singleton
``````

Here is the complete working example:

``````import compiletime.{erasedValue, constValue}

case class TypedColumn[Label <: Singleton](label: Label)

type IsSingleton[T <: Singleton] = T

type Find[Columns <: Tuple, Label] =
Columns match
case TypedColumn[Label] *: t => TypedColumn[Label]
case h *: t => Find[t, Label]

inline def findT[C <: Tuple, Label <: Singleton]: Find[C, Label] =
inline erasedValue[C] match
case _: (TypedColumn[Label] *: t) =>
TypedColumn[Label](constValue[Label])
case _: (h *: t) =>
findT[t, Label]

type Pick[Columns <: NonEmptyTuple, Labels <: Tuple] <: Tuple =
Labels match
case IsSingleton[l] *: t => Find[Columns, l] *: Pick[Columns, t]
case EmptyTuple => EmptyTuple

inline def pickT[C <: NonEmptyTuple, Labels <: Tuple]: Pick[C, Labels] =
inline erasedValue[Labels] match
case _: (IsSingleton[h] *: t) =>
findT[C, h] *: pickT[C, t]
case _: EmptyTuple => EmptyTuple

type In = (TypedColumn["one"], TypedColumn["two"], TypedColumn["three"])
pickT[In, ("two", "one")]
``````

1. there is a trick where you can use a type alias to constrain a type variable - see `IsSingleton`
2. use `inline` match
3. add `EmptyTuple` base cases to matches
4 Likes

That’s an awesome trick! Thank you so much, @bishabosha!

N.B. I tried to go against your advice of using `inline` match and got a fairly misleading error:

``````scala> pickT[res0.Row#TypedColumns, ("bar", "quiz")]
-- Error: ----------------------------------------------------------------------
1 |pickT[res0.Row#TypedColumns, ("bar", "quiz")]
|^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|not a constant type: h; cannot take constValue
|---------------------------------------------------------------------------
|Inline stack trace
|- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
|This location contains code that was inlined from Action.scala:229
229 |          TypedColumn[Label, a, t, c](constValue[Label], None, summonInline[Primitive[a]])
|                                      ^^^^^^^^^^^^^^^^^
|- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
|This location contains code that was inlined from Action.scala:229
236 |        case _: (IsSingleton[h] *: t) => findT[C, h] *: pickT[C, t]
|                                         ^^^^^^^^^^^
---------------------------------------------------------------------------
``````

If you didn’t mention that explicitly - I would spent few more hours on figuring this out.

Is it the case, that we always need to use `inline match` in match type functions?

you only need an inline match if you are using the `compiletime` operations

1 Like