A proof that the type `A` is of the form `F[elem]` for some type `elem`

IsA.scala

/** A proof that the type {{{A}}} is of
  * the form {{{F[elem]}}} for some type
  * {{{elem}}}.
  */
sealed abstract class IsA[F[_], A] {
  type elem
  def fold[G[_]](p: G[F[elem]]): G[A]

  @inline implicit final def to: A =:= F[elem] = {
    type G[X] = X =:= F[elem]
    fold[G](implicitly[F[elem] =:= F[elem]])
  }

  @inline implicit final def from: F[elem] =:= A = {
    type G[X] = F[elem] =:= X
    fold[G](implicitly[F[elem] =:= F[elem]])
  }
}
object IsA {
  final case class Proof[F[_], X]() extends IsA[F, F[X]] {
    final type elem = X
    @inline final def fold[G[_]](p: G[F[elem]]): G[F[X]] = p
  }

  @inline implicit def proof[F[_],elem]: IsA[F, F[elem]] =
    Proof[F, elem]()
}

def length[A](a: A)(implicit proof: IsA[List, A]): Int = {
  import proof._
  a.length
}

def reverse[A](a: A)(implicit proof: IsA[List, A]): A = {
  import proof._
  a.reverse
}