Implicit proof that a case class contains certain fields

checkfields.scala

import shapeless._, record._, ops.record._ , syntax.singleton._, labelled._

object console extends App {

  case class Foo(i: Int,s: String)

  trait Check[L] extends SingletonProductArgs {
    def applyProduct[T <: HList, LR <: HList]
      (t: T)
      (implicit 
        lg: LabelledGeneric.Aux[L, LR],
        sa: SelectAll[LR, T]
      ): T = t
  }

  object Check {
    implicit def check[T] = new Check[T] {} 
  } 

  def foo[T, R <: HList, L]
    (t: T)
    (implicit 
      g: Generic.Aux[T, L],
      c: Check[L]) = {
    val l = c(g.to(t))

  }

}