Type-Level Instant Insanity in Scala

InstantInsanity.scala

object InstantInsanity extends App {

  // scalastyle:off

  def undefined[T]: T = ???
  def ⊥[T]: T = undefined

  trait R
  trait G
  trait B
  trait W

  trait Cube[u, f, b, r, l, d]

  type Cube1 = Cube[B, G, W, G, B, R]
  type Cube2 = Cube[W, G, B, W, R, R]
  type Cube3 = Cube[G, W, R, B, R, R]
  type Cube4 = Cube[B, R, G, G, W, W]

  trait Transform[u, f, r, b, l, d] {
    def rot: Cube[u, f, r, b, l, d] => Cube[u, r, b, l, f, d]
    def twist: Cube[u, f, r, b, l, d] => Cube[f, r, u, l, d, b]
    def flip: Cube[u, f, r, b, l, d] => Cube[d, l, b, r, f, u]
  }

  implicit def transform[u, f, r, b, l, d] = new Transform[u, f, r, b, l, d] {
    def rot: (Cube[u, f, r, b, l, d]) => Cube[u, r, b, l, f, d] = ⊥
    def twist: (Cube[u, f, r, b, l, d]) => Cube[f, r, u, l, d, b] = ⊥
    def flip: (Cube[u, f, r, b, l, d]) => Cube[d, l, b, r, f, u] = ⊥
  }

  def rot[u, f, r, b, l, d](cube: Cube[u, f, r, b, l, d])(implicit t: Transform[u, f, r, b, l, d]) = t.rot(cube)
  def twist[u, f, r, b, l, d](cube: Cube[u, f, r, b, l, d])(implicit t: Transform[u, f, r, b, l, d]) = t.twist(cube)
  def flip[u, f, r, b, l, d](cube: Cube[u, f, r, b, l, d])(implicit t: Transform[u, f, r, b, l, d]) = t.flip(cube)

  // :type rot(⊥[Cube1])
  // :type twist(flip(rot(⊥[Cube1])))

  trait True
  trait False

  trait And[l, r, o]

  implicit object ttt extends And[True, True, True]
  implicit object tff extends And[True, False, False]
  implicit object ftf extends And[False, True, False]
  implicit object fff extends And[False, False, False]

  def and[l, r, o](l: l, r: r)(implicit and: And[l, r, o]): o = ⊥

  // :type and(⊥[True], ⊥[False])

  trait Nil
  trait :::[x, xs]

  trait ListConcat[l1, l2, l]

  implicit def nilConcat[l]: ListConcat[Nil, l, l] = ⊥
  implicit def notNilConcat[x, xs, ys, zs](implicit
    lc: ListConcat[xs, ys, zs]
  ): ListConcat[x ::: xs, ys, x ::: zs] = ⊥

  def listConcat[xs, ys, zs](l1: xs, l2: ys)(implicit
    lc: ListConcat[xs, ys, zs]
  ): zs = ⊥

  // :type listConcat(⊥[R ::: Nil], ⊥[G ::: W ::: Nil])

  trait Rotation
  trait Twist
  trait Flip
  
  trait Apply[f, a, b]

  implicit def apRotation[u, f, r, b, l, d]: Apply[Rotation, Cube[u, f, r, b, l, d], Cube[u, r, b, l, f, d]] = ⊥
  implicit def apTwist[u, f, r, b, l, d]: Apply[Twist, Cube[u, f, r, b, l, d], Cube[f, r, u, l, d, b]] = ⊥
  implicit def apFlip[u, f, r, b, l, d]: Apply[Flip, Cube[u, f, r, b, l, d], Cube[d, l, b, r, f, u]] = ⊥

  def ap[t, u, f, r, b, l, d, o](r: t, c1: Cube[u, f, r, b, l, d])(implicit
    ap: Apply[t, Cube[u, f, r, b, l, d], o]
  ): o = ⊥

  // :type ap(⊥[Rotation], ⊥[Cube1])

  trait Map[f, xs, zs]

