Trying to mimic Idris Enum in scala3

enum.scala

import TList.{TCons, TNil}

import scala.annotation.targetName

enum TList[A]:
  case TNil[A]() extends TList[A]
  case TCons[A, X <: A, T <: TList[A]](x: X, t: T) extends TList[A]

sealed trait Elem[A, X, XS <: TList[A]]:
  def get(l: XS): X

case class Here[A, X <: A, XS <: TList[A]]() extends Elem[A, X, TCons[A, X, XS]]:
  override def get(l: TCons[A, X, XS]): X = l.x

case class There[A, Y <: A, X <: A, XS <: TList[A]](elem: Elem[A, X, XS]) extends Elem[A, X, TCons[A, Y, XS]]:
  override def get(l: TCons[A, Y, XS]): X = elem.get(l.t)

object Test:
  type t1 = TCons[Int, 1, TCons[Int, 2, TCons[Int, 3, TNil[Int]]]]
  val l1: t1 = TCons(1, TCons(2, TCons(3, TNil())))

  val firstElemOfL1: Elem[Int, 1, t1] = Here()
  val secondElemOfL1: Elem[Int, 2, t1] = There(Here())

  val l1_0: 1 = firstElemOfL1.get(l1)