In scala shapeless, how to use Record.updateWith inside another method?

From what I have read online, the shapeless Record.updateWith seems to be the only way to update both the value & type of a Record entry. So I gave it a try:

  import shapeless.syntax.singleton.mkSingletonOps
  import shapeless.record._

    val existing = ("i" ->> 3.0) :: ("j" ->> "Abc") :: HNil

    val uu = existing.updateWith("i")(_ => 123)

It worked! the output is 123 :: Abc :: HNil, however I encounter a different problem: I cannot call this function inside another function, namely, it cannot use typeclasses in scope:

    def update[HH <: HList, O](existing: HH, k: Witness.Lt[String], v: Int)(
        implicit
        lemma1: Selector.Aux[HH, k.T, O],
        lemma2: Modifier[HH, k.T, O, Int]
    ) = {

      val result = existing.updateWith(k.value)(_ => v)
      result
    }

The latest compiler (2.13.4) gave the following error information:

[Error] ... : Unable to resolve implicit value of type shapeless.ops.record.Selector[HH,Witness.this.value.type]
one error found

Despite that lemma1 totally qualifies this condition. So my questions are:

• How do I instruct the type class summoner of updateWith to use lemma1? (it is written in macro)

• If this is not possible, what are my other options to implement a proper update in a method?

Thanks a lot for your help

Despite that lemma1 totally qualifies this condition.

No, it doesn't. Selector[HH, k.T] and Selector[HH, k.value.type] are different types. k.value.type is a subtype of k.T. Selector is invariant.

I already advised you to use type classes rather than extension methods

def update[HH <: HList, O](existing: HH, k: Witness.Lt[String], v: Int)(
  implicit
  lemma1: Selector.Aux[HH, k.T, O],
  lemma2: Modifier[HH, k.T, O, Int]
) = {
  lemma2(existing, _ => v)
}

or

def update[HH <: HList, K <: String, O](existing: HH, k: K, v: Int)(
  implicit
  witness: Witness.Aux[K],
  lemma1: Selector.Aux[HH, K, O],
  lemma2: Modifier[HH, K, O, Int]
) = {
  lemma2(existing, _ => v)
}