Aux pattern cannot infer path dependent type

Question

I have this set of type classes that work together to resolve the SQL equivalent of scala types. Basically, values can be encoded as either rows or columns, with the special case of Option being able to wrap both column types and row types. in the case of the latter, an optional row is encoded as a row the columns of which are all nullable.

import scala.deriving.*

sealed trait Column
sealed trait Row

type Encodings = Row | Column

sealed trait SQLRep[A]:
  type Encoding <: Encodings
  type Mirror <: Any

object SQLRep:
  type Aux[A, E <: Encodings, M] = SQLRep[A] {type Encoding = E; type Mirror = M}
  given option[A, E <: Encodings, M](using ta: SQLRep.Aux[A, E, M]): SQLRep.Aux[Option[A], E, MapTo[M, Option]] = new SQLRep[Option[A]]:
    final type Encoding = E
    final type Mirror = MapTo[M, Option]

  given tuple[T <: Tuple, M <: Tuple](using sqlTup: SQLTuple.Aux[T, M]): SQLRep.Aux[T, Row, M] = sqlTup

  given SQLBase[Int] with {}
  given SQLBase[String] with {}

sealed trait SQLBase[A] extends SQLRep[A]:
  final type Encoding = Column
  final type Mirror = A

sealed trait SQLTuple[A <: Tuple] extends SQLRep[A] {
  final type Encoding = Row
  override type Mirror <: Tuple
}    

object SQLTuple: 
  type Aux[A <: Tuple, M <: Tuple] = SQLTuple[A] {type Mirror = M}
  given emptyTuple: SQLTuple[EmptyTuple] with
    final type Mirror = EmptyTuple

  given inductiveTuple[H, T <: Tuple, MH, MT <: Tuple](using th: SQLRep.Aux[H, _, MH])(using tt: SQLTuple.Aux[T, MT]): SQLTuple[H *: T] with
    final type Mirror = Tuple.Concat[ToTuple[MH], MT]


trait SQLProduct[P <: Product] extends SQLRep[P] {
  final type Encoding = Row
  type Mirror <: Tuple
}

object SQLProduct:
  type Aux[A <: Product, M <: Tuple] = SQLProduct[A] {type Mirror = M}
  given derived[P <: Product, M <: Tuple](using prodMirr: Mirror.ProductOf[P], sqlTup: SQLTuple.Aux[prodMirr.MirroredElemTypes, M]): SQLProduct.Aux[P, M] = new SQLProduct[P] {
    final type Mirror = M
  }

The two type-level functions used in the snippet above are:

type MapTo[X,F[_]] = X match
  case Tuple => Tuple.Map[X, F]
  case _ => F[X]

type ToTuple[X] <: Tuple = X match
  case Tuple => Tuple.Map[X, [x] =>> x] //Bonus question: weird that "case Tuple => X" does not compile. why?!
  case _ => X *: EmptyTuple     

Now to put it altogether:

case class ContactInfo(phone: String, email: String) derives SQLProduct
case class User(id: Int, name: String, contactInfo: Option[ContactInfo]) derives SQLProduct
    
def assertTypeEq[A, M](using rep: SQLRep[A])(using ev: M =:= rep.Mirror): Unit = ()
      
assertTypeEq[Int, Int] //simple one
      
assertTypeEq[Option[(String, String)], (Option[String], Option[String])] // more advanced
      
assertTypeEq[ContactInfo, (String, String)] // I need this to compile
//Cannot prove that (String, String) =:= this.ContactInfo.derived$SQLProduct.Mirror.

assertTypeEq[User, (Int, String, Option[String], Option[String])] // If I solve the above, this should be a piece of cake!

It should be self-explanatory that despite all my efforts I cannot make the case classes' types be inferred correctly without it being denoted as a path-dependent type. I would appreciate the help to move past this obstacle preferably without changing the type member Mirror in the SQLRep[A] type class to be another type parameter.