Witness that a case class has proper subset of properties of another case class

prop_subset_3.sc

//> using scala 3.3
import scala.util.NotGiven
// //> using file shapeless_3.sc

import scala.annotation.implicitNotFound
import scala.compiletime.{constValue, erasedValue}
import scala.compiletime.ops.boolean.*
import scala.deriving.Mirror
//import shapeless_3.* 

case class EmpProj(name: String, age: Int)
case class Employee(name: String, age: Int, active: Boolean)

val bob: Employee = Employee("Bob", 42, false)
val bobTuple: (String, Int, Boolean) = Tuple.fromProductTyped(bob)

val mirror = summon[Mirror.Of[Employee]]

val bobAgain: Employee = mirror.fromProduct(bobTuple)

//https://stackoverflow.com/a/68309890/3819595
inline def constValueTuple[T <: Tuple]: T =
  (inline erasedValue[T] match
    case _: EmptyTuple => EmptyTuple
    case _: (t *: ts) => constValue[t] *: constValueTuple[ts]
  ).asInstanceOf[T]

val labels = constValueTuple[mirror.MirroredElemLabels]

val labelled = labels.zip(bobTuple)

println(labelled)

type ContainsIn[T, Tup <: Tuple] <: Boolean = Tup match
  case EmptyTuple => false
  case T *: _ => true
  case _ *: tail => ContainsIn[T, tail]

type Contains[T] = [Tup <: Tuple] =>> true =:= ContainsIn[T, Tup]

def ok[Tup <: Tuple : Contains[Int]](tpl: Tup) = ()

ok((1, "2"))

type IsPropSubset[P <: Tuple, S <: Tuple] <: Boolean =
  P match
    case EmptyTuple => true
    case phead *: ptail =>
      S match
        case EmptyTuple => false
        case shead *: stail => ContainsIn[phead, shead *: stail] && IsPropSubset[ptail, shead *: stail]

type IsPropConstraint[S <: Tuple] = [P <: Tuple] =>> true =:= IsPropSubset[P, S]  

println(constValue[IsPropSubset[(Int, String), (Int, Int, String)]])

def okTuple[S <: Tuple, P <: Tuple : IsPropConstraint[S]](p: P, s: S) = ()

okTuple((1, "2"), (1, 2, "3"))

type GetByLabel[TL <: String, TPL <: Tuple] =
  TPL match
    case (TL, t) *: _ => t
    case _ *: (t *: ts) => GetByLabel[TL, t *: ts]
  
/*
  Witnesses, that all fields of `Projection` exists in `Source` with the same types and names
 */
@implicitNotFound("${Projection} is not a valid projection of ${Source}")
trait PropSubset[Projection, Source]

object PropSubset {
  private val anySubset = new PropSubset[Any, Any] {}

  given [T]: PropSubset[T, T] = anySubset.asInstanceOf[PropSubset[T, T]]

  given [P, S](using NotGiven[P =:= S], PropSubset[P, S]): PropSubset[Option[P], Option[S]] = anySubset.asInstanceOf[PropSubset[Option[P], Option[S]]]

  given [T <: Tuple]: PropSubset[EmptyTuple, T] = anySubset.asInstanceOf[PropSubset[EmptyTuple, T]]

  //given [SH, ST <: Tuple, PH, PT <: Tuple : IsPropConstraint[S]]: PropSubset[P, S] = anySubset.asInstanceOf[PropSubset[P, S]]

  given [PHL <: String, PHT, PT <: Tuple, S <: Tuple](using PropSubset[PHT, GetByLabel[PHL, S]], PropSubset[PT, S]): PropSubset[(PHL, PHT) *: PT, S] = anySubset.asInstanceOf[PropSubset[(PHL, PHT) *: PT, S]]

  given [P <: Product, S <: Product](using mp: Mirror.ProductOf[P], ms: Mirror.ProductOf[S], tps: PropSubset[Tuple.Zip[mp.MirroredElemLabels, mp.MirroredElemTypes], Tuple.Zip[ms.MirroredElemLabels, ms.MirroredElemTypes]]): PropSubset[P, S] =
    anySubset.asInstanceOf[PropSubset[P, S]]
}

def okp[P, S](using PropSubset[P, S]) = ()

okp[EmpProj, Employee]

PropSubset.scala

import shapeless._
import shapeless.labelled.FieldType
import shapeless.ops.record.Selector

import scala.annotation.implicitNotFound

/*
  Witnesses, that all fields of `Projection` exists in `Source` with the same types and names
 */
@implicitNotFound("${Projection} is not a valid projection of ${Source}")
trait PropSubset[Projection, Source]

object PropSubset {
  def apply[P, S](implicit propSubset: PropSubset[P, S]): PropSubset[P, S] = propSubset

  private val anySubset = new PropSubset[Any, Any] {}

  implicit def identitySubset[T]: PropSubset[T, T] =
    anySubset.asInstanceOf[PropSubset[T, T]]

  implicit def optionSubset[P, S](implicit notEq: P =:!= S, ps: PropSubset[P, S]): PropSubset[Option[P], Option[S]] =
    ps.asInstanceOf[PropSubset[Option[P], Option[S]]]

  implicit def hNilSubset[S <: HList]: PropSubset[HNil, S] =
    anySubset.asInstanceOf[PropSubset[HNil, S]]

  implicit def hListSubset[K <: Symbol, PH, PT <: HList, SF, S <: HList](implicit
    notEq: (FieldType[K, PH] :: PT) =:!= S,
    s: Selector.Aux[S, K, SF],
    ps0: Lazy[PropSubset[PH, SF]],
    psTail: PropSubset[PT, S]
  ): PropSubset[FieldType[K, PH] :: PT, S] =
    anySubset.asInstanceOf[PropSubset[FieldType[K, PH] :: PT, S]]

  implicit def genericSubset[P, S, PHL <: HList, SHL <: HList](implicit
    notEq: P =:!= S,
    pgen: LabelledGeneric.Aux[P, PHL],
    sgen: LabelledGeneric.Aux[S, SHL],
    hlSubset: Lazy[PropSubset[PHL, SHL]]
  ): PropSubset[P, S] =
    hlSubset.asInstanceOf[PropSubset[P, S]]
}

PropSubsetTest.scala

import java.time.{LocalDate, Year}

import fields.PropSubset

case class EmptyEvidence()
case class Inner(fc: String)
case class Source(id: Int, text: String, date: LocalDate, in: Option[Inner])
case class InnerP(fc: String)
case class Projection(id: Int, in: Option[InnerP], text: String)
case class Projection2(id: Int, text: String, yoba: String)

object PropSubsetTest {
  PropSubset[Source, Source]
  PropSubset[EmptyEvidence, Source]
  PropSubset[Projection, Source]
  //PropSubset[Projection2, Source] //Will fail
}