Q:

Coercing the value of a shapeless record

I have a wrapper around a shapeless record.
I want to extract a value from that record, and prove that it is an instance of a polymorphic type, e.g. List[_]
import shapeless._
import shapeless.record._
import shapeless.ops.record._
import shapeless.syntax.singleton._

case class All[L <: HList](containers: L) {

  def getValue[Value, A](containerKey: Witness)
                        (implicit sel: Selector.Aux[L, containerKey.T, Value],
                         equiv: Value =:= List[A]
                        ): List[A] =
    equiv.apply(containers.get(containerKey))

}

Right now, I can call getValue if I explicitly specify the type params Value and A, but since i'm working with much more complex types than List, I really need these type params to be inferred.
val all = All(
  'x ->> List[Int](1, 2, 3) ::
  'y ->> List[String]("a", "b") ::
  'z ->> 90
  HNil
)

// doesn't compile: Cannot prove that Value =:= List[A].
all.getValue('x)

// compiles
all.getValue[List[Int], Int]('x)

Is there a way to extract a value, coerce it to e.g. List[_], while not having to specify any type params?
Note that this strategy works completely fine if I want to prove that value is a simple monomorphic type , e.g. Value =:= Int, just not for Value =:= List[A]

A:

There are at least two ways to do it, and both involve changing the signature of getValue.
First, you can just use a constrained generic parameter:
  def getValue[R <: List[_]](containerKey: Witness)
                        (implicit sel: Selector.Aux[L, containerKey.T, R]): R =
    containers.get(containerKey)

Note that because we're using R as return type, the compile-time information about result won't be lost. You just won't be able to call this function if the value at a containerKey is not a list.

Second, you can use subtype bounds. I have no idea why it works, really. I suspect that using too strict constraints causes the compiler to dismiss some solutions that use refinement types. This works both if you replace the type parameter in Selector with a bounded wildcard:
  def getValue[A](containerKey: Witness)
                        (implicit sel: Selector.Aux[L, containerKey.T, _ <: List[A]]): List[A] =
    containers.get(containerKey)

Or if you use subtyping evidence <:< instead of equality =:=:
  def getValue[Value, A](containerKey: Witness)
                        (implicit sel: Selector.Aux[L, containerKey.T, Value],
                         equiv: Value <:< List[A]
                        ): List[A] =
    equiv.apply(containers.get(containerKey))

