Type safe type combinations with shapeless

Question

Having the following code:

import shapeless.{::, Generic, HList, HNil, Lazy}

object Problem {
  trait In {
    def bar: Double
  }

  trait A {
    def foo: Int
    type I <: In
  }

  /////////////////////////////////////////////////////

  final case class A1In(d: Double) extends In {
    override def bar: Double = 1.1 + d
  }

  final case class A1() extends A {
    override def foo: Int = 1
    override type I = A1In
  }

  final case class A2In(d: Double) extends In {
    override def bar: Double = 1.1 + d
  }

  final case class A2() extends A {
    override def foo: Int = 1
    override type I = A2In
  }


  final case class AListIn[T <: HList](items: T)(implicit ev: isIn[T]) extends In {
    override def bar = 1.1
  }

  final case class AList[T <: HList](items: T)(implicit ev: isA[T]) extends A {
    override def foo: Int = 555
    override type I = AListIn[???]
  }

  trait isA[T] {
    def aux_foo(value: T): Int
  }

  trait isIn[T] {
    def aux_bar(value: T): Double
  }
  /////////////////////////////////////////////////////

  def alloc(a: A): In = ????

  def usage() = {
    val a1: A1 = A1() 
    val a2: A2 = A2() 

    val l: AList[::[A1, ::[A2, ::[A1, HNil]]]] = AList(a1 :: a2 :: a1 :: HNil) 

    val a1In: A1In = A1In(1.2) 
    val a2In: A2In = A2In(9.3) 

    val lIn: AListIn[::[A2In, ::[A1In, HNil]]] = AListIn(a2In :: a1In :: HNil)
  }

}

How can I fix it so it works as expected? E.g how do I get correct type in place of ??? which is a proper type HList being result of applying isA -> isIn type mapping. The mapping must follow the natural association of A -> In mapping defined as type I <: In in trait A And how to implement alloc function which for any concrete instance of In will produce corresponding instance of A? Should concrete implementations of In be path dependent types of corresponding As?

Below is the code for isA the code for isIn is analogous

trait isA[T] {
    def aux_foo(value: T): Int
  }

  object isA {
    // "Summoner" method
    def apply[T](implicit enc: isA[T]): isA[T] = enc

    // "Constructor" method
    def instance[T](func: T => Int): isA[T] = new isA[T] {
      override def aux_foo(value: T): Int = func(value)
    }

    implicit def a1Encoder: isA[A1] = instance(i => 4)
    implicit def a2Encoder: isA[A2] = instance(i => 9)

    implicit def hnilEncoder: isA[HNil] = instance(hnil => 0)

    implicit def hlistEncoder[H, T <: HList](implicit
                                             hInstance: Lazy[isA[H]],
                                             tInstance: isA[T]
                                            ): isA[H :: T] = instance {
      case h :: t => hInstance.value.aux_foo(h) + tInstance.aux_foo(t)
    }

    implicit def genericInstance[A, R](implicit
                                       generic: Generic.Aux[A, R],
                                       rInstance: Lazy[isA[R]]
                                      ): isA[A] = instance { value => rInstance.value.aux_foo(generic.to(value)) }
  }