Scala 3 type bound `<:<` trick for tuples

Question

During online session Adam Warski showed a trick to prove that tuple has a certain structure:

The first implementation is

    def sequence[T <: Tuple](t: T): Option[InverseMap[T, Option]] =
        val unwrapped = t.productIterator.collect { case Some(v) => v}.toArray[Any]
        if unwrapped.length == t.productArity then Some(Tuple.fromArray(unwrapped).asInstanceOf[InverseMap[T, Option]])
        else None

which allows (but shouldn't)

sequence(("x", true)) // compiles

And implementation with a trick

def betterSequence[T <: Tuple](t: T)(using T <:< Map[InverseMap[T, Option], Option]): Option[InverseMap[T, Option]] =
    val unwrapped = t.productIterator.collect { case Some(v) => v}.toArray[Any]
    if unwrapped.length == t.productArity then Some(Tuple.fromArray(unwrapped).asInstanceOf[InverseMap[T, Option]])
    else None

betterSequence(("x", true)) // compile error

Could some explain how

(using T <:< Map[InverseMap[T, Option], Option])

works and why T is a subtype of Map?

Answer 1

InverseMap[T, Foo] takes a tuple T that looks like (Foo[t1], Foo[t2], ..., Foo[tn]) and turns it into a tuple (t1, t2, ..., tn). If T does not have that structure, i.e. it's not a bunch of Foos, it will not compile (with a somewhat cryptic error). This is the main thing that proves the tuple only has Options in it.

The next question is how to insert this type into the betterSequence method. Map[T, Foo] turns a tuple T that looks like (t1, t2, ..., tn) into (Foo[t1], Foo[t2], ..., Foo[tn]) (the inverse of InverseMap). Thus, Map[InverseMap[T, Option], Option] is just T (think of maths, where f(f^-1(x)) is again x. The bound T <:< T will always be true, but only if the InverseMap succeeds first.