Transitivity, or How To Chain Generic Implicits in Scala

I'm attempting to extend the functionality described in this excellent article by Miles Sabin: Unboxed Union Types to support n-ary type unions, e.g.:

def if[T](t: T)(implicit ev: T <<: (Int | String | Symbol | Double)): String = ???

I've modified Sabin's code and written my own version of the <:< operator as show below.

object UnboxedTypeUnion extends TypeUnion {

  def is[T](t: T)(implicit ev: T <<: (Int | String | Double | Symbol)) =
    t match {
      case _: Int    => "int"
      case _: String => "string"
      case _: Double => "double"
      case _: Symbol => "symbol"
    }

  // Does not compile
  val x = implicitly[Int <<: (Int | String | Double)]
  val y = implicitly[Int <<: Not[Not[Not[Not[Int]]]]]

}

trait TypeUnion {
  type Not[A] = A => Nothing
  type |[A, B] = Not[Not[A] with Not[B]]

  sealed abstract class <<:[-A, +B] extends (A => B)

  object <<: {
    val singleton = new <<:[Any, Any] { override def apply(v1: Any): Any = v1 }

    implicit def instance[A]: A <<: A = singleton.asInstanceOf[A <<: A]
    implicit def negation[A]: A <<: Not[Not[A]] = singleton.asInstanceOf[A <<: Not[Not[A]]]
    implicit def transitivity[A, B, C](implicit ab: A <<: B, bc: B <<: C): A <<: C = singleton.asInstanceOf[A <<: C]
  }

}

The underlying issue is that each additional logical disjunction (OR) wraps the resulting evidentiary subclass in a new double negation, i.e.

implicitly[Not[Not[Int]] <<: (Int | String)]
implicitly[Not[Not[Not[Not[Int]]]] <<: (Int | String | Double )]
implicitly[Not[Not[Not[Not[Not[Not[Int]]]]]] <<: (Int | String | Double | Symbol )]
// etc.

In theory, I would expect the definition of double negation identity in conjunction with a definition of transitivity to allow for this to work, however I am unable to get this to compile. Does anyone know if this is possible, or if recursively chained generics is beyond the capabilities of the Scala compiler?

Try

type | [A, B]

trait <<: [A, B]

trait LowPriority_<<: {
  implicit def monotonicR[A, B, C](implicit ab: A <<: B): A <<: (B | C) = null
}

object <<: extends LowPriority_<<: {
  implicit def sym[A]: A <<: A = null
  implicit def monotonicL[A, B, C](implicit ab: A <<: B): A <<: (C | B) = null
}

implicitly[Int <<: (Int | String | Double | Long)]
implicitly[String <<: (Int | String | Double | Long)]
implicitly[Double <<: (Int | String | Double | Long)]
implicitly[Long <<: (Int | String | Double | Long)]
// implicitly[Char <<: (Int | String | Double | Long)] // doesn't compile

or

type Not[A] = A => Nothing

trait DisjNot[A] {
  type Or[B] = DisjNot[A with Not[B]]
  type Build = Not[A]
}

type Disj[A] = DisjNot[Not[A]]

type Disj2[A, B] = Disj[A]#Or[B]#Build
type Disj3[A, B, C] = Disj[A]#Or[B]#Or[C]#Build  
type Disj4[A, B, C, D] = Disj[A]#Or[B]#Or[C]#Or[D]#Build

type <<: [A, B] = Not[Not[A]] <:< B

implicitly[Int <<: Disj4[Int, String, Boolean, Double]]
implicitly[String <<: Disj4[Int, String, Boolean, Double]]
implicitly[Boolean <<: Disj4[Int, String, Boolean, Double]]
implicitly[Double <<: Disj4[Int, String, Boolean, Double]]
// implicitly[Char <<: Disj4[Int, String, Boolean, Double]] // doesn't compile