How to prove that `Tuple.Map[H *: T, F] =:= (F[H] *: Tuple.Map[T, F])` in Scala 3

Question

I'm trying to write a trait that contains given instances for a tuple type (yes I know that summonAll exists):

trait TupleInstances[C[_], T <: Tuple] {
  val instances: Tuple.Map[T, C]
}

given[C[_]]: TupleInstances[C[_], EmptyTuple] with {
  val instances = EmptyTuple
}

inline given[C[_], H, T <: Tuple] (using ch: C[H], ti: TupleInstances[C, T]): TupleInstances[C, H *: T] with {
  val instances: Tuple.Map[H *: T, C] = ch *: ti.instances
}

and getting the error

 val instances: Tuple.Map[H *: T, C] = ch *: ti.instances
  |                                        ^^^^^^^^^^^^^^^^^^
  |               Found:    C[H] *: Tuple.Map[T, C]
  |               Required: Tuple.Map[H *: T, C]
  |
  |               Note: a match type could not be fully reduced:
  |
  |                 trying to reduce  Tuple.Map[T, C]
  |                 failed since selector  T
  |                 does not match  case EmptyTuple => EmptyTuple
  |                 and cannot be shown to be disjoint from it either.
  |                 Therefore, reduction cannot advance to the remaining case
  |
  |                   case h *: t => C[h] *: scala.Tuple.Map[t, C]

So essentially I need to prove that for all F[_], Tup:

Tuple.Map[Tup, F] =:= (F[Tuple.Head[Tup]] *: Tuple.Map[Tuple.Tail[Tup], F])

How do I go about doing that?

Answer 1

Firstly, TupleInstances[C[_], EmptyTuple] (for C[_] and trait TupleInstances[C[_], T <: Tuple]) is incorrect

Type argument C[?] does not have the same kind as its bound [_$1]

Correct is higher-kinded TupleInstances[C, EmptyTuple] or TupleInstances[C[*], EmptyTuple] (with scalacOptions += "-Ykind-projector") or TupleInstances[[t] =>> C[t], EmptyTuple]. TupleInstances[C[_], EmptyTuple] is supposed to mean the same eventually but currently it means existential TupleInstances[C[?], EmptyTuple].

Polymorphic method works with type lambda, but not with type wildcard in Scala 3

Rules for underscore usage in Higher Kinded Type parameters

Secondly,

• match types, and

• type classes

are two different ways to perform type-level calculations in Scala 3 (like type projections and type classes in Scala 2 or like type families and type classes in Haskell). If you want to mix them, some corner cases are possible.

You can add one more constraint

trait TupleInstances[C[_], T <: Tuple]:
  def instances: Tuple.Map[T, C]
object TupleInstances:
  given[C[_]]: TupleInstances[C, EmptyTuple] with
    val instances = EmptyTuple

  given[C[_], H, T <: Tuple](using
    ch: C[H],
    ti: TupleInstances[C, T],
    ev: (C[H] *: Tuple.Map[T, C]) =:= Tuple.Map[H *: T, C] // <-- HERE!!!
  ): TupleInstances[C, H *: T] with
    val instances: Tuple.Map[H *: T, C] = ch *: ti.instances

Or using summonFrom and inline

import scala.compiletime.summonFrom

trait TupleInstances[C[_], T <: Tuple]:
  def instances: Tuple.Map[T, C]
object TupleInstances:
  given[C[_]]: TupleInstances[C, EmptyTuple] with
    val instances = EmptyTuple

  given[C[_], H, T <: Tuple](using
    ch: C[H],
    ti: TupleInstances[C, T]
  ): TupleInstances[C, H *: T] with
    inline def instances: Tuple.Map[H *: T, C] =
      summonFrom {
        case _: ((C[H] *: Tuple.Map[T, C]) =:= Tuple.Map[H *: T, C]) =>
          ch *: ti.instances
      }

Scala is not an actual theorem prover. It can check that C[H] *: Tuple.Map[T, C] =:= Tuple.Map[H *: T, C] for specific C, H, T but can't for arbitrary

How to define induction on natural numbers in Scala 2.13?

Also you should reconsider whether you'd like to formulate the whole logic in terms of match types rather than type classes

import scala.compiletime.{erasedValue, summonInline}

inline def tupleInstances[C[_], T <: Tuple]: Tuple.Map[T, C] = erasedValue[T] match
  case _: EmptyTuple => EmptyTuple
  case _: (h *: t)   => summonInline[C[h]] *: tupleInstances[C, t]

or you'd like to formulate the whole logic in terms of type classes rather than match types

trait TupleInstances[C[_], T <: Tuple]:
  type Out <: Tuple
  def instances: Out
object TupleInstances:
  given[C[_]]: TupleInstances[C, EmptyTuple] with
    type Out = EmptyTuple
    val instances = EmptyTuple

  given[C[_], H, T <: Tuple](using
    ch: C[H],
    ti: TupleInstances[C, T]
  ): TupleInstances[C, H *: T] with
    type Out = C[H] *: ti.Out
    val instances = ch *: ti.instances

In Scala 3, how to replace General Type Projection that has been dropped?

What does Dotty offer to replace type projections?