Questions about what subtyping information Match Types / matches introduce

[s5bug]

Given

type Elem[C] = C match {
  case String => Char
  case Iterable[t] => t
}

the following programs typecheck:

def initial[C <: Matchable](c: C): Elem[C] =
  c match {
    case s: String => s(0)
    case i: Iterable[t] => i.head
  }

def initial[C <: Matchable](c: C): Elem[C] =
  c match {
    case s: String => (s(0): Char)
    case i: Iterable[t] => i.head
  }

These do not:

def initial[C <: Matchable](c: C): Elem[C] =
  c match {
    case s: String => (s(0): Elem[C])
    case i: Iterable[t] => i.head
  }

def initial[C <: Matchable](c: C): Elem[C] =
  c match {
    case s: String =>
      summon[Char <:< Elem[C]]
      s(0)
    case i: Iterable[t] => i.head
  }

Why is it that a Char can be returned in an Elem[C] position (implying that Char <:< Elem[C]), but that evidence is not available?

The goal here is essentially

extension[X <: Tuple, Y <: Tuple, F[_]](x: X)(using yx: Y =:= Tuple.InverseMap[X, F], xy: X =:= Tuple.Map[Y, F], app: Applicative[F]) {
  def mapN[B](f: Function1[Y, B]): F[B] =
    x match {
      case _: (F[h] *: t) =>
        val here: F[h] = x.head
        val next: F[h => B] = x.tail.mapN[h => B]((ty: Tuple.Tail[Y]) => (hv: h) => f(hv *: ty))
        app.ap(next)(here)
      case _: EmptyTuple.type =>
        app.pure(f(EmptyTuple))
    }
}

but I don't know how to accomplish it.