scalac-checked restricting recursion

build.sbt

name := "sbt_playground"

scalaVersion := "2.11.7"

scalaSource in Compile := baseDirectory.value / "src"

scalaSource in Test := baseDirectory.value / "test"

libraryDependencies ++= Seq(
  "com.chuusai" %% "shapeless" % "2.2.5"
)

initialCommands in console := """
import net.iximeow.sbt_playground._
"""

test.scala

package net.iximeow.sbt_playground

import shapeless._

object test extends App {
  // Assert A and B are different types
  trait =:!=[A, B]

  implicit def nsub[A, B]: A =:!= B = new =:!=[A, B] {}
  implicit def nsubAmbig1[A]: A =:!= A = sys.error("unexpected")
  implicit def nsubAmbig2[A]: A =:!= A = sys.error("unexpected")

  // liberally lifted from shapeless, but reiterated mainly for easy access to (re)learn
  type |!=|[T] = {
    type L[U] = U =:!= T
  }

  // type lambda expressing that types T and U are not equal
  type Contains[M] = {
    type L[U <: HList] = BasisConstraint[M :: HNil, U]
  }

  // Type class witnessing that no `L` is an element of `M`
  //   heavily inspired by BasisConstraint
  trait BasisNotConstraint[L, M <: HList]

  object BasisNotConstraint {
    // witness is built constructively:
    //   start with a witness that L is not in HNil (always true!)
    implicit def hnilBasis[L, M <: HNil] = new BasisNotConstraint[L, M] {}

    //   then let scalac unravel the implicits, but...
    //     given a list of permitted types M,
    //     for each type H,
    //     so long as H is not the same as the forbidden type L,
    //     we can assert that H :: M is a list of permitted types
    //   if we build this from HNil and eventually travel through all types being witnessed,
    //   this constructs a proof that some list M does not contain a type L

    //              and this is a renaming for ease of reading: |
    //              it asserts that any M is already witnessed  |
    //              to not contain a type L                     v
    implicit def hlistBasis[L, H : |!=|[L]#L, M <: HList : ContainsNot[L]#L] =
      new BasisNotConstraint[L, H :: M] {}
  }

  type ContainsNot[M] = {
    type L[U <: HList] = BasisNotConstraint[M, U]
  }

  def testContains[T <: HList : Contains[String]#L](t: T) = true
  // compiles
  testContains("asdf" :: HNil)
  // does not compile
  //testContains(1 :: HNil)


  def testContainsNot[T <: HList : ContainsNot[String]#L](t: T) = true
  // does not compile
  //testContainsNot2("asdf" :: HNil)
  // compiles
  testContainsNot(1 :: 2 :: HNil)
  // does not compile
  //testContainsNot(1 :: "asdf" :: HNil)

  object ResultContainer {
    def point[A](a: A) = ResultContainer[A, HNil](a)
  }

  case class ResultContainer[A, B <: HList](private val a: A) {
    implicit private[this] def resultId[U, UComp <: HList] = (x: ResultContainer[U, UComp]) => x

    def flatMap[U, UC <: HList](op: Q[A, ResultContainer[U, UC]])(implicit ev: ContainsNot[op.FnType]#L[B], p: shapeless.ops.hlist.Prepend[UC, op.FnType :: B]): ResultContainer[U, p.Out] = {
      ResultContainer[ResultContainer[U, UC], op.FnType :: B](
        op.apply(a)
      ).flatten[U, UC]
    }

    def map[U](op: Q[A, U])(implicit ev: ContainsNot[op.FnType]#L[B]): ResultContainer[U, op.FnType :: B] = {
      ResultContainer[U, op.FnType :: B](op.apply(a))
    }

/*
 * Given proof that in a(b)
 * that b is contained in a (via type?)
 * A, B, C
 * ResultContainer[ResultContainer[A, B], C]
 */
  // should make sure that UComputations and B don't share any types... how would that even work?
    def flatten[U, UComputations <: HList](implicit ev: A =:= ResultContainer[U, UComputations], p: shapeless.ops.hlist.Prepend[UComputations, B]): ResultContainer[U, p.Out] = {
      val t: ResultContainer[U, UComputations] = a

      // just casting because I can't figure out scalaz Leibniz
      val this2: ResultContainer[ResultContainer[U, UComputations], B] =
        this.asInstanceOf[ResultContainer[ResultContainer[U, UComputations], B]]

      t.collapse(this2)
    }

    private def collapse[C <: HList](container: ResultContainer[ResultContainer[A, B], C])(implicit p: ops.hlist.Prepend[B, C]): ResultContainer[A, p.Out] = {
      ResultContainer(a)
    }
  }

  // Q just wraps a function and provides a function-specific type, to track usage in a computation
  trait Q[A, B] {
    trait FnType

    def apply(arg: A): B
  }

  object x extends Q[Int, Int] {
    override def apply(a: Int): Int = {
      1
    }
  }
  object double extends Q[Int, Int] {
    override def apply(a: Int): Int = a * 2
  }

  object sub1 extends Q[Int, Int] {
    override def apply(a: Int): Int = a - 1
  }

  object wrap extends Q[Int, ResultContainer[Int, HNil]] {
    override def apply(a: Int) = ResultContainer.point(a)
  }

  // compiles
  ResultContainer[Int, HNil](3).map(x)

  // does not compile
  // could not find implicit value for evidence parameter of type net.iximeow.sbt_playground.test.BasisNotConstraint[net.iximeow.sbt_playground.test.x.FnType,shapeless.::[net.iximeow.sbt_playground.test.x.FnType,shapeless.HNil]]
  //x(x(ResultContainer[Int, HNil](3)))

  val res1 = ResultContainer[Int, HNil](3).map(x)
  //val res2 = res1.map(x) // shouldn't compile?
  println(res1)

  println(
    ResultContainer.point(3)
      .flatMap(wrap)
    /*.flatMap(wrap)*/ // causes compilation failure!~
  )
}