  implicit def mapNil[f]: Map[f, Nil, Nil] = ⊥
  implicit def mapCons[f, x, z, xs, zs](implicit
    ap: Apply[f, x, z],
    map: Map[f, xs, zs]
  ): Map[f, x ::: xs, z ::: zs] = ⊥

  def map[f, xs, zs](f: f, xs: xs)(implicit
    map: Map[f, xs, zs]
  ): zs = ⊥

  // :type map(⊥[Flip], ⊥[Cube1 ::: Cube2 ::: Nil])

  trait AppendIf[b, x, ys, zs]

  implicit def appendIfTrue[x, ys]: AppendIf[True, x, ys, x ::: ys] = ⊥
  implicit def appendIfFalse[x, ys]: AppendIf[False, x, ys, ys] = ⊥

  def append[b, x, ys, zs](b: b, x: x, ys: ys)(implicit
    apn: AppendIf[b, x, ys, zs]
  ): zs = ⊥

  // :type append(⊥[True], ⊥[R], ⊥[G ::: W ::: Nil])
  // :type append(⊥[False], ⊥[R], ⊥[G ::: W ::: Nil])


  trait Filter[f, xs, zs]

  implicit def filterNil[f]: Filter[f, Nil, Nil] = ⊥
  implicit def filterCons[f, x, b, xs, ys, zs](implicit
    ap: Apply[f, x, b],
    f: Filter[f, xs, ys],
    apn: AppendIf[b, x, ys, zs]
  ): Filter[f, x ::: xs, zs] = ⊥


  //

  trait MapAppend[f, xs, zs]

  implicit def mapAppendNil[f]: MapAppend[f, Nil, Nil] = ⊥
  implicit def mapAppendCons[f, xs, ys, zs](implicit
    m: Map[f, xs, ys],
    lc: ListConcat[xs, ys, zs]
  ): MapAppend[f, xs, zs] = ⊥

  trait MapAppend2[f, xs, zs]

  implicit def mapAppend2Nil[f]: MapAppend2[f, Nil, Nil] = ⊥
  implicit def mapAppend2Cons[f, xs, ys, _ys, zs](implicit
    m: Map[f, xs, ys],
    ma: MapAppend[f, ys, _ys],
    lc: ListConcat[xs, _ys, zs]
  ): MapAppend2[f, xs, zs] = ⊥

  trait MapAppend3[f, xs, zs]

  implicit def mapAppend3Nil[f]: MapAppend3[f, Nil, Nil] = ⊥
  implicit def mapAppend3Cons[f, xs, ys, _ys, zs](implicit
    m: Map[f, xs, ys],
    ma2: MapAppend2[f, ys, _ys],
    lc: ListConcat[xs, _ys, zs]
  ): MapAppend3[f, xs, zs] = ⊥


  trait Orientations

  implicit def orientations[c, fs, ts, zs](implicit
    ma: MapAppend[Flip, c ::: Nil, fs],
    ma2: MapAppend2[Twist, fs, ts],
    ma3: MapAppend3[Rotation, ts, zs]
  ): Apply[Orientations, c, zs] = ⊥

  // :type ap(⊥[Orientations], ⊥[Cube1])

  trait NE[x, y, b]

  implicit object neRR extends NE[R, R, False]
  implicit object neRG extends NE[R, G, True]
  implicit object neRB extends NE[R, B, True]
  implicit object neRW extends NE[R, W, True]

  implicit object neGR extends NE[G, R, True]
  implicit object neGG extends NE[G, G, False]
  implicit object neGB extends NE[G, B, True]
  implicit object neGW extends NE[G, W, True]

  implicit object neBR extends NE[B, R, True]
  implicit object neBG extends NE[B, G, True]
  implicit object neBB extends NE[B, B, False]
  implicit object neBW extends NE[B, W, True]

  implicit object neWR extends NE[W, R, True]
  implicit object neWG extends NE[W, G, True]
  implicit object neWB extends NE[W, B, True]
  implicit object neWW extends NE[W, W, False]

