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

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?

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].

https://stackoverflow.com/questions/74267610/polymorphic-method-works-with-type-lambda-but-not-with-type-wildcard-in-scala-3

https://stackoverflow.com/questions/63942937/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

https://stackoverflow.com/questions/75742747/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

https://stackoverflow.com/questions/75227132/in-scala-3-how-to-replace-general-type-projection-that-has-been-dropped

https://stackoverflow.com/questions/50043630/what-does-dotty-offer-to-replace-type-projections