型レベルズンドコキヨシ

repl

scala> implicitly[ZDK[_5, _3, _8, _1, _4, HNil]].apply(HNil)

ZDK.scala

import shapeless._, ops.nat._

trait ズン
trait ドコ
trait `キ・ヨ・シ！`
case object ズン extends ズン
case object ドコ extends ドコ
case object `キ・ヨ・シ！` extends `キ・ヨ・シ！`

trait GenZD[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, ズンドコ, OutX <: Nat] {
  def apply: ズンドコ
}

object GenZD {
  implicit def zun[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, `A*X` <: Nat, `A*X+C` <: Nat, `(A*X+C)%M` <: Nat](
    implicit prod: Prod.Aux[A, X, `A*X`], sum: Sum.Aux[`A*X`, C, `A*X+C`], mod: Mod.Aux[`A*X+C`, M, `(A*X+C)%M`], gteq: GTEq[`(A*X+C)%M`, T]): GenZD[A, C, M, X, T, ズン, mod.Out] =
    new GenZD[A, C, M, X, T, ズン, mod.Out] {
      def apply: ズン = ズン
    }

  implicit def doko[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, `A*X` <: Nat, `A*X+C` <: Nat, `(A*X+C)%M` <: Nat](
    implicit prod: Prod.Aux[A, X, `A*X`], sum: Sum.Aux[`A*X`, C, `A*X+C`], mod: Mod.Aux[`A*X+C`, M, `(A*X+C)%M`], lt: LT[`(A*X+C)%M`, T]): GenZD[A, C, M, X, T, ドコ, mod.Out] =
    new GenZD[A, C, M, X, T, ドコ, mod.Out] {
      def apply: ドコ = ドコ
    }
}

trait ZDK[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, Acc <: HList] {
  type Out <: HList
  def apply(acc: Acc): Out
}

trait LowerPriorityZDK {

  implicit def loop[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, ZD, NextX <: Nat, Acc <: HList](
    implicit genZD: GenZD[A, C, M, X, T, ZD, NextX], zdk: Lazy[ZDK[A, C, M, NextX, T, ZD :: Acc]]): ZDK[A, C, M, X, T, Acc] =
    new ZDK[A, C, M, X, T, Acc] {
      type Out = zdk.value.Out
      def apply(acc: Acc): Out = zdk.value(genZD.apply :: acc)
    }
}

object ZDK extends LowerPriorityZDK {
  type Aux[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, Acc <: HList, Out0 <: HList] = ZDK[A, C, M, X, T, Acc] { type Out = Out0 }

  implicit def end[A <: Nat, C <: Nat, M <: Nat, X <: Nat, T <: Nat, Acc <: HList](
    implicit ev: Acc <:< (ドコ :: ズン :: ズン :: ズン :: HList)): ZDK[A, C, M, X, T, Acc] = new ZDK[A, C, M, X, T, Acc] {

    type Out = `キ・ヨ・シ！` :: Acc
    def apply(acc: Acc): Out = `キ・ヨ・シ！` :: acc
  }
}