  trait All[l, b]

  implicit def allNil: All[Nil, True]

  = ⊥
  implicit def allFalse[xs]: All[False ::: xs, False] = ⊥
  implicit def allTrue[b, xs](implicit all: All[xs, b]): All[True ::: xs, b] = ⊥

  def all[b, xs](l: xs)(implicit all: All[xs, b]): b = ⊥

  // :type all(⊥[Nil])
  // :type all(⊥[False ::: Nil])
  // :type all(⊥[True ::: False ::: Nil])
  // :type all(⊥[True ::: True ::: Nil])


  trait Compatible[c1, c2, b]

  implicit def compatibleInstance[f1, f2, bF, r1, r2, bR, b1, b2, bB, l1, l2, bL, u1, u2, d1, d2, b](implicit
    ne1: NE[f1, f2, bF],
    ne2: NE[r1, r2, bR],
    ne3: NE[b1, b2, bB],
    ne4: NE[l1, l2, bL],
    all: All[bF ::: bR ::: bB ::: bL ::: Nil, b]
  ): Compatible[Cube[u1, f1, r1, b1, l1, d1], Cube[u2, f2, r2, b2, l2, d2], b] = ⊥

  def compatible[c1, c2, b](c1: c1, c2: c2)(implicit
    c: Compatible[c1, c2, b]
  ): b = ⊥

  // :type compatible(⊥[Cube[R, R, R, R, R, R]], ⊥[Cube[B, B, B, B, B, B]])
  // :type compatible(⊥[Cube[R, R, G, R, R, R]], ⊥[Cube[B, B, G, B, B, B]])

  trait Allowed[c, cs, b]

  implicit def allowedNil[c]: Allowed[c, Nil, True] = ⊥
  implicit def allowedCons[c, y, b1, ys, b2, b](implicit
    c: Compatible[c, y, b1],
    allowed: Allowed[c, ys, b2],
    and: And[b1, b2, b]
  ): Allowed[c, y ::: ys, b] = ⊥

  def allowed[c, cs, b](c: c, cs: cs)(implicit a: Allowed[c, cs, b]): b = ⊥

  type CubeRed = Cube[R, R, R, R, R, R]
  type CubeBlue = Cube[B, B, B, B, B, B]

  // :type allowed(⊥[CubeRed], ⊥[CubeBlue ::: CubeRed ::: Nil])

  trait MatchingOrientations[os, sols, zs]

  implicit def matchingOrientationsNil[sol]: MatchingOrientations[Nil, sol, Nil] = ⊥
  implicit def matchingOrientationsCons[os, sol, as, o, b, zs](implicit
    mo: MatchingOrientations[os, sol, as],
    a: Allowed[o, sol, b],
    apn: AppendIf[b, o ::: sol, as, zs]
  ): MatchingOrientations[o ::: os, sol, zs] = ⊥

  trait AllowedCombinations[os, sols, zs]

  implicit def allowedCombinationsNil[os]: AllowedCombinations[os, Nil, Nil] = ⊥
  implicit def allowedCombinationsCons[os, sols, as, s, bs, zs](implicit
    ac: AllowedCombinations[os, sols, as],
    mo: MatchingOrientations[os, s, bs],
    lc: ListConcat[as, bs, zs]
  ): AllowedCombinations[os, s ::: sols, zs] = ⊥

  class Solutions[cs, ss]

  implicit def solutionsNil: Solutions[Nil, Nil ::: Nil] = ⊥
  implicit def solutionsCons[cs, sols, c, os, zs](implicit
    s: Solutions[cs, sols],
    ap: Apply[Orientations, c, os],
    ac: AllowedCombinations[os, sols, zs]
  ): Solutions[c ::: cs, zs] = ⊥

  type Cubes = (Cube1 ::: Cube2 ::: Cube3 ::: Cube4 ::: Nil)

  def solutions[cs, ss](cs: cs)(implicit sol: Solutions[cs, ss]): ss = ⊥

  // :type solutions(⊥[Cubes])
  